Blog
About

142
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 of the 3rd Workshop on Designing Correct Circuits (DCC96) (DCC)

      Designing Correct Circuits

      2 - 4 September 1996

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references 2

          • Record: found
          • Abstract: not found
          • Article: not found

          A new fault-tolerant algorithm for clock synchronization

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Non-restoring integer square root A case study in design by principled optimization

              Bookmark

              Author and article information

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

              Hampton, VA, USA
              Department of Computer Science, Indiana University

              Bloomington, IN, USA
              Article
              10.14236/ewic/DCC1996.9
              © 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 (journal page): https://ewic.bcs.org/
              Categories
              Electronic Workshops in Computing

              Comments

              Comment on this article