Techniques for efficient satisfiability checking

Satisfiability checking is a core algorithm in almost all approaches to verification and testing. Hence, enabling effective high-level verification or testing requires satisfiability checkers to leverage the abstraction present in high-level designs. This implies that satisfiability checkers should be able to efficiently solve problems that span multiple arithmetic domains. It remains unclear whether these multi-domain problems can be more efficiently solved using a single decision procedure (such as Boolean SAT after design translation) or as a Combination of Decision Procedures (CDPs), simply because CDPs that can handle large designs do not exist to-date. We propose an algorithm called Hybrid DPLL (HDPLL) that efficiently combines theories for Boolean and integer bit-vector arithmetic. HDPLL effectively applies 2-literal watching, conflict analysis and other modern Boolean SAT techniques at the word level. We present results on RTL benchmarks comparing HDPLL with other CDPs.; Even with this migration toward high-level verification and testing, the need for efficient sequential Boolean satisfiability solvers will continue. Traditional approaches to solving this problem include Symbolic Model Checking using Boolean Decision Diagrams (BDDs), Bounded Model Checking (BMC) using SAT and Sequential ATPG. We present a new approach to sequential satisfiability checking called Sequential SAT. Sequential SAT leverages the advantages of Boolean SAT and Sequential ATPG into an efficient solver. We compare Sequential SAT against other approaches on both public and industrial benchmarks.; System on Chip (SoC) designs have gained popularity over the years because of the need for varied functionality within the same IC. Typically, such devices integrate processor, memories and other functional blocks (also called IP cores) together using a communication architecture. The complexity of such systems present difficult challenges for traditional timing verification (delay testing) methods. We propose a new methodology for testing the functional cores in SoCs using the resources of the SoCs. The embedded processor itself is used to run a test program, deliver test patterns to functional blocks and process its response. Such a scheme allows great flexibility in the type of test patterns that can be applied, allowing a mix of deterministic and non-deterministic test patterns. (Abstract shortened by UMI.)...