Equivalence Checking of a Floating-Point Unit Against a High-Level C Model

Springer International Publishing
Rajdeep Mukherjee Saurabh Joshi Andreas Griesmayer Daniel Kroening Tom Melham
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 ...