Automatic derivation of FSM specification to implementation encoding

Efficient decision procedures based on binary decision diagrams (BDDs) have recently been developed for formal verification of hardware. A novel application of these procedures is presented. An algorithm is described for deciding whether a gate-level design satisfies a finite state machine specification. The unique feature of this method is that it does not require knowing the state encoding and, in fact, derives the encoding from the specification and a net-list description of the design. This algorithm is related to the algorithms that implement a computational theory of sequential hardware equivalence, as realized in the MCC-CAD sequential equivalence tool (SET). This theory of sequential hardware equivalence does not require knowledge of an initial state of the design