Accurate QBF-Based Test Pattern Generation in Presence of Unknown Values

Unknown (X) values emerge during the design process as well as during system operation and test application. X-sources are for instance black boxes in design models, clock-domain boundaries, analog-to-digital converters, or uncontrolled or uninitialized sequential elements. To compute a test pattern for a given fault, well-defined logic values are required both for fault activation and propagation to observing outputs. In presence of X-values, conventional test generation algorithms, based on structural algorithms, Boolean satisfiability (SAT), or binary decision diagram-based reasoning may fail to generate test patterns or to prove faults untestable. This paper proposes the first efficient stuck-at and transition-delay fault test generation algorithm able to prove testability or untestability of faults in presence of X-values. It overcomes the principal pessimism of conventional algorithms when X-values are considered by mapping the test generation problem to the SAT of quantified Boolean formulas. Experiments on ISCAS benchmarks and larger industrial circuits investigate the increase in fault coverage for conventional deterministic and potential detection requirements for both randomized and clustered X-sources.