Name
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 | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-48989-6_33 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Formal equivalence checking,Programming language,Reference model,Computer science,Floating-point unit,SystemC,Real-time computing,Software,Equivalence (measure theory),Verilog,Register-transfer level | Conference | 9995 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.35 |
References | Authors | |
16 | 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 |