|
|
|---|
|
|
|
|---|
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 is to appear in FMCAD21 by Mertcan Temel and Warran A. Hunt, Jr.. This method is also described in Mertcan Temel's PhD thesis from University of Texas at Austin.
Our framework currently supports (System) Verilog with design hierarchy as inputs only. These designs are translated to svl design without flattening the adder modules such as full-adders and final stage-adders. 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.
We present two demos that show how this tool can be used in new designs. Multiplier-Verification-demo-1 shows a very basic verification case on a stand-alone 64x64-bit Booth Encoded Dadda multiplier. Multiplier-Verification-demo-2 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. This prevents our method from working properly because we need to identify instantiated adder modules. Therefore, we soundly replace adder modules with their identifiable copies even when flattened. Then, we call defsvtv on the redefined multiplier design and we can verify this test vector with out tool. This mechanism is described in Multiplier-Verification-demo-3.
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/mult/fgl, fgl::fgl book and use rp::defthmrp-then-fgl utility instead of rp::defthmrp to submit conjectures to ACL2.
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