Understanding Formal Verification Concepts, Part 3
This final white paper in a three-part series about formal verification concepts examines the assertion-based verification flow and some of the formal verification algorithms.
This kind of approach has become necessary as SoC designs become more challenging and the traditional method of simulation proves too slow, too costly, and insufficient in terms of coverage.
Some satisfiability (SAT) tools work partly on the circuit and partly on conjunctive normal form (CNF). These are called hybrid SAT solvers. The netlist is kept along with learned clauses and conflict clauses, which are added during analysis. Click here for part 3.