| | |
| | |
Stat |
Members: 3667 Articles: 2'599'751 Articles rated: 2609
07 February 2025 |
|
| | | |
|
Article overview
| |
|
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version) | Rajdeep Mukherjee
; Saurabh Joshi
; Andreas Griesmayer
; Daniel Kroening
; Tom Melham
; | Date: |
1 Sep 2016 | 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. | Source: | arXiv, 1609.0169 | Services: | Forum | Review | PDF | Favorites |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|