• Top

• Sv::vl-moddb.lisp

Vl-portinfo-to-svex-assign-or-alias

Signature

(vl-portinfo-to-svex-assign-or-alias x instname range) 
  → 
(mv warnings assigns aliases)

Arguments

x — Guard (vl-portinfo-p x).

instname — Guard (stringp instname).

range — Guard (vl-maybe-range-p range).

Returns

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

assigns — Type (sv::assigns-p assigns).

aliases — Type (sv::lhspairs-p aliases).

Definitions and Theorems

Function: vl-portinfo-to-svex-assign-or-alias

(defun vl-portinfo-to-svex-assign-or-alias (x instname range)
 (declare (xargs :guard (and (vl-portinfo-p x)
                             (stringp instname)
                             (vl-maybe-range-p range))))
 (declare
      (xargs :guard (and (sv::svarlist-addr-p (vl-portinfo-vars x))
                         (vl-maybe-range-resolved-p range))))
 (let ((__function__ 'vl-portinfo-to-svex-assign-or-alias))
  (declare (ignorable __function__))
  (b* ((instname (string-fix instname))
       (range (vl-maybe-range-fix range))
       (warnings nil))
   (vl-portinfo-case
    x :bad (mv (ok) nil nil)
    :regular
    (b*
     (((when (and (not x.conn-expr)
                  (not x.port-lhs)))
       (mv (ok) nil nil))
      (xwidth (if (and range (not x.replicatedp))
                  (* x.port-size (vl-range-size range))
                x.port-size))
      (lhsp (sv::lhssvex-bounded-p xwidth x.conn-svex))
      ((when (and (not lhsp) x.interfacep))
       (mv
        (fatal :type :vl-interfaceport-bad-connection
               :msg "Non-LHS connection on interfaceport: .~s0(~a1)"
               :args (list x.portname x.conn-expr))
        nil nil))
      (warnings
          (if (and (not lhsp)
                   (eq x.port-dir :vl-output))
              (warn :type :vl-port-direction-mismatch
                    :msg "Non-LHS expression ~a1 on output port ~s0"
                    :args (list x.portname x.conn-expr))
            (ok)))
      ((when (not x.port-lhs))
       (mv (ok)
           (and lhsp
                (list (cons (sv::svex->lhs-bound xwidth x.conn-svex)
                            (sv::make-driver :value (sv::svex-z)))))
           nil))
      ((unless (equal x.port-size (sv::lhs-width x.port-lhs)))
       (mv
        (fatal
         :type :vl-port-resolution-programming-error
         :msg
         "On port ~s0: Port size ~a1 didn't match port expression width ~a2"
         :args (list x.portname
                     x.port-size (sv::lhs-width x.port-lhs)))
        nil nil))
      (alias? (and lhsp x.conn-expr))
      (conn (if alias? (sv::svex->lhs-bound xwidth x.conn-svex)
              (sv::make-driver :value x.conn-svex))))
     (if range
      (b* ((size (vl-range-size range))
           (lsb (vl-resolved->val (vl-range->lsb range)))
           (incr (if (vl-range-revp range) -1 1)))
       (if x.replicatedp
        (if alias? (mv (ok)
                       nil
                       (vl-instarray-replicated-port-aliases
                            x.port-lhs instname conn lsb size incr))
          (mv (ok)
              (vl-instarray-replicated-port-assigns
                   x.port-lhs instname conn lsb size incr)
              nil))
        (b* ((port-lhs (vl-instarray-nonreplicated-port-lhs
                            x.port-lhs instname lsb size incr)))
          (if alias? (mv (ok)
                         nil (list (cons conn port-lhs)))
            (mv (ok)
                (list (cons port-lhs conn))
                nil)))))
      (b* ((port-lhs (sv::lhs-add-namespace instname x.port-lhs)))
        (if alias? (mv (ok)
                       nil (list (cons port-lhs conn)))
          (mv (ok)
              (list (cons port-lhs conn))
              nil)))))))))

Theorem: vl-warninglist-p-of-vl-portinfo-to-svex-assign-or-alias.warnings

(defthm
   vl-warninglist-p-of-vl-portinfo-to-svex-assign-or-alias.warnings
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfo-to-svex-assign-or-alias x instname range)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: assigns-p-of-vl-portinfo-to-svex-assign-or-alias.assigns

(defthm assigns-p-of-vl-portinfo-to-svex-assign-or-alias.assigns
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfo-to-svex-assign-or-alias x instname range)))
    (sv::assigns-p assigns))
  :rule-classes :rewrite)

Theorem: lhspairs-p-of-vl-portinfo-to-svex-assign-or-alias.aliases

(defthm lhspairs-p-of-vl-portinfo-to-svex-assign-or-alias.aliases
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfo-to-svex-assign-or-alias x instname range)))
    (sv::lhspairs-p aliases))
  :rule-classes :rewrite)

Theorem: var-of-vl-portinfo-to-svex-assign-or-alias

(defthm var-of-vl-portinfo-to-svex-assign-or-alias
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfo-to-svex-assign-or-alias x instname range)))
    (implies
         (sv::svarlist-addr-p (vl-portinfo-vars x))
         (and (sv::svarlist-addr-p (sv::assigns-vars assigns))
              (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))))

Theorem: vl-portinfo-to-svex-assign-or-alias-mvtypes-1

(defthm vl-portinfo-to-svex-assign-or-alias-mvtypes-1
 (true-listp
    (mv-nth 1
            (vl-portinfo-to-svex-assign-or-alias x instname range)))
 :rule-classes :type-prescription)

Theorem: vl-portinfo-to-svex-assign-or-alias-mvtypes-2

(defthm vl-portinfo-to-svex-assign-or-alias-mvtypes-2
 (true-listp
    (mv-nth 2
            (vl-portinfo-to-svex-assign-or-alias x instname range)))
 :rule-classes :type-prescription)

Theorem: vl-portinfo-to-svex-assign-or-alias-of-vl-portinfo-fix-x

(defthm vl-portinfo-to-svex-assign-or-alias-of-vl-portinfo-fix-x
  (equal (vl-portinfo-to-svex-assign-or-alias (vl-portinfo-fix x)
                                              instname range)
         (vl-portinfo-to-svex-assign-or-alias x instname range)))

Theorem: vl-portinfo-to-svex-assign-or-alias-vl-portinfo-equiv-congruence-on-x

(defthm
 vl-portinfo-to-svex-assign-or-alias-vl-portinfo-equiv-congruence-on-x
 (implies
  (vl-portinfo-equiv x x-equiv)
  (equal
      (vl-portinfo-to-svex-assign-or-alias x instname range)
      (vl-portinfo-to-svex-assign-or-alias x-equiv instname range)))
 :rule-classes :congruence)

Theorem: vl-portinfo-to-svex-assign-or-alias-of-str-fix-instname

(defthm vl-portinfo-to-svex-assign-or-alias-of-str-fix-instname
  (equal (vl-portinfo-to-svex-assign-or-alias x (str-fix instname)
                                              range)
         (vl-portinfo-to-svex-assign-or-alias x instname range)))

Theorem: vl-portinfo-to-svex-assign-or-alias-streqv-congruence-on-instname

(defthm
  vl-portinfo-to-svex-assign-or-alias-streqv-congruence-on-instname
 (implies
  (streqv instname instname-equiv)
  (equal
      (vl-portinfo-to-svex-assign-or-alias x instname range)
      (vl-portinfo-to-svex-assign-or-alias x instname-equiv range)))
 :rule-classes :congruence)

Theorem: vl-portinfo-to-svex-assign-or-alias-of-vl-maybe-range-fix-range

(defthm
    vl-portinfo-to-svex-assign-or-alias-of-vl-maybe-range-fix-range
  (equal (vl-portinfo-to-svex-assign-or-alias
              x instname (vl-maybe-range-fix range))
         (vl-portinfo-to-svex-assign-or-alias x instname range)))

Theorem: vl-portinfo-to-svex-assign-or-alias-vl-maybe-range-equiv-congruence-on-range

(defthm
 vl-portinfo-to-svex-assign-or-alias-vl-maybe-range-equiv-congruence-on-range
 (implies
  (vl-maybe-range-equiv range range-equiv)
  (equal
      (vl-portinfo-to-svex-assign-or-alias x instname range)
      (vl-portinfo-to-svex-assign-or-alias x instname range-equiv)))
 :rule-classes :congruence)