Repository navigation
cnf: cache the ISOP cover of each distinct cut function (pinned line) - #19
Merged
Merged
Conversation
Cnf_ComputeClauses() calls Kit_TruthIsop() twice for every non-AND cone it turns into clauses, once for the function and once for its complement, and computes both covers from scratch every time. A cover depends on nothing but the truth table and the leaf count, and the cuts of a bit-blasted circuit are a handful of adder, mux and xor functions repeated across the netlist, so nearly all of that is recomputation. Key the covers by (truth table, leaf count) in a table that lives for one Cnf_DeriveFastClauses() call, and replay a stored cover cube for cube. Mf_ManDeriveCnfs() does the same thing where the mapper has already assigned each truth function an id. The clauses come out of the same cubes in the same order, so the CNF is unchanged. Over bit-vector queries the covers are reused nearly every time: 7.0M cover requests over 42 distinct functions on one 512-bit arithmetic query, 3.2M over 26 on a second and 2.4M over 196 on a third, with the whole table a few hundred ints. CNF derivation on those three goes 2528 -> 1643 ms, 1244 -> 754 ms and 793 -> 448 ms, a 35-44% cut, and peak memory is unchanged. Cnf_ComputeClauses() keeps its signature and its uncached behaviour for the callers outside this file.
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.
#10 rebased onto the branch the pin points into; it targeted
stp, so the win reached no build.Cnf_ComputeClauses()recomputes an ISOP cover for every cone it turns into clauses, once for the function and once for its complement. A cut has at most 6 leaves and a bit-blasted circuit uses a handful of adder, mux and xor functions over and over, so nearly all of that is recomputation. Keying the cover on(truth table, leaf count)and replaying it cube for cube removes it: on a 293k-AND multiplier, 146,304 cover requests become 4 calls toKit_TruthIsop(). Measured through a bit-vector solver, the CNF-derivation stage falls 35-43%.Identical patch-id to #10's commit, and it applies cleanly over #14's non-static
S[256]in this file. The table is insert-only and freed per derivation; its size is bounded by two entries per cone, 196 distinct functions being the most observed.The CNF is unchanged by construction, since the cubes are replayed in the same order, and checked: 12 byte-identical comparisons over generated multipliers and an adder at three flag settings, plus 24 over
i10.aigacross twelve synthesis scripts. The second set is the one that matters —i10presents 150-166 distinct cut functions where a multiplier presents 4, so it is what actually exercises the key.