一句话：提出 Chisel 静态分析形式基础与硬件值流分析方法，并实现首个 Chisel 静态分析器 ChiSA，支持轻量级验证。
Chisel 等敏捷 HDL 提升硬件开发效率，但其验证仍耗时且依赖人工。本文倡导用静态分析实现轻量级 Chisel 验证，并建立形式基础：提出核心演算 λC，刻画 Chisel/CHAIR 本质并证明反映硬件特性的性质；定义硬件值流分析（HVFA）问题，针对时钟驱动寄存器的同步行为提出同步不动点求解，并证明其保证与局限。作者实现首个 Chisel 静态分析器 ChiSA（30K+ LoC）及基准 ChiSABench（11M+ LoC）。评估中，ChiSA 在 9.7M+ LoC 设计里 200 秒内发现 69 个可违反断言（8 个被开发者确认），并在 1 秒内检出 TrustHub 全部 60 个信息泄漏漏洞，优于 ChiselTest 有界模型检测和 ChiselFlow 安全类型系统。
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 λ C , a formal core calculus of ChAIR (a Chisel-specific intermediate representation for analysis). λ C is the first formalism that captures the essence of Chisel while being deliberately minimal to ease rigorous reasoning about static analysis built on λ C . We prove key properties of λ C that reflect real hardware characteristics, which in turn offer a form of retrospective validation for its design. On the basis of λ C , 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).
@article{CuiCZTL26,
title = {ChiSA: Static Analysis for Lightweight Chisel Verification},
author = {Jiacai Cui and Qinlin Chen and Zhongsheng Zhan and Tian Tan and Yue Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776660}
}