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

      Specifying and Property Checking the AMULET1 Address Interface

      ,

      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

          We describe work completed on the specification and verification of the address interface of AMULET1, an industrial strength asynchronousmicroprocessor designed, fabricated and tested by Manchester University. AMULET1 is an asynchronous version of ARM, the best selling RISC chip in the 1980’s, and now a leading macro-cell. The address interface is a substantial floor plan element, shared by several processes,which acts as a filter into memory for pc-values, memory swap, and single and multiple load/store operations. The specification is at the register transfer level and is sufficiently detailed to detect the known deadlocks in earlier designs and verify that the final version is deadlock free. The specification work was carried out in Milner’s Calculus of Communicating Systems (CCS) and property checked using the ConcurrencyWorkbench (CWB). The work described is post facto—it was started after the AMULET1 chip had been sent for fabrication.

          Related collections

          Most cited references 3

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

          Micropipelines

           I. Sutherland (1989)
            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            An introduction to modal and temporal logics for CCS

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

              Computing without Clocks Micropipelining the ARM Processor

               Steve Furber (1995)
                Bookmark

                Author and article information

                Conference
                September 1996
                September 1996
                : 1-20
                Affiliations
                Northern Telecomm, Ottawa, Canada
                Computer Studies, Leeds, UK
                Article
                10.14236/ewic/DCC1996.6
                © Ying Liu 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