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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.

Original languageEnglish
Title of host publicationReversible Computation : 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings
EditorsSimon Devitt, Ivan Lanese
Number of pages7
Publication date2016
ISBN (Print)978-3-319-40577-3
ISBN (Electronic)978-3-319-40578-0
Publication statusPublished - 2016
Event8th International Conference on Reversible Computation - Bologna, Italy
Duration: 7 Jul 20168 Jul 2016
Conference number: 8


Conference8th International Conference on Reversible Computation
SeriesLecture notes in computer science

ID: 172140550