date16.pdf (96.92 kB)
Unbounded safety verification for hardware using software analyzers
chapter
posted on 2023-06-09, 01:09 authored by Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, Tom MelhamDemand 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.
History
Publication status
- Published
File Version
- Accepted version
Publisher
IEEEPage range
1152-1155Book title
2016 Design, Automation & Test in Europe Conference & Exhibition (DATE)Place of publication
Dresden, GermanyISBN
9783981537079Department affiliated with
- Informatics Publications
Notes
Conference paper from 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE), 14-18 March 2016, Dresden, GermanyFull text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2016-05-09First Open Access (FOA) Date
2018-03-14First Compliant Deposit (FCD) Date
2016-05-09Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC