Integration of learning techniques into Incremental Satisfiability for efficient path-delay fault test generation

In recent years, several electronic design automation (EDA) problems in testing and verification have been formulated as Boolean satisfiability (SAT) instances due to the development of efficient general-purpose SAT solvers. Problem-specific learning techniques and heuristics can be integrated into the SAT solver to further speed-up the search for a satisfying assignment. In this paper, we target the problem of generating a complete test-suite for the path delay fault (PDF) model. We provide an incremental satisfiability framework that learns from (1) static logic implications, (2) segment-specific clauses, and (3) unsatisfiability cores of each untestable partial PDF. These learning techniques improvise the test generation for path delay faults that have common testable and/or untestable segments. The experimental results show that a significant portion of PDFs can be excluded dynamically in the proposed incremental SAT formulation for large benchmark circuits, thus potentially achieving speed-ups for PDF test generation.