ISA Modeling with Trace Notation for Context Free Property Generation

Keerthikumara Devarajegowda, Endri Kaja, Sebastian Prebeck, Wolfgang Ecker

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

3 Zitate (Scopus)


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

Titel2021 58th ACM/IEEE Design Automation Conference, DAC 2021
Herausgeber (Verlag)Institute of Electrical and Electronics Engineers Inc.
ISBN (elektronisch)9781665432740
PublikationsstatusVeröffentlicht - 5 Dez. 2021
Extern publiziertJa
Veranstaltung58th ACM/IEEE Design Automation Conference, DAC 2021 - San Francisco, USA/Vereinigte Staaten
Dauer: 5 Dez. 20219 Dez. 2021


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


Konferenz58th ACM/IEEE Design Automation Conference, DAC 2021
Land/GebietUSA/Vereinigte Staaten
OrtSan Francisco


Untersuchen Sie die Forschungsthemen von „ISA Modeling with Trace Notation for Context Free Property Generation“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren