SAT-based semiformal verification of hardware

Semiformal, or hybrid, verification techniques are extensively used in pre-silicon hardware verification. Most approaches combine simulation and formal verification (FV) algorithms to achieve better design coverage than conventional simulation and scale better than FV. In this paper we introduce a purely SAT-based semiformal verification (SFV) method that is based on new algorithms for generating multiple heterogeneous models for a propositional formula. An additional novelty of our paper is the extension of the SFV algorithm to liveness properties. The experimental data presented in this paper clearly shows that the proposed method can effectively find bugs in complex industrial designs that neither simulation nor FV reveal.