		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-design-elaborate

Signature
(vl-design-elaborate x config) → new-x
Arguments: x — Guard (vl-design-p x).; config — Guard (vl-simpconfig-p config).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-design-elaborate

(defun vl-design-elaborate (x config)
 (declare (xargs :guard (and (vl-design-p x)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-design-elaborate))
   (declare (ignorable __function__))
   (b*
    (((vl-design x) (vl-design-fix x))
     ((local-stobjs elabindex)
      (mv new-x elabindex))
     (elabindex (vl-elabindex-init x))
     (warnings x.warnings)
     (elablimit (vl-simpconfig->elab-limit config))
     ((wmv ?ok1 warnings x elabindex)
      (vl-design-elaborate-aux x elabindex
                               :reclimit elablimit))
     ((mv ?ok warnings elabindex new-packages)
      (vl-packagelist-elaborate x.packages elabindex warnings))
     (topmods (vl-design-toplevel x))
     (top-names
          (append (vl-programlist->names (vl-design->programs x))
                  (vl-udplist->names (vl-design->udps x))))
     (ledger
          (make-vl-unparam-ledger
               :ndb (vl-starting-namedb top-names)
               :omit-default-params
               (vl-simpconfig->name-without-default-params config)))
     ((mv top-sigs warnings elabindex ledger)
      (vl-toplevel-signatures topmods warnings elabindex ledger))
     ((wmv warnings new-mods new-ifaces
           new-classes donelist elabindex ledger)
      (vl-unparameterize-main-list
           top-sigs nil 1000 elabindex ledger))
     (new-x1 (change-vl-design x
                               :mods new-mods
                               :interfaces new-ifaces
                               :classes new-classes
                               :packages new-packages))
     (elabindex (vl-elabindex-init new-x1))
     ((mv final-mods elabindex)
      (vl-finish-unparameterized-modules new-mods elabindex))
     ((mv final-ifaces elabindex)
      (vl-finish-unparameterized-interfaces new-ifaces elabindex))
     ((mv final-classes elabindex)
      (vl-finish-unparameterized-classes new-classes elabindex))
     (new-x (change-vl-design x
                              :mods final-mods
                              :interfaces final-ifaces
                              :classes final-classes))
     ((wmv ?ok1 warnings new-x elabindex)
      (vl-design-elaborate-aux new-x elabindex
                               :reclimit elablimit))
     ((mv ?ok warnings elabindex new-packages)
      (vl-packagelist-elaborate (vl-design->packages new-x)
                                elabindex warnings))
     (final-x (change-vl-design new-x
                                :packages new-packages
                                :warnings warnings)))
    (fast-alist-free donelist)
    (vl-free-namedb (vl-unparam-ledger->ndb ledger))
    (fast-alist-free (vl-unparam-ledger->instkeymap ledger))
    (vl-scopestacks-free)
    (mv (vl-recover-modules-lost-from-elaboration :pre x
                                                  :post final-x)
        elabindex))))

Theorem: vl-design-p-of-vl-design-elaborate

(defthm vl-design-p-of-vl-design-elaborate
  (b* ((new-x (vl-design-elaborate x config)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-design-elaborate-of-vl-design-fix-x

(defthm vl-design-elaborate-of-vl-design-fix-x
  (equal (vl-design-elaborate (vl-design-fix x)
                              config)
         (vl-design-elaborate x config)))

Theorem: vl-design-elaborate-vl-design-equiv-congruence-on-x

(defthm vl-design-elaborate-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design-elaborate x config)
                  (vl-design-elaborate x-equiv config)))
  :rule-classes :congruence)

Theorem: vl-design-elaborate-of-vl-simpconfig-fix-config

(defthm vl-design-elaborate-of-vl-simpconfig-fix-config
  (equal (vl-design-elaborate x (vl-simpconfig-fix config))
         (vl-design-elaborate x config)))

Theorem: vl-design-elaborate-vl-simpconfig-equiv-congruence-on-config

(defthm vl-design-elaborate-vl-simpconfig-equiv-congruence-on-config
  (implies (vl-simpconfig-equiv config config-equiv)
           (equal (vl-design-elaborate x config)
                  (vl-design-elaborate x config-equiv)))
  :rule-classes :congruence)