Equivalence Checking a Floating-point Unit against a High-level C Model

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

[img]
Preview
Text (arXiv copy)
1609.00169.pdf - Published Version

Download (138kB) | Preview

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.

[error in script]
IITH Creators:
IITH CreatorsORCiD
Joshi, SaurabhUNSPECIFIED
Item Type: Book Section
Uncontrolled Keywords: VERIFOX, HW-CBMC
Subjects: Computer science > Big Data Analytics
Divisions: Department of Computer Science & Engineering
Depositing User: Team Library
Date Deposited: 06 Sep 2016 05:33
Last Modified: 12 Sep 2017 11:14
URI: http://raiithold.iith.ac.in/id/eprint/2725
Publisher URL: https://doi.org/10.1007/978-3-319-48989-6_33
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 2725 Statistics for this ePrint Item