PaperlayerView exact revision on arXiv

Source-linked AI summary

A Version Space Approach for Digital Circuit Analysis

Mitchell A. Thornton

arXiv:2609.00609v1cs.CRcs.AR

TL;DR

The paper asks how many hidden circuit objects remain consistent with accumulated observations and which observation should come next. It develops exact version-space counting through block-sum and factor-graph recursion, applying it to equivalence checking and locked-netlist key counting. The method closes the general 2002 CEC counting case and shows across seventy TrustHub instances that surviving entropy falls below advertised key length every time.

  • Problem

    The 2002 equivalence-checking method solved only single-coefficient and disjoint-support cases, leaving general shared-support version-space counting as exponential enumeration.

  • Method

    The paper reparameterizes spectral constraints as local block sums and applies exact sum–product recursion to Haar trees and gate-level netlist factor graphs.

  • Results

    The general CEC count is computed exactly in polynomial truth-table time, and seventy TrustHub instances retain less security than their advertised key lengths.

  • Takeaways & Limitations

    Exact version-space counts provide a common measure of evidence and residual secret uncertainty across equivalence checking and logic locking.

  • Takeaways & Limitations

    The locking application does not recover keys faster or introduce a new locking scheme; it measures how many keys remain after queries.

Abstract

from arXiv · show

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 remain consistent and which observation to make next. The set of surviving candidates is the version space, and its size, on a logarithmic scale, measures how much the observations have settled. This paper develops the version-space view as one method and applies it to two circuit-analysis problems 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 this counting problem and solved only two special cases, leaving the general case an enumeration exponential 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 counts the surviving functions exactly in time polynomial in the truth-table size, closed forms follow for a single coefficient, a coefficient pair, and every ancestor-closed set, and the error of the independence approximation the 2002 work resorted to equals a computable lattice index. Every formula is checked against exhaustive enumeration and reproduces the 2002 tables. 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 removes candidates, and the version space is counted exactly.

I. INTRODUCTION

The paper frames digital circuit analysis as exact version-space counting: observations shrink candidate objects, while their number measures evidential resolution. It applies this view to probabilistic equivalence checking and logic-locked netlists.

  • I. INTRODUCTION: The version space contains candidates consistent with all observations, and its logarithmic size measures how far evidence has narrowed the hypothesis class.The paper also asks which observation should be requested next.
  • I. INTRODUCTION: The paper applies one version-space method to probabilistic combinational equivalence checking and key counting for logic-locked netlists.The hidden objects are Boolean functions in the first application and secret keys in the second.
  • I. INTRODUCTION: The 2002 equivalence-checking method handled only single coefficients and disjoint supports, leaving shared-support counting as exponential enumeration.Agreement on observed coefficients quantifies evidence rather than proving equivalence; a mismatch proves inequivalence.
  • I. INTRODUCTION: The paper counts surviving keys exactly by running the same recursion over a locked netlist’s gate-level factor graph.Oracle input–output queries eliminate keys inconsistent with observed responses.
  • I. INTRODUCTION: In both applications, exact posterior counts support query selection rather than heuristic estimation.The paper presents the CEC case as a closed-form validation setting before carrying the machinery into hardware security.

B. The Modified Haar Transform

The modified Haar transform organizes spectral constraints on a dyadic block tree. This locality permits coefficient counting to be reparameterized as local block-sum inference.

  • B. The Modified Haar Transform: The modified Haar transform uses a binary block tree whose rows are signed differences on dyadic truth-table blocks.The root is the global signed sum; deeper rows have progressively smaller supports.
  • B. The Modified Haar Transform: Reparameterizing from coefficients to block sums converts dependence among nested coefficients into locality.Locality enables a tree-structured sum–product recursion.
  • B. The Modified Haar Transform: The 2002 method posed the general shared-support counting problem but left it as coefficient-grid enumeration exponential in the number of coefficients.Its special cases were a single coefficient and coefficients on disjoint supports.
  • B. The Modified Haar Transform: A Haar coefficient specifies how a block’s total is split between its two children.The map between parent sum/coefficient pairs and child sums is bijective, with inverse S = SL+SR and H = SL−SR.
  • B. The Modified Haar Transform: For a free block of size m, the number of fillings with sum S is determined by a binomial count, subject to range and parity.This free-block census supplies the unconstrained pieces of the recursion.

C. The General Recursion

The general method counts functions consistent with arbitrary conditioned Haar coefficients by dynamic programming on block sums. Its tractability depends on structural conditions that make the state space small.

  • C. The General Recursion: Theorem 1 computes the exact count for any conditioned coefficient set by propagating block-sum censuses up the tree.Conditioned nodes force splits, while unconstrained nodes combine child censuses by convolution.
  • C. The General Recursion: The recursion is sum–product inference on a cycle-free factor graph with truth-table entries and auxiliary partial sums.The factor scopes connect each node to its two children, yielding the block tree.
  • C. The General Recursion: Laminar supports, descendant constancy, and bounded ±1 coefficients make the propagated state one integer with range |v|+1.Descendant constancy is the load-bearing condition for the Haar system’s one-dimensional state.
  • C. The General Recursion: Replacing Haar signs with arbitrary ±1 patterns preserves dyadic supports but destroys the state-space collapse.Thus laminar support alone does not explain the method’s tractability.
  • C. The General Recursion: Counting remains #P-complete for broader laminar linear constraints, including encodings of the permanent with bounded coefficients.The result identifies the special structure used by the Haar system rather than claiming general tractability.

E. Cost

The recursion removes the prior exponential dependence on the number of conditioned coefficients and supports exact closed forms for important coefficient patterns. Its implementation also improves the unconstrained convolution cost.

  • E. Cost: Sub-quadratic convolution reduces the arithmetic cost to O(N log^2 N), versus O(N^2) entry-by-entry operations.The corresponding bit-operation bound is ˜O(N^2) instead of ˜O(N^3).
  • E. Cost: 3.55× speedup is measured at n = 13, where the naive path takes 176 s against 49 s.The speedups are 1.70× at n = 8 and 2.28× at n = 12.
  • E. Cost: The recursion is polynomial in truth-table size and does not depend on the number of conditioned coefficients.This replaces the 2002 coefficient-value grid enumeration; additional constraints only prune states.
  • F. Closed Forms: The single-coefficient case has a binomial closed form and reproduces the 2002 worked example k(H0=2) = 4 at n = 2.Parity or range failures give zero.
  • F. Closed Forms: Ancestor-closed coefficient sets have a product form, while disjoint supports recover exact independence.The product form follows because ancestor constraints force the block sums on the constraint skeleton.

G. Error due to an Independence Assumption

The paper shows that assuming coefficient independence introduces an exact lattice-index error: coupled constraints make the approximation overconfident, while disjoint supports remain exactly independent.

  • General result: Under the local central limit approximation, the true density exceeds the independence estimate by the image-lattice index.The Gaussian exponents agree; the discrepancy is the ratio of lattice covolumes.
  • Closed forms: For ancestor-closed coefficient sets, the asymptotic error ratio is 2^|C|−1.Adding each ancestor-closed coefficient doubles the index, starting from index 1 for a single root coefficient.
  • Closed forms: For pairwise disjoint supports, the index is 1, so the coefficients are exactly independent.This recovers the paper's disjoint-support corollary.
  • Scope and warning: Counting the gap by constrained root paths fails for general sets because lateral dependencies can produce an index of 2 without any complete root path.A coefficient together with both children is linearly dependent in the relevant way, despite containing no root path.
  • General result: The independence approximation is wrong by a factor equal to the computable lattice index on coupled constraint sets.The index is obtained from the image lattice of the constraint map and can be computed in polynomial time using the Smith normal form.
  • Scope and warning: The closed forms extend the two special cases solved in 2002 to nested partial structures through the same product form or the general theorem.The single-coefficient and disjoint-support cases are the extremes; intermediate partial BDD structures are also covered.

H. Ordering the Coefficients

The paper makes coefficient ordering exact by computing each candidate coefficient’s information gain from the same version-space recursion. This ordering is validated experimentally and clarifies when spectral observations outperform random tests for detecting inequivalence.

  • Greedy ordering: Maximum-entropy coefficient selection is the greedy policy for expected one-step reduction in log2 k under the uniform posterior.The conditional distribution of an unobserved coefficient is computed from the same recursion.
  • Exact information gain: Theorem 1 makes the posterior and exact information gain of every candidate coefficient computable before that coefficient is evaluated.The contribution is exact evaluability, not a new information-gain criterion.
  • Greedy ordering: The policy ranks uncomputed coefficients by expected information per unit decision-diagram cost, avoiding the 2002 method’s dependence on whichever coefficients the diagram exposed.Small-block coefficients can have low-entropy distributions and provide little evidence, while the ranking is available before computation.
  • Validation: The recursion, closed forms, and brute-force enumeration agree wherever brute force is affordable, including all sixteen reproduced rows of the 2002 table.At n = 4, exhaustive checks covered all 65,536 functions for random constraint sets.
  • Experimental results: For n = 4, the version space starts at 2^16 = 65536 candidates and reaches one function after all sixteen matched coefficients, with different functions shrinking at different rates.The threshold function is fixed after H0 = 0 and H1 = 16, whereas parity and a random function retain thousands of candidates after two coefficients.
  • Haar matching against random tests: A single differing minterm changes H0 by ±2 and is detected on the first Haar observation, while random testing needs an expected (N + 1)/2 vectors.The Haar advantage narrows as the number d of differing minterms grows but remains an order of magnitude or more across the measured range.

IV. APPLICATION II: KEY COUNTING FOR LOCKED NETLISTS

This application treats secret keys as version-space candidates and oracle input–output pairs as observations, then counts the keys still consistent with those queries. The method is evaluated under a combinational, acyclic-netlist threat model and related to SAT-attack termination.

  • Each oracle query keeps keys reproducing the observed response and discards inconsistent keys, forming a version space whose logarithm is surviving entropy.
  • Threat model: The attacker has a gate-level locked netlist and an activated oracle chip, but cannot read the key, probe internal nets, or observe beyond input–output behavior.
  • Threat model: Queries may be random, requiring only a chip evaluation, or chosen by reasoning about the netlist to separate surviving keys.
  • Assumptions: The method assumes a combinational, acyclic netlist and identifiable key ports, excluding cyclic locking because topological evaluation and counting change.
  • Relation to SAT attacks: The method counts keys remaining after a query set, whereas SAT attacks seek a key or timeout; their termination test is the same satisfiability condition as the paper’s tightness certificate.
  • Scope caveat: If key preprocessing is non-injective, the reported raw-key count is an upper bound on distinguishable effective keys.

C. Past Reported Results and Omissions

Prior locking metrics and counting studies do not quantify how many keys remain indistinguishable after oracle observations. This section positions the paper’s conditioned key count within earlier security, information-flow, and structural analyses.

  • Key length, SAT iteration count, output corruptibility, and solver runtime describe locking claims but do not report how many keys remain unr ruled out.
  • Recent surveys report neither key counts nor entropy for schemes, while formal security work defines security without quantifying how far a given attack has progressed.
  • Earlier ApproxMC work estimates corruption fractions for the lock itself, not the query-conditioned number of keys surviving accumulated observations.
  • Quantitative information-flow methods count secret-input partitions or residual uncertainty, providing precedents for counting information leakage and adaptive uncertainty.
  • The paper combines hardware locking with quantitative information flow by measuring locking-key secrecy under oracle access rather than data leakage through observable outputs.
  • Functionally equivalent keys can reduce the effective key space below 2^k, so nominal key length may overstate distinguishable secrets.
  • Conditional independence across logic cones supplies a structural premise for exploiting sum–product message passing in locking analysis.
  • Problem formulation: The counted object is |V_t|, the number of keys K satisfying every observed relation C(x_i,K)=y_i.

G. Two Widths

The paper contrasts key-moral width with gate-level factor width and shows why retaining internal signals can make key counting tractable even when eliminating them creates dense key relations.

  • Definitions: Key-moral width eliminates internal variables first, while factor width retains them and measures the induced width of the gate-level factor graph.
  • Point-function locking: For point-function locks, eliminating an AND-tree makes the key-moral graph a k-vertex clique with width k −1, while retaining internal nets keeps factor width constant.
  • Locking structure: Strong locking can make key relations dense through interference placement without implying dense gate-level factor graphs.
  • Alternative representation: A second exact representation symbolically simulates each query, conjoins output-agreement constraints, and counts models of the resulting Boolean function.
  • Representation trade-off: As queries accumulate, factor-graph width can grow while the decision diagram contracts with the shrinking version space, making representation choice instance-dependent.
  • Exactness: Exact counting requires arbitrary-precision minterm counts because double precision fails above 2^53.
  • Stress cases: Routing-network locking is identified in advance as a likely failure case because banyan and butterfly topologies are worst cases for graph width.
  • Stress cases: For point-function locks, every query touches every key bit and adds a residual copy, so factor width grows with query count while each query removes only one key.

E.1 Experiments: Locked Netlist Examples

The E.1 campaign tests exact key counting and width behavior across generated adders, multipliers, and comparators under three locking schemes. Results show sharply different version-space trajectories and engine limits.

  • Setup: The generated E.1 netlists use ripple-carry adders, array multipliers, and equality comparator trees under random, interference-maximizing, and point-function locking.
  • Validation: 81 cases matched exhaustive enumeration with zero mismatches across key lengths three to five, query counts one to three, and all three locking schemes.
  • Width results: At 32 key bits, point-function instances have key-moral width 31 but factor width 10 to 12, demonstrating a large width gap.
  • Width results: Factor width reaches 18 for interference-maximizing locking on a 4 × 4 array multiplier at 32 key bits, the hardest sweep case.
  • Version-space trajectories: Point-function locking removes one key per random query, while interference-maximizing locking falls to one surviving key after eight queries.
  • Version-space trajectories: Random locking stops at 8,192 survivors because those keys are functionally equivalent, leaving thirteen of twenty-four key bits without secret information.
  • Engine halting: Engine A exceeds its time budget at the eighth point-function query, reaches the twelfth for interference-maximizing locking, and survives to the ninety-eighth for random locking.
  • Engine comparison: Engine B reaches 300 queries on all three schemes and remains small on point-function instances despite their growing factor width.

E. Reachable Instances

The reachability screen exposes complementary strengths: Engine A remains usable at larger key lengths, while Engine B benefits from accumulated queries but can fail when version spaces remain large. Across the campaign, exact counts show substantial and circuit-dependent key loss, with reported entropies treated as upper bounds.

  • Screening: Neither screen computes a count: Engine A tests residual-factor-graph width, whereas Engine B tests accumulated-diagram size against a node budget.At three queries, the threshold is 25 and the node budget is eight million.
  • Screening: At k = 32, Engine B reaches every instance and Engine A reaches five of six, with successful widths ranging from 8 to 24.Across the whole screen, Engine A reaches eight instances that Engine B does not, while Engine B reaches five that Engine A does not.
  • Complementary reachability: Engine A’s width stays between 16 and 25 on AntiSAT variants carrying 140 to 379 key bits, while Engine B fails because their version spaces remain enormous after three queries.The three-query screen favors Engine A, even though Engine B’s cost can fall as more queries constrain the version space.
  • Complementary reachability: On four of five Table VI benchmarks, Engine B leads at every query count as its diagram remains 30 to 425 nodes, while Engine A’s runtime rises three orders of magnitude and exhausts its four-minute budget twice.c432-RN640 reverses the pattern: Engine B reaches 152,097 and 3,661,940 nodes, whereas Engine A finishes the third query at width 26 in nine and a half minutes.
  • Campaign results: Across seventy instances, every case loses key material, with losses from 4.65 to 152.09 bits; two c6288 instances reach |V_T| = 1.The campaign spans all ten ISCAS-85 circuits and advertised key lengths of 32, 64, 128 and 256 bits.
  • Campaign results: Circuit structure matters more than locking scheme: c880, c1355, c5315 and c6288 lose most key material, while c432 retains substantially more.The paper reports this as a cross-circuit pattern in surviving entropy rather than an iteration-count result.
  • Interpretation: The reported surviving entropies are upper bounds because random-query plateaus are not proofs of exhaustion, and thirteen runs ended before plateauing or when an engine failed.Only the two instances with |V_T| = 1 have no remaining uncertainty to lose.

I. Reading the Campaign by Circuit Family

Reading the campaign by circuit family shows that circuit structure dominates surviving key entropy and also shapes which counting engine is practical. The BDD-based family separates sharply into variants that lose most, part, or none of their key material.

  • c6288: Both uniquely determined instances are c6288 circuits: c6288-RN320 collapses after eleven random queries and c6288-RN640 after twenty-three.The array multiplier’s arithmetic density makes its input function difficult to represent, but does not preserve secrecy when inputs are fixed.
  • c5315 and c880: c5315 has the campaign’s largest losses: c5315-RN2560 loses 152.09 of 256 bits, while c5315-RN1280 retains 13.91 of 128 bits.On c880, secure logic locking retains 19.81 bits versus 8.49 for random insertion at 64 bits, a difference of roughly eleven bits.
  • c432: c432 retains more entropy than other circuits but is hardest to count, with unfinished bounds, a failed c432-RN640 instance, and a c432-SL320 exception retaining one bit.The paper connects large version spaces with both stronger resistance and more expensive diagrams.
  • Cross-family pattern: Across circuits, absolute loss grows with key length while the fraction lost does not fall; across schemes, the spread is narrower than across circuits.This makes circuit identity the stronger organizing variable for interpreting the campaign.
  • BDD-based family: The BDD-based family contains twenty-four instances over six circuits and three variants, so it is reported separately because averaging their behaviors would describe none of them.The variants are BE, BR and BS, covering 28-, 32-, 64- and 128-bit keys.
  • BDD-based family: Engine B reaches every BDD-based instance and Engine A reaches twenty-three of twenty-four, with widths from 3 to 17.The family is a counterexample to treating Engine A as uniformly weaker than Engine B.
  • BDD-based family: All twenty-four BDD-based campaigns plateau: BE loses 25.00 to 126.00 bits, BR loses 2.97 to 48.80 bits, and BS loses nothing.For BS, the count remains 2^k and the accumulated diagram never exceeds one node.
  • BDD-based family: The zero-loss BS result is not inert-key behavior: key ports reach outputs, independent-key satisfiability exhibits disagreement, and random inputs simply rarely hit key-sensitive patterns.An independent simulator agrees with the netlist reader on these instances.

K. The Floor and Bound Tightness

The section identifies the irreducible equivalent-key floor and gives a certificate for when the reported entropy is exact rather than an upper bound. It also distinguishes query-budget plateaus from structural floors and compares random with solver-chosen queries.

  • The Floor: |Vt| decreases monotonically but cannot fall below the equivalent-key class |E(K∗)|, which random queries eventually reach almost surely.The plateau reflects keys no observation can distinguish, not merely a stopping rule.
  • Budget Versus Barrier: Four instances exhausted the shorter query budget while counts were still falling; with 3,000 queries, c432-RN320 reached 11.03 bits and c432-CS320 reached 3.00 bits.The corresponding 120-query values were 19.02 and 18.77 bits, respectively.
  • Bound Tightness: A distinguishing input exists exactly when two surviving keys disagree on some output, so unsatisfiability certifies Vt = E(K∗).This certificate can establish that the entropy is exact rather than an upper bound.
  • Certification Limits: The solver certificate closes the barrier left by the joint-diagram formulation, including cases where a 100-million-node budget still cannot certify the floor.On c5315-BS320, ten chosen queries reach 24.44 bits and the solver proves that value exact, whereas 100 random queries leave the full 32-bit space.
  • Query Choice: At equal query counts, solver-chosen queries leave no more entropy than random queries, while 100 random queries can outperform fewer chosen queries when effort is measured differently.For c1355-RN320, 100 random queries leave 1.00 bit versus 5.46 bits after 12 chosen queries.

M. Engines and Implementation

The implementation provides two independent exact engines for counting surviving keys: factor-graph elimination and key-variable decision diagrams. Their complementary resource costs extend reachability, while agreement and brute-force checks validate results.

  • Independent Engines: The two engines are deliberately independent, so exact agreement between them provides evidence beyond repeating one computation.Brute-force enumeration up to k = 20 adds a further check where feasible.
  • Engine A: Factor-Graph Elimination: Engine A fixes query inputs, propagates constants, and applies sum–product elimination to the residual gate-level factor graph.Its cost is governed by the induced width of the elimination order.
  • Engine B: Key-Variable Diagram: Engine B converts each queried netlist output into a Boolean function of the key bits and counts satisfying assignments in a reduced ordered binary decision diagram.The satisfying assignments are exactly the surviving version space Vt.
  • Complementary Costs: Engine A fails on many-query, wide-residual instances, whereas Engine B fails when the represented version space remains enormous.The engines therefore fail in opposite regimes and together extend the reachable range.
  • Measurement: The key-counting application reports exact, machine-independent counts and widths, while wall-clock measurements remain machine-specific.The campaign separates hardware across three machines rather than mixing timing measurements.
  • Shared Method: The same recursion supports both applications, and exact counts expose dependence errors that overstate surviving secret entropy.In the spectral case the error is a computable lattice index; in locking it explains why advertised key length can exceed measured entropy.

B. Limitations of the Locking Application

The locking application measures surviving-key entropy rather than attack speed, but its interpretation depends on query strategy, uniform-prior assumptions, and the measured circuit families. The paper also reports concrete engine, certification, data, and scope boundaries.

  • Contribution Boundary: The paper does not recover keys faster than existing methods or introduce a locking scheme; it adds exact post-query counts and query-value estimates.Its contribution is measurement and query selection, not a faster attack.
  • Prior Assumption: The security interpretation assumes a designer-chosen key uncorrelated with the netlist, making all keys equally likely before queries.A key preprocessor deriving an internal key from chip-unique data changes the interpretation, though not the internal-key count.
  • Applicability: The approach requires low-rate observations and an elimination order with small induced width; under point-function locking, width grows with query count and Engine A stops early.The width evidence comes from generated adders, multipliers, and comparators rather than widths supplied by the published release.
  • Interpretation: Key length, iteration count, and runtime do not measure how many keys remain; the method computes that surviving-key count exactly.This reframes evaluation around the version space rather than advertised size or attack duration.
  • Observed Scope: The reported locking behaviors differ sharply: point-function locks remove one key per query, interference-maximizing locks fall after eight random queries, and random locks can plateau at 8,192 keys.For the random-lock case, thirteen of twenty-four key bits carry no further distinguishable information.
  • Caveat: A random-query plateau is not proof that the structural floor has been reached; certification is required to distinguish a budget limit from an actual barrier.The paper recommends reporting |Vt| alongside iteration count and checking whether the advertised key length reflects distinguishable keys.
  • Data Availability: TrustHub benchmarks are third-party and must be obtained separately, so the repository documents their source and provides digests rather than redistributing them.The code and self-check remain available in the repository.
Loading 2609.00609v1…