|
|
|---|
|
|
|
|---|
An efficient library to verify large integer multiplier designs following the S-C-Rewriting algorithm.
Implemented and verified completely in ACL2, we provide a new method to verify complex integer multiplier designs implemented in (System) Verilog. With a very efficient proof-time scaling factor, this tool can verify integer multipliers that may be implemented with Booth Encoding, various summation trees such as Wallace and Dadda, and numerous final stage adders such as carry-lookahead. For example, we can verify 64x64-bit multipliers in around a second; 128x128 in 2-4 seconds; 256x256 in 6-12 seconds and 1024x1024-bit multipliers in around 5 minutes as tested with almost 100 different designs. This library can also verify other multiplier-centric designs such as multiply-accumulate and dot-product. Designs can be truncated, right-shifted, bit-masked, rounded, saturated, and input sizes can be arbitrary.
The outline of this new verification method first appeared in CAV 2020 (Automated and Scalable Verification of Integer Multipliers by Mertcan Temel, Anna Slobodova, Warren A. Hunt, Jr.) available here: http://doi.org/10.1007/978-3-030-53288-8_23. A follow-up study appeared in FMCAD21 by Mertcan Temel and Warran A. Hunt, Jr. ( http://doi.org/10.34727/2021/isbn.978-3-85448-046-4_13). This method is also described in Mertcan Temel's ( Ph.D. thesis) from University of Texas at Austin.
Our framework currently supports (System) Verilog with design hierarchy as inputs only for the time being. In one of our schemes, these designs are translated to svl design without flattening the adder modules such as full-adders and final stage-adders. Another method is to use defsvtv on flattened designs. Then RP-Rewriter are used as the clause-processor to carry out all the rewriting instead of the built-in rewriter, and our meta rules and rewrite rules dedicated for multiplier designs are used to simplify them and prove them equivalent to their specification.
Our library uses various heuristics and modes to simplify various designs. We give the users the option to enable/disable some of the heuristics that might help speed-up the proofs (and/or reduce memory use) or in some cases help proofs finish. We enable very aggressive heuristics by default for best coverage. If you wish to tune the performance of your proofs by enabling/disabling these heuristics, you can check out Multiplier-Verification-Heuristics. Enabling/disabling these heuristics might help a proof attempt to go through, and in some cases, it may cause them to fail.
We deliver various demos that show how this tool can be used in new designs. For the SVL system: Multiplier-Verification-demo-1-svl shows a very basic verification case on a stand-alone 64x64-bit Booth Encoded Dadda multiplier. Multiplier-Verification-demo-2-svl shows how this tool can be used on much more complex designs where a stand-alone integer multiplier is reused as a submodule for various operations such as MAC dot-product and merged multiplication. It also shows a simple verification case on a sequential circuit.
Alternatively, we present a different framework that uses defsvtv instead of svl. Defsvtv is more capable than SVL at handling combinational loops but it flattens designs completely. Since we want to take advantage of design hierarchy and identify adder modules inside a multiplier module, we take extra steps when using the SVTV system. This SVTV system can be used to verify multipliers in very complex industrial designs. Please see Multiplier-Verification-demo-3-svtv to use the SVTV system to simulate and verify multipliers.
This library can be used to quickly generate counterexamples using an external SAT solver, or help finish proofs with a SAT solver when our library fails to finish the job. You may include the book projects/rp-rewriter/lib/mult3/fgl, fgl::fgl book and use rp::defthmrp-then-fgl utility instead of rp::defthmrp to submit conjectures to ACL2. This macro will use RP-Rewriter first to simplify conjectures and if the result is not 't, then it prepares it for FGL and then submits the simplified term to it. Then, FGL uses SAT solver to generate a counterexample or finalize the proof if it is a theorem.
There are two older versions of this library. If you would like to use
those for some reason, you may view their demo files at