281
views
0
recommends
+1 Recommend
1 collections
    4
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Verification of an Optimized Fault-Tolerant Clock Synchronization Circuit

      proceedings-article
      ,
      Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96) (DCC)
      Designing Correct Circuits
      2 - 4 September 1996
      Bookmark

            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.

            Content

            Author and article information

            Conference
            September 1996
            September 1996
            : 1-15
            Affiliations
            [0001]Flight Electronics Technology Division, NASA Langley Research Center

            Hampton, VA, USA
            [0002]Department of Computer Science, Indiana University

            Bloomington, IN, USA
            Article
            10.14236/ewic/DCC1996.9
            f0c0def7-f988-473d-8064-94db696f5ebb
            © 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

            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/

            Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96)
            DCC
            3
            Båstad, Sweden
            2 - 4 September 1996
            Electronic Workshops in Computing (eWiC)
            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
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction

            Comments

            Comment on this article