Verification driven formal architecture and microarchitecture modeling

Yogesh Mahajan, Carven Chan, Ali Bayazit, Sharad Malik, Wei Qin

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

11 Scopus citations

Abstract

Our ability to verify complex hardware lags far behind our capacity to design and fabricate it. We argue that this gap is partly due to the limitations of RTL models when used for verification. Higher level models such as SystemC and SystemVerilog aim to raise the level of abstraction to enhance designer productivity; however, they largely provide for executable but not analyzable descriptions. We propose the use of formally analyzable design models at two distinct levels above RTL: the architecture and the microarchitecture level. At both these levels, we describe concurrent units of data computation termed transactions. The architecture level describes the computation/state updates in the transactions and their interaction through shared data. The microarchitecture level adds to this the resource usage in the transactions as well as their interaction based on shared resources. We then illustrate the applicability of these models in a top-down verification methodology which addresses several concerns of current methodologies.

Original languageEnglish (US)
Title of host publicationProceedings - Fifth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07
Pages123-132
Number of pages10
DOIs
StatePublished - Sep 26 2007
Event5th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07 - Nice, France
Duration: May 30 2007Jun 1 2007

Publication series

NameProceedings - Fifth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07

Other

Other5th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07
CountryFrance
CityNice
Period5/30/076/1/07

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'Verification driven formal architecture and microarchitecture modeling'. Together they form a unique fingerprint.

  • Cite this

    Mahajan, Y., Chan, C., Bayazit, A., Malik, S., & Qin, W. (2007). Verification driven formal architecture and microarchitecture modeling. In Proceedings - Fifth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07 (pp. 123-132). [4231786] (Proceedings - Fifth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07). https://doi.org/10.1109/MEMCOD.2007.371235