mux-stv-works.lisp

(in-package "ACL2")

(include-book "centaur/sv/top" :dir :system)
(include-book "centaur/vl/loader/top" :dir :system)
(include-book "centaur/gl/gl" :dir :system)
(include-book "centaur/aig/g-aig-eval" :dir :system)
(include-book "centaur/sv/svtv/top" :dir :system) ; may be redundant
(include-book "centaur/4v-sexpr/top" :dir :system)
(include-book "tools/plev-ccl" :dir :system)
(include-book "centaur/misc/memory-mgmt" :dir :system)

(gl::def-gl-clause-processor my-glcp)

(defmodules *mux-vl-design*
  (vl2014::make-vl-loadconfig :start-files (list "mux.v")))

(defconst *mux*
  (vl2014::vl-module->esim
   (vl2014::vl-find-module "mux"
                           (vl2014::vl-design->mods
                            (vl2014::vl-translation->good *mux-vl-design*)))))

(defstv mux-test-vector
  :mod *mux*
  :inputs '(("in0" in0 _)
            ("in1" in1 _)
            ("sel" sel _))
  :outputs '(("out" out _)))

(def-gl-thm mux-boolean-spec
  :hyp (and (bitp sel)
            (bitp in1)
            (equal sel 1))
  :concl (equal (cdr (assoc 'out (stv-run (mux-test-vector)
                                           `((in0 . ,in0)
                                             (in1 . ,in1)
                                             (sel . ,sel)))))
                (if (logbitp 0 sel)
                    in1
                  in0))
  :g-bindings (gl::auto-bindings (:nat sel 1)
                                 (:nat in1 1)))

mux-svtv-does-not-work.lisp

(in-package "ACL2")

(include-book "centaur/sv/top" :dir :system)
(include-book "centaur/vl/loader/top" :dir :system)
(include-book "centaur/gl/gl" :dir :system)
(include-book "centaur/aig/g-aig-eval" :dir :system)
(include-book "tools/plev-ccl" :dir :system)
(include-book "centaur/misc/memory-mgmt" :dir :system)

(gl::def-gl-clause-processor my-glcp)

(defconsts (*mux-vl-design* state)
  (b* (((mv loadresult state)
        (vl::vl-load (vl::make-vl-loadconfig
                      :start-files '("mux.v")))))
    (mv (vl::vl-loadresult->design loadresult) state)))

(defconsts (*mux* *mux-simplified-good* *mux-simplified-bad*)
    (b* (((mv errmsg svex-design good bad)
          (vl::vl-design->svex-design "mux" *mux-vl-design*
                                      (vl::make-vl-simpconfig))))
      (and errmsg (raise "~@0~%" errmsg))
      (mv svex-design good bad)))

(sv::defsvtv mux-test-vector
  :mod *mux*
  :inputs '(("in0" in0 _)
            ("in1" in1 _)
            ("sel" sel _))
  :outputs '(("out" out _)))

(def-gl-thm mux-boolean-spec

; Results in this error output:
;; ****  WARNING ****
;; The following variables are present in the theorem but have no symbolic
;; object bindings:
;; (IN0)

;; not 4vec-boolmaskp: IN0
;; ; svex->aigs: 0.00 sec, 128 bytes.
;; ; env -> aig env: 0.00 sec, 38,256 bytes.
;; ; SV bit-blasting: a4veclist->aiglist: 0.00 sec, 128 bytes.
;; Unknown: 0
;; The alist is not well-formed for aig-eval-list-symbolic
;; Bddify with x-weakening, threshold 256 ... done
;; ; SV bit-blasting: aig-eval-list: 0.00 sec, 4,368 bytes.
;; ; bits->4vecs: 0.00 sec, 19,312 bytes.
;; ERROR: some bits assumed to be Boolean were not


;; ACL2 Error in ( DEFTHM MUX-BOOLEAN-SPEC ...):  Error in clause-processor
;; hint:

;;   Error: GL-ERROR call encountered.  Data associated with the error
;; is accessible using (@ GL::GL-ERROR-RESULT).

  :hyp (and (bitp sel)
            (bitp in1)
            (equal sel 1))
  :concl (equal (cdr (assoc 'out (svtv-run (mux-test-vector)
                                           `((in0 . ,in0)
                                             (in1 . ,in1)
                                             (sel . ,sel))
                                           :boolvars t)))
                (if (logbitp 0 sel)
                    in1
                  in0))
  :g-bindings (GL::AUTO-BINDINGS (:NAT SEL 1)
                                 (:NAT IN1 1)))

mux.v

module mux (in0, in1, sel, out );
   input in0;
   input in1;
   input sel;
   output out;

   assign out = sel ? in1 : in0;

endmodule