Paper Info
Title
Complete Test Sets And Their Approximations
Abstract
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 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">|X|</sup> 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 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">|X|</sup> 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 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">|W|</sup> assignments to W. Importantly, real-life formulas can have non-trivial SSAs that are much smaller than 2 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">|W|</sup> . 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.
Year
DOI
Venue
2018
10.23919/FMCAD.2018.8603006
2018 Formal Methods in Computer Aided Design (FMCAD)
Keywords
DocType
Volume
input variables,complete test set,input assignments,stable set of assignments,unsatisfiable CNF formula,SSA,CTS,combinational circuit,verification flows
Conference
abs/1808.05750
ISBN
Citations 
PageRank 
978-1-5386-7567-0
1
0.42
References 
Authors
8
1
Name
Order
Citations
PageRank
Eugene Goldberg1258.01