		Search-engine friendly clone of the ACL2 documentation.

Vescmul-verify

A macro to verify a multiplier using VeSCmul from an already created simulation test vector with vesmul-parse

vescmul-verify can take the following arguments:

:name has to be provided. It should be a symbol and be the name corresponding to the name picked in vesmul-parse.
:concl has to be provided. The body of the conjecture to be proved.
:thm-name is optional. It will be the name of the final theorem proved. When provided, it should be a symbol. When not provided, the program will automatically calculate a thm-name by append "-is-correct" to the name provided with the :name argument.
:hyp is optional. A term that will be used as hypothesis when verifying a multiplier. It can be useful when setting some control signals or when assuming some simulation conditions.
:vacuity-check is optional and should be nil (default) or t. When set to t, the program checks whether something in the assumptions / hypotheses (passed in :hyp) are contradictory.
:then-fgl is optional. To invoke FGL (calls a SAT solver) after rewriter finishes. FGL is configurable, for example, to call the desired SAT solver and/or perform AIG transforms. See below.
:read-from-file is optional. It should be a string be the value corresponding to the one in the :save-to-file argument of vesmul-parse.
:cases is optional. A list of terms that can be used to casesplit upon starting the program. Casesplit hints may be useful for some corner cases.
:keep-going is optional, should be t or nil. When set to t, the program will not stop ACL2 if a proof-attempt fails. This is useful when running a lot of experiments in the same file, and you expect that some may fail to prove.
:print-message is optional and should be a string if given. The program will also generate a proof summary file after it has run. Users may pass a custom message through this argument that will appear in the proof summary file.

vescmul-verify will create a proof-summary file under the generated-proof-summary directory showing the proof time and what the program verified about multiplier design.

Example call 1:


(vescmul-verify :name my-multiplier-example
                :concl (equal result
                              (loghead 128 (* (logext 64 in1)
                                              (logext 64 in2))))
                :read-from-file "parsed/")

Example call 2:


(vescmul-verify :name my-multiplier-example
                :concl (equal result
                              (loghead 128 (* (logext 64 in1)
                                              (logext 64 in2)))))

Example call 3:


;; Casesplit on 63th bits of in1 and in2. This may be helpful in some corner
;; cases. 
(vescmul-verify :name my-multiplier-example
                :cases ((logbitp 63 in1) (logbitp 63 in2))
                :concl (equal result
                              (loghead 128 (* (logext 64 in1)
                                              (logext 64 in2)))))

Example call 4:


;; If VeSCmul cannot finish the proofs, this will call FGL after rewriting is done 
(vescmul-verify :name my-multiplier-example
                :then-fgl t
                :concl (equal result
                              (loghead 128 (* (logext 64 in1)
                                              (logext 64 in2)))))

You may also configure FGL. For example this will call kissat for SAT Solver:


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

Or, this will perform AIG transform using incremental SAT solvers. You need to set up IPASIR library (see ipasir::ipasir). This can improve the performance in some cases such as equivalance checking during hierarchical reasoning scheme.


(progn
  (local (include-book "centaur/ipasir/ipasir-backend" :dir :system))
  (local (include-book "centaur/aignet/transforms" :dir :system))
  (local (defun transforms-config ()
           (declare (Xargs :guard t))
           #!aignet
           (list (make-observability-config)
                 (make-balance-config :search-higher-levels t
                                      :search-second-lit t)
                 (change-fraig-config *fraig-default-config*
                                      :random-seed-name 'my-random-seed
                                      :ctrex-queue-limit 8
                                      :sim-words 1
                                      :ctrex-force-resim nil
                                      :ipasir-limit 4
                                      :initial-sim-rounds 2
                                      :initial-sim-words 2
                                      :ipasir-recycle-count 2000)
                 )))
  (local (defattach fgl::fgl-aignet-transforms-config transforms-config))
  (local (define monolithic-sat-with-transforms ()
           (fgl::make-fgl-satlink-monolithic-sat-config :transform t)))
  (local (defattach fgl::fgl-toplevel-sat-check-config monolithic-sat-with-transforms)))