Unbounded Hardware Verification using Software Analyzers
Demand for scalable hardware verification is ever growing. We present an unbounded safety verification framework for hardware, at the heart of which is a software verifier. To this end, we synthesize the Verilog at register transfer level into software netlist, which is expressed in C language. The proposed tool flow allows us to leverage the precision and scalability of the state-of-the-art software verification techniques. In particular, we evaluate unbounded proof techniques such as predicate abstraction, k-induction, interpolation, IC3/PDR, abstract interpretation and present a performance comparison of the verification tools employing these techniques from the hardware and software domains. The property verification benchmarks (in Verilog RTL and C) are available for download here.
Contact Rajdeep Mukherjee or send an email here with questions or feedback.
Installation
Download the latest tarball from the above link. Extract its
content and you can access the benchmarks in Verilog
and C. The safety properties in SVA and C are instrumented
in the design files, Verilog and C, respectively.
The tarball also contains various scripts for running
YOSYS 0.5, v2c, ABC,
EBMC 4.2 and other software verification tools
such as 2LS, CPAChecker, SeaHorn
and IMPARA. The benchmark files for abstract interpretation
tool Astree is available using the command
git clone -b astree https://github.com/rajdeep87/verilog-c.git.
Work Flow
Tool Flow
Tools
We use the following software and hardware verification tools for our experiments. EBMC, ABC, CBMC, v2c, Astree and tools from CPAChecker. UltimateAutomizer. SeaHorn.
Similar Tool Links
Verilog RTL to C Translator Tool
If you are interested in Verilog to C translator tool, please use our tool v2c.
Equivalence Checking Tool for C and Verilog RTL Designs
If you are interested in hardware/software co-verification or C-RTL equivalence checking, please use our tool HW-CBMC.
Bounded Model Checking Tool for Verilog RTL
If you are interested in bounded model checking for Verilog designs, please use our tool EBMC.
Path-based Symbolic Execution Tool
If you are interested in path-based symbolic execution tool for C models generated from Verilog or any software (in C) in general, please use our tool VerifOx.