ChiSA: Static Analysis for Lightweight Chisel Verification

The growing demand for productivity in hardware development opens up new opportunities for applying programming language (PL) techniques to hardware description languages (HDLs). Chisel, a leading agile HDL, embraces this shift by leveraging modern PL features to enhance hardware design productivity. However, verification for Chisel remains a major productivity bottleneck, requiring substantial time and manual effort. To address this issue, we advocate the use of static analysis-a technique proven well-suited to agile development workflows in software-for lightweight Chisel verification.

This work establishes a theoretical foundation for Chisel static analysis. At its core is 𝜆 𝐶 , a formal core calculus of ChAIR (a Chisel-specific intermediate representation for analysis). 𝜆 𝐶 is the first formalism that captures the essence of Chisel while being deliberately minimal to ease rigorous reasoning about static analysis built on 𝜆 𝐶 . We prove key properties of 𝜆 𝐶 that reflect real hardware characteristics, which in turn offer a form of retrospective validation for its design. On the basis of 𝜆 𝐶 , we define and formalize the hardware value flow analysis (HVFA) problem, which underpins our static analyses for critical Chisel verification tasks, including bug detection and security analysis. We then propose a synchronized fixed-point solution to the HVFA problem, featuring hardware-specific treatment of the synchronous behavior of clock-driven hardware registers-the essential feature of Chisel programs. We further prove key theorems establishing the guarantees and limitations of our solution.

As a proof of concept, we develop ChiSA (30K+ LoC)-the first Chisel static analyzer that can analyze intricate hardware value flows to enable lightweight analyses for critical Chisel verification tasks such as bug detection and security analysis. To facilitate thorough evaluation of both ChiSA and future work, we provide ChiSABench (11M+ LoC), a comprehensive benchmark for Chisel static analysis.

Our evaluation on ChiSABench demonstrates that ChiSA offers an effective and significantly more lightweight approach for critical Chisel verification tasks, especially on large and complex real-world designs. For example, ChiSA identified 69 violable developer-inserted assertions in large-scale Chisel designs (9.7M+ LoC) in under 200 seconds-eight of which were recognized by developers and scheduled for future fixes-and detected all 60 information-leak vulnerabilities in the well-known TrustHub benchmark (1.1M+ LoC) in just one second-outperforming state-of-the-art Chisel approaches like ChiselTest's bounded model checking and ChiselFlow's secure type system. These results underscore the high promise of static analysis for lightweight Chisel verification. To encourage continued research and innovation, we will fully open-source ChiSA (30K+ LoC) and ChiSABench (11M+ LoC).