paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Exploiting Sophisticated Static Analysis for Verilog

面向 Verilog 的精密静态分析探索
PLDI 10(PLDI)2026匹配度 4/10 · 论文属于静态分析与抽象解释方向,且强调模块化分析套件、工程基础设施和工业真实项目缺陷检出,符合用户对理论+工程、工业落地和问题驱动研究的偏好;但其研究对象是 Verilog 硬件设计,与用户当前核心关注的 ML/Agentic 程序静态分析、LLM 与静态分析/形式化验证交叉、浮点程序分析或贝叶斯程序分析均无直接交集。引用 0 inbox
Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, Yue Li
crossref: 2026-09-10

AI 速览

一句话:为 Verilog 构建模块化精密静态分析套件与基础设施,在真实硬件项目中检出多个未知缺陷。

硬件静态分析长期停留在编译优化与 lint 阶段,无法发现复杂设计缺陷;许多文献报道的硬件 bug 本可由考虑硬件语义与数据流的精密静态分析识别。本文针对主流硬件描述语言 Verilog,提出一组模块化的 bug 检测分析,其建立在一系列基础分析之上,这些基础分析刻画位向量算术、寄存器同步、数字组件并发等硬件特有性质,并支撑硬件数据流与控制流检查。作者还实现了专用基础设施,包括 Verilog 前端、面向分析的中间表示与分析管理器。在平均 1.5K+ GitHub star 的真实 Verilog 项目上评估,发现 9 个此前未知的 bug,均被开发者确认,并检出 18 个现有 linter 无法发现的 bug;每个检测客户端平均仅需约 270 行代码,而从零开发约需 5700 行。系统已开源,含 10 万+ 行代码。

问题
硬件静态分析远落后于软件分析,现有工具多局限于编译优化与 lint,缺乏考虑硬件特有语义的精密分析,难以发现复杂设计缺陷。
方法
构建捕获位向量算术、寄存器同步、数字组件并发等硬件特性的基础分析,并据此设计模块化 bug 检测分析套件,配套 Verilog 前端、分析 IR 与分析管理器等基础设施。
评估
在平均 1.5K+ GitHub star 的真实 Verilog 项目上评估,发现的 9 个未知 bug 均被开发者确认,并检出 18 个现有 linter 无法发现的 bug。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@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}
}