Symbolic asynchronous hardware protocol verification for compositions with relative timing

This thesis work provides a methodology and a tool flow for verifying asynchronous hardware protocols through compositional model checking with symbolic methods. Correct interaction of asynchronous hardware protocols requires verification. Performance and power of asynchronous hardware circuits and protocols can be vastly improved by modifying them with judicious application of timing constraints. This approach uses relative timing constraints for modeling timed asynchronous hardware protocols. This work illustrates the modeling techniques for interleaving and simultaneous compositions with relative timing, which helps in pruning the reachable state space with an overhead of enforcing relative timing constraints. The modeling technique for relative timing does not alter the individual initial protocols. Relative timing constraints are enforced at the interface external to the protocol component. Different modeling types are explored for modeling relative timing. Symbolic model checking is performed with properties required for ensuring compositional correctness using the NuSMV engine. Environment complying to behavior is used for verification. Translators and an automation flow is built which automates the process of generating NuSMV models and temporal properties by reading structural verilog, formal models and relative timing constraints. Case studies of a C-element, pipeline linear controller with various stages and model types and an arithmetic pipeline example are discussed by applying BDD and SAT methods. In addition, the control paths of the global STP---a clocked pulse logic used in the integer unit of Intel's Pentium 4 processor---is validated with this approach. Comparison of this methodology is performed with the Analyze verification engine. The simultaneous model yields better execution times when compared to the interleaving model. SAT-based methods find a counter example in less time compared to the BDD method for a large number of compositions using the simultaneous model. Automatic generation of models and properties leading to a push button solution has enabled verification of medium to large control planes of timed asynchronous protocols with symbolic model checking.