一句话：Hassert 将 SystemVerilog 断言自动调度映射到 FPGA 与待测设计并行执行，并以运行时重构与硬件快照实现细粒度调试。
硬件验证是芯片开发周期的瓶颈：软件仿真检查断言耗时极长，而 FPGA 原型又缺乏细粒度调试能力。本文提出 Hassert，一个软硬件结合的断言验证（ABV）框架。它自动调度并把 SystemVerilog 断言（SVA）映射到 FPGA 上与待测设计（DUT）一同运行，并可在运行时通过部分重构动态切换断言（用户指定或依据 SVA 覆盖率满足情况），无需重新编译 DUT。为进一步提升调试效率，作者提出微架构引导的硬件快照方案：断言触发时自动对整个 FPGA 状态拍快照，再传输到外部仿真器，在软件中重建执行以支持调试。在多种硬件基准与 RISC-V 处理器设计上，Hassert 相比传统软件仿真显著提升验证效率，同时保持完整可见性与调试能力，面积开销很小。
Hardware verification is typically the bottleneck of the chip development cycle, mainly due to the time-consuming simulation and debugging process using software simulators. Assertion-Based Verification (ABV) has been widely adopted to provide better visibility into microarchitecture details and automatically detect unexpected behaviors. While ABV significantly improves verification efficiency, checking assertions using software simulators requires extremely long times for large benchmarks. Prototyping designs on an FPGA is a potential alternative to verify hardware, but it lacks fine-grained debugging capabilities for when errors occur. To address these challenges, we present Hassert, an efficient ABV framework that combines high-performance verification on FPGAs with fine-grained debugging in software. Hassert automates the scheduling and mapping of SystemVerilog Assertions (SVAs) to the available FPGA fabric with the design-under-test (DUT), allowing for extensive hardware testing. Hassert also enables dynamic switching between different assertions, either user-specified or based on SVA coverage satisfaction, by partially reconfiguring the FPGA at runtime, eliminating the need to recompile the DUT. To further improve debugging efficiency, we also propose a microarchitecture-guided hardware snapshot scheme. If any assertion is fired, Hassert automatically generates snapshots of the current status of the entire FPGA hardware. These snapshots are then transferred to an external simulator, where the operation is reconstructed in software for further debugging. We demonstrate that these contributions can improve significant verification efficiency over traditional software simulation-based approaches for various hardware benchmarks and RISC-V processor designs whilst maintaining full visibility and debugging capabilities at the cost of only a small area overhead.
@inproceedings{ZhangWLCWBBS24,
title = {Hassert: Hardware Assertion-Based Verification Framework with FPGA Acceleration},
author = {Ziqing Zhang and Weijie Weng and Yaning Li and Lijia Cai and Haoyu Wang and David Boland and Yungang Bao and Kan Shi},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3622781.3698899}
}