A Version Space Approach for Digital Circuit Analysis

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.Source: §I · p. 1, A. The Version Space as a Measure · p. 1
• 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.Source: B. Two Applications · pp. 1–2
• 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.Source: B. Two Applications · p. 2
• 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.Source: B. Two Applications · p. 2
• 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.Source: A. The Version Space as a Measure · p. 1, B. Two Applications · p. 2

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.Source: B. The Modified Haar Transform · p. 2
• Reparameterizing from coefficients to block sums converts dependence among nested coefficients into locality.Locality enables a tree-structured sum–product recursion.Source: C. Lineage and Past Applications · p. 3, B. The Counting Problem, Reparameterized · p. 3
• 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.Source: A. The Previous CEC Method · p. 3
• 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.Source: B. The Counting Problem, Reparameterized · p. 3
• 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.Source: B. The Counting Problem, Reparameterized · p. 3

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.Source: C. The General Recursion · p. 4
• 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.Source: D. Recursion Details · p. 4
• 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.Source: D. Recursion Details · p. 4
• 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.Source: D. Recursion Details · p. 4
• 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.Source: D. Recursion Details · p. 4

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).Source: E. Cost · p. 4
• 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.Source: E. Cost · p. 5
• 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.Source: E. Cost · p. 5

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.Source: F. Closed Forms · p. 5
• 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.Source: F. Closed Forms · p. 5

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.Source: G. Error due to an Independence… · p. 5

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.Source: G. Error due to an Independence… · p. 5
• For pairwise disjoint supports, the index is 1, so the coefficients are exactly independent.This recovers the paper's disjoint-support corollary.Source: G. Error due to an Independence… · p. 5

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.Source: G. Error due to an Independence… · p. 6

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.Source: G. Error due to an Independence… · pp. 5–6

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.Source: G. Error due to an Independence… · p. 6

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.Source: H. Ordering the Coefficients · p. 6

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.Source: H. Ordering the Coefficients · p. 6

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.Source: H. Ordering the Coefficients · p. 6

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.Source: §I · p. 6, J. Experimental Results · p. 7, Table II · p. 8

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.Source: J. Experimental Results · p. 7

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.Source: K. Haar Matching Against Random Test… · p. 7

• Each oracle query keeps keys reproducing the observed response and discards inconsistent keys, forming a version space whose logarithm is surviving entropy.Source: §IV · p. 9

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.Source: B. The Threat Model and Its Assumptions · p. 9
• Queries may be random, requiring only a chip evaluation, or chosen by reasoning about the netlist to separate surviving keys.Source: B. The Threat Model and Its Assumptions · p. 9

Assumptions

• The method assumes a combinational, acyclic netlist and identifiable key ports, excluding cyclic locking because topological evaluation and counting change.Source: B. The Threat Model and Its Assumptions · p. 9

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.Source: B. The Threat Model and Its Assumptions · pp. 9–10

Scope caveat

• If key preprocessing is non-injective, the reported raw-key count is an upper bound on distinguishable effective keys.Source: B. The Threat Model and Its Assumptions · p. 10

• Key length, SAT iteration count, output corruptibility, and solver runtime describe locking claims but do not report how many keys remain unr ruled out.Source: C. Past Reported Results and Omissions · p. 10
• 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.Source: C. Past Reported Results and Omissions · p. 10
• Earlier ApproxMC work estimates corruption fractions for the lock itself, not the query-conditioned number of keys surviving accumulated observations.Source: C. Past Reported Results and Omissions · p. 10
• Quantitative information-flow methods count secret-input partitions or residual uncertainty, providing precedents for counting information leakage and adaptive uncertainty.Source: D. Relation to Quantitative… · p. 10
• The paper combines hardware locking with quantitative information flow by measuring locking-key secrecy under oracle access rather than data leakage through observable outputs.Source: D. Relation to Quantitative… · p. 10
• Functionally equivalent keys can reduce the effective key space below 2^k, so nominal key length may overstate distinguishable secrets.Source: D. Relation to Quantitative… · p. 10
• Conditional independence across logic cones supplies a structural premise for exploiting sum–product message passing in locking analysis.Source: D. Relation to Quantitative… · p. 10

Problem formulation

• The counted object is |V_t|, the number of keys K satisfying every observed relation C(x_i,K)=y_i.Source: E. The Constraint System · p. 10

Definitions

• Key-moral width eliminates internal variables first, while factor width retains them and measures the induced width of the gate-level factor graph.Source: G. Two Widths · p. 11

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.Source: G. Two Widths · p. 11

Locking structure

• Strong locking can make key relations dense through interference placement without implying dense gate-level factor graphs.Source: G. Two Widths · p. 11

Alternative representation

• A second exact representation symbolically simulates each query, conjoins output-agreement constraints, and counts models of the resulting Boolean function.Source: H. A Second Representation · p. 11

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.Source: H. A Second Representation · p. 11

Exactness

• Exact counting requires arbitrary-precision minterm counts because double precision fails above 2^53.Source: H. A Second Representation · p. 11

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.Source: §I · pp. 11–12
• 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.Source: §I · p. 12

Setup

• The generated E.1 netlists use ripple-carry adders, array multipliers, and equality comparator trees under random, interference-maximizing, and point-function locking.Source: §E.1 · p. 12

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.Source: A. Validating the Counter · p. 12

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.Source: Figure 1 · p. 12, B. Measuring the Two Widths · p. 12
• Factor width reaches 18 for interference-maximizing locking on a 4 × 4 array multiplier at 32 key bits, the hardest sweep case.Source: B. Measuring the Two Widths · p. 12

Version-space trajectories

• Point-function locking removes one key per random query, while interference-maximizing locking falls to one surviving key after eight queries.Source: C. Version-Space Trajectories · pp. 12–13
• Random locking stops at 8,192 survivors because those keys are functionally equivalent, leaving thirteen of twenty-four key bits without secret information.Source: C. Version-Space Trajectories · p. 13

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.Source: C. Version-Space Trajectories · p. 13

Engine comparison

• Engine B reaches 300 queries on all three schemes and remains small on point-function instances despite their growing factor width.Source: C. Version-Space Trajectories · p. 13

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.Source: E. Reachable Instances · p. 13
• 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.Source: E. Reachable Instances · p. 13

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.Source: E. Reachable Instances · pp. 13–14
• 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.Source: F. Failure Modes for Each Engine · p. 14

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.Source: H. Advertised Key Length Versus… · pp. 14–15
• 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.Source: H. Advertised Key Length Versus… · pp. 15–16

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.Source: H. Advertised Key Length Versus… · pp. 14, 16

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.Source: §I · pp. 16–17

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.Source: §I · p. 17

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.Source: §I · p. 17

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.Source: §I · p. 17

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.Source: J. The BDD-Based Family · p. 17
• 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.Source: J. The BDD-Based Family · p. 17, Table IX · p. 17
• 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.Source: J. The BDD-Based Family · p. 17
• 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.Source: J. The BDD-Based Family · pp. 17–18

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.Source: K. The Floor and Bound Tightness · p. 18

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.Source: K. The Floor and Bound Tightness · p. 18

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.Source: K. The Floor and Bound Tightness · p. 18, L. Chosen Queries Versus Random Queries · p. 19

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.Source: K. The Floor and Bound Tightness · p. 18, L. Chosen Queries Versus Random Queries · p. 19

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.Source: L. Chosen Queries Versus Random Queries · p. 19

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.Source: M. Engines and Implementation · pp. 19–20

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.Source: M. Engines and Implementation · pp. 19–20

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.Source: M. Engines and Implementation · p. 20

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.Source: M. Engines and Implementation · p. 20

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.Source: N. Reproducibility and the… · p. 20

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.Source: O. A Unified View: One Method, Two… · pp. 20–21, A. Status of the Equivalence-Checking… · p. 21

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.Source: B. Limitations of the Locking… · p. 21

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.Source: C. The Uniform Prior over Keys · p. 21

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.Source: D. Scope and What Remains · p. 21

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.Source: B. Limitations of the Locking… · p. 21, §VII · p. 22

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.Source: §VII · p. 22

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.Source: §VII · p. 22

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.Source: CODE AND DATA AVAILABILITY · p. 22