|
|
|---|
|
|
|
|---|
Some heuristics that can be enabled/disabled by the user for vescmul
Our vescmul multiplier verification system implements various heuristics to efficiently verify different designs. Some of those heuristics are applied for all the designs, some are specific to certain corner cases, and some are just alternatives to others that might prove more beneficial in different cases. We are continually experimenting with these heuristics, and we let users control whether or not some of these heuristics should be enabled. By default, we leave our heuristic settings to be very aggressive so that our tool is readily applicable to the majority of design patterns. However, that might notably slow down proof-time performance for some designs, or in some cases, they might be too aggressive (i.e., cause proofs to fail that otherwise would be successful). If you are not happy with the default configuration for any reason, you may benefit from enabling/disabling some of our heuristics by following the instructions below. Beware that these heuristics and related events might change over time.
UNPACK-BOOTH-LATER (disabled by default)
In Booth encoded multipliers, partial products are generated with basic logical gates. We perform algebraic rewriting on these gates when rewriting the overall circuit. In some corner cases, this can prevent some simplifications and cause a proof attempt to fail. We implement a heuristic that we call "unpack-booth-later" that doesn't perform algebraic rewriting right away but leaves logical gates from Booth encoding intact. When all the other rewriting is finished, we perform a second pass and only then these gates are rewritten in the algebraic form. This heuristic is not expected to be necessary for the majority of designs and it is disabled by default. If a proof attempt of a Booth encoded design is failing, we recommend that you enable this heuristic:
(rp::enable-unpack-booth-later <t-or-nil>)
This feature might not be working for the time-being
S-PATTERN1-REDUCE (enabled by default)
Enabled by default, this heuristic can cover some corner cases that emerge especially in merged multipliers. This usually does not affect the proof-time performance, but in some cases (e.g., constant propagated designs), it can have a negative impact. We have never observed this heuristic to cause a proof to fail, therefore it is enabled by default. To disable it (rp::enable-s-pattern1-reduce nil), or to enable it (rp::enable-s-pattern1-reduce t).
(rp::enable-s-pattern1-reduce <t-or-nil>)
PATTERN2-REDUCE (enabled by default)
Similar to S-PATTERN1-REDUCE. Enabled by default. To disable (rp::enable-pattern2-reduce nil), to enable (rp::enable-pattern2-reduce t)
(rp::enable-pattern2-reduce <t-or-nil>)
PATTERN3-REDUCE (disabled by default)
Similar to other "pattern-reduce" heuristics but it is too aggressive and disabled by default. It removes "1" instances from (s 1 others) and (c 1 others) terms. We have added this pattern for experimentation purposes and have yet to observe its usefulness. This can cause proofs to go through very slowly, therefore, it is disabled by default.
(rp::enable-pattern3-reduce <t-or-nil>)
RECOLLECT-PP (disabled by default)
We have discovered that after partial products are flatten (i.e., rewritten in algebraic form), the result can be shrunk by rewriting (collecting) some terms into c and s terms. When enabled, this heuristic tries to perform such rewriting. It is currently only modified for Booth encoding radix-4 multipliers and may or may not have any performance effect on other configurations. We have observed that it can have considerable advantages in proof-time and memory usage in larger multipliers (up to 30%). This setting is not thoroughly tested for comprehensiveness and it may cause failures in some cases so it is disabled by default.
(rp::enable-recollect-pp <t-or-nil>)
UNPACK-BOOTH-LATER-HONS-COPY (disabled by default)
When enabled, this causes terms to be hons-copied in the meta function that performs the second pass when unpack-booth-later is enabled. This can help prevent some repeated work for some memoized functions but we have seen so far that cost of hons-copy mostly overwhelms the benefits it brings. So we leave this heuristic disabled. It might be worth a shot if you think that a proof is too slow. This setting has no effect if unpack-booth-later is disabled.
(rp::enable-unpack-booth-later-hons-copy <t-or-nil>)
CROSS-PRODUCT-TWO-LARGES (disabled by default)
Another experimental feature that may or may not ever find its usefulness. When enabled, ANDed two s/c/s-c-res terms will be dissolved into a large list of terms. This will likely slow down in some cases (e.g., saturated multipliers) but won't affect much else.
(rp::enable-cross-product-two-larges <t-or-nil>)
C-PATTERN4-COMPRESS (disabled by default)
Another newly-added experimental feature that is expected to speed up the proofs for Booth radix-16 multipliers. It compresses some c instances by pulling out common multipliers inside its terms. It is left disabled because it is not properly integrated into all parts of the tool and it may cause proof failures in some cases.
(rp::enable-c-pattern4-compress <t-or-nil>)
PP-LISTS-LIMIT (set to 16000 by default)
We don't want terms to blow up when doing algebraic rewriting of logical gates. We call this function in this library pp-flatten, as we use it to flatten out partial product logic. Since there could be other terms representing logical gates in given conjectures, and they may cause blow-up if this rewriting is performed on them, we set a limit to how large a term can grow during the pp-flatten stage. This limit can be changed by the user byt defining a funciton that returns a certain number, and calling defattach. For example:
(define return-16000 () 16000)
(defattach pp-lists-limit return-16000)
If this limit is set too low, then some proofs may fail - likely Booth encoded multipliers with large radices, such as, radix-16. On the other hand, if this limit is set too high, the program may try to flatten parts of the design that is not needed (parts that would be simplified away through other means), or in case something goes wrong in adder identification and you end up with a large tree of logical gates. In such a case, you'd likely not want to flatten those gates, which might eventually help prove the conjecture but it can also cause a blow up. If you are tring to prove something and it is stalling, then it may be a good idea to decrease this number to see what is going on.
UNDO-RW-AND-OPEN-UP-ADDERS (disabled by default)
In some cases, our program might mistakenly mark some parts of a multiplier design as half-adder. If we proceed to keep assuming that this was correct, our proofs may fail. We implemented a system to undo some rewriting and open up the definition of some adder instances when it seems appropriate. If the proof-time performance is too slow, disabling this heuristic may help:
(rp::enable-undo-rw-and-open-up-adders <t-or-nil>)