Checking combinational equivalence of speed-independent circuits

We introduce the notion of combinational equivalence to relate two speed-independent asynchronous (sequential) circuits: a "golden" hazard-free circuit C-1 and a "target" circuit C-2 that can be derived from C-1 through only combinational decomposition and extraction. Both circuits are assumed to be networks of single-output basic gates; multiple output gates such as arbiters, toggles, and dual-rail function blocks are not considered. We say that the circuits are combinationally equivalent if the decomposition and extraction preserves the essential functionality of the combinational blocks in the circuit and does not introduce hazards. The paper's focus is the bottleneck of the verification procedure, checking whether C-2 is hazard-free. We show that C-2 is hazard-free if and only if all of its signals are monotonic and acknowledged. We then show how cubes that approximate sets of reachable circuit states can be used to give sufficient conditions for monotonicity and acknowledgement. These sufficient conditions are used to develop a verification technique for combinational equivalence that can be exponentially faster than applying traditional, more general verification techniques. This result can be useful for verifying logic synthesis and technology mapping procedures.