• Design&Test
  • PrePrints
  • Abstract - xMAS: Quick Formal Modeling of Communication Fabrics to Enable Verification
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
xMAS: Quick Formal Modeling of Communication Fabrics to Enable Verification
PrePrint
ISSN: 0740-7475
Satrajit Chatterjee, Intel, Hillsboro
Mike Kishinevsky, Intel , Hillsboro
Umit Ogras, Intel Corp. , Hillsboro
Although communication fabrics at the microarchitectural level are mainly composed of standard primitives such as queues and arbiters, to get an executable model one has to connect these primitives with glue logic to complete the description. In this paper we identify a richer set of microarchitectural primitives that allows us to describe complete systems by composition alone. This enables us to build models faster (since models are now simply wiring diagrams at an appropriate level of abstraction) and to avoid common modeling errors such as inadvertent loss of data due to incorrect timing assumptions. Our models are formal and they are used for model checking as well as dynamic validation and performance modeling. However, unlike other formalisms this approach leads to a precise yet intuitive graphical notation for microarchitecture that captures timing and functionality in sufficient detail to be useful for reasoning about correctness and for communicating microarchitectural ideas to RTL and circuit designers and validators.
Index Terms:
C.1 Processor Architectures, C.0.d Modeling of computer architecture, C.0.e System architectures, integration and modeling, B.4.3.f Topology, B Hardware, B.6.2 Reliability and Testing, C.3.d Real-time and embedded systems, B.7.2.e Verification, B Hardware, B.1.4.e Verification,
Citation:
Satrajit Chatterjee, Mike Kishinevsky, Umit Ogras, "xMAS: Quick Formal Modeling of Communication Fabrics to Enable Verification," IEEE Design & Test of Computers, 08 June 2011. IEEE computer Society Digital Library. IEEE Computer Society, <http://doi.ieeecomputersociety.org/10.1109/MDT.2011.72>
Usage of this product signifies your acceptance of the Terms of Use.