Exploiting inherent characteristics of reversible circuits for faster combinational equivalence checking


Abstract:

Reversible circuits implement invertible logic functions. They are of great interest to cryptography, coding theory, interconnect design, computer graphics, quantum computing, and many other fields. As for conventional circuits, checking the combinational equivalence of two reversible circuits is an important but difficult (coNP-complete) problem. In this work, we present a new approach for solving this problem significantly faster than the state-of-the-art. For this purpose, we exploit inherent characteristics of reversible computation, namely bi-directional (invertible) execution and the XOR-richness of reversible circuits. Bi-directional execution allows us to create an identity miter out of two reversible circuits to be verified, which naturally encodes the equivalence checking problem in the reversible domain. Then, the abundant presence of XOR operations in the identity miter enables an efficient problem mapping into XOR-CNF satisfiability. The resulting XOR-CNF formulas are eventually more compact than pure CNF formulas and potentially easier to solve. As previously anticipated, experimental results show that our equivalence checking methodology is more than one order of magnitude faster, on average, than the state-of-the-art solution based on established CNF-formulation and standard SAT solvers.
Date of Conference: 14-18 March 2016
Date Added to IEEE Xplore: 28 April 2016
Electronic ISBN:978-3-9815-3707-9
Electronic ISSN: 1558-1101
Conference Location: Dresden, Germany

I. Introduction

Reversible computing is a non-conventional computing style where all logic processing is conducted through bijective, i.e., invertible, Boolean functions. Reversible circuits implement invertible Boolean functions at the logic level and are represented as cascades of reversible gates. In conventional technologies, reversible circuits find application in cryptography [1], coding theory [2], interconnect design [3], computer graphics [4] and many other fields where the logic invertibility is a key asset. In emerging technologies, such as quantum computing [5], reversible circuits are one of the primitive computational building blocks.

References

References is not available for this document.