Equivalence of the Arbiter, the Synchronizer, the Latch, and the Inertial Delay

An axiomatic method for proving correctness properties about digital circuit implementations under the influence of asynchronous inputs is presented. This method, termed hardware correctness, is used to prove properties about a target digital circuit that is implemented in terms of constituent digital circuits. The proof consists of deducing theorems about properties of the target circuit from known properties of the constituent circuits. Three types of properties are considered, and they are expressed as axioms in first order predicate calculus. The axioms describe ideal behavior of the four most commonly studied asynchronous circuits, the inertial delay, the synchronizer, the time-bounded arbiter, and the latch. These axioms are derived from the less precise behavioral descriptions used by other investigators.