|
|
|---|
|
|
|
|---|
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 (VeSCmul) can verify integer multipliers that may be implemented with Booth Encoding (e.g., radix-16), 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-15 minutes as tested with thousands of different designs. This library can also verify other multiplier-centric designs such as multiply-accumulate and dot-product, or even be used in other verification flows to verify floating-point operations. Designs can be truncated, right-shifted, bit-masked, rounded, saturated, and input sizes can be arbitrary. This library now supports flattened designs.
This method is called S-C-Rewriting and the tool is called VeSCmul (Verified Implementation of S-C-Rewriting algorithm for Multiplier Verification)
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. These papers describe this method as working on hierarchical reasoning; however, VeSCmul now supports flattened designs as well. More papers are coming soon.
Our framework currently supports (System) Verilog. In one of our schemes, we use sv::defsvtv$ (also see sv::sv-tutorial) to simulate designs. This SVTV system has been used for complex design at Centaur Technology and now at Intel Corporation. SVTV system flattens designs. The multiplier verification program still supports other simulators such as svl but we now only use SVTV.
This library uses various heuristics and modes to simplify various designs. Users have 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. Aggressive heuristics are enabled by default for best coverage. If you wish to tune the performance of your proofs by enabling/disabling these heuristics, you can check out vescmul-heuristics. Enabling/disabling these heuristics might help a proof attempt to go through, but in some cases, it may cause others to fail.
If you have a combinational multiplier design you need to verify, you may follow these steps.
(include-book "projects/vescmul/top" :dir :system)
(vesmul-parse :file "DT_SB4_HC_64_64_multgen.sv" :topmodule "DT_SB4_HC_64_64" :name my-multiplier-example)
Here, logext sign-extends its argument, and loghead zero-extends it.(vescmul-verify :name my-multiplier-example :concl (equal result ;; -> output signal name ;; design specification -> (loghead 128 (* (logext 64 in1) (logext 64 in2)))))
See vesmul-parse and vescmul-verify for more ways to use these utilities.
Including projects/vescmul/top everytime can take a long time (almost a minute). However, you can save an executable with that book in it to quickly pull up this multiplier verification library. See save-exec. Alternatively, download a package that does that for you. This package also includes some demo files.
Various demos in much more detail are present to 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. Finally, Multiplier-Verification-demo-3 shows how hierarchical reasoning may be used if it ever becomes necessary to provide hints to the program.
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. By default, glucose is used as SAT solver. This can be configured to call a different SAT solver (see fgl::fgl-solving).
If you are using macros from Quick Start above, then ":then-fgl t" argument as shown below will be enough to call FGL, which will invoke a SAT solver after VeSCmul finishes rewriting:
(vescmul-verify :name my-multiplier-example :then-fgl t :concl (equal result (loghead 128 (* (logext 64 in1) (logext 64 in2)))))
VeSCmul allows users to export a Verilog file after the adder detection stage. The exported file contains basic adder modules and a large Verilog module instantiating those adder modules. The exported module is expected to be equivalant to the original design. The difference will be the exported Verilog module will have the design hierarchy around adder components (even if the original design did not have any design hierarchy). If the original design had any complex adders (e.g., 4-to-2 compressors, parallel prefix adders), the exported module is expected to have replaced those with only simple full/half-adders. Researchers may use this feature in their verification flows.
To use this tool, simply run:
(export-to-verilog-after-adder-detection "my-mult_module_with_hier")
IMPORTANT: This program should be run after the vescmul-verify event for the desired multiplier design. The vescmul-verify event does not need to succeed for this to work; that is, you can set the :keep-going flag and try to prove a false conjecture and the export-to-verilog-after-adder-detection program can still export the processed design for you anyway.
The Verilog translation is not verified and it can potentially output a design with problems (syntactical or purely functional). Therefore, users are strongly recommended to perform a sanity check. This program allows a reliable sanity check mechanism, which performs formal equivalance checking between the exported desig the original one. For sanity check, run the following events:
;; First load some libraries and setup AIG transforms for fast equivalance checking. (progn (local (include-book "centaur/ipasir/ipasir-backend" :dir :system)) (local (include-book "centaur/aignet/transforms" :dir :system)) (local (defun transforms-config () (declare (Xargs :guard t)) #!aignet (list (make-observability-config) (make-balance-config :search-higher-levels t :search-second-lit t) (change-fraig-config *fraig-default-config* :random-seed-name 'my-random-seed :ctrex-queue-limit 8 :sim-words 1 :ctrex-force-resim nil :ipasir-limit 4 :initial-sim-rounds 2 :initial-sim-words 2 :ipasir-recycle-count 2000) ))) (local (defattach fgl::fgl-aignet-transforms-config transforms-config)) (local (define monolithic-sat-with-transforms () (fgl::make-fgl-satlink-monolithic-sat-config :transform t))) (local (defattach fgl::fgl-toplevel-sat-check-config monolithic-sat-with-transforms))) ;; Export the multiplier design and perform the sanity check. (export-to-verilog-after-adder-detection "my-mult_module_with_hier" :sanity-check t)
Above, the first set of events configures FGL to perform AIG transformations which are essential for equivalance checking to finish in a timely manner. You may need to set up the ipasir::ipasir libraries before this if you are setting up for the first time. If the above export-to-verilog-after-adder-detection event succeeds, it means that the exported design is proved to be equivalant to the original design. Speed of sanity check is usually high but it can vary, and tweaking and tuning the parameters above in transforms-config may make a huge difference.
If need be, another way to perform sanity check is as follows. The run-time performance of this method may be better or worse.
(export-to-verilog-after-adder-detection "my-mult_module_with_hier"
:sanity-check :rp-then-fgl)