Automation of hardware-correctness proofs
Zerksis D. Umrigar · 1986
The ubiquity of the digital computer and its use in critical applications makes verification of its correctness an extremely important issue. Unfortunately present verification methodologies, which rely almost exclusively on simulation, have difficulty handling the complexity of modern hardware designs. In this dissertation we explore an alternate verification methodology in which the functional correctness of a design is proved using formal proof techniques. To prove the correctness of a design, a formal hardware verification system is given two formal descriptions of the design which correspond to a functional specification and an implementation. It must then establish an implication or equivalence between these two descriptions. This can be done using exhaustive simulation, but this is slow and cannot be used to verify parameterized circuits. A more general method is to use algebraic simulation to derive verification conditions and then use a theorem prover to establish the validity of these verification conditions. An interactive general purpose theorem prover which is a partial decision procedure for first-order logic is used as a shell for more efficient but specialized algorithms. A specialized algorithm, called the bounds algorithm is used to establish the validity of formulas involving universally quantified linear inequalities over the integer domain. This algorithm is goal-directed and is easily extended to handle some properties of interpreted functions. Theoretical properties of these theorem proving procedures are established. The usefulness of the formal verification system is limited by its theorem proving component. It has successfully been used to verify the functional correctness of simple arithmetic circuits, including an array multiplier.