A Version Space Approach for Digital Circuit Analysis

From bibtex.

Abstract

Many questions about a digital circuit take the same form. A hidden object is consistent with a set of observations, and one wants to know how many objects remain consistent and which observation to make next. The set of surviving candidates is the version space, and its size, reported on a logarithmic scale, is a direct measure of how much the observations have settled. This paper develops the version-space view as a single method and applies it to two problems in circuit analysis that are usually treated as unrelated. The first is probabilistic combinational equivalence checking, where the candidates are Boolean functions and the observations are modified-Haar spectral coefficients. A method proposed in 2002 posed exactly this counting problem and solved only two special cases, leaving the general case as an enumeration that grew exponentially in the number of observations. We close it: a reparameterization onto block sums turns the dependence among nested coefficients into locality, a sum-product recursion then counts the surviving functions exactly in time polynomial in the truth-table size, closed forms follow for a single coefficient, for a coefficient pair, and for every ancestor-closed set, and the error of the independence approximation that the 2002 work resorted to is shown to equal a computable lattice index. Every formula is checked against exhaustive enumeration and reproduces the tables of the 2002 paper. The second application is key counting for logic-locked netlists, where the candidates are keys and the observations are oracle responses. The same recursion, run over the gate-level factor graph, computes the number of keys still consistent with a set of queries; across seventy instances of the TrustHub obfuscation release the surviving entropy falls below the advertised key length every time. The two applications are one method: a witness supplies observations, each observation removes candidates, and the version space is counted exactly.