The Community for Technology Leaders
2014 47th Hawaii International Conference on System Sciences (2003)
Big Island, Hawaii
Jan. 6, 2003 to Jan. 9, 2003
ISBN: 0-7695-1874-5
pp: 279b
Dominique Borrione , TIMA Laboratory
Antoine Sirianni , TIMA Laboratory
Emil Dumitrescu , TIMA Laboratory
Menouer Boubekeur , TIMA Laboratory
Marc Renaudin , TIMA Laboratory
Jean-Baptiste Rigaud , TIMA Laboratory
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.
Dominique Borrione, Antoine Sirianni, Emil Dumitrescu, Menouer Boubekeur, Marc Renaudin, Jean-Baptiste Rigaud, "An Approach to the Introduction of Formal Validation in an Asynchronous Circuit Design Flow", 2014 47th Hawaii International Conference on System Sciences, vol. 09, no. , pp. 279b, 2003, doi:10.1109/HICSS.2003.1174811
96 ms
(Ver 3.1 (10032016))