Automatic Optimization Techniques for Formal Verification of Asynchronous Circuits

Even medium size asynchronous circuits may display a complex behavior, due to the combinational explosion in the chronology of events that may happen. It is thus essential to apply automatic optimization techniques to avoid such complexity when formally verifying the correctness of the circuit. This paper presents dedicated techniques for optimization of formal verification of asynchronous circuits, these include for instance: automata reduction, pre-order reduction and automatic abstraction. All these techniques have been implemented and tested in a formal verification environment.