A look at hybrid SAT solvers and why this kind of approach has become necessary as SoC designs become more complex.
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.
To download the first two papers in this series, click here for part one and here for part two.
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.
 |
 |
 |
 |
 |
 |
 |
 |
 |
