Mukherjee, R and Joshi, Saurabh and Griesmayer, A and Kroening, D and Melham, T
(2016)
Equivalence Checking a Floating-point Unit against a High-level C Model.
In:
FM 2016: Formal Methods (21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings).
Lecture Notes in Computer Science, 9995
.
Springer Int Publishing Ag, Switzerland, pp. 1-14.
ISBN 978-3-319-48989-6
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.
Actions (login required)
 |
View Item |
Altmetric
Altmetric