基于acl2镜像快速验证乘法器

1）写这篇文章的原因：使用acl2的安装和vescmul的运行教程在第一次验证乘法器后，会在bin目录中编译生成一个名称为vescmul.lx86cl64的镜像文件，再次验证时会使用这个镜像，验证时间会大幅度减少，编译生成这个镜像文件比较耗时，如果在其他机器上验证乘法器，把这个镜像复制过去就可以

2）在acl2镜像同级目录中有一个可执行脚本文件，在其中设置acl2的解释器ccl的路径CCL_DEFAULT_DIRECTORY，把ccl/lx86cl64、acl2镜像vescmul.lx86cl64的路径设置好。

3）设置sat solver的路径，如果验证有反例，可以打印反例，设置的方式如下所示：

(local(progn(defun my-sat-config ()(declare (xargs :guard t))(satlink::make-config :cmdline "/home/codespace/kissat/build/kissat " :verbose t :mintime 1/2 :remove-temps t))(defattach fgl::fgl-satlink-config my-sat-config)))

4）在acl2镜像的bin目录中有vescmul脚本，执行命令

vescmul < verify.lisp

5）如果验证成功，在generated-proof-summary/interactive-summary.txt，有如下日志

Proof for this conjecture finished in -- 0.749 seconds --.

如果验证失败，在generated-proof-summary/interactive-summary.txt，有如下日志

!!! This proof has failed !!!

而且在acl2的验证日志中有如下打印反例的日志

*** Counterexample assignment: ***
((B . 0) (A . 0))

6）以下给出一个具体示例，包括RTL、acl2验证脚本

mul.v(乘法器RTL)如下所示：

module top(a, b, res);input [31:0] a;input [31:0] b;output [63:0] res;assign res = a * b;
endmodule

acl2验证脚本如下所示：

(in-package "RP")(include-book "projects/rp-rewriter/lib/mult3/top" :dir :system)(rp::set-rw-step-limit (expt 2 30))
(rp::set-rp-backchain-limit 10000)(value-triple (acl2::set-max-mem (* 16 (expt 2 30))))
(SET-SLOW-ALIST-ACTION :WARNING)(parse-and-create-svtv :file "mul.v":topmodule "top":save-to-file "parsed/":name mul)(local(progn(defun my-sat-config ()(declare (xargs :guard t))(satlink::make-config :cmdline "/home/codespace/kissat/build/kissat " :verbose t :mintime 1/2 :remove-temps t))(defattach fgl::fgl-satlink-config my-sat-config)))(verify-svtv-of-mult :name mul:then-fgl t:concl (equal res (* a b)):read-from-file "parsed/":keep-going t)