Xmas: Quick formal modeling of communication fabrics to enable verification

Satrajit Chatterjee, Michael Kishinevsky, Umit Ogras

Research output: Contribution to journalArticle

30 Citations (Scopus)

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)
Article number6225465
Pages (from-to)80-88
Number of pages9
JournalIEEE Design and Test of Computers
Volume29
Issue number3
DOIs
StatePublished - 2012
Externally publishedYes

Fingerprint

Communication
Glues
Model checking
Electric wiring
Networks (circuits)
Chemical analysis

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software
  • Electrical and Electronic Engineering

Cite this

Xmas : Quick formal modeling of communication fabrics to enable verification. / Chatterjee, Satrajit; Kishinevsky, Michael; Ogras, Umit.

In: IEEE Design and Test of Computers, Vol. 29, No. 3, 6225465, 2012, p. 80-88.

Research output: Contribution to journalArticle

Chatterjee, Satrajit ; Kishinevsky, Michael ; Ogras, Umit. / Xmas : Quick formal modeling of communication fabrics to enable verification. In: IEEE Design and Test of Computers. 2012 ; Vol. 29, No. 3. pp. 80-88.
@article{8327a56aa4ed4427b0f89ebc9af3e64b,
title = "Xmas: Quick formal modeling of communication fabrics to enable verification",
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.",
author = "Satrajit Chatterjee and Michael Kishinevsky and Umit Ogras",
year = "2012",
doi = "10.1109/MDT.2012.2205998",
language = "English (US)",
volume = "29",
pages = "80--88",
journal = "IEEE Design and Test",
issn = "2168-2356",
publisher = "IEEE Computer Society",
number = "3",

}

TY - JOUR

T1 - Xmas

T2 - Quick formal modeling of communication fabrics to enable verification

AU - Chatterjee, Satrajit

AU - Kishinevsky, Michael

AU - Ogras, Umit

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84867811985&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84867811985&partnerID=8YFLogxK

U2 - 10.1109/MDT.2012.2205998

DO - 10.1109/MDT.2012.2205998

M3 - Article

AN - SCOPUS:84867811985

VL - 29

SP - 80

EP - 88

JO - IEEE Design and Test

JF - IEEE Design and Test

SN - 2168-2356

IS - 3

M1 - 6225465

ER -