Initial ideas for automatic design and verification of control logic in reversible HDLs: work in progress report
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Initial ideas for automatic design and verification of control logic in reversible HDLs : work in progress report. / Wille, Robert; Keszocze, Oliver; Othmer, Lars; Thomsen, Michael Kirkedal; Drechsler, Rolf.
Reversible Computation: 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings. red. / Simon Devitt; Ivan Lanese. Springer, 2016. s. 160-166 (Lecture notes in computer science, Bind 9720).Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Initial ideas for automatic design and verification of control logic in reversible HDLs
AU - Wille, Robert
AU - Keszocze, Oliver
AU - Othmer, Lars
AU - Thomsen, Michael Kirkedal
AU - Drechsler, Rolf
N1 - Conference code: 8
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84978922947&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-40578-0_11
DO - 10.1007/978-3-319-40578-0_11
M3 - Article in proceedings
AN - SCOPUS:84978922947
SN - 978-3-319-40577-3
T3 - Lecture notes in computer science
SP - 160
EP - 166
BT - Reversible Computation
A2 - Devitt, Simon
A2 - Lanese, Ivan
PB - Springer
Y2 - 7 July 2016 through 8 July 2016
ER -
ID: 172140550