Introduction to a computational theory and implementation of sequential hardware equivalence

Abstract

A theory of sequential hardware equivalence [1] is presented, including the notions of gate-level model (GLM), hardware finite state machine (HFSM), state equivalence (∼), alignability, resetability, and sequential hardware equivalence (≈). This 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. Binary decision diagrams are used to represent predicates about pairs of harware designs. Algorithms are given for computing pairs of equivalent states and sequential hardware equivalence as implemented in the MCC CAD Sequential Equivalence Tool (SET). Microelectronics and Computer Technology Corporation (MCC) Computer Aided Design Program