|
|
|---|
|
|
|
|---|
The third demo for vescmul showing how an a hierarchical reasoning hint may be passed for designs whose adders may not be automatically identified.
VeSCmul may not always be able to find adder components in a given
design. However, our system still supports hierarhical reasoning, and we can
provide hierarhical reasoning hints to help the program. Below is a demo
showing how it can be achieved for a 64x64-bit multiplier with 7-to-3
compressor tree. This module is given in this file:
1. As a hierarchical reasoning hint, we offer alternative definitions for some of the adder modules in this design. Particularly, we redefined 7to3, 6to3, 5to3, and 4to3 compressor modules. So first, we create a new file contaning those easier-to-identify definitions.
(defwarrant str::fast-string-append-lst) (defwarrant str::int-to-dec-string$inline) (write-string-to-file-event "better-homma-7-3.v" ;; homma designs for some reason repeat the same module many times with ;; different names. So below creates a better copy of some adder modules with ;; a loop. (string-append-lst (append (loop$ for x from 0 to 123 collect (str::cat "module UB7_3C" (str::intstr x) " (output S1, S2, S3, input X1,X2,X3,X4,X5,X6,X7); wire car1,car2,sum1,sum2,car3; // make it look like a group of full-adders: assign {car1,sum1} = (X1+X2+X3); assign {car2,sum2} = (X5+X6+X7); assign {car3,S3} = (X4+sum1+sum2); assign {S1,S2} = car1+car2+car3; endmodule ")) (loop$ for x from 0 to 123 collect (str::cat "module UB6_3C" (str::intstr x) " (output S1, S2, S3, input X1,X2,X3,X4,X5,X6); wire car1,car2,sum1,sum2,car3; // make it look like a group of full-adders: assign {car1,sum1} = (X1+X2+X3); assign {car2,sum2} = (X4+X5+X6); assign {car3,S3} = (sum1+sum2); assign {S1,S2} = car1+car2+car3; endmodule ")) (loop$ for x from 0 to 123 collect (str::cat "module UB5_3C" (str::intstr x) " (output S1, S2, S3, input X1,X2,X3,X4,X5); wire car1,car2,sum1,sum2,car3; // make it look like a group of full-adders: assign {car1,sum1} = (X1+X2+X3); assign {car2,sum2} = (X4+X5); assign {car3,S3} = (sum1+sum2); assign {S1,S2} = car1+car2+car3; endmodule ")) (loop$ for x from 0 to 123 collect (str::cat "module UB4_3C" (str::intstr x) " (output S1, S2, S3, input X1,X2,X3,X4); wire car1,car2,sum1,sum2,car3; // make it look like a group of full-adders: assign {car1,sum1} = (X1+X2+X3); assign {car3,S3} = (sum1+X4); assign {S1,S2} = car1+car3; endmodule ")))))
2. Parse the design. This program will parse and create two simulation vectors for the design. One will be the simulation of the original design, and the other will be similation of the design whose adder modules are replaced with the ones in better-homma-7-3.v file. vescmul-verify will later perform equivalance checking between the two to make sure that the two designs are functionally equivalant.
(vesmul-parse :file "homma-7-to-3-64x64-signed-carry-select.v" :topmodule "Multiplier_63_0_6000" :name homma-7-to-3 :modified-modules-file "better-homma-7-3.v")
3. Verify the design. vescmul-verify will perform equivalance checking between the modified and original design first using FGL. For fast equivalance checking, we set up AIG transforms which will use an incremental SAT solver. Make sure you have IPASIR set up: ipasir::ipasir. After equivalance checking, vescmul will use the modified version to verify the multiplier and once proved, state a theorem for the correctness of the unmodified, original design.
Set up AIG trannsforms for fast equiv checking. Tweaking the parameters can affect the proof-time result a lot.
(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)))
Finally, call verify:
(vescmul-verify :name homma-7-to-3 :concl (equal p (loghead 128 (* (logext 64 in1) (logext 64 in2)))))
This should take a few seconds to run all the proofs. You can see the generated proof summary file or run:
to see what is proved. We have a final corectness theorem based on the original design.:pe homma-7-to-3-is-correct