Paper Info
Title
A theory and implementation of sequential hardware equivalence
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
Year
DOI
Venue
1992
10.1109/43.180261
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Keywords
DocType
Volume
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
Journal
11
Issue
ISSN
Citations 
12
0278-0070
53
PageRank 
References 
Authors
4.72
7
1
Name
Order
Citations
PageRank
Carl Pixley112111.69