Expanded events for the second demo for vescmul showing how an industrial-design-mimicking module including a MAC, dot-product and merged multipliers can be verified.
In the first demo (Multiplier-Verification-demo-1), we have
shown how our tool can be used on an isolated multiplier. This is a good
starting point; however, real-world applications of integer multipliers
involve more intricate design strategies. We tried to recreate some of those
strategies and compiled a more complex multiplier module given in
The fact that this multiplier module reuses the same smaller integer
multipliers for different modes of operations, the design itself is slightly
more complicated which may cause further challenges to verification
systems. Therefore, we show how our tool can handle such cases and our
framework to verify them with a similar efficiency as stand-alone multipliers.
The same events we give below are also included in
1. Include necessary books. svl system uses sv and vl packages. So we start with them.
(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) ;; takes just a few seconds
Then, include has the rewrite and meta rules to carry out simplification of multiplier modules:
(include-book "projects/vescmul/svtv-top" :dir :system)
2. Parse the System Verilog design. All events take a few seconds in total.
Load VL design:
(acl2::defconsts (*mult-vl-design* state) (b* (((mv loadresult state) (vl::vl-load (vl::make-vl-loadconfig :start-files '("integrated_multipliers.sv"))))) (mv (vl::vl-loadresult->design loadresult) state)))
Load SV design:
(acl2::defconsts (*mul-sv-design* *simplified-good* *simplified-bad*) (b* (((mv errmsg sv-design good bad) (vl::vl-design->sv-design "Integrated_Multiplier" *mult-vl-design* (vl::make-vl-simpconfig)))) (and errmsg (acl2::raise "~@0~%" errmsg)) (mv sv-design good bad)))
3. The integrated multiplier module has an input signal called
(define mode (&key (acc-on 'nil) (reload-acc 'nil) (signed 'nil) (dot-product 'nil) (four-lanes-lo 'nil) (four-lanes-hi 'nil) (one-lane 'nil)) (b* (((unless (= 1 (+ (if dot-product 1 0) (if four-lanes-lo 1 0) (if four-lanes-hi 1 0) (if one-lane 1 0)))) (or (cw "One and only one of dot-product, four-lanes-lo, four-lanes-hi and one-lane should be set to 1.~%") (hard-error 'mode "" nil) 0)) (mode 0) (mode (svl::sbits 0 1 (if acc-on 0 1) mode)) (mode (svl::sbits 1 1 (if reload-acc 0 1) mode)) (mode (svl::sbits 2 1 (if signed 0 1) mode)) (mode (cond (dot-product (svl::sbits 3 2 0 mode)) (four-lanes-lo (svl::sbits 3 2 1 mode)) (four-lanes-hi (svl::sbits 3 2 2 mode)) (t (svl::sbits 3 2 3 mode))))) mode))
4. We are now ready to verify the top module for various multiplication modes. First, we verify various combinational modes (one-lane 64x64-bit MAC 4-32x32-bit dot-product, and four-lane 32x32-bit multiplication with lower and higher half truncation), then we show verification for a sequential mode (accumulated dot-product).
We define our first simulation pattern. Since we are currently only interested in the combinational functionality, we set "clk" to "0", and the other signals to some free variables.
(sv::defsvtv one-lane-mult2-svtv :mod *mult2-sv-design* :inputs '(("clk" 0) ("IN1" in1) ("IN2" in2) ("IN3" in3) ("mode" mode)) :outputs '(("result" result))) (add-rp-rule one-lane-mult2-svtv-autoins-fn)
Below is our first correctness proof of a multiplication mode. SVTV-run returns an association list of all the variables stated in outputs above. In this case, there is only one entry whose key is 'result'. We state the expression of this signal in our conjecture. Here it is [in3 + in2*in1 (both sign-extended)] and the complete result is truncated at 128 bits. This is the specification of this multiplication mode. When writing the specification, it is imperative to have loghead wrapping the arithmetic functions as seen here. Proving this lemma takes around a second. Alternatively, we could set in3 to "0", and verify only the multiplication function (but not MAC). In fact, we could set any portion of any input signals to any constants.
(defthmrp-multiplier signed-one-lane-mult-is-correct (implies (and (integerp in1) (integerp in2) (integerp in3)) (equal (sv::svtv-run (one-lane-mult2-svtv) (one-lane-mult2-svtv-autoins :mode (mode :one-lane t :signed t))) `((result . ,(loghead 128 (+ (* (logext 64 in1) (logext 64 in2)) in3)))))))
We can prove the same for the mode for unsigned numbers by changing the specification accordingly:
(defthmrp-multiplier unsigned-one-lane-mult-is-correct (implies (and (integerp in1) (integerp in2) (integerp in3)) (equal (sv::svtv-run (one-lane-mult2-svtv) (one-lane-mult2-svtv-autoins :mode (mode :one-lane t :signed nil))) `((result . ,(loghead 128 (+ (* (loghead 64 in1) (loghead 64 in2)) in3)))))))
5. Now, let's verify the dot product operation. To make it more readable, we split two of the input signals to four lanes. This conjecture, similarly, takes about a second to prove. We omit the proofs for unsigned for brevity.
(sv::defsvtv dotproduct-mult2-svtv :mod *mult2-sv-design* :inputs '(("clk" 0) ("IN1[31:0]" in1_0) ("IN2[31:0]" in2_0) ("IN1[63:32]" in1_1) ("IN2[63:32]" in2_1) ("IN1[95:64]" in1_2) ("IN2[95:64]" in2_2) ("IN1[127:96]" in1_3) ("IN2[127:96]" in2_3) ("IN3" in3) ("mode" mode)) :outputs '(("result" result))) (add-rp-rule dotproduct-mult2-svtv-autoins-fn) (defthmrp-multiplier signed-dot-product-is-correct (implies (and (integerp in1_0) (integerp in2_0) (integerp in1_1) (integerp in2_1) (integerp in1_2) (integerp in2_2) (integerp in1_3) (integerp in2_3) (integerp in3)) (equal (sv::svtv-run (dotproduct-mult2-svtv) (dotproduct-mult2-svtv-autoins :mode (mode :dot-product t :signed t))) `((result . ,(loghead 128 (+ (* (logext 32 in1_0) (logext 32 in2_0)) (* (logext 32 in1_1) (logext 32 in2_1)) (* (logext 32 in1_2) (logext 32 in2_2)) (* (logext 32 in1_3) (logext 32 in2_3)) in3)))))))
6. Another mode is four-lane multiplication that truncate at the lower half of multiplication. Similarly, we define new input and output simulation patterns, splitting all three inputs and the output to four lanes:
We can prove a similar lemma for unsigned mode as well (omittied in this doc).(sv::defsvtv four-lanes-mult2-svtv :mod *mult2-sv-design* :inputs '(("clk" 0) ("IN1[31:0]" in1_0) ("IN2[31:0]" in2_0) ("IN1[63:32]" in1_1) ("IN2[63:32]" in2_1) ("IN1[95:64]" in1_2) ("IN2[95:64]" in2_2) ("IN1[127:96]" in1_3) ("IN2[127:96]" in2_3) ("IN3[31:0]" in3_0) ("IN3[63:32]" in3_1) ("IN3[95:64]" in3_2) ("IN3[127:96]" in3_3) ("mode" mode)) :outputs '(("result[31:0]" result0) ("result[63:32]" result1) ("result[95:64]" result2) ("result[127:96]" result3))) (add-rp-rule four-lanes-mult2-svtv-autoins-fn) (defthmrp-multiplier signed-four-lanes-lo-is-correct (implies (and (integerp in1_0) (integerp in2_0) (integerp in3_0) (integerp in1_1) (integerp in2_1) (integerp in3_1) (integerp in1_2) (integerp in2_2) (integerp in3_2) (integerp in1_3) (integerp in2_3) (integerp in3_3)) (equal (sv::svtv-run (four-lanes-mult2-svtv) (four-lanes-mult2-svtv-autoins :mode (mode :four-lanes-lo t :signed t))) `((result0 . ,(loghead 32 (+ (* (logext 32 in1_0) (logext 32 in2_0)) in3_0))) (result1 . ,(loghead 32 (+ (* (logext 32 in1_1) (logext 32 in2_1)) in3_1))) (result2 . ,(loghead 32 (+ (* (logext 32 in1_2) (logext 32 in2_2)) in3_2))) (result3 . ,(loghead 32 (+ (* (logext 32 in1_3) (logext 32 in2_3)) in3_3)))))))
7. We have another combinational mode that is four-lane multiplication that truncate at the higher half. Function ash right or left shift numbers. In this case, we right shift the multiplication result by 32 bits to retrieve the higher end of the result.
(defthmrp-multiplier signed-four-lanes-hi-is-correct (implies (and (integerp in1_0) (integerp in2_0) (integerp in3_0) (integerp in1_1) (integerp in2_1) (integerp in3_1) (integerp in1_2) (integerp in2_2) (integerp in3_2) (integerp in1_3) (integerp in2_3) (integerp in3_3)) (equal (sv::svtv-run (four-lanes-mult2-svtv) (four-lanes-mult2-svtv-autoins :mode (mode :four-lanes-hi t :signed t))) `((result0 . ,(loghead 32 (+ (ash (* (logext 32 in1_0) (logext 32 in2_0)) -32) in3_0))) (result1 . ,(loghead 32 (+ (ash (* (logext 32 in1_1) (logext 32 in2_1)) -32) in3_1))) (result2 . ,(loghead 32 (+ (ash (* (logext 32 in1_2) (logext 32 in2_2)) -32) in3_2))) (result3 . ,(loghead 32 (+ (ash (* (logext 32 in1_3) (logext 32 in2_3)) -32) in3_3)))))) )
8. Finally, let's show our framework on a sequential operation. The design in integrated_multipliers.sv has an accumulator that can store the result across different clock cycles. We can use this feature to increase the size of dot product. So we create a simulation pattern where we load the accumulator with an initial value, and perform two dot-product operations in two clock cycles and accumulate the result. So we create a 8-32x32-bit dot product out of the existing 4-32x32-bit one.
(sv::defsvtv sequential-dotproduct-mult2-svtv :mod *mult2-sv-design* :inputs `(("clk" 0 1 ~) ("IN1[31:0]" _ _ in1[0] _ in1[4]) ("IN2[31:0]" _ _ in2[0] _ in2[4]) ("IN1[63:32]" _ _ in1[1] _ in1[5]) ("IN2[63:32]" _ _ in2[1] _ in2[5]) ("IN1[95:64]" _ _ in1[2] _ in1[6]) ("IN2[95:64]" _ _ in2[2] _ in2[6]) ("IN1[127:96]" _ _ in1[3] _ in1[7]) ("IN2[127:96]" _ _ in2[3] _ in2[7]) ("IN3" acc-init-val) ("mode" ,(mode :acc-on t :dot-product t :reload-acc t) mode mode mode mode)) :outputs '(("result" _ _ _ _ result))) (add-rp-rule sequential-dotproduct-mult2-svtv-autohyps) (add-rp-rule sequential-dotproduct-mult2-svtv-autoins)
In the previous proofs given above, we stated the specification of each mode explicitly in the conjectures. We can alternatively wrap these specifications with new functions for better readability. So we create a dot product specification function as given below.
(define dot-product-spec ((in1-lst integer-listp) (in2-lst integer-listp) (dot-product-size natp) (signed booleanp) (acc-init-val integerp) (acc-size natp)) :verify-guards nil :guard (and (equal dot-product-size (len in1-lst)) (equal dot-product-size (len in2-lst))) (if (zp dot-product-size) (loghead acc-size acc-init-val) (let* ((dot-product-size (1- dot-product-size))) (loghead acc-size (+ (if signed (* (logext 32 (nth dot-product-size in1-lst)) (logext 32 (nth dot-product-size in2-lst))) (* (loghead 32 (nth dot-product-size in1-lst)) (loghead 32 (nth dot-product-size in2-lst)))) (dot-product-spec in1-lst in2-lst dot-product-size signed acc-init-val acc-size))))) /// ;; We need to add the definition rule of this function to RP-Rewriter so that ;; it can know to expand it. (add-rp-rule dot-product-spec))
Then, we can state the correctness for the 8-32x32-bit dot product mode as:
(defthmrp-multiplier signed-dot-product-with-acc-is-correct (implies (and (equal signed t) (equal acc-size 128) (equal dot-product-size 8) (equal mode (mode :dot-product t :acc-on t :signed signed)) (sequential-dotproduct-mult2-svtv-autohyps)) (equal (sv::svtv-run (sequential-dotproduct-mult2-svtv) (sequential-dotproduct-mult2-svtv-autoins)) `((result . ,(dot-product-spec (list in1[0] in1[1] in1[2] in1[3] in1[4] in1[5] in1[6] in1[7]) (list in2[0] in2[1] in2[2] in2[3] in2[4] in2[5] in2[6] in2[7]) dot-product-size ; signed acc-init-val acc-size))))))