Utility of transaction-level hardware models in refinement checking

Yogesh Mahajan, Sharad Malik

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

Abstract

Verifying a cycle-accurate RTL model against its functional specification using refinement checking uses a joint execution model to compare the executions of the two models. Creating and instrumenting such a joint execution model manually can be tedious and error-prone. In this paper, we illustrate the use of transaction-based models (e.g. [1]) in simplifying the process of creating and instrumenting joint execution models for refinement checking. We first show how transaction-based specification and implementation models allow simple refinement relations to be written using model variables and constructs. We then show how a joint encoding of the two models can be generated together with assertions expressing the specified refinement relation. This approach avoids the manual bookkeeping otherwise needed for coordinating the executions of the design and the specification, and exchanging information between the two models. We illustrate the ideas on a toy example.

Original languageEnglish (US)
Title of host publicationHLDVT'10 - IEEE International High Level Design Validation and Test Workshop, Conference Proceedings
Pages121-128
Number of pages8
DOIs
StatePublished - Oct 27 2010
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

All Science Journal Classification (ASJC) codes

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

Fingerprint Dive into the research topics of 'Utility of transaction-level hardware models in refinement checking'. Together they form a unique fingerprint.

  • Cite this

    Mahajan, Y., & Malik, S. (2010). Utility of transaction-level hardware models in refinement checking. In HLDVT'10 - IEEE International High Level Design Validation and Test Workshop, Conference Proceedings (pp. 121-128). [5496650] (Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT). https://doi.org/10.1109/HLDVT.2010.5496650