|
|
|---|
|
|
|
|---|
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 the books to parse Verilog designs and crete symbolic simulation vectors.
(include-book "projects/vescmul/top" :dir :system)
Including this book can take a long time (around a minute). However, we can save an executable that has this image already loaded. You can either follow the instructions at save-exec or download a package that does that for you. This package also includes some demo files.
2. The integrated multiplier module has an input signal called
(define calculate-mode-value (&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) ;; check for illegal combination (if four-lanes-lo 1 0) (if four-lanes-hi 1 0) (if one-lane 1 0)))) -1) (mode 0) (mode (install-bit 0 (if acc-on 0 1) mode)) (mode (install-bit 1 (if reload-acc 0 1) mode)) (mode (install-bit 2 (if signed 0 1) mode)) (mode (cond (dot-product (part-install 0 mode :low 3 :width 2)) (four-lanes-lo (part-install 1 mode :low 3 :width 2)) (four-lanes-hi (part-install 2 mode :low 3 :width 2)) (t (part-install 3 mode :low 3 :width 2))))) mode))
3. Parse the design and create the simulation vector to test out cases that can be simulated combinationally.
(vesmul-parse :name integrated_multipliers-combinational-modes :file "integrated_multipliers.sv" :topmodule "Integrated_Multiplier")
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).
Below is our first correctness proof of a multiplication mode. In this case it is signed one-lane mode, which is expected to implement [in3 + in2*in1 (both sign-extended)] and the complete result is truncated at 128 bits. We set the mode signals value in the hypothesis with the :hyp argument. We pass a custom name to the theorem that will be submitted with the :thm-name argument.
(vescmul-verify :name integrated_multipliers-combinational-modes :thm-name signed-one-lane-mult-correct :hyp (equal mode (calculate-mode-value :one-lane t :signed t)) :concl (equal 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:
(vescmul-verify :name integrated_multipliers-combinational-modes :thm-name unsigned-one-lane-mult-correct :hyp (equal mode (calculate-mode-value :one-lane t :signed nil)) :concl (equal 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 here for brevity.
(vescmul-verify :name integrated_multipliers-combinational-modes :thm-name signed-comb-dot-product-is-correct :hyp (equal mode (calculate-mode-value :dot-product t :signed t)) :concl (equal result (loghead 128 (+ (* (logext 32 (nth-slice32 0 in1)) (logext 32 (nth-slice32 0 in2))) (* (logext 32 (nth-slice32 1 in1)) (logext 32 (nth-slice32 1 in2))) (* (logext 32 (nth-slice32 2 in1)) (logext 32 (nth-slice32 2 in2))) (* (logext 32 (nth-slice32 3 in1)) (logext 32 (nth-slice32 3 in2))) 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:
(vescmul-verify :name integrated_multipliers-combinational-modes :thm-name signed-four-lanes-lo-is-correct :hyp (equal mode (calculate-mode-value :four-lanes-lo t :signed t)) :concl (equal result (merge-4-u32s ;; most significant portion first. (loghead 32 (+ (* (nth-slice32 3 in1) (nth-slice32 3 in2)) (nth-slice32 3 in3))) (loghead 32 (+ (* (nth-slice32 2 in1) (nth-slice32 2 in2)) (nth-slice32 2 in3))) (loghead 32 (+ (* (nth-slice32 1 in1) (nth-slice32 1 in2)) (nth-slice32 1 in3))) (loghead 32 (+ (* (nth-slice32 0 in1) (nth-slice32 0 in2)) (nth-slice32 0 in3))))))
We can prove a similar lemma for unsigned mode as well (omittied in this doc).
7. We have another combinational mode that is four-lane multiplication that truncate at the higher half. Function logtail right shift numbers. In this case, we right shift the multiplication result by 32 bits to retrieve the higher end of the result.
(vescmul-verify :name integrated_multipliers-combinational-modes :thm-name signed-four-lanes-hi-is-correct :hyp (equal mode (calculate-mode-value :four-lanes-hi t :signed t)) :concl (equal result (merge-4-u32s ;; as in Verilog concatenation, most ;; significant portion first. (loghead 32 (+ (logtail 32 (* (logext 32 (nth-slice32 3 in1)) (logext 32 (nth-slice32 3 in2)))) (nth-slice32 3 in3))) (loghead 32 (+ (logtail 32 (* (logext 32 (nth-slice32 2 in1)) (logext 32 (nth-slice32 2 in2)))) (nth-slice32 2 in3))) (loghead 32 (+ (logtail 32 (* (logext 32 (nth-slice32 1 in1)) (logext 32 (nth-slice32 1 in2)))) (nth-slice32 1 in3))) (loghead 32 (+ (logtail 32 (* (logext 32 (nth-slice32 0 in1)) (logext 32 (nth-slice32 0 in2)))) (nth-slice32 0 in3))))))
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.
(vesmul-parse :name integrated_multipliers-sequential-mode :file "integrated_multipliers.sv" :topmodule "Integrated_Multiplier" ;; Define the clock: (clk signal should continuously toggle) :cycle-phases (list (sv::make-svtv-cyclephase :constants '(("clk" . 0)) :inputs-free t :outputs-captured t) (sv::make-svtv-cyclephase :constants '(("clk" . 1)))) :stages (;; reload the ACC in the first clock cycle (:label reload-acc :inputs (("IN3" acc-init-val) ("mode" mode-init-val))) ;; Feed some values in the second clock cycle for dot product (:label 1st-vectors :inputs (("IN1" in1-1) ("IN2" in2-1) ;; keep the mode value the same in the next cycles. ("mode" mode :hold t)) :outputs (("result" result1))) ;; Feed more values for dot-product. (:label 2nd-vectors :inputs (("IN1" in1-2) ("IN2" in2-2)) :outputs (("result" result2)))))
The call for vesmul-parse is more complicated here as we need to define what happens in each clock cycle. With the :cycle-phases argument we tell the program what signal represents the clock in a given design. In this case it is "clk". This defines stages (each clock cycle), and we describe how the design should be simulated at each stage. The first clock cycle will be used to load the accumulator. The second and third clock cycles will be used to feed in the input vectors for dot-product. The lane width for dot-product is 32-bits. The input signals "IN1" and "IN2" are 128-bit wide, storing 4-lanes of data. We bind those signals to free variables (e.g., in1-1) which will be refered to in the proofs we will run below.
The users of our tool can also define custom functions to define specification. This can help with readability. As an example, we define the spec function below.
(define dot-product32 ((in1 integerp) (in2 integerp) (signed booleanp) (dot-size natp)) (if (zp dot-size) 0 (+ (if signed (* (logext 32 in1) (logext 32 in2)) (* (loghead 32 in1) (loghead 32 in2))) (dot-product32 (logtail 32 in1) (logtail 32 in2) signed (1- dot-size)))) /// ;; tell the rewriter to expand the definition of this spec function. (add-rp-rule dot-product32))
Then, we can state the correctness for the 8-32x32-bit dot product mode as:
(vescmul-verify :name integrated_multipliers-sequential-mode :thm-name signed-dot-product-with-acc-is-correct :hyp (and ;; set the first mode value to reload ACC. (equal mode-init-val (calculate-mode-value :acc-on t :dot-product t :reload-acc t)) ;; mode in the following clock cycle is set to ;; dot-product accumulate (equal mode (calculate-mode-value :dot-product t :acc-on t :signed t))) ;; we can validate the value of the output in different cycles: :concl (and (equal result1 (loghead 128 (+ (dot-product32 in1-1 in2-1 t 4) acc-init-val))) (equal result2 (loghead 128 (+ (dot-product32 in1-1 in2-1 t 4) (dot-product32 in1-2 in2-2 t 4) acc-init-val)))))
Note that the conclusion has a conjunct of two expressions. This is optional and only here to show the flexibility of our program. "result1" refers to the value of the output signal at the second clock cycle, and "result2" refers to the value of the output signal at the third clock cycle.