A theory and implementation of sequential hardware equivalence
- 1 January 1992
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
- Vol. 11 (12) , 1469-1478
- https://doi.org/10.1109/43.180261
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 presentedKeywords
This publication has 11 references indexed in Scilit:
- State assignment for initializable synthesis (gate level analysis)Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Logic verification using binary decision diagrams in a logic synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Evaluation and improvement of Boolean comparison method based on binary decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Automatic derivation of FSM specification to implementation encodingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- ATPG aspects of FSM verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient implementation of a BDD packagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Implicit state enumeration of finite state machines using BDD'sPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On the verification of sequential machines at differing levels of abstractionPublished by Association for Computing Machinery (ACM) ,1987
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite state concurrent system using temporal logic specificationsPublished by Association for Computing Machinery (ACM) ,1983