• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
            • Shadowcheck
            • Implicit-wires-minutia
            • Implicit-wires-generate-scoping
            • Vl-genbase-make-implicit-wires
            • Vl-expr-names-for-implicit
            • Vl-make-implicit-wires-main
            • Vl-implicitst
            • Vl-make-port-implicit-wires
            • Vl-import-update-implicit
            • Vl-blockitemlist-update-implicit
            • Vl-blockitem-update-implicit
            • Vl-make-ordinary-implicit-wires
            • Vl-remove-declared-wires
            • Vl-implicitsts-restore-fast-alists
            • Vl-genblock-under-cond-make-implicit-wires
            • Vl-collect-exprs-for-implicit-wires-from-namedargs
            • Vl-genblock-make-implicit-wires
            • Vl-collect-exprs-for-implicit-wires-from-portargs
            • Vl-collect-exprs-for-implicit-wires-from-namedarg
            • Vl-gateinst-exprs-for-implicit-wires
            • Vl-modinst-exprs-for-implicit-wires
            • Vl-genelementlist-make-implicit-wires
            • Vl-packagemap-find-name
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Make-implicit-wires

Vl-implicitsts-restore-fast-alists

Assuming new-st is a modified version of st, restores any changed fast alists in st and frees them in new-st. Side effects only.

Signature

(vl-implicitsts-restore-fast-alists st new-st) → *

Arguments

st — Guard (vl-implicitst-p st).

new-st — Guard (vl-implicitst-p new-st).

Definitions and Theorems

Function: vl-implicitsts-restore-fast-alists

(defun vl-implicitsts-restore-fast-alists (st new-st)
  (declare (xargs :guard (and (vl-implicitst-p st)
                              (vl-implicitst-p new-st))))
  (let ((__function__ 'vl-implicitsts-restore-fast-alists))
    (declare (ignorable __function__))
    (b* (((vl-implicitst st))
         ((vl-implicitst new-st)))
      (or (same-lengthp st.portdecls new-st.portdecls)
          (progn$ (fast-alist-free new-st.portdecls)
                  (make-fast-alist st.portdecls)))
      (or (same-lengthp st.decls new-st.decls)
          (progn$ (fast-alist-free new-st.decls)
                  (make-fast-alist st.decls))))))

Theorem: vl-implicitsts-restore-fast-alists-of-vl-implicitst-fix-st

(defthm vl-implicitsts-restore-fast-alists-of-vl-implicitst-fix-st
  (equal (vl-implicitsts-restore-fast-alists (vl-implicitst-fix st)
                                             new-st)
         (vl-implicitsts-restore-fast-alists st new-st)))

Theorem: vl-implicitsts-restore-fast-alists-vl-implicitst-equiv-congruence-on-st

(defthm
 vl-implicitsts-restore-fast-alists-vl-implicitst-equiv-congruence-on-st
 (implies
      (vl-implicitst-equiv st st-equiv)
      (equal (vl-implicitsts-restore-fast-alists st new-st)
             (vl-implicitsts-restore-fast-alists st-equiv new-st)))
 :rule-classes :congruence)

Theorem: vl-implicitsts-restore-fast-alists-of-vl-implicitst-fix-new-st

(defthm
     vl-implicitsts-restore-fast-alists-of-vl-implicitst-fix-new-st
 (equal
  (vl-implicitsts-restore-fast-alists st (vl-implicitst-fix new-st))
  (vl-implicitsts-restore-fast-alists st new-st)))

Theorem: vl-implicitsts-restore-fast-alists-vl-implicitst-equiv-congruence-on-new-st

(defthm
 vl-implicitsts-restore-fast-alists-vl-implicitst-equiv-congruence-on-new-st
 (implies
      (vl-implicitst-equiv new-st new-st-equiv)
      (equal (vl-implicitsts-restore-fast-alists st new-st)
             (vl-implicitsts-restore-fast-alists st new-st-equiv)))
 :rule-classes :congruence)