Experiment notes and instructions to run VeSCmul for multiplier verification
This page serves as a guidance to reproduce the experiment results for the VeSCmul tool (Verified implementation of S-C-Rewriting algorithm for multiplier verification). VeSCmul is a verified program that can automaticaly and very quickly verify various integer multiplier-based designs. For further details, please see the Publications page and view related papers.
Experiment notes. I kept notes when I ran multiplier verification experiments particularly for other state-of-the-art tools. See those notes here.
VeSCmul source code is distributed with ACL2 on github. The most recent version can be obtained from the master branch. A short documentation for the library is also present in the public ACL2 documentation pages.
Quick start with VeSCmul. A small package with a few examples showing how to run VeSCmul is given here. This is most useful when using VeSCmul for new designs. This package includes a README file to guide you through the installation and execution steps.
To run VeSCmul Experiments (updated 2023), please use this link to download benchmarks and scripts to rerun experiments for VeSCmul: [Download Here (~80 MB)]. This package includes a README file to guide you through the installation and execution steps.
Older experiments from FMCAD 2021. Please use this link to download benchmarks as seen in the FMCAD21 publication: [Download Here]. This package includes a README file to guide you through the installation and execution steps. Note that this package is not maintained anymore and you are recommended to use the updated package above.