Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)

TL;DR

This paper introduces two equivalence checking tools, VERIFOX and HW-CBMC, for validating C models against RTL implementations, demonstrated on ARM's floating-point unit and an open-source adder.

Contribution

The paper presents a two-step equivalence checking methodology with dedicated tools for C and RTL levels, improving verification of high-level system designs.

Findings

Successfully verified ARM's floating-point unit

Validated an open-source floating-point adder

Demonstrated effectiveness of the tools in industrial scenarios

Abstract

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.