Exploiting Sophisticated Static Analysis for Verilog
summary
A Verilog static-analysis framework named THU provides a front end, IR, analysis manager and a suite of 40 analyses built on reusable fundamentals (bit-vector arithmetic, register/clock/reset mapping, synchronization) and ships as 100K+ LoC open source. A missing reset detector reasons about cyclic register dependencies and undefined-value loops. Applied to million-line codebases it runs 40 analyses in ~6 minutes, finds 18 real bugs across eight categories (nine previously unknown, all confirmed), and yields 97% precision/recall on clock/reset/register inference.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:23Hardware static analysis potential
- 1:28Evolution of static analysis
- 3:16THU framework intro
- 4:41Fundamental THU analysis
- 5:43Missing reset problem
- 8:35Hardware challenges: missing reset
- 10:43Building missing reset analysis
- 12:06THU’s analysis suite
- 12:47Experimental bug detection results
- 14:57Community adoption and resources
- 15:39Q&A: soundness and implementation
- 16:44Q&A: bug reporting and expressiveness
- 17:52Q&A: physical design and timing
- 19:19Closing remarks
related talks
21mTowards Compiler-Guided Static Analysis
01h 01m“Static Analysis and C++: More Than Lint"
23mTargeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code
53mFrom Within: Compiler Testing and Validation via Compilers
14mCollapsing Towers for Side-Channel Security
18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...
53mLocknote: How Badly Do We Want Correct Compilers?
15mFormulog: Datalog for SMT-Based Static Analysis