Formal techniques for verification of synchronous sequential circuits

The integration of automated techniques for the formal verification of sequential circuits into the design cycle is imperative to handle today's complex circuits. This thesis presents a unified framework for the multilevel verification of sequential circuits viewed as finite state machines. Experimental results are presented on designs from industry.;Verification of circuit implementations against their specifications (circuit descriptions at a higher level in the design hierarchy) is formulated as checking for containment of the specification state machine in the implementation state machine to ensure that all specified behavior is correctly implemented. The concept of strong containment is introduced to exploit correspondences between data registers of descriptions at different stages in the design cycle. It is also shown that containment can be checked by considering subsets of outputs, thus reducing the sizes of the Binary Decision Diagrams used to represent the output functions for large circuits. The concept of strong containment is extended to verify circuits after retiming transformations which destroy the simple data register correspondences.;A framework is also presented for the specification of correctness properties as labeled state machines to aid the designer in verifying the behavioral circuit descriptions which serve as top-level specifications in the design cycle. Algorithms have been developed and implemented for generating counterexamples and witnesses to help in debugging the design. In addition, the applicability of formal techniques to improve simulation-based verification is shown in the form of an Extracted Control Flow Machine model. This model, extracted automatically, embodies the flow of control in a sequential circuit and is used to evaluate the control flow coverage of the simulation vectors used for design verification.;The power of theorem proving techniques in handling data abstraction is utilized in the form of a library of Boolean templates to handle high level descriptions in a commercial hardware description language, VHDL. The correctness of the templates is proved using the Boyer Moore theorem prover before their inclusion in the library.;The hierarchical verification of a simple microprocessor, the Viper, is attempted in this framework. A behavioral description is verified against user-specified properties, including part of the instruction set, and a gate level implementation is proved to correctly implement the behavioral VHDL description.