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:	Publisher
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