Integrating circuit design and formal verification
Vishal Patel, R.J. Offen · 2002
The application of formal methods to the specification and design derivation of integrated circuits is addressed. The initial specification is expressed as an abstract relation between data tuples. This relation is a combination of conditional statements and associated data actions. Structural circuit descriptions are derived by step-wise application of proven laws to the specification while maintaining behavioral equivalence. This yields designs that are correct by construction. An example of a simple microprocessor design is used to illustrate the method.>