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, ...
(read more)
Topics: 
Embedded system
Computer hardware
Software engineering