Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata

Using a variant of Clariso-Cortadella's parametric method for verifying asynchronous circuits, we formally derive a set of linear constraints that ensure the correctness of some crucial timing behaviours of the architecture of SPSMALL memory. This allows us to check two different implementations of this architecture.

• Type: Conference
• Year: 2006
• Where: FORMATS
• Authors: Remy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, Weiwen Xu
• Keywords: Asynchronous Circuits, Clariso-Cortadella's Parametric Method, Crucial Timing Behaviours, Formal Methods, FORMATS 2006