Generating high-quality tests for boolean circuits by treating tests as proof encoding

Abstract

We consider the problem of test generation for Boolean combinational circuits. We use a novel approach based on the idea of treating tests as a proof encoding rather than as a sample of the search space. In our approach, a set of tests is complete for a circuit N, and a property p, if it "encodes" a formal proof that N satisfies p. For a combinational circuit of k inputs, the cardinality of such a complete set of tests may be exponentially smaller than 2 k . In particular, if there is a short resolution proof, then a small complete set of tests also exists. We show how to use the idea of treating tests as a proof encoding to directly generate high-quality tests. We do this by generating tests that encode mandatory fragments of any resolution proof. Preliminary experimental results show the promise of our approach. © 2010 Springer-Verlag.