SystemVerilog Assertion Verification with CIRCT

on YouTube ↗16m

" summary

Claims that CIRCT can represent and process concurrent SystemVerilog Assertions by importing slang ASTs and lowering SVA to a CIRCT LTL dialect, with prototype transformations that already translate many sequences and removes name sequences so they become analyzable. Built a transformation pipeline that targets simulation and potential synthesis via Yosys lowering, but handling clock switches, sequential regular expressions and local variables remains unfinished; current work proves feasibility and accepts small PRs to extend support.

AI-written summary · about

" chapters (9)

1. 0:00SystemVerilog Assertions intro
2. 2:51Open-source EDA limits
3. 4:17CIRCT for SVA support
4. 7:51Complex SVA behavior
5. 9:18Current SVA in CIRCT
6. 10:02CIRCT future for SVA
7. 11:29Q&A: Linear Temporal Logic
8. 12:11Q&A: Backend & formal flow
9. 13:57Q&A: Debugging sequences

" related talks

• 24mOpen source RTL verification with VerilatorKarol Gugala · Latch-Up 2024
• 18mMore than the Core Verifying RISC V SoCsNicolae Tusinschi · RISC-V Summit 2019
• 46mIntroduction to Formal Verification with Symbiotic EDA Open Source ToolsMatt Venn, Clifford Wolf · Week of Open Source Hardware 2019
• 25mRISC-V System-level Certification from Verification FoundationsAdnan Hamid · RISC-V Summit North America 2025
• 24mRISC V Processor Verification based on Open source FrameworkLee Moore, Richard Ho · RISC-V Summit 2019
• 47mTutorial: Choosing Appropriate Verification Techniques for Desired RISC...Aimee Sutton, Lee Moore · RISC-V Summit 2022
• 21mCombined Dynamic and Formal Verification Approach to Processor VerificationAimee Sutton, Xiaolin Chen · RISC-V Summit North America 2024
• 23mOpen Source Verification Platform for RISC V ProcessorsTao Liu, Richard Ho · RISC-V Summit 2019