Name
Title | ||
|---|---|---|
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version). |
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. |
Year | Venue | Field |
|---|---|---|
2016 | arXiv: Software Engineering | Formal equivalence checking,Programming language,Reference model,Floating-point unit,Computer science,SystemC,Software,Equivalence (measure theory),Register-transfer level,Verilog |
DocType | Volume | Citations |
Journal | abs/1609.00169 | 0 |
PageRank | References | Authors |
0.34 | 0 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rajdeep Mukherjee | 1 | 11 | 3.40 |
| saurabh joshi | 2 | 6 | 2.47 |
| Andreas Griesmayer | 3 | 288 | 17.58 |
| Daniel Kroening | 4 | 3084 | 187.60 |
| Thomas F. Melham | 5 | 384 | 35.63 |