Demonstration of hardware-accelerated formal verification

A semi-formal verification technique, which performs a brute-force compiled simulation with a sophisticated search space pruning, has been proposed and shown to be competitive with the state-of-the-art SAT-based verification techniques. This paper presents a novel approach for accelerating the semi-formal verification by utilizing hardware/software co-execution. To maximize the gain from hardware acceleration, we propose two novel techniques such as hardwired conflict analysis for learning and speculative input pattern generation. We demonstrate that our FPGA-based prototype system achieves about 7× speedup compared against the software implementation of the semi-formal verifier.