一句话:为 Verilog 构建模块化精密静态分析套件与基础设施,在真实硬件项目中检出多个未知缺陷。
硬件静态分析长期停留在编译优化与 lint 阶段,无法发现复杂设计缺陷;许多文献报道的硬件 bug 本可由考虑硬件语义与数据流的精密静态分析识别。本文针对主流硬件描述语言 Verilog,提出一组模块化的 bug 检测分析,其建立在一系列基础分析之上,这些基础分析刻画位向量算术、寄存器同步、数字组件并发等硬件特有性质,并支撑硬件数据流与控制流检查。作者还实现了专用基础设施,包括 Verilog 前端、面向分析的中间表示与分析管理器。在平均 1.5K+ GitHub star 的真实 Verilog 项目上评估,发现 9 个此前未知的 bug,均被开发者确认,并检出 18 个现有 linter 无法发现的 bug;每个检测客户端平均仅需约 270 行代码,而从零开发约需 5700 行。系统已开源,含 10 万+ 行代码。
Static analysis has profoundly improved software quality over the past decades, evolving from compiler-integrated optimizations and simple linting to sophisticated analyses for bug detection, security, and program understanding. In contrast, static analysis for hardware remains underexploited, resembling the early state of software analysis. Most existing hardware static analyses are confined to compiler optimizations and linting, lacking the sophistication needed to uncover complex design flaws. Furthermore, we observe that many hardware bugs reported in recent literature could have been identified by sophisticated static analyses that account for hardware-specific semantics and data flow; however, such bug detection analyses are absent today. To exploit the untapped potential of sophisticated hardware analysis, we present a series of bug detection analyses for Verilog, the predominant hardware description language (HDL). Moreover, these analyses are built upon our fundamental analyses that capture essential hardware-specific characteristics---such as bit-vector arithmetic, register synchronization, and digital component concurrency---and enable the examination of hardware data and control flows. Together, these analyses form a well-organized analysis suite with a modular design, in which diverse fundamental analyses combine to support bug detection, hardware understanding, and other potential clients. To implement these analyses, we further offer dedicated infrastructure, including a Verilog front end, an intermediate representation (IR) for analysis, and an analysis manager. To validate the utility of our analyses, we applied them to real-world hardware projects. Unlike software, real-world hardware projects tend to contain fewer but harder-to-detect bugs, as they typically undergo extensive simulation and rigorous verification to prevent the prohibitive costs of hardware defects. Despite this, our preliminary experimental results are highly promising: applying these proposed analyses to popular real-world Verilog projects (averaging 1.5K+ GitHub stars) uncovered nine previously unknown bugs, all confirmed by developers; moreover, we successfully identified a total of 18 bugs beyond the capabilities of existing static analyses for Verilog bug detection (i.e., linters). These results underscore the transformative potential of sophisticated static analysis in hardware design. Our analysis suite and infrastructure are also highly reusable: on average, each bug-detection client built on our analysis suite requires about 270 LoC, compared to 5,700 LoC when developed from scratch. By open-sourcing the entire system, involving substantial engineering effort (100K+ LoC), we aim to encourage further innovation and applications of sophisticated static analysis for hardware, hopefully fostering a similarly vibrant ecosystem that software analysis enjoys.
@article{ChenZWCTMXLL26,
title = {Exploiting Sophisticated Static Analysis for Verilog},
author = {Qinlin Chen and Nairen Zhang and Jinpeng Wang and Jiacai Cui and Tian Tan and Xiaoxing Ma and Chang Xu and Jian Lu and Yue Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808300}
}