使用sat一类的求解器验证乘法器，通常无法收敛，Mertcan Temel博士基于acl2实现了数字电路中乘法器的验证。下面简单介绍一下acl2的安装、vescmul的运行。

1.下载acl2

git clone https://github.com/acl2/acl2.git

2.acl2基于lisp编程语言实现，这里需下载lisp的一个编译器ccl

wget https://github.com/Clozure/ccl/releases/download/v1.13/ccl-1.13-linuxx86.tar.gz

测试刚下载的ccl在本地是否可用

cd ccl
./lx86cl64 --verion

如果报告“./lx86cl64: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.33' not found (required by ./lx86cl64)”，则需重新编译lx86cl64

cd lisp-kernel/linuxx8664
make clean && make

在acl2/books/projects/rp-rewriter/lib/mult3中确认top.lisp文件的存在

按照Building-an-ipasir-solver-library教程，构建libipasirglucose4.so

设置IPASIR_SHARED_LIBRARY环境变量

export IPASIR_SHARED_LIBRARY=/absolute_path/libipasirglucose4.so

3.编译acl2

cd acl2/books
make LISP=ccl/lx86cl64 basic add-ons centaur -j

4.下载vescmul

wget https://temelmertcan.github.io/vescmul.zip

vescmul目前使用acl2验证乘法器的接口为parse-and-create-svtv、verify-svtv-of-mult

github上的acl2验证乘法器的接口已经更新为vescmul-parse、vescmul-verify，接口参数大致相同，写好acl2验证脚本verify.lisp后，执行如下命令

bin/cert.sh verify.lisp

最后在generated-proof-summary中查看验证结果