Complete Test Sets And Their Approximations
Eugene Goldberg · 2018
We use testing to check if a combinational circuit N always evaluates to 0 (written as N ≡ 0). We call a set of tests proving N ≡ 0 a complete test set (CTS). The conventional point of view is that to prove N ≡ 0 one has to generate a trivial CTS. It consists of 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 non-trivial CTS consisting of less than 2|X|tests. Given an unsatisfiable CNF formula H(W ), an SSA of H is a set of assignments to W that proves unsatisfiability of H. A trivial SSA is the set of all 2|W|assignments to W. Importantly, real-life formulas can have non-trivial SSAs that are much smaller than 2|W|. In general, construction of even non-trivial CTSs is inefficient. We describe a much more efficient approach where tests are extracted from an SSA built for a projection of N on a subset of its variables. These tests can be viewed as an approximation of a CTS for N. We describe potential applications of our approach. We show experimentally that it can be used to facilitate hitting corner cases and expose bugs in sequential circuits overlooked due to checking "misdefined" properties.