This package contains over 250 Verilog files implementing various multiplier designs. These include isolated multipliers as well as multiplier-centric modules such as multiply-accumulate and dot-product. These modules are created with 3 different circuit generators (more on this below).
We have created scripts to run our verification tool on these benchmarks with a single "make" command and put the timing results together on a single text file "result.txt". Follow the instructions below to run our tool.Download the benchmarks for operands sizes 256 or less here (134 MB). Since they are too large, we do not share 512x512-bit and 1024x1024-bit multipliers but you may request them or generate them using the generators given below.
1. A Common Lisp implementation needs to be installed on your system. We use SBCL and sometimes CCL. SBCL can be faster. You can either obtain this software from their corresponding GitHub pages or using a third party tool. For example, "brew install sbcl" will give you SBCL on an OSX.
2. The most recent ACL2 version from GitHub (https://github.com/acl2/acl2) needs to be installed on your system. The most recent ACL2 release may not work, and you need to clone from the master branch. You may follow the instructions at https://www.cs.utexas.edu/users/moore/acl2/v8-2/HTML/installation/installation.html to build ACL2. You basically need to say "make LISP=sbcl" to build an ACL2 executable.
Once ACL2 executable is created, do not forget to create a shortcut to it so that calling "acl2" from shell starts ACL2. If you cannot do that for some reason, you can update the given Makefile so that "ACL2" points to your executable.
3. Python needs to be installed in the system. Calling "python" from shell should start a python version.
4. A system with 16 GB memory, which is only necessary for designs with 256-bit inputs.
1. Run "make" to start running all the proofs. There are some large multipliers and this can take almost an hour. If you have just built ACL2 without certifying books, you can expect this to take another hour for some ACL2 books to build before the proofs can start.
Alternatively, you can run "make 64", "make 128", "make 256", or "make dot-product" to verify only a subset of the benchmarks. For example "make 128" will only verify 128x128-bit multipliers.
make 64 && make 128 ...
2. Check the proof-time results from result.txt. These are parsed from *.cert.out files after proofs are finished.
Other make commands:
- "make clean" will clean all the proofs in case you want to rerun them.
- "make clean-proofs" is the same as "make clean"
- "make clean-certs" will clean all the proofs as well as some helper files. Probably not useful for users of this package.
- "make clean-svl-designs" is the most aggressive clean command and it clears previously parsed SVL designs. We verify Verilog designs by converting them to SVL format. For some smaller designs, this package includes .svl-design files that represents Verilog design in SVL format. .svl-design files can save users time so that they don't have to parse these designs into SVL every time they want to run the proofs. If you run this make command, these files will be removed. Then, users would have to run "make parse" before they can verify designs.
- "make parse" parses all the Verilog designs and converts them to the SVL format. Necessary after "make clean-svl-designs".
Organization of the files
As mentioned above, the benchmarks in this package are generated from 3 different sources. These are:
- Arithmetic Module Generator (shortened as homma): https://www.ecsis.riec.tohoku.ac.jp/topics/amg/i-amg/request/multiplier
- GENMUL (shortened as sca or sca-genmul): http://www.informatik.uni-bremen.de/agra/sca-verification/genmul.html
- MULTGEN (shortened as tem): https://github.com/temelmertcan/multgen
You will see that the directories in this package are separated with respect to these generators. In each directory, there is another called "verilog-files" where you will find the verilog files as implied by the name.
Since our method takes advantage of design hierarchy, we have a different script for each generator so that we can automatically detect the adder modules and quickly verify different designs. The file parse-macros.lisp has functions to parse designs and make sure that adders are not flattened. The file proof-macros.lisp has functions that runs multiplier proofs quickly.
Under the parsed-modules subdirectories, you will find the scripts that call the functions from parsed-modules.lisp. These files convert Verilog designs into SVL format. They will later be read by our proof files.
Under the proofs subdirectories, you will find files that calls the functions from proof-macros.lisp to verify each multiplier design. After we run the proofs, *-proof.summary files are created. Users can read these files to see the conjectures we proved for each design.
Other useful links:
You can find another artifact here of the same project. This one involves an VM image so that you do not have to install ACL2 but it is very large in size:Old artifacts
Tutorial to run our tool on new designs can be found here:Multiplier verification documentation
Our source code, ACL2 Demo files, example modules in Verilog (including the integrated multipliers module) are redistributed with ACL2:Multiplier verification demo files in the ACL2 repository
Please visit the "Contacts" Page for any feedback or questions