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 2k . 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.

• Type: Conference
• Year: 2010
• Where: TAP
• Authors: Eugene Goldberg, Panagiotis Manolios
• Keywords: Boolean Combinational Circuits, Combinational Circuit, Complete Set, TAP 2010