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.