Mukherjee, Rajdeep, Schrammel, Peter, Kroening, Daniel and Melham, Tom (2016) Unbounded safety verification for hardware using software analyzers. In: 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE (Institute of Electrical and Electronics Engineers), Dresden, Germany, pp. 1152-1155. ISBN 9783981537079
![]() |
PDF
- Accepted Version
Download (99kB) |
Abstract
Demand for scalable hardware verification is ever-increasing. We propose an unbounded safety verification framework for hardware, at the heart of which is a software verifier. To this end, we synthesize Verilog at register transfer level into a software-netlist, represented as a word-level ANSI-C program. The proposed tool flow allows us to leverage the precision and scalability of state-of-the-art software verification techniques. In particular, we evaluate unbounded proof techniques, such as predicate abstraction, k-induction, interpolation, and IC3/PDR; and we compare the performance of verification tools from the hardware and software domains that use these techniques. To the best of our knowledge, this is the first attempt to perform unbounded verification of hardware using software analyzers.
Item Type: | Book Section |
---|---|
Additional Information: | Conference paper from 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE), 14-18 March 2016, Dresden, Germany |
Keywords: | Hardware verification, RTL, Software netlist, Software verification tools, Program analysis |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Subjects: | Q Science > QA Mathematics > QA0075 Electronic computers. Computer science |
Related URLs: | |
Depositing User: | Peter Schrammel |
Date Deposited: | 09 May 2016 11:40 |
Last Modified: | 14 Mar 2018 02:00 |
URI: | http://srodev.sussex.ac.uk/id/eprint/60812 |
View download statistics for this item
📧 Request an update