Quick formal modeling of communication fabrics to enable verification

Satrajit Chatterjee, Michael Kishinevsky, Umit Y. Ogras

Research output: Chapter in Book/Report/Conference proceedingConference contribution

25 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationHLDVT'10 - IEEE International High Level Design Validation and Test Workshop, Conference Proceedings
Pages42-49
Number of pages8
DOIs
StatePublished - Oct 27 2010
Externally publishedYes
Event2010 15th IEEE International High Level Design Validation and Test Workshop, HLDVT'10 - Anaheim, CA, United States
Duration: Jun 11 2010Jun 12 2010

Publication series

NameProceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT
ISSN (Print)1552-6674

Other

Other2010 15th IEEE International High Level Design Validation and Test Workshop, HLDVT'10
CountryUnited States
CityAnaheim, CA
Period6/11/106/12/10

ASJC Scopus subject areas

  • Software
  • Computer Science Applications
  • Theoretical Computer Science
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Quick formal modeling of communication fabrics to enable verification'. Together they form a unique fingerprint.

Cite this