An automated approach for generating and checking control logic for reversible hardware description language-based designs

TY - GEN

T1 - An automated approach for generating and checking control logic for reversible hardware description language-based designs

AU - Wille, Robert

AU - Keszocze, Oliver

AU - Othmer, Lars

AU - Thomsen, Michael Kirkedal

AU - Drechsler, Rolf

N1 - Conference code: 6

PY - 2017/12

Y1 - 2017/12

N2 - Although different from the conventional computing paradigm, reversible computation received significant interest due to its applications in various (emerging) technologies. Here, computations can be executed not only from the inputs to the outputs, but also in the reverse direction. This leads to significantly different design challenges to be addressed. In this work, we consider problems that occur when describing a reversible control flow using Hardware Description Languages (HDLs). Here, the commonly used conditional statements must, in addition to the established if-condition for forward computation, be provided with an additional fi-condition for backward computation. Unfortunately, deriving correct and consistent fi-conditions is often not obvious. Moreover, HDL descriptions exist which may not be realized with a reversible control flow at all. In this work, we propose automatic solutions, which generate the required and check whether a reversible control flow indeed can be realized. The solution utilizes predicate transformer semantics based on Hoare logic. This has exemplary been implemented for the reversible HDL SyReC and evaluated with a variety of circuit description examples. The proposed solution constitutes the first automatic method for these important designs steps in the domain of reversible circuit design.

AB - Although different from the conventional computing paradigm, reversible computation received significant interest due to its applications in various (emerging) technologies. Here, computations can be executed not only from the inputs to the outputs, but also in the reverse direction. This leads to significantly different design challenges to be addressed. In this work, we consider problems that occur when describing a reversible control flow using Hardware Description Languages (HDLs). Here, the commonly used conditional statements must, in addition to the established if-condition for forward computation, be provided with an additional fi-condition for backward computation. Unfortunately, deriving correct and consistent fi-conditions is often not obvious. Moreover, HDL descriptions exist which may not be realized with a reversible control flow at all. In this work, we propose automatic solutions, which generate the required and check whether a reversible control flow indeed can be realized. The solution utilizes predicate transformer semantics based on Hoare logic. This has exemplary been implemented for the reversible HDL SyReC and evaluated with a variety of circuit description examples. The proposed solution constitutes the first automatic method for these important designs steps in the domain of reversible circuit design.

KW - Control Flow

KW - Hardware Descriptions Languages

KW - Hoare Logic

KW - Reversible Circuits

KW - Synthesis

UR - http://www.scopus.com/inward/record.url?scp=85039049000&partnerID=8YFLogxK

U2 - 10.1166/jolpe.2017.1515

DO - 10.1166/jolpe.2017.1515

M3 - Conference article

AN - SCOPUS:85039049000

SN - 1546-1998

VL - 13

SP - 633

EP - 641

JO - Journal of Low Power Electronics

JF - Journal of Low Power Electronics

IS - 4

T2 - 6th International Symposium on Embedded Computing and System Design

Y2 - 15 December 2016 through 17 December 2016

ER -