../

ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation

Year
2024
Authors
Bhabesh Mali, Karthik Maddala, Vatsal Gupta, Sweeya Reddy, Chandan Karfa, Ramesh Karri
DOI
10.1109/ISVLSI61997.2024.00130

Related

Persistent Notes

  • Their approach involves converting the RTL and the design specification into a JSON format.
  • Their benchmarks used are design from OpenTitan
    • RV_TIMER
    • PattGen
    • GPIO
    • ROM_Ctrl
    • sram_ctrl
    • adc_ctrl
  • There is no mention of coverage
  • Since they are continuously iterating, I am assuming that they generated assertions are correct
  • For each module they are generating only handful of assertions
  • Their comparison against the number of assertions given in OpenTitan is flawed. I am not sure if OpenTitan is trying to perform formal verification on all their designs
    • As per https://opentitan.org/book/hw/index.html, they mostly do dynamic testing at first. They have plans to do formal verification but it is not yet complete
    • Hence it is not appropriate to compare the #(assertions)

In-text annotations

“I. INTRODUCTION” Page 680

“II. RELATED WORKS” Page 680

“III. CHIRAAG: OUR SVA GENERATION FRAMEWORK” Page 681

“A. Formatting of specification” Page 681

“B. Automatic Assertion Generation” Page 681

“IV. CASE STUDY: RV TIMER” Page 681

“V. EXPERIMENTAL RESULTS AND DISCUSSIONS” Page 682

“Interestingly, ChIRAAG generates more assertions than that was provided in OpenTitan. Importantly, ChIRAAG-generated assertions are important and satisfy some aspects of the design that were missed by the OpenTitan assertions." Page 683

Define “missed”? There is no coverage metric. We cannot naively compare #(assertions). It is pretty easy to write vacuous assertions that prove nothing. Page 683

“VI. CONCLUSION” Page 683

%% Import Date: 2026-01-02T15:44:11.028-05:00 %%