An approach to the introduction of formal validation in an asynchronous circuit design flow

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.