|
|
|---|
|
|
|
|---|
First demo for vescmul showing how an isolated integer multiplier is verified.
Below is a demo to verify a multiplier design coded in (System) Verilog. 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.
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. Parse the design.
(vesmul-parse :name my-multiplier-example :file "DT_SB4_HC_64_64_multgen.sv" :topmodule "DT_SB4_HC_64_64")
This verilog file is located in
3. Verify the design.
(vescmul-verify :name my-multiplier-example :concl (equal result (loghead 128 (* (logext 64 in1) (logext 64 in2)))))
Here, the variables are case-insensitive and they correspond to input/output names in the original design. For example, "result" is the output signal name, and "in1" and "in2" are input signals. This design performs 64x64-bit signed multiplication; therefore, the inputs are sign-extended with logext and the first 128-bit of multiplication is taken with loghead. This proof takes about 1.5 seconds to finish.
vescmul-verify event will also create a file under the generated-proof-summary directory showing what the program proved and how long it took. This can be handy when running many experiments. Alternatively, if you would like to view what is proved you can run the following command in an interactive session:
:pe my-multiplier-example-is-correct
vesmul-parse and vescmul-verify have other options that may be useful in some cases.
This program is tested for multipliers up to 1024x1024; and they each finished in a matter of minutes on our machines. However, verifying large multiplier may require users to increase the the stack size in ACL2 image (e.g., saved_acl2 under you ACL2 directory) and run the proofs again. What it should be increased to depends on your system (e.g., memory), and it is best to test and tune various options until you do not get an error. That is straightforward for systems with large memory (e.g., 32gb). 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.