Verifying a sequential circuit consists in proving that the given implementation of the circuit satisfies its specification. In the present work the input-output specification of the circuit, which is required to hold for the given implementation, is assumed to be available in the form of a Tempura program segment B. It captures the desired ongoing behavior of the circuit in terms of input-output relationships that are expected to hold at various time instants of the interval in question. The implementation is given as a formula W/sub S/ of a first-order temporal equality theory, /spl Fscr/. Goal formulas of the form P /spl sup/ B have been introduced to capture the correctness property of the circuit in question. P is a formula of the equality theory /spl epsiv/ contained in /spl Fscr/ and encodes the initial state(s) of the circuit. A goal reduction paradigm has been used to formulate the proof calculus capturing the state transitions produced along the intervals. Formulas, called verification conditions (VC's), whose validity ensures the correctness of the circuit, are produced corresponding to the output equality statements in B. For finite state machines, VC's are formulas of propositional calculus and, therefore, require no temporal reasoning for their proofs. In fact, since binary decision diagram (BDD) representations are used throughout, their proofs become quite simple. The goal reduction rules proposed for iterative constructs also incorporate synthesis of invariant assertions over the states of the circuit. The proof of a nontrivial example has been presented. The paper concludes with a discussion on a broad overview of the building blocks of the verifier.
展开▼
