Equivalence Checking of Reversible Circuits
Robert Wille, Daniel Grosse, D. Michael Miller and Rolf Dreschler
Reversible logic has become an intensely studied research subject due to its application in areas such as quantum computation and low power design. In contrast to traditional CMOS circuits, reversible logic is subject to important restrictions in that fanout and feedback are not allowed. As a result, a new gate library and circuit structure are required. This affects the design flow which has to be reorganized and in which single steps need considerable modification to support reversible logic.
In this paper, circuit equivalence checking is considered in detail. The goal is to show that two reversible circuits are equivalent with respect to a common target functionality which may include don’t-care conditions. The paper explores well-known techniques from irreversible equivalence checking and how those techniques can be applied to reversible circuits.
Two approaches are proposed. The first employs decision diagram techniques and the second uses Boolean satisfiability. In particular, we consider how circuits obtained from different reversible embeddings of the same irreversible target function can be checked. Experimental results show that for both methods, circuits with up to 27,000 gates, as well as adders with more than 100 inputs and outputs, are handled in under three minutes with reasonable memory requirements.
Keywords: reversible logic, equivalence checking, quantum circuits, multi-valued encoding, decision diagrams, Boolean satisfiability.