• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
            • Increment-elim
            • Make-implicit-wires
              • Shadowcheck
                • Vl-shadowcheck-genelement
                • Vl-shadowcheck-reference-name
                • Vl-shadowcheck-declare-name
                • Deltemps
                • Vl-shadowcheck-modelement
                • Vl-lexscope
                • Vl-shadowcheck-reference-scopeexpr
                • Vl-shadowcheck-reference-names
                • Vl-shadowcheck-declare-names
                • Vl-shadowcheck-paramtype
                • Vl-shadowcheck-fun/task-loaditems
                • Vl-shadowcheck-fun/task-loaditem
                • Vl-shadowcheck-fundecl
                • Vl-shadowcheck-declare-typedefs
                • Vl-shadowcheck-blockitemlist
                • Vl-shadowcheck-portdecllist
                • Vl-shadowcheck-paramdecls
                • Vl-shadowcheck-dpiimports
                • Vl-shadowcheck-taskdecls
                • Vl-shadowcheck-taskdecl
                • Vl-shadowcheck-push-scope
                • Vl-shadowcheck-blockitem
                • Vl-shadowcheck-vardecls
                • Vl-shadowcheck-vardecl
                • Vl-shadowcheck-typedef
                • Vl-shadowcheck-portdecl
                • Vl-shadowcheck-paramdecl
                • Vl-shadowcheck-modport
                • Vl-shadowcheck-modinst
                • Vl-shadowcheck-imports
                • Vl-shadowcheck-import
                • Vl-shadowcheck-gateinst
                • Vl-shadowcheck-fundecls
                • Vl-shadowcheck-dpiimport
                • Vl-shadowcheck-ports
                • Vl-shadowcheck-port
                • Vl-shadowcheck-initial
                • Vl-shadowcheck-assign
                • Vl-shadowcheck-always
                • Vl-shadowcheck-final
                • Vl-shadowcheck-alias
                • Vl-shadowcheck-state
                • Vl-shadowcheck-module
                • Vl-shadowcheck-interface
                • Vl-shadowcheck-interfaces
                • Vl-shadowcheck-modules
                • Vl-packagemap-find-packages-for-name
                • Vl-shadowcheck-design
                • Vl-lexscopes
                  • Vl-lexscopes-fix
                  • Vl-lexscopes-direct-import-name
                  • Vl-lexscopes-declare-name
                  • Vl-lexscopes-do-import
                    • Vl-lexscopes-find
                    • Vl-lexscopes-equiv
                    • Vl-lexscopes-p
                    • Vl-lexscopes-exit-scope
                    • Vl-lexscopes-enter-new-scope
                  • Vl-expr->maybe-subtype
                  • Vl-shadowcheck-pop-scope
                  • Nameclash
                  • Vl-portdecl-or-blockitem
                  • Vl-lexscope-decls
                  • Vl-packagemap
                  • Vl-portdecl-or-blockitem-list
                • 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
    • Vl-lexscopes

    Vl-lexscopes-do-import

    Extend the lexscopes with a package import.

    Signature
    (vl-lexscopes-do-import x scopes warnings design) 
      → 
    (mv scopes warnings)
    Arguments
    x — Guard (vl-import-p x).
    scopes — Guard (vl-lexscopes-p scopes).
    warnings — Guard (vl-warninglist-p warnings).
    design — Guard (vl-design-p design).
    Returns
    scopes — Type (vl-lexscopes-p scopes).
    warnings — Type (vl-warninglist-p warnings).

    Definitions and Theorems

    Function: vl-lexscopes-do-import

    (defun vl-lexscopes-do-import (x scopes warnings design)
     (declare (xargs :guard (and (vl-import-p x)
                                 (vl-lexscopes-p scopes)
                                 (vl-warninglist-p warnings)
                                 (vl-design-p design))))
     (let ((__function__ 'vl-lexscopes-do-import))
      (declare (ignorable __function__))
      (b*
       (((vl-import x) (vl-import-fix x))
        (scopes (vl-lexscopes-fix scopes))
        (warnings (vl-warninglist-fix warnings))
        ((when (atom scopes))
         (raise "Expected at least one scope.")
         (mv scopes warnings))
        (pkg (vl-find-package x.pkg (vl-design->packages design)))
        (warnings
         (if pkg warnings
           (fatal
                :type :vl-bad-import
                :msg "~a0: trying to import from undefined package ~s1."
                :args (list x x.pkg))))
        (pkg-item-alist (and pkg
                             (vl-package-scope-item-alist-top pkg)))
        ((unless (eq x.part :vl-import*))
         (b*
          ((item (hons-get x.part pkg-item-alist))
           (warnings
              (if item warnings
                (fatal :type :vl-bad-import
                       :msg "~a0: no declaration of ~s1 in package ~s2."
                       :args (list x x.part x.pkg)))))
          (vl-lexscopes-direct-import-name
               x.pkg x.part scopes x warnings)))
        ((vl-lexscope scope1) (car scopes))
        ((when (hons-assoc-equal x.pkg scope1.wildpkgs))
         (mv scopes warnings)))
       (mv
        (cons
         (change-vl-lexscope scope1
                             :wildpkgs (cons (cons x.pkg pkg-item-alist)
                                             scope1.wildpkgs))
         (cdr scopes))
        warnings))))

    Theorem: vl-lexscopes-p-of-vl-lexscopes-do-import.scopes

    (defthm vl-lexscopes-p-of-vl-lexscopes-do-import.scopes
      (b* (((mv ?scopes ?warnings)
            (vl-lexscopes-do-import x scopes warnings design)))
        (vl-lexscopes-p scopes))
      :rule-classes :rewrite)

    Theorem: vl-warninglist-p-of-vl-lexscopes-do-import.warnings

    (defthm vl-warninglist-p-of-vl-lexscopes-do-import.warnings
      (b* (((mv ?scopes ?warnings)
            (vl-lexscopes-do-import x scopes warnings design)))
        (vl-warninglist-p warnings))
      :rule-classes :rewrite)

    Theorem: vl-lexscopes-do-import-of-vl-import-fix-x

    (defthm vl-lexscopes-do-import-of-vl-import-fix-x
      (equal (vl-lexscopes-do-import (vl-import-fix x)
                                     scopes warnings design)
             (vl-lexscopes-do-import x scopes warnings design)))

    Theorem: vl-lexscopes-do-import-vl-import-equiv-congruence-on-x

    (defthm vl-lexscopes-do-import-vl-import-equiv-congruence-on-x
     (implies
        (vl-import-equiv x x-equiv)
        (equal (vl-lexscopes-do-import x scopes warnings design)
               (vl-lexscopes-do-import x-equiv scopes warnings design)))
     :rule-classes :congruence)

    Theorem: vl-lexscopes-do-import-of-vl-lexscopes-fix-scopes

    (defthm vl-lexscopes-do-import-of-vl-lexscopes-fix-scopes
      (equal (vl-lexscopes-do-import x (vl-lexscopes-fix scopes)
                                     warnings design)
             (vl-lexscopes-do-import x scopes warnings design)))

    Theorem: vl-lexscopes-do-import-vl-lexscopes-equiv-congruence-on-scopes

    (defthm
         vl-lexscopes-do-import-vl-lexscopes-equiv-congruence-on-scopes
     (implies
        (vl-lexscopes-equiv scopes scopes-equiv)
        (equal (vl-lexscopes-do-import x scopes warnings design)
               (vl-lexscopes-do-import x scopes-equiv warnings design)))
     :rule-classes :congruence)

    Theorem: vl-lexscopes-do-import-of-vl-warninglist-fix-warnings

    (defthm vl-lexscopes-do-import-of-vl-warninglist-fix-warnings
     (equal
          (vl-lexscopes-do-import x scopes (vl-warninglist-fix warnings)
                                  design)
          (vl-lexscopes-do-import x scopes warnings design)))

    Theorem: vl-lexscopes-do-import-vl-warninglist-equiv-congruence-on-warnings

    (defthm
     vl-lexscopes-do-import-vl-warninglist-equiv-congruence-on-warnings
     (implies
        (vl-warninglist-equiv warnings warnings-equiv)
        (equal (vl-lexscopes-do-import x scopes warnings design)
               (vl-lexscopes-do-import x scopes warnings-equiv design)))
     :rule-classes :congruence)

    Theorem: vl-lexscopes-do-import-of-vl-design-fix-design

    (defthm vl-lexscopes-do-import-of-vl-design-fix-design
     (equal
         (vl-lexscopes-do-import x
                                 scopes warnings (vl-design-fix design))
         (vl-lexscopes-do-import x scopes warnings design)))

    Theorem: vl-lexscopes-do-import-vl-design-equiv-congruence-on-design

    (defthm vl-lexscopes-do-import-vl-design-equiv-congruence-on-design
     (implies
        (vl-design-equiv design design-equiv)
        (equal (vl-lexscopes-do-import x scopes warnings design)
               (vl-lexscopes-do-import x scopes warnings design-equiv)))
     :rule-classes :congruence)