Open-source model checkers: Ready for the industry?

on YouTube ↗22m

" summary

An experimental comparison of several open-source model checkers for Verilog, evaluating their Verilog support and property-checking on both typical and industrial-scale modules using open benchmarks. Also presents Retrascope, an open-source tool that verifies Verilog against SVA properties and provides HDL analysis, model reconstruction and visualization, plus using those models for test generation and property checking.

AI-written summary · about

" chapters (14)

1. 0:00Intro
2. 0:19Formal Verification in HDL
3. 2:34HDL Model Checkers: History
4. 5:02Problem statement
5. 6:36Tool Overview
6. 7:27Retrascope Toolkit (1)
7. 9:09Hardware benchmarks
8. 10:02Selected Verilog benchmarks
9. 10:24Experiment #1: Verilog support
10. 11:28Experiment #1: Results
11. 13:00Experiment #2: Property checking
12. 15:53Case study
13. 16:57Conclusion
14. 18:37Unsupported (but correct!) Verilog

" related talks

• 18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...Simon Davidmann · RISC-V Summit 2022
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...Larry Lapides · RISC-V Summit 2022
• 11mDemo: More Than Point Tools: RISC-V SolutionsLarry Lapides · RISC-V Summit North America 2024
• 18mThe Essence of Verilog: A Tractable and Tested Operational Semantics for Verilo...Yue Li, Tian Tan, Qinlin Chen, Nairen Zhang, Jinpeng Wang, Chang Xu, Xiaoxing Ma · OOPSLA 2023
• 19mExploiting Sophisticated Static Analysis for VerilogYue Li, Tian Tan, Qinlin Chen, Nairen Zhang, Jinpeng Wang, Chang Xu, Xiaoxing Ma, Jiacai Cui, Jian Lu · PLDI 2026
• 51mSynthesis and Verification for AllEmina Torlak · Clojure/west 2017
• 53mSemantics-based program manipulation in the age of LLMsWilliam J. Bowman, Sam Lindley, Brigitte Pientka, Satnam Singh · PEPM 2025