Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)
This addresses the need for reliable equivalence checking in semiconductor design to prevent errors in hardware implementations, though it appears incremental as it builds on existing verification methodologies.
The paper tackles the problem of verifying consistency between high-level C models and RTL implementations in hardware design, presenting a two-step approach using tools VERIFOX and HW-CBMC, which were applied to a commercial ARM FPU and an open-source floating-point adder.
Semiconductor companies have increasingly adopted a methodology that starts with a system-level design specification in C/C++/SystemC. This model is extensively simulated to ensure correct functionality and performance. Later, a Register Transfer Level (RTL) implementation is created in Verilog, either manually by a designer or automatically by a high-level synthesis tool. It is essential to check that the C and Verilog programs are consistent. In this paper, we present a two-step approach, embodied in two equivalence checking tools, VERIFOX and HW-CBMC, to validate designs at the software and RTL levels, respectively. VERIFOX is used for equivalence checking of an untimed software model in C against a high-level reference model in C. HW-CBMC verifies the equivalence of a Verilog RTL implementation against an untimed software model in C. To evaluate our tools, we applied them to a commercial floating-point arithmetic unit (FPU) from ARM and an open-source dual-path floating-point adder.