Automating hazard checking in transaction-level microarchitecture models

Yogesh Mahajan, Sharad Malik

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

5 Scopus citations

Abstract

Traditional hardware modeling using RTL presents a time-stationary view of the design state space which can be used to specify temporal properties for model checking. However, high-level information in terms of computation being performed on units of data (transactions) is not directly available. In contrast, transaction-level microarchitecture models view the computation as sequences of (data-stationary) transactions. This makes it easy to specify properties which involve both transaction sequencing and temporal ordering (e.g. data hazards). In RTL models, additional book-keeping state must be manually introduced in order to specify and check these properties. We show here that a transaction-level microarchitecture model can help automate checks for such properties via the automated creation of the book-keeping structures, and illustrate this for a simple pipeline using SMV. A key challenge in model-checking the transactionlevel microarchitecture is representing the dynamic transaction state space. We describe an encoding as well as a fixed point computation for this.

Original languageEnglish (US)
Title of host publicationProceedings - Formal Methods in Computer Aided Design, FMCAD 2007
Pages62-65
Number of pages4
DOIs
StatePublished - Dec 1 2007
EventFormal Methods in Computer Aided Design, FMCAD 2007 - Austin, TX, United States
Duration: Nov 11 2007Nov 14 2007

Publication series

NameProceedings - Formal Methods in Computer Aided Design, FMCAD 2007

Other

OtherFormal Methods in Computer Aided Design, FMCAD 2007
CountryUnited States
CityAustin, TX
Period11/11/0711/14/07

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Automating hazard checking in transaction-level microarchitecture models'. Together they form a unique fingerprint.

  • Cite this

    Mahajan, Y., & Malik, S. (2007). Automating hazard checking in transaction-level microarchitecture models. In Proceedings - Formal Methods in Computer Aided Design, FMCAD 2007 (pp. 62-65). [4401983] (Proceedings - Formal Methods in Computer Aided Design, FMCAD 2007). https://doi.org/10.1109/FAMCAD.2007.33