ISA Modeling with Trace Notation for Context Free Property Generation

Keerthikumara Devarajegowda, Endri Kaja, Sebastian Prebeck, Wolfgang Ecker

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations


The scalable and extendable RISC-V ISA introduced a new level of flexibility in designing highly customizable processors. This flexibility in processor designs adds to the complexity of already complex functional verification process. Although formal methods are increasingly used to exhaustively verify the processors, the required manual effort and verification expertise become the major hurdles in industrial flows. Furthermore, efficient ISA modeling techniques are required that are scalable to multiple ISA extensions and to different architectural variants of a processor. This paper proposes a trace notation for ISA definition to capture the implicit execution behavior of a processor and specific characteristics. The proposed trace notation can be annotated with timing and hierarchy information to adapt the trace to any kind of processor architecture. From this trace notation, a complete set of properties are generated to detect all functional bugs in a processor implementation. The approach requires significantly less manual effort compared to the contemporary techniques. Its industry strength has been demonstrated by formally verifying a wide variety of RISC-V processor implementations with one or more ISA extensions (RV32I, C, Zicsr, M and custom extensions supporting AI acceleration and safety features).

Original languageEnglish
Title of host publication2021 58th ACM/IEEE Design Automation Conference, DAC 2021
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages6
ISBN (Electronic)9781665432740
StatePublished - 5 Dec 2021
Externally publishedYes
Event58th ACM/IEEE Design Automation Conference, DAC 2021 - San Francisco, United States
Duration: 5 Dec 20219 Dec 2021

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X


Conference58th ACM/IEEE Design Automation Conference, DAC 2021
Country/TerritoryUnited States
CitySan Francisco


  • Formal verification
  • ISA modeling
  • Model-driven generation
  • Processor designs


Dive into the research topics of 'ISA Modeling with Trace Notation for Context Free Property Generation'. Together they form a unique fingerprint.

Cite this