• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
        • Vl-ealist-p
        • Modinsts-to-eoccs
        • Vl-module-make-esim
        • Exploding-vectors
        • Resolving-multiple-drivers
        • Vl-modulelist-make-esims
        • Vl-module-check-e-ok
        • Vl-collect-design-wires
        • Adding-z-drivers
        • Vl-design-to-e
        • Vl-design-to-e-check-ports
        • Vl-design-to-e-main
        • Port-bit-checking
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• E-conversion

Vl-module-make-esim

Convert a Verilog module into an E module.

Signature

(vl-module-make-esim x mods modalist eal) → (mv new-x eal)

Arguments

x — The module we want to convert into an E module. We assume that the module has no unsupported constructs, okay port bits, etc, since these are checked in vl-modulelist-make-esims.
    Guard (vl-module-p x).

mods — The list of all modules. Note: this stays fixed as we recur, so the modules generally here don't have their esim fields filled in yet.
    Guard (vl-modulelist-p mods).

modalist — For fast module lookups.
    Guard (equal modalist (vl-modalist mods)).

eal — The vl-ealist-p that we are constructing and extending. This allows us to look up the E modules for previously processed modules.
    Guard (vl-ealist-p eal).

Returns

new-x — New version of x with its esim field filled in, if possible.
    Type (vl-module-p new-x), given (force (vl-module-p x)).

eal — Extended version of eal with the esim for x.

We try to compute the esim for x, install it into x, and extend eal with the newly produced esim.

Definitions and Theorems

Function: vl-module-make-esim

(defun vl-module-make-esim (x mods modalist eal)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-modulelist-p mods)
                             (vl-ealist-p eal)
                             (equal modalist (vl-modalist mods)))))
 (let ((__function__ 'vl-module-make-esim))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    ((when x.esim)
     (if (good-esim-modulep x.esim)
         (mv x (hons-acons x.name x.esim eal))
      (b*
       ((w
         (make-vl-warning
          :type :vl-bad-esim
          :msg
          "~a0 already has an esim provided, but it does ~
                           not even satisfy good-esim-modulep."
          :args (list x.name)
          :fatalp t
          :fn 'vl-module-make-esim)))
       (mv (change-vl-module x
                             :esim nil
                             :warnings (cons w x.warnings))
           eal))))
    (warnings x.warnings)
    ((mv okp warnings)
     (vl-module-check-e-ok x warnings))
    ((unless okp)
     (mv (change-vl-module x :warnings warnings)
         eal))
    ((mv okp warnings walist)
     (vl-module-wirealist x warnings))
    ((unless okp)
     (er
      hard? 'vl-module-make-esim
      "Wire-alist construction failed?  Shouldn't be possible: we ~
               should have already done this in vl-module-check-port-bits.")
     (mv x eal))
    (starname (vl-starname x.name))
    ((mv okp & in out)
     (vl-portdecls-to-i/o x.portdecls walist))
    ((unless okp)
     (er
      hard? 'vl-module-make-esim
      "Portdecl i/o pattern construction failed?  Shouldn't be ~
               possible: we should have already done this in ~
               vl-module-check-port-bits.")
     (mv x eal))
    (flat-in (pat-flatten1 in))
    (flat-out (pat-flatten1 out))
    (flat-ios (append flat-in flat-out))
    ((mv okp warnings occs)
     (vl-modinstlist-to-eoccs x.modinsts
                              walist mods modalist eal warnings))
    ((unless okp)
     (mv (change-vl-module x :warnings warnings)
         eal))
    (all-names (vl-eocclist-allnames-exec occs flat-ios))
    ((unless (vl-emodwirelist-p all-names))
     (er
      hard? 'vl-module-make-esim
      "Found names that are not emodwires in the list of allnames?  ~
               This shouldn't be possible because of how the occurrences and ~
               i/o patterns are constructed.")
     (mv x eal))
    (occs (vl-add-zdrivers all-names flat-in flat-out occs))
    ((when (let ((driven-sigs (collect-signal-list :o occs)))
             (or (member 't driven-sigs)
                 (member 'acl2::f driven-sigs))))
     (b*
      ((w
        (make-vl-warning
         :type :vl-output-constant
         :msg
         "In ~a0, somehow we have occurrences driving the ~
                         wires T and F. Is this module somehow trying to ~
                         drive a value onto a constant or something?"
         :args (list x.name)
         :fatalp t
         :fn 'vl-module-make-esim)))
      (mv (change-vl-module x
                            :warnings (cons w warnings))
          eal)))
    ((when (or (member 'acl2::vl-driver-for-constant-t
                       all-names)
               (member 'acl2::vl-driver-for-constant-f
                       all-names)))
     (b*
      ((w
        (make-vl-warning
         :type :vl-name-clash
         :msg
         "~a0 contains a wire named vl-driver-for-constant-t or ~
                         vl-driver-for-constant-f, so we're dying badly."
         :args (list x.name)
         :fatalp t
         :fn 'vl-module-make-esim)))
      (mv (change-vl-module x
                            :warnings (cons w warnings))
          eal)))
    (occs (list* (list :u 'acl2::vl-driver-for-constant-t
                       :op acl2::*esim-t*
                       :i nil
                       :o '((t)))
                 (list :u 'acl2::vl-driver-for-constant-f
                       :op acl2::*esim-f*
                       :i nil
                       :o '((acl2::f)))
                 occs))
    (occs (vl-add-res-modules all-names occs))
    (driven-sigs (collect-signal-list :o occs))
    ((unless (uniquep driven-sigs))
     (b*
      ((w
        (make-vl-warning
         :type :vl-programming-error
         :msg
         "~a0: after resolving multiply driven wires, we ~
                         somehow have multiple drivers for ~&1."
         :args (list x.name (duplicated-members driven-sigs))
         :fatalp t
         :fn 'vl-module-make-esim)))
      (mv (change-vl-module x
                            :warnings (cons w warnings))
          eal)))
    (in-driven (intersect (mergesort driven-sigs)
                          (mergesort flat-in)))
    ((when in-driven)
     (b*
      ((w
        (make-vl-warning
         :type :vl-backflow
         :msg
         "~a0: input bits ~&1 are being driven from within ~
                         the module!"
         :args (list x.name
                     (vl-verilogify-emodwirelist in-driven))
         :fatalp t
         :fn 'vl-module-make-esim)))
      (mv (change-vl-module x
                            :warnings (cons w warnings))
          eal)))
    ((mv warnings dwires)
     (vl-collect-design-wires x walist warnings))
    (esim (list :n starname
                :i in
                :o out
                :occs occs
                :a (list (cons :design-wires dwires)
                         (cons :wire-alist walist))))
    ((unless (good-esim-modulep esim))
     (b* (((cons details args)
           (bad-esim-modulep esim))
          (w (make-vl-warning
                  :type :vl-programming-error
                  :msg (cat x.name
                            ": failed to make a good esim module.  "
                            "Details: " details)
                  :args args
                  :fatalp t
                  :fn 'vl-module-make-esim)))
       (mv (change-vl-module x
                             :warnings (cons w warnings))
           eal)))
    (x-prime (change-vl-module x
                               :warnings warnings
                               :esim esim))
    (eal (hons-acons x.name esim eal)))
   (mv x-prime eal))))

Theorem: vl-module-p-of-vl-module-make-esim.new-x

(defthm vl-module-p-of-vl-module-make-esim.new-x
  (implies (force (vl-module-p x))
           (b* (((mv ?new-x ?eal)
                 (vl-module-make-esim x mods modalist eal)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-module->name-of-vl-module-make-esim

(defthm vl-module->name-of-vl-module-make-esim
  (let ((ret (vl-module-make-esim x mods modalist eal)))
    (equal (vl-module->name (mv-nth 0 ret))
           (vl-module->name x))))

Theorem: good-esim-modulep-of-vl-module-make-esim

(defthm good-esim-modulep-of-vl-module-make-esim
  (let ((ret (vl-module-make-esim x mods modalist eal)))
    (implies (and (vl-module->esim (mv-nth 0 ret))
                  (force (vl-module-p x))
                  (force (vl-ealist-p eal)))
             (good-esim-modulep (vl-module->esim (mv-nth 0 ret))))))

Theorem: vl-ealist-p-vl-module-make-esim

(defthm vl-ealist-p-vl-module-make-esim
  (let ((ret (vl-module-make-esim x mods modalist eal)))
    (implies (and (force (vl-module-p x))
                  (force (vl-ealist-p eal)))
             (vl-ealist-p (mv-nth 1 ret)))))