Expanded events for the first demo for vescmul showing how an isolated integer multiplier is verified.
Below is a demo that showing every single event to input a multiplier design coded in (System) Verilog into ACL2, and verify it efficiently. We choose a 64x64-bit Booth Encoded Dadda Tree multiplier with Han-Carlson adder as our example. If you wish, you can skip to Multiplier-Verification-demo-2 for a more complex arithmetic module. What is different here than Multiplier-Verification-demo-1 is that this one does not use the vesmul-parse and vescmul-verify macros but deliver the events individually. This may be useful to some users.
1. Include the books to parse Verilog designs and crete symbolic simulation vectors.
(include-book "centaur/sv/top" :dir :system) ;; a big book; takes around 30 seconds (include-book "centaur/vl/loader/top" :dir :system) ;; takes around 10 seconds (include-book "oslib/ls" :dir :system)
2. Load VL design for the modules in DT_SB4_HC_64_64_multgen.sv. This file
is located under
(acl2::defconsts (*vl-design* state) (b* (((mv loadresult state) (vl::vl-load (vl::make-vl-loadconfig :start-files '("DT_SB4_HC_64_64_multgen.sv"))))) (mv ({vl::vl-loadresult->design loadresult) state)))
3. Load SV design:
(acl2::defconsts (*sv-design* *simplified-good* *simplified-bad*) (b* (((mv errmsg sv-design good bad) (vl::vl-design->sv-design "DT_SB4_HC_64_64" *vl-design* (vl::make-vl-simpconfig)))) (and errmsg (acl2::raise "~@0~%" errmsg)) (mv sv-design good bad)))
4. Create the test vector for symbolic simulation:
(sv::defsvtv mult-run :mod *sv-design* :inputs '(("IN1" a) ("IN2" b)) :outputs '(("result" res)))
5. Include the book that has the rewrite and meta rules for multiplier proofs:
(include-book "projects/vescmul/svtv-top" :dir :system)
6. Finally, prove the multiplier correct:
(defthmrp-multiplier multiplier-correct (implies (and (integerp a) (integerp b)) (b* (((sv::assocs res) (sv::svtv-run (mult-run) `((a . ,a) (b . ,b))))) (equal res (loghead 128 (* (logext 64 a) (logext 64 b)))))))This proof takes about 1.5 seconds to finish.
Here, we first extract the output value from svtv-run function. Then on the right hand-side, we state the specification. Here numbers a and b are sign extended at 64th-bits and multiplied. Then the first 128-bit of the multiplication result is compared to the design's output.
This program is tested for multipliers up to 1024x1024; and they each finished in a matte of minutes on our machines.
For large multipliers, users may need to increase the stack size in ACL2 image (e.g., saved_acl2 under you ACL2 directory) and run the proofs again. In our tests, we have observed SBCL to be faster than CCL; however, for large multipliers garbage collector of CCL does a better job with ACL2::set-max-mem and it can finish large proofs when SBCL terminates with memory errors.
You may continue to Multiplier-Verification-demo-2-expanded.