		Search-engine friendly clone of the ACL2 documentation.

Vl-ppc-module

Vl-make-item-map-for-ppc-module

Build a commentmap that has the encoded items for a module.

Signature
(vl-make-item-map-for-ppc-module x ss &key (ps 'ps)) → (mv map ps)
Arguments: x — Guard (vl-module-p x).; ss — Should already be extended with x.
Guard (vl-scopestack-p ss).
Returns: map — Type (vl-commentmap-p map).

Definitions and Theorems

Function: vl-make-item-map-for-ppc-module-fn

(defun vl-make-item-map-for-ppc-module-fn (x ss ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (vl-module-p x)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-make-item-map-for-ppc-module))
    (declare (ignorable __function__))
    (b* (((vl-module x) x)
         (rchars (vl-ps->rchars))
         (col (vl-ps->col))
         (misc (vl-ps->misc))
         (ps (vl-pp-set-portnames x.portdecls))
         (imap nil)
         ((mv imap ps)
          (vl-paramdecllist-ppmap x.paramdecls imap))
         ((mv imap ps)
          (vl-portdecllist-ppmap x.portdecls imap))
         ((mv imap ps)
          (vl-vardecllist-ppmap x.vardecls imap))
         ((mv imap ps)
          (vl-fundecllist-ppmap x.fundecls imap))
         ((mv imap ps)
          (vl-taskdecllist-ppmap x.taskdecls imap))
         ((mv imap ps)
          (vl-assignlist-ppmap x.assigns imap))
         ((mv imap ps)
          (vl-modinstlist-ppmap x.modinsts ss imap))
         ((mv imap ps)
          (vl-gateinstlist-ppmap x.gateinsts imap))
         ((mv imap ps)
          (vl-alwayslist-ppmap x.alwayses imap))
         ((mv imap ps)
          (vl-initiallist-ppmap x.initials imap))
         (imap (rev imap))
         (ps (vl-ps-update-rchars rchars))
         (ps (vl-ps-update-col col))
         (ps (vl-ps-update-misc misc)))
      (mv imap ps))))

Theorem: vl-commentmap-p-of-vl-make-item-map-for-ppc-module.map

(defthm vl-commentmap-p-of-vl-make-item-map-for-ppc-module.map
  (b* (((mv ?map ?ps)
        (vl-make-item-map-for-ppc-module-fn x ss ps)))
    (vl-commentmap-p map))
  :rule-classes :rewrite)

Theorem: vl-make-item-map-for-ppc-module-fn-of-vl-module-fix-x

(defthm vl-make-item-map-for-ppc-module-fn-of-vl-module-fix-x
  (equal (vl-make-item-map-for-ppc-module-fn (vl-module-fix x)
                                             ss ps)
         (vl-make-item-map-for-ppc-module-fn x ss ps)))

Theorem: vl-make-item-map-for-ppc-module-fn-vl-module-equiv-congruence-on-x

(defthm
 vl-make-item-map-for-ppc-module-fn-vl-module-equiv-congruence-on-x
 (implies
      (vl-module-equiv x x-equiv)
      (equal (vl-make-item-map-for-ppc-module-fn x ss ps)
             (vl-make-item-map-for-ppc-module-fn x-equiv ss ps)))
 :rule-classes :congruence)

Theorem: vl-make-item-map-for-ppc-module-fn-of-vl-scopestack-fix-ss

(defthm vl-make-item-map-for-ppc-module-fn-of-vl-scopestack-fix-ss
 (equal (vl-make-item-map-for-ppc-module-fn x (vl-scopestack-fix ss)
                                            ps)
        (vl-make-item-map-for-ppc-module-fn x ss ps)))

Theorem: vl-make-item-map-for-ppc-module-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-make-item-map-for-ppc-module-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-make-item-map-for-ppc-module-fn x ss ps)
             (vl-make-item-map-for-ppc-module-fn x ss-equiv ps)))
 :rule-classes :congruence)

Subtopics

Vl-modinstlist-ppmap
Vl-vardecllist-ppmap
Vl-taskdecllist-ppmap
Vl-portdecllist-ppmap
Vl-paramdecllist-ppmap
Vl-modportlist-ppmap
Vl-initiallist-ppmap
Vl-gateinstlist-ppmap
Vl-fundecllist-ppmap
Vl-assignlist-ppmap
Vl-alwayslist-ppmap