Generation of complete test sets

TL;DR

This paper introduces a novel approach using Stable Sets of Assignments (SSAs) to generate complete test sets for combinational circuits more efficiently than traditional methods, with promising experimental results.

Contribution

It presents a faster algorithm combining SSAs and resolution derivation to produce complete test sets for circuit projections, improving over naive exhaustive testing.

Findings

Generated smaller complete test sets using SSAs

Algorithm outperforms traditional exhaustive methods

Potential applications in circuit verification and testing

Abstract

We use testing to check if a combinational circuit N always evaluates to 0. The usual point of view is that to prove that N always evaluates to 0 one has to check the value of N for all 2^|X| input assignments where X is the set of input variables of N. We use the notion of a Stable Set of Assignments (SSA) to show that one can build a complete test set (i.e. a test set proving that N always evaluates to 0) that consists of less than 2^|X| tests. Given an unsatisfiable CNF formula H(W), an SSA of H is a set of assignments to W proving unsatisfiability of H. A trivial SSA is the set of all 2^|W| assignments to W. Importantly, real-life formulas can have SSAs that are much smaller than 2^|W|. Generating a complete test set for N using only the machinery of SSAs is inefficient. We describe a much faster algorithm that combines computation of SSAs with resolution derivation and produces a complete test set for a "projection" of N on a subset of variables of N. We give experimental results and describe potential applications of this algorithm.