Equivalence checking of a floating-point unit against a high-level C model

Conference item

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.

Authors: Mukherjee, R; Joshi, S; Griesmayer, A; Kroening, D; Melham, T

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Host title: 21st International Symposium on Formal Methods
• Journal: 21st International Symposium on Formal Methods
• Volume: 9995 LNCS
• Pages: 551-558
• Publication date: 2016-11-01
• Acceptance date: 2016-08-23
• DOI: 10.1007/978-3-319-48989-6_33
• ISSN: 0302-9743 and 1611-3349
• ISBN: 9783319489889