Unbounded Safety Verification for Hardware Using Software Analyzers
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 pr...
Main Authors: | , , , |
---|---|
Format: | Conference item |
Published: |
European Design and Automation Association
2015
|
_version_ | 1797090996040761344 |
---|---|
author | Mukherjee, R Schrammel, P Kroening, D Melham, T |
author_facet | Mukherjee, R Schrammel, P Kroening, D Melham, T |
author_sort | Mukherjee, R |
collection | OXFORD |
description | 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. |
first_indexed | 2024-03-07T03:26:42Z |
format | Conference item |
id | oxford-uuid:b9466ecb-f730-4f94-9ddc-85a6dd76f4ae |
institution | University of Oxford |
last_indexed | 2024-03-07T03:26:42Z |
publishDate | 2015 |
publisher | European Design and Automation Association |
record_format | dspace |
spelling | oxford-uuid:b9466ecb-f730-4f94-9ddc-85a6dd76f4ae2022-03-27T05:01:55ZUnbounded Safety Verification for Hardware Using Software AnalyzersConference itemhttp://purl.org/coar/resource_type/c_5794uuid:b9466ecb-f730-4f94-9ddc-85a6dd76f4aeSymplectic Elements at OxfordEuropean Design and Automation Association2015Mukherjee, RSchrammel, PKroening, DMelham, TDemand 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. |
spellingShingle | Mukherjee, R Schrammel, P Kroening, D Melham, T Unbounded Safety Verification for Hardware Using Software Analyzers |
title | Unbounded Safety Verification for Hardware Using Software Analyzers |
title_full | Unbounded Safety Verification for Hardware Using Software Analyzers |
title_fullStr | Unbounded Safety Verification for Hardware Using Software Analyzers |
title_full_unstemmed | Unbounded Safety Verification for Hardware Using Software Analyzers |
title_short | Unbounded Safety Verification for Hardware Using Software Analyzers |
title_sort | unbounded safety verification for hardware using software analyzers |
work_keys_str_mv | AT mukherjeer unboundedsafetyverificationforhardwareusingsoftwareanalyzers AT schrammelp unboundedsafetyverificationforhardwareusingsoftwareanalyzers AT kroeningd unboundedsafetyverificationforhardwareusingsoftwareanalyzers AT melhamt unboundedsafetyverificationforhardwareusingsoftwareanalyzers |