A theory and implementation of sequential hardware equivalence

Author

Pixley, Carl

Author_Institution

Microelectronics & Computer Technology Corp., Austin, TX, USA

Volume

11

Issue

12

fYear

1992

fDate

12/1/1992 12:00:00 AM

Firstpage

1469

Lastpage

1478

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;

fLanguage

English

Journal_Title

Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on

Publisher

ieee

ISSN

0278-0070

Type

jour

DOI

10.1109/43.180261

Filename

180261