• 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-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
  • Math
  • Testing-utilities

• Modinsts-to-eoccs

Vl-modinst-eocc-bindings

Build a (slow) alist binding the "formals" for a module to the "actuals" from an instance.

Signature

(vl-modinst-eocc-bindings actuals portpat walist warnings inst) 
  → 
(mv successp warnings binding-alist)

Arguments

actuals — Arguments in the module instance.
    Guard (vl-plainarglist-p actuals).

portpat — Port pattern for the module being instanced; see modinsts-to-eoccs. We assume (in the guard) that it is the same length as the actuals (i.e., the module instance has the proper arity), but we still have to check the lengths on the sub-lists.
    Guard (vl-emodwirelistlist-p portpat).

walist — Wire alist for the superior module. Used to generate the E wires for the actuals.
    Guard (vl-wirealist-p walist).

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

inst — Context for warnings, semantically irrelevant.
    Guard (vl-modinst-p inst).

Returns

successp — Type (booleanp successp).

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

binding-alist — Type (and (alistp binding-alist) (vl-emodwirelist-p (alist-keys binding-alist)) (vl-emodwirelist-p (alist-vals binding-alist))) .

Definitions and Theorems

Function: vl-modinst-eocc-bindings

(defun vl-modinst-eocc-bindings
       (actuals portpat walist warnings inst)
 (declare (xargs :guard (and (vl-plainarglist-p actuals)
                             (vl-emodwirelistlist-p portpat)
                             (vl-wirealist-p walist)
                             (vl-warninglist-p warnings)
                             (vl-modinst-p inst))))
 (declare (xargs :guard (and (true-list-listp portpat)
                             (same-lengthp actuals portpat))))
 (let ((__function__ 'vl-modinst-eocc-bindings))
  (declare (ignorable __function__))
  (b*
   (((when (atom actuals)) (mv t (ok) nil))
    ((vl-modinst inst) inst)
    (expr1 (vl-plainarg->expr (car actuals)))
    ((unless expr1)
     (mv nil
         (fatal :type :vl-programming-error
                :msg "~a0: expected all arguments to be non-blank."
                :args (list inst))
         nil))
    ((mv successp warnings expr1-msb-bits)
     (vl-msb-expr-bitlist expr1 walist warnings))
    ((unless successp)
     (mv nil
         (fatal :type :vl-bad-instance
                :msg "~a0: error generating wires for ~a1."
                :args (list inst.loc expr1))
         nil))
    (formal1-msb-bits (car portpat))
    ((unless (and (same-lengthp expr1-msb-bits formal1-msb-bits)
                  (mbt (vl-emodwirelist-p formal1-msb-bits))))
     (b* ((nactuals (length expr1-msb-bits))
          (nformals (length formal1-msb-bits)))
      (mv
       nil
       (fatal
        :type :vl-bad-instance
        :msg
        "~a0: we produced ~x1 wire~s2 for an argument whose ~
                           corresponding port has ~x3 wire~s4.  ~
                            - Argument wires: ~x5;  ~
                            - Port wires: ~x6."
        :args (list inst nactuals (if (= nactuals 1) "" "s")
                    nformals (if (= nformals 1) "" "s")
                    (symbol-list-names expr1-msb-bits)
                    (symbol-list-names formal1-msb-bits)))
       nil)))
    ((mv successp warnings binding-alist)
     (vl-modinst-eocc-bindings (cdr actuals)
                               (cdr portpat)
                               walist warnings inst))
    (binding-alist
         (append (pairlis$ formal1-msb-bits expr1-msb-bits)
                 binding-alist)))
   (mv successp warnings binding-alist))))

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

(defthm booleanp-of-vl-modinst-eocc-bindings.successp
  (b* (((mv ?successp ?warnings ?binding-alist)
        (vl-modinst-eocc-bindings
             actuals portpat walist warnings inst)))
    (booleanp successp))
  :rule-classes :type-prescription)

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

(defthm vl-warninglist-p-of-vl-modinst-eocc-bindings.warnings
  (b* (((mv ?successp ?warnings ?binding-alist)
        (vl-modinst-eocc-bindings
             actuals portpat walist warnings inst)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-modinst-eocc-bindings.binding-alist

(defthm return-type-of-vl-modinst-eocc-bindings.binding-alist
  (b* (((mv ?successp ?warnings ?binding-alist)
        (vl-modinst-eocc-bindings
             actuals portpat walist warnings inst)))
    (and (alistp binding-alist)
         (vl-emodwirelist-p (alist-keys binding-alist))
         (vl-emodwirelist-p (alist-vals binding-alist))))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-modinst-eocc-bindings.binding-alist

(defthm true-listp-of-vl-modinst-eocc-bindings.binding-alist
  (b* (((mv ?successp ?warnings ?binding-alist)
        (vl-modinst-eocc-bindings
             actuals portpat walist warnings inst)))
    (true-listp binding-alist))
  :rule-classes :type-prescription)