		Search-engine friendly clone of the ACL2 documentation.

Inline-mods

Vl-make-inlining-assigns

Make assignments that hook up the superior module to the new, mangled wires that have been derived from the module's ports.

Signature
(vl-make-inlining-assigns ports plainargs scope loc warnings) → (mv successp warnings assigns)
Arguments: ports — Guard (vl-portlist-p ports).; plainargs — Guard (and (vl-plainarglist-p plainargs) (same-lengthp ports plainargs)).; scope — Guard (vl-scope-p scope).; loc — Guard (vl-location-p loc).; warnings — Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; assigns — Type (vl-assignlist-p assigns), given the guard.

Definitions and Theorems

Function: vl-make-inlining-assigns

(defun vl-make-inlining-assigns (ports plainargs scope loc warnings)
 (declare (xargs :guard (and (vl-portlist-p ports)
                             (vl-scope-p scope)
                             (vl-location-p loc)
                             (vl-warninglist-p warnings)
                             (and (vl-plainarglist-p plainargs)
                                  (same-lengthp ports plainargs)))))
 (let ((__function__ 'vl-make-inlining-assigns))
  (declare (ignorable __function__))
  (b*
   (((when (atom ports)) (mv t (ok) nil))
    (port1 (vl-port-fix (car ports)))
    ((when (eq (tag port1) :vl-interfaceport))
     (mv
      nil
      (warn
           :type :vl-inline-fail
           :msg "Interface ports aren't supported for inlining. ~a0"
           :args (list port1))
      nil))
    (inside (vl-regularport->expr port1))
    (outside (vl-plainarg->expr (car plainargs)))
    ((mv warnings dir)
     (vl-port-direction port1 scope nil))
    ((unless dir) (mv nil warnings nil))
    ((when (eq dir :vl-inout))
     (mv nil
         (warn :type :vl-inline-fail
               :msg "Inout ports aren't supported for inlining. ~a0"
               :args (list port1))
         nil))
    (assigns1 (cond ((or (not inside) (not outside)) nil)
                    ((eq dir :vl-input)
                     (list (make-vl-assign :lvalue inside
                                           :expr outside
                                           :loc loc)))
                    (t (list (make-vl-assign :lvalue outside
                                             :expr inside
                                             :loc loc)))))
    ((mv okp warnings assigns2)
     (vl-make-inlining-assigns (cdr ports)
                               (cdr plainargs)
                               scope loc warnings)))
   (mv okp
       warnings (append assigns1 assigns2)))))

Theorem: booleanp-of-vl-make-inlining-assigns.successp

(defthm booleanp-of-vl-make-inlining-assigns.successp
  (b*
   (((mv ?successp ?warnings ?assigns)
     (vl-make-inlining-assigns ports plainargs scope loc warnings)))
   (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-make-inlining-assigns.warnings

(defthm vl-warninglist-p-of-vl-make-inlining-assigns.warnings
  (b*
   (((mv ?successp ?warnings ?assigns)
     (vl-make-inlining-assigns ports plainargs scope loc warnings)))
   (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-assignlist-p-of-vl-make-inlining-assigns.assigns

(defthm vl-assignlist-p-of-vl-make-inlining-assigns.assigns
 (implies
  (and (force (vl-portlist-p ports))
       (force (vl-scope-p scope))
       (force (vl-location-p loc))
       (force (vl-warninglist-p warnings))
       (force (vl-plainarglist-p plainargs))
       (force (same-lengthp ports plainargs)))
  (b*
   (((mv ?successp ?warnings ?assigns)
     (vl-make-inlining-assigns ports plainargs scope loc warnings)))
   (vl-assignlist-p assigns)))
 :rule-classes :rewrite)

Theorem: vl-make-inlining-assigns-mvtypes-2

(defthm vl-make-inlining-assigns-mvtypes-2
 (true-listp
  (mv-nth
     2
     (vl-make-inlining-assigns ports plainargs scope loc warnings)))
 :rule-classes :type-prescription)