Repository navigation
cnf: bound the ISOP cover table - #20
Merged
Merged
Conversation
Nothing bounds how many distinct cut functions a circuit can present. The table is keyed by (truth table, leaf count) and inserts on every miss, so its size is bounded only by two entries per cone, which is O(AIG): at 32 bytes plus four per cube, and a 6-input ISOP running to 32 cubes over the symmetric functions, a twelve-million-gate blast could in principle reach a gigabyte of table. It does not happen because the reuse is extreme and concentrated -- four functions answer all 146,304 requests of a 293k-AND multiplier -- but nothing in the code relied on that. Bound it at 1024 entries, about 200 KB with the initial allocation. Replaying the five request streams measured so far against a bound of 1024, an LRU of 1024 and a direct-mapped 1024 gives the same hit rate as an unbounded table to three decimal places: 99.997% on the multiplier, 81.265% on i10, which presents 160 distinct functions and is the most diverse of them. LRU and the bound are identical to the digit at every size from 256 up, and direct-mapped is slightly worse because collisions evict functions that are still hot. So the policy is the simplest one that bounds the table: past the bound a function already stored is still replayed, and one that is not is computed and not stored. The memo is a pure function of its key, so declining to store an entry cannot change a clause. Checked rather than assumed: with the bound at 4, so the unstored path runs on nearly every request, the CNF is byte-identical to the unbounded build over two multipliers, a ripple adder and i10 at four synthesis settings each, 16 of 16.
This was referenced Oct 4, 2026
TrevorHansen
added a commit
to stp/stp
that referenced
this pull request
Oct 4, 2026
The ISOP cover table the previous commit's pin brought in inserts on every miss and never evicts, so its size was bounded only by two entries per cone, which is O(AIG). stp/abc#20 bounds it at 1024 entries, about 200 KB. It costs nothing measurable. Replaying the request streams against a bound of 1024, an LRU of 1024 and a direct-mapped 1024 gives the same hit rate as the unbounded table to three decimal places, the most distinct cut functions any measured circuit presents being 166. Rebuilt and retested against an ABC built at exactly this revision: 357 of 357.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The ISOP table #19 added inserts on every miss and never evicts, so its size is bounded only by two entries per cone — O(AIG). At 32 bytes plus four per cube, and a 6-input ISOP reaching 32 cubes over the symmetric functions, a twelve-million-gate blast could in principle reach a gigabyte of table. It does not happen because four functions answer all 146,304 requests of a 293k-AND multiplier, but nothing in the code relied on that.
Bounded at 1024 entries, about 200 KB with the initial allocation.
Replaying the five request streams measured so far, a bound of 1024, an LRU of 1024 and a direct-mapped 1024 all give the same hit rate as the unbounded table to three decimal places — 99.997% on the multiplier, 81.265% on
i10.aig, the most diverse at 160 distinct functions. LRU and the bound agree to the digit at every size from 256 up, and direct-mapped is slightly worse because collisions evict functions that are still hot. So the policy is the simplest one that bounds the table: past the bound a stored function is still replayed, and one that is not is computed and not stored.Declining to store an entry cannot change a clause, the memo being a pure function of its key. Checked rather than assumed: with the bound at 4, so the unstored path runs on nearly every request, the CNF is byte-identical to the unbounded build over two multipliers, a ripple adder and
i10.aigat four synthesis settings each — 16 of 16.