ChiSA: Static Analysis for Lightweight Chisel Verification
summary
ChiSA gives a formal core calculus lambda_C and a synchronized fixed‑point solver for hardware value flow analysis (HVFA), plus a 30K+ LoC analyzer and an 11M+ LoC benchmark ChiSABench. It proves soundness/limits for synchronous registers and clock semantics, finds 69 developer‑inserted violable assertions in 9.7M+ LoC in under 200s, and detects all 60 TrustHub info‑leak bugs in 1.1M+ LoC in one second — outperforming ChiselTest BMC and ChiselFlow.
AI-written summary · about