Formal verification of peephole optimization in asynchronous circuits

This thesis proposes and applies novel techniques for formal verification of peephole optimizations in asynchronous circuits. Our task is to verify whether locally optimized modules can replace parts of an existing circuit under certain assumptions regarding the operation of the optimized modules in context. Two main difficulties in verifying peephole optimizations are state explosion in the implementation models and increased complexity of the interfaces of optimized modules. A novel technique is proposed for constructing in a modular manner specifications and functional models of pulse-mode circuits. A verification rule related to assume-guarantee and hierarchical verification is presented, using relative timing constraints as optimization assumptions. We present two case studies to illustrate the proposed techniques: verification of speed-optimizations in an asynchronous arbiter, and verification of one step of communication refinement in a globally asynchronous, locally synchronous (GALS) architecture