• Top

• Sv::vl-moddb.lisp

Vl-interfaceports->svex

Signature

(vl-interfaceports->svex x ss self-lsb context-mod) 
  → 
(mv warnings wires insts aliases modalist width)

Arguments

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

ss — Guard (vl-scopestack-p ss).

self-lsb — Guard (maybe-natp self-lsb).

context-mod — Guard (sv::modname-p context-mod).

Returns

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

wires — Type (sv::wirelist-p wires).

insts — Type (sv::modinstlist-p insts).

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

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

width — Type (natp width).

Definitions and Theorems

Function: vl-interfaceports->svex

(defun vl-interfaceports->svex (x ss self-lsb context-mod)
 (declare (xargs :guard (and (vl-interfaceportlist-p x)
                             (vl-scopestack-p ss)
                             (maybe-natp self-lsb)
                             (sv::modname-p context-mod))))
 (let ((__function__ 'vl-interfaceports->svex))
   (declare (ignorable __function__))
   (b*
     (((when (atom x))
       (mv nil nil nil nil nil 0))
      (warnings nil)
      (self-lsb (maybe-natp-fix self-lsb))
      ((wmv warnings
            wires2 insts2 aliases2 modalist2 width2)
       (vl-interfaceports->svex (cdr x)
                                ss self-lsb context-mod))
      ((wmv warnings
            wires1 insts1 aliases1 modalist1 width1)
       (vl-interfaceport->svex (car x)
                               ss (and self-lsb (+ width2 self-lsb))
                               context-mod)))
     (mv warnings
         (append-without-guard wires1 wires2)
         (append-without-guard insts1 insts2)
         (append-without-guard aliases1 aliases2)
         (append-without-guard modalist1 modalist2)
         (+ width1 width2)))))

Theorem: vl-warninglist-p-of-vl-interfaceports->svex.warnings

(defthm vl-warninglist-p-of-vl-interfaceports->svex.warnings
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: wirelist-p-of-vl-interfaceports->svex.wires

(defthm wirelist-p-of-vl-interfaceports->svex.wires
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (sv::wirelist-p wires))
  :rule-classes :rewrite)

Theorem: modinstlist-p-of-vl-interfaceports->svex.insts

(defthm modinstlist-p-of-vl-interfaceports->svex.insts
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (sv::modinstlist-p insts))
  :rule-classes :rewrite)

Theorem: lhspairs-p-of-vl-interfaceports->svex.aliases

(defthm lhspairs-p-of-vl-interfaceports->svex.aliases
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (sv::lhspairs-p aliases))
  :rule-classes :rewrite)

Theorem: modalist-p-of-vl-interfaceports->svex.modalist

(defthm modalist-p-of-vl-interfaceports->svex.modalist
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (sv::modalist-p modalist))
  :rule-classes :rewrite)

Theorem: natp-of-vl-interfaceports->svex.width

(defthm natp-of-vl-interfaceports->svex.width
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (natp width))
  :rule-classes :type-prescription)

Theorem: vars-of-vl-interfaceports->svex

(defthm vars-of-vl-interfaceports->svex
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceports->svex x ss self-lsb context-mod)))
    (and (sv::svarlist-addr-p (sv::lhspairs-vars aliases))
         (sv::svarlist-addr-p (sv::modalist-vars modalist)))))

Theorem: vl-interfaceports->svex-of-vl-interfaceportlist-fix-x

(defthm vl-interfaceports->svex-of-vl-interfaceportlist-fix-x
  (equal (vl-interfaceports->svex (vl-interfaceportlist-fix x)
                                  ss self-lsb context-mod)
         (vl-interfaceports->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceports->svex-vl-interfaceportlist-equiv-congruence-on-x

(defthm
 vl-interfaceports->svex-vl-interfaceportlist-equiv-congruence-on-x
 (implies
  (vl-interfaceportlist-equiv x x-equiv)
  (equal (vl-interfaceports->svex x ss self-lsb context-mod)
         (vl-interfaceports->svex x-equiv ss self-lsb context-mod)))
 :rule-classes :congruence)

Theorem: vl-interfaceports->svex-of-vl-scopestack-fix-ss

(defthm vl-interfaceports->svex-of-vl-scopestack-fix-ss
  (equal (vl-interfaceports->svex x (vl-scopestack-fix ss)
                                  self-lsb context-mod)
         (vl-interfaceports->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceports->svex-vl-scopestack-equiv-congruence-on-ss

(defthm vl-interfaceports->svex-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-interfaceports->svex x ss self-lsb context-mod)
         (vl-interfaceports->svex x ss-equiv self-lsb context-mod)))
 :rule-classes :congruence)

Theorem: vl-interfaceports->svex-of-maybe-natp-fix-self-lsb

(defthm vl-interfaceports->svex-of-maybe-natp-fix-self-lsb
  (equal (vl-interfaceports->svex x ss (maybe-natp-fix self-lsb)
                                  context-mod)
         (vl-interfaceports->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceports->svex-maybe-nat-equiv-congruence-on-self-lsb

(defthm
     vl-interfaceports->svex-maybe-nat-equiv-congruence-on-self-lsb
 (implies
  (acl2::maybe-nat-equiv self-lsb self-lsb-equiv)
  (equal (vl-interfaceports->svex x ss self-lsb context-mod)
         (vl-interfaceports->svex x ss self-lsb-equiv context-mod)))
 :rule-classes :congruence)

Theorem: vl-interfaceports->svex-of-modname-fix-context-mod

(defthm vl-interfaceports->svex-of-modname-fix-context-mod
 (equal
    (vl-interfaceports->svex x ss
                             self-lsb (sv::modname-fix context-mod))
    (vl-interfaceports->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceports->svex-modname-equiv-congruence-on-context-mod

(defthm
    vl-interfaceports->svex-modname-equiv-congruence-on-context-mod
 (implies
  (sv::modname-equiv context-mod context-mod-equiv)
  (equal (vl-interfaceports->svex x ss self-lsb context-mod)
         (vl-interfaceports->svex x ss self-lsb context-mod-equiv)))
 :rule-classes :congruence)