An approach to the introduction of formal validation in an asynchronous circuit design flow
D. Borrione, Menouer Boubekeur, Emil Dumitrescu, Marc Renaudin, Jean-Baptiste Rigaud, S. Sirianni · 2003
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.