Title :
A theory and implementation of sequential hardware equivalence
Author_Institution :
Microelectronics & Computer Technology Corp., Austin, TX, USA
fDate :
12/1/1992 12:00:00 AM
Abstract :
A theory of sequential hardware equivalence is presented. This theory includes the notions of gate-level model (GLM), hardware finite state machine (HFSM), quotient machine, state equivalence (~), alignability, resetability, essential resetability, isomorphism, and sequential hardware equivalence. The theory is motivated by (1) the observation that it is impossible to control the initial state of a machine when it is powered on and (2) the desire to decide equivalence of two designs based solely on their netlists and logic device models, without knowledge of intended initial states or intended environments. Algorithms based upon a binary decision diagram (BDD) implementation of predicate calculus over Boolean domains are presented. This calculus is employed to calculate properties of hardware designs. Experimental results based upon these algorithms as implemented in the MCC sequential equivalence tool (SET) are presented
Keywords :
equivalence classes; finite state machines; logic design; sequential machines; Boolean domains; MCC sequential equivalence tool; alignability; binary decision diagram; gate-level model; hardware finite state machine; logic device models; netlists; quotient machine; resetability; sequential hardware equivalence; state equivalence; Automata; Binary decision diagrams; Boolean functions; Calculus; Data structures; Design automation; Design optimization; Hardware; Logic devices; Timing;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
