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

Robert Wille; Oliver Keszocze; Lars Othmer; Michael Kirkedal Thomsen; Rolf Drechsler

doi:10.1007/978-3-319-40578-0_11

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

Robert Wille^*, Oliver Keszocze, Lars Othmer, Michael Kirkedal Thomsen, Rolf Drechsler

^*Corresponding author for this work

Department of Computer Science

1 Citation (Scopus)

Abstract

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 language	English
Title of host publication	Reversible Computation : 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings
Editors	Simon Devitt, Ivan Lanese
Number of pages	7
Publisher	Springer
Publication date	2016
Pages	160-166
ISBN (Print)	978-3-319-40577-3
ISBN (Electronic)	978-3-319-40578-0
DOIs	https://doi.org/10.1007/978-3-319-40578-0_11
Publication status	Published - 2016
Event	8th International Conference on Reversible Computation - Bologna, Italy Duration: 7 Jul 2016 → 8 Jul 2016 Conference number: 8

Conference

Conference	8th International Conference on Reversible Computation
Number	8
Country/Territory	Italy
City	Bologna
Period	07/07/2016 → 08/07/2016

Series	Lecture notes in computer science
Volume	9720
ISSN	0302-9743

Access to Document

10.1007/978-3-319-40578-0_11

Cite this

Wille, R., Keszocze, O., Othmer, L., Thomsen, M. K., & Drechsler, R. (2016). Initial ideas for automatic design and verification of control logic in reversible HDLs: work in progress report. In S. Devitt, & I. Lanese (Eds.), Reversible Computation: 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings (pp. 160-166). Springer. Lecture notes in computer science Vol. 9720 https://doi.org/10.1007/978-3-319-40578-0_11

Initial ideas for automatic design and verification of control logic in reversible HDLs : work in progress report. / Wille, Robert; Keszocze, Oliver; Othmer, Lars et al.

Reversible Computation: 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings. ed. / Simon Devitt; Ivan Lanese. Springer, 2016. p. 160-166 (Lecture notes in computer science, Vol. 9720).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Wille, R, Keszocze, O, Othmer, L, Thomsen, MK & Drechsler, R 2016, Initial ideas for automatic design and verification of control logic in reversible HDLs: work in progress report. in S Devitt & I Lanese (eds), Reversible Computation: 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings. Springer, Lecture notes in computer science, vol. 9720, pp. 160-166, 8th International Conference on Reversible Computation, Bologna, Italy, 07/07/2016. https://doi.org/10.1007/978-3-319-40578-0_11

Wille R, Keszocze O, Othmer L, Thomsen MK, Drechsler R. Initial ideas for automatic design and verification of control logic in reversible HDLs: work in progress report. In Devitt S, Lanese I, editors, Reversible Computation: 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings. Springer. 2016. p. 160-166. (Lecture notes in computer science, Vol. 9720). doi: 10.1007/978-3-319-40578-0_11

Wille, Robert ; Keszocze, Oliver ; Othmer, Lars et al. / Initial ideas for automatic design and verification of control logic in reversible HDLs : work in progress report. Reversible Computation: 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings. editor / Simon Devitt ; Ivan Lanese. Springer, 2016. pp. 160-166 (Lecture notes in computer science, Vol. 9720).

@inproceedings{3cf360c858044bc996dbf534147f7032,

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

abstract = "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.",

author = "Robert Wille and Oliver Keszocze and Lars Othmer and Thomsen, {Michael Kirkedal} and Rolf Drechsler",

year = "2016",

doi = "10.1007/978-3-319-40578-0_11",

language = "English",

isbn = "978-3-319-40577-3 ",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "160--166",

editor = "Simon Devitt and Ivan Lanese",

booktitle = "Reversible Computation",

note = "8th International Conference on Reversible Computation ; Conference date: 07-07-2016 Through 08-07-2016",

}

TY - GEN

T1 - Initial ideas for automatic design and verification of control logic in reversible HDLs

T2 - 8th International Conference on Reversible Computation

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 -

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

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this