Hassert: Hardware Assertion-Based Verification Framework with FPGA Acceleration

Hassert: Hardware Assertion-Based Verification Framework with FPGA Acceleration

연구 분야: Verification

학회: ASPLOS '24: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 4

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.