Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encodings

---

Eugene Goldberg and Panagiotis Manolios . TAP: Tests and Proofs, © Springer

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 encodings 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 proof encodings 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.

PDF © Springer