# 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