Verification of an Optimized Fault-Tolerant Clock Synchronization Circuit

Abstract

In previous work, we explored the interaction between different formal hardware development techniques in the implementation of a fault-tolerant clock synchronization circuit. This case study presents a clever optimization of the earlier design and illustrates how we have extended our framework to support its incremental design refinement. The primary design tool represents circuits as systems of stream equations, where each stream corresponds to a signal within the circuit. These signals are annotated with invariants which can be established using proof by co-induction. These invariants are exploited to verify localized design refinements. This study lays groundwork for a more formal integration of disparate reasoning tools.

Conference

Publication date: September 1996

Publication date (Print): September 1996

Pages: 1-15

Affiliations

Flight Electronics Technology Division, NASA Langley Research Center

Hampton, VA, USA

Department of Computer Science, Indiana University

Bloomington, IN, USA

Article

DOI: 10.14236/ewic/DCC1996.9

Copyright statement: © Paul S. Miner et al. Published by BCS Learning and Development Ltd. Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96), Båstad, Sweden

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96)

Conference acronym: DCC

Conference number: 3

Conference location: Båstad, Sweden

Conference date: 2 - 4 September 1996

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Designing Correct Circuits

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/DCC1996.9

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing