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