VERIFICATION OF TEMPURA SPECIFICATION OF SEQUENTIAL-CIRCUITS

Verifying a sequential circuit consists in proving that the given impl ementation 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 ire t he form of a Tempura program segment B. It captures the desired ongoin g behavior of the circuit in terms of input-output relationships that are expected to hold at various time instants of the interval in quest ion, The implementation is given as a formula Ws of a first-order temp oral equality theory, F. Goal formulas of the form P superset of B hav e been introduced to capture the correctness property of the circuit i n question, P is a formula of the equality theory E contained in F and encodes the initial state(s) of the circuit. A goal reduction paradig m has been used to formulate the proof calculus capturing the state tr ansitions produced along the Intervals, Formulas, called verification conditions (VC's), whose validity ensures the correctness of the circu it, are produced corresponding to the output equality statements in B. For finite state machines, VC's are formulas of propositional calculu s and, therefore, require no temporal reasoning for their proofs, In f act, since binary decision diagram (BDD) representations are used thro ughout, their proofs become quite simple. The goal reduction rules pro posed 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.