paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Simulator Independent Coverage for RTL Hardware Languages

RTL 硬件语言的模拟器无关覆盖率
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32023匹配度 2/10 · 论文属于硬件 RTL 覆盖率与编译器插桩/形式验证后端,虽涉及编译器 pass、覆盖率与形式化验证,但用户核心方向是 LLM/Agent 与静态分析/形式化验证的结合,以及浮点程序分析、贝叶斯程序分析与 LLM 的交叉;本文不涉及 AI、LLM、浮点或贝叶斯,因此匹配度低。引用 7 inbox
Kevin Laeufer, Vighnesh Iyer, David Biancolin, Jonathan Bachrach, Borivoje Nikolić, Koushik Sen
crossref: 2026-09-12

AI 速览

一句话:提出一种通过编译器 pass 和 cover 原语实现的模拟器无关 RTL 覆盖率框架,支持多种仿真、FPGA 加速与形式验证后端。

硬件验证中的行覆盖率、翻转覆盖率和有限状态机覆盖率通常与具体仿真器绑定,难以跨工具合并和复用。本文提出一种与后端解耦的覆盖率实现方法:每种覆盖率由编译器 pass 插入基于新 cover 原语的探测代码,并由独立报告生成器汇总,通过简单 API 适配软件仿真、仿真加速和形式验证工具。作者在 Chisel 硬件构造语言中实现原型,并展示其在三个软件仿真器、FPGA 加速的 FireSim 以及一个形式工具上的支持。实验中,他们在 FireSim 上以 65MHz 目标频率启动 Linux 并收集行覆盖率;由于设计上统一了原语,覆盖率可跨后端直接合并。

问题
如何为 RTL 硬件语言实现不依赖特定仿真或验证后端的自动化覆盖率指标,并支持跨后端合并与复用。
方法
将行、翻转和 FSM 覆盖率分别实现为编译器 pass 和报告生成器,围绕单一 cover 原语设计 API,使其与底层仿真、FPGA 仿真或形式工具解耦。
评估
在 Chisel 原型上接入三个软件仿真器、FireSim 和形式工具,并在 FireSim 以 65MHz 启动 Linux 时收集行覆盖率,验证跨后端覆盖率合并。
原文摘要(Abstract)

We demonstrate a new approach to implementing automated coverage metrics including line, toggle, and finite state machine coverage. Each metric is implemented through a compiler pass with a report generator. They are decoupled from the backend simulation, emulation, or formal verification tool through a simple API designed around a single new cover primitive. Our prototype for the Chisel hardware construction language demonstrates support across three software simulators, the FPGA-accelerated FireSim simulator and a formal tool. We demonstrate collecting line coverage while booting Linux with FireSim at a target frequency of 65MHz. By construction, coverage can be trivially merged across backends.

链接与引用

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

BibTeX
@inproceedings{paperbot10105,
  title = {Simulator Independent Coverage for RTL Hardware Languages},
  author = {Kevin Laeufer and Vighnesh Iyer and David Biancolin and Jonathan Bachrach and Borivoje Nikolić and Koushik Sen},
  booktitle = {ASPLOS},
  year = {2023},
  doi = {10.1145/3582016.3582019}
}