Initial Ideas for Automatic Design and Verification of Control Logic in Reversible HDLs
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Conference on Reversible Computation
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
In imperative reversible languages the commonly used con-
ditional statements must, in addition to the established
if-condition for
forward computation, be extended with an additional
fi-condition for
backward computation. Unfortunately, deriving correct and consistent
fi-conditions is often not obvious. Moreover, implementations exist which
may not be realized with a reversible control flow at all. In this work,we propose automatic methods for descriptions in the reversible HDL
SyReC that can generate the required
fi-conditions and check whether
a reversible control flow indeed can be realized. The envisioned solution utilizes
predicate transformer semantics
based on Hoare logic. The presented ideas constitute the first steps towards automatic methods for
these important designs steps in the domain of reversible circuit design.
Forschungs-