A CLP-based Functional ATPG for Extended FSMs

It is a common opinion that semi-formal verification offers a good compromise between speed and exhaustiveness. In this context, the paper presents a semi-formal functional ATPG that joins static and dynamic techniques to generate high-quality test sequences. The ATPG works on a set of concurrent extended finite state machines (EFSMs) that models the design under verification (DUV). The test generation procedure relies on backjumping, for traversing the EFSM transitions, and constraint logic programming (CLP), for covering corner cases through the deterministic propagation of functional faults observed, but not detected, during the transition traversal.