Mertcan Temel

Formal Verification Engineer, M.S., PhD Student

Introduction

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.

Prerequisites

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.

Instructions

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.

make

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:

Organization of the files

As mentioned above, the benchmarks in this package are generated from 3 different sources. These are:

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

Contact

Please visit the "Contacts" Page for any feedback or questions

www.000webhost.com