Initial ideas for automatic design and verification of control logic in reversible HDLs: work in progress report

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

In imperative reversible languages the commonly used conditional 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.

OriginalsprogEngelsk
TitelReversible Computation : 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings
RedaktørerSimon Devitt, Ivan Lanese
Antal sider7
ForlagSpringer
Publikationsdato2016
Sider160-166
ISBN (Trykt)978-3-319-40577-3
ISBN (Elektronisk)978-3-319-40578-0
DOI
StatusUdgivet - 2016
Begivenhed8th International Conference on Reversible Computation - Bologna, Italien
Varighed: 7 jul. 20168 jul. 2016
Konferencens nummer: 8

Konference

Konference8th International Conference on Reversible Computation
Nummer8
LandItalien
ByBologna
Periode07/07/201608/07/2016
NavnLecture notes in computer science
Vol/bind9720
ISSN0302-9743

ID: 172140550