• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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-modinst-to-eocc
          • Vl-modinst-eocc-bindings
          • Vl-portdecls-to-i/o
          • Vl-plainarglist-lsb-pattern
          • Vl-modinstlist-to-eoccs
          • Vl-portlist-msb-bit-pattern
          • Vl-plainarg-lsb-bits
          • Vl-port-msb-bits
        • 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
  • Testing-utilities
  • Math

• Modinsts-to-eoccs

Vl-modinst-to-eocc

Main function for transforming a Verilog module instance into an (preliminary) E language occurrence.

Signature

(vl-modinst-to-eocc x walist mods modalist eal warnings) 
  → 
(mv successp warnings eocc)

Arguments

x — The module instance that we want to convert into an E occurrence.
    Guard (vl-modinst-p x).

walist — The wire alist for the superior module. We use it to build the wire lists for the actuals.
    Guard (vl-wirealist-p walist).

mods — The list of all modules. Needed so we can look up the submodule being instantiated, so we can compute its port pattern.
    Guard (vl-modulelist-p mods).

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

eal — The already-processed vl-ealist-p that binds module names to the E modules we've built for them so far. We use this to look up the definiton of the submodule for the :op field of the E occurrence.
    Guard (vl-ealist-p eal).

warnings — Warnings accumulator for the superior module.
    Guard (vl-warninglist-p warnings).

Returns

successp — Type (booleanp successp).

warnings — Type (vl-warninglist-p warnings).

We do a lot of sanity checking to make sure the module instance is simple enough to transform, that the submodule exists and was translated into an E module successfully, etc. Then, we figure out the bindings to use for the :i and :o fields of the occurrence, as described in modinsts-to-eoccs.

Definitions and Theorems

Function: vl-modinst-to-eocc

(defun
 vl-modinst-to-eocc
 (x walist mods modalist eal warnings)
 (declare (xargs :guard (and (vl-modinst-p x)
                             (vl-wirealist-p walist)
                             (vl-modulelist-p mods)
                             (vl-ealist-p eal)
                             (vl-warninglist-p warnings)
                             (equal modalist (vl-modalist mods)))))
 (let
  ((__function__ 'vl-modinst-to-eocc))
  (declare (ignorable __function__))
  (b*
   (((vl-modinst x) x)
    ((unless x.instname)
     (mv
      nil
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: expected all module instances to be named.  Did ~
                         you run the addinstnames transform?"
       :args (list x))
      nil))
    ((when x.range)
     (mv
      nil
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: expected only simple module instances, but ~s1 ~
                         is an array of module instances.  Did you run the ~
                         replicate transform?"
       :args (list x x.instname))
      nil))
    ((unless (vl-paramargs-empty-p x.paramargs))
     (mv
      nil
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: expected only simple module instances, but ~s1 ~
                         still has parameters.  Did you run the ~
                         unparameterization transform?"
       :args (list x x.instname))
      nil))
    ((when (eq (vl-arguments-kind x.portargs)
               :vl-arguments-named))
     (mv
      nil
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: expected only resolved module instances, but ~
                         ~s1 still has named arguments.  Did you run the ~
                         argresolve transform?"
       :args (list x x.instname))
      nil))
    (sub (vl-fast-find-module x.modname mods modalist))
    ((unless sub)
     (mv nil
         (fatal :type :vl-bad-instance
                :msg "~a0 refers to undefined module ~m1."
                :args (list x x.modname))
         nil))
    (sub-esim (cdr (hons-get x.modname eal)))
    ((unless sub-esim)
     (mv
      nil
      (fatal
       :type :vl-bad-submodule
       :msg
       "~a0 refers to module ~m1, but we failed to build an ~
                         E module for ~m1."
       :args (list x x.modname))
      nil))
    ((mv okp & sub-walist)
     (vl-module-wirealist sub nil))
    ((unless okp)
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: failed to build a wire alist for ~x0?  Jared ~
                         thinks this should never happen since we were able ~
                         to build the ESIM module for it."
       :args (list x.modname))
      nil))
    ((mv successp & portpat)
     (vl-portlist-msb-bit-pattern (vl-module->ports sub)
                                  sub-walist))
    ((unless successp)
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: failed to build a portlist pattern for module ~
                         ~m1. Jared thinks this should never happen because ~
                         we check that these lists can be built before trying ~
                         to make E occurrences from module instances."
       :args (list x x.modname))
      nil))
    (actuals (vl-arguments-plain->args x.portargs))
    ((unless (same-lengthp actuals portpat))
     (mv
      nil
      (fatal
          :type :vl-bad-instance
          :msg
          "~a0: wrong arity.  Expected ~x1 arguments but found ~x2."
          :args (list x (len portpat) (len actuals)))
      nil))
    ((mv successp warnings binding-alist)
     (vl-modinst-eocc-bindings actuals portpat walist warnings x))
    ((unless successp)
     (mv nil warnings nil))
    ((mv successp & in-pat out-pat)
     (vl-portdecls-to-i/o (vl-module->portdecls sub)
                          sub-walist))
    ((unless successp)
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: failed to build :i and :o patterns for module ~
                         ~m1.  Jared thinks this should never happen because ~
                         we already built its esim and should have checked ~
                         that this was all okay due to port-bit-checking."
       :args (list x x.modname))
      nil))
    ((unless (and (equal in-pat (gpl :i sub-esim))
                  (equal out-pat (gpl :o sub-esim))))
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: the :i and :o patterns we built for ~m1 do ~
                         not agree with the :i and :o patterns of its ESIM? ~
                         Jared thinks this should never happen because the ~
                         patterns should be being built in the same way. ~%  ~
                          - in-pat: ~x2~%  ~
                          - found:  ~x3~%  ~
                          - out-pat: ~x4~%  ~
                          - found:   ~x5~%"
       :args (list x x.modname in-pat (gpl :i sub-esim)
                   out-pat (gpl :o sub-esim)))
      nil))
    ((with-fast binding-alist))
    (all-formal-bits (pat-flatten out-pat (pat-flatten1 in-pat)))
    (all-actual-bits (alist-keys binding-alist))
    ((unless (equal (mergesort all-formal-bits)
                    (mergesort all-actual-bits)))
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: the binding alist we produced doesn't contain ~
                         bindings for exactly the right bits.  Jared thinks ~
                         vl-modinst-to-eocc-bindings should ensure that this ~
                         never happens."
       :args (list x))
      nil))
    (inputs (al->pat in-pat binding-alist nil))
    (outputs (al->pat out-pat binding-alist nil))
    (instname (vl-plain-wire-name x.instname))
    (eocc (list* :u instname
                 :op sub-esim :o outputs :i inputs
                 (if x.atts (list :a x.atts) nil))))
   (mv t (ok) eocc))))

Theorem: booleanp-of-vl-modinst-to-eocc.successp

(defthm
    booleanp-of-vl-modinst-to-eocc.successp
    (b* (((mv ?successp ?warnings ?eocc)
          (vl-modinst-to-eocc x walist mods modalist eal warnings)))
        (booleanp successp))
    :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-modinst-to-eocc.warnings

(defthm
    vl-warninglist-p-of-vl-modinst-to-eocc.warnings
    (b* (((mv ?successp ?warnings ?eocc)
          (vl-modinst-to-eocc x walist mods modalist eal warnings)))
        (vl-warninglist-p warnings))
    :rule-classes :rewrite)

Theorem: good-esim-occp-of-vl-modinst-to-eocc

(defthm
 good-esim-occp-of-vl-modinst-to-eocc
 (let
    ((ret (vl-modinst-to-eocc x walist mods modalist eal warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-modinst-p x))
                  (force (vl-wirealist-p walist))
                  (force (vl-modulelist-p mods))
                  (force (equal modalist (vl-modalist mods)))
                  (force (vl-ealist-p eal)))
             (good-esim-occp (mv-nth 2 ret)))))