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...

Full description

Bibliographic Details
Main Authors: Mukherjee, R, Schrammel, P, Kroening, D, Melham, T
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