Timed verification of the generic architecture of a memory circuit using parametric timed automata |
| |
Authors: | Remy Chevallier Emmanuelle Encrenaz-Tiphene Laurent Fribourg Weiwen Xu |
| |
Affiliation: | (1) STMicroelectronics, FTM, Central R&D, Crolles, France;(2) LSV-CNRS, ENS de Cachan, Cachan, France |
| |
Abstract: | Using a variant of Clariso-Cortadella’s parametric method for verifying asynchronous circuits, we analyse some crucial timing
behaviors of the architecture of SPSMALL memory, a commercial product of STMicroelectronics. Using the model of parametric
timed automata and model checker HYTECH, we formally derive a set of linear constraints that ensure the correctness of the
response times of the memory. We are also able to infer the constraints characterizing the optimal setup timings of input
signals. We have checked, for two different implementations of this architecture, that the values given by our model match
remarkably with the values obtained by the designer through electrical simulation.
Partially supported by project MEDEA+ Blueberries.
A preliminary version appeared in the Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed
Systems (FORMATS’06), Sept. 2006. |
| |
Keywords: | Memory circuit Timed automata Model checking |
本文献已被 SpringerLink 等数据库收录! |
|