RT Journal Article
JF 2014 47th Hawaii International Conference on System Sciences
YR 2003
VO 09
SP 279b
TI An Approach to the Introduction of Formal Validation in an Asynchronous Circuit Design Flow
A1 Dominique Borrione,
A1 Antoine Sirianni,
A1 Emil Dumitrescu,
A1 Menouer Boubekeur,
A1 Marc Renaudin,
A1 Jean-Baptiste Rigaud,
K1 null
AB This paper discusses the integration of model-checking inside a design flow for Quasi-Delay Insensitive circuits. Both the formal validation of an asynchronous behavioral specification and the formal verification of the asynchronous synthesis result are considered. The method follows several steps: formal model extraction, model simplification, environment modeling, writing temporal properties and proof. The approach is illustrated on a small, yet characteristic, asynchronous selection circuit.
PB IEEE Computer Society, [URL:http://www.computer.org]
LA English
DO 10.1109/HICSS.2003.1174811
LK http://doi.ieeecomputersociety.org/10.1109/HICSS.2003.1174811