Robert Wille, Oliver Keszöcze, Lars Othmer, Michael Kirkedal Thomsen, Rolf Drechsler,
"Initial Ideas for Automatic Design and Verification of Control Logic in Reversible HDLs"
, in Simon Devitt, Ivan Lanese: Conference on Reversible Computation, Springer International Publishing, Switzerland, Seite(n) 160-166, 2016, ISBN: 978-3-319-40577-3
Original Titel:
Initial Ideas for Automatic Design and Verification of Control Logic in Reversible HDLs
Sprache des Titels:
Englisch
Original Buchtitel:
Conference on Reversible Computation
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-