Exploiting inherent characteristics of reversible circuits for faster combinational equivalence checking

Luca Amarú, Pierre Emmanuel Gaillardon, Robert Wille, Giovanni De Micheli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

18 Scopus citations

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.

Original languageEnglish
Title of host publicationProceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages175-180
Number of pages6
ISBN (Electronic)9783981537062
StatePublished - 25 Apr 2016
Externally publishedYes
Event19th Design, Automation and Test in Europe Conference and Exhibition, DATE 2016 - Dresden, Germany
Duration: 14 Mar 201618 Mar 2016

Publication series

NameProceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016

Conference

Conference19th Design, Automation and Test in Europe Conference and Exhibition, DATE 2016
Country/TerritoryGermany
CityDresden
Period14/03/1618/03/16

Fingerprint

Dive into the research topics of 'Exploiting inherent characteristics of reversible circuits for faster combinational equivalence checking'. Together they form a unique fingerprint.

Cite this