On the verification of sequential machines at differing levels of abstraction

摘要

An algorithm is presented for the verification of the equivalence of two sequential circuit descriptions at the same of differing levels of abstraction, namely, at the register-transfer (RT) level and the logic level. The descriptions represent general finite automata at the differing levels. A finite automaton can be described in ISP-like language and its equivalence to a logic level implementation can be verified using this algorithm. Two logic-level automata can be similarly verified for equivalence. The technique is shown to be computationally efficient for complex circuits. The efficiency of the algorithm lies in the exploitation of don't care information derivable from the RT or logic-level description during the verification process. Using efficient cube enumeration procedures at the logic level, the equivalence of finite automata with a large number of states in small amounts of CPU time was verified. A two-phase enumeration-simulation algorithm for verifying the equivalence of two logic-level finite automata with the same or differing number of latches is also presented.