On bridging simulation and formal verification

Abstract. Simulation and formal verification are two complementary techniques for checking the correctness of hardware and software designs. Formal verification proves that a design property holds for all points of the search space while simulation checks this property by probing the search space at a subset of points. A known fact is that simulation works surprisingly well taking into account the negligible part of the search space covered by test points. We explore this phenomenon by the example of the satisfiability problem (SAT). We believe that the success of simulation can be understood if one interprets a set of test points not as a sample of the search space, but as a “prover ” that can rigorously prove unsatisfiability of CNF formulas. We introduce the notion of a sufficient test set of a CNF formula which is a test set that has “enough power ” to prove the unsatisfiability of this formula. We show how sufficient test sets can be built. We discuss applications of “tight ” sufficient test sets in manufacturing testing and functional verification and give some experimental results.