• 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
            • Elabindex
              • Vl-elabindex-traverse
              • Vl-elabkey
              • Vl-elabscopes-update-subscope
              • Vl-elabscopes-do-instruction/update
              • Vl-elabtraversals-remove-common-prefix
              • Vl-elabscopes-pop/update-one
              • Vl-elabscopes
              • Vl-maybe-elabkey
              • Vl-elabscopes-traverse/update
              • Vl-elabscopes-pop/update
              • Vl-elabscope-update-package-subscope
              • Vl-elabinstruction
              • Vl-elabscope-update-subscope?
              • Vl-elabscope-update-subscope
              • Vl-elabscope-update-item-subscope
              • Vl-elabscope-update-index-subscope
              • Vl-elabscope-update-def-subscope
              • Vl-elabscope-update-class-subscope
              • Vl-elabscope-update-item-info
              • Vl-elabscope
              • Vl-elabscopes-do-instruction
              • Vl-elabpaths-append
              • Vl-elabscopes-traverse
              • Vl-elabscopes-push-named
              • Vl-elabscopes-item-info
              • Vl-elabscopes-push-scope
              • Vl-elabindex-update-item-info
              • Vl-elabscopes-subscope
              • Vl-elabscopes-push-anon
              • Vl-elabscopes-root/update
              • Vl-elabscopes-pop
              • Vl-elabindex-push
              • Vl-elabscope-package-subscope
              • Vl-elabscope-item-subscope
              • Vl-elabscope-class-subscope
              • Vl-elabindex-traverse-undo-entry
              • Vl-elabscope-subscope
              • Vl-elabscope-item-info
              • Vl-elabscope-def-subscope
              • Vl-scope->elabkey
                • Vl-elabscopes->elabtraversal
                • Vl-elabscopes-root
                • Vl-elabscopes-init-ss
                • Vl-elabscopes->top-scope
                • Vl-elabindex-update-undostack
                • Vl-elabindex-init
                • Vl-elabindex-sync-scopes
                • Vl-elabindex-update-scopes
                • Vl-elabindex-push-undo-entry
                • Vl-elabindex-update-ss
                • Vl-elabindex-undo
                • Vl-elabtraversal-stack
                • Vl-elabscopes-init
                • Vl-elabindex->undostack
                • Vl-elabindex->scopes
                • Vl-elabtraversal
                • Vl-elabindex->ss
              • Vl-override-parameter
              • Vl-genblob-elaborate
              • Vl-modelement-elaborate
              • Vl-design-elaborate-aux
              • Vl-package-elaborate-aux
              • Vl-taskdecl-elaborate
              • Vl-clkdecl-elaborate
              • Vl-defaultdisablelist-elaborate
              • Vl-modport-portlist-elaborate
              • Vl-modinst-elaborate-aux
              • Vl-maybe-parse-temps-elaborate
              • Vl-ansi-portdecllist-elaborate
              • Vl-ansi-portdecl-elaborate
              • Vl-parse-temps-elaborate
              • Vl-dpiimportlist-elaborate
              • Vl-clkassignlist-elaborate
              • Vl-cassertionlist-elaborate
              • Vl-assertionlist-elaborate
              • Vl-taskdecllist-elaborate
              • Vl-sequencelist-elaborate
              • Vl-propportlist-elaborate
              • Vl-propertylist-elaborate
              • Vl-plainarglist-elaborate
              • Vl-namedarglist-elaborate
              • Vl-maybe-clkskew-elaborate
              • Vl-gclkdecllist-elaborate
              • Vl-gateinstlist-elaborate
              • Vl-elabtasklist-elaborate
              • Vl-defaultdisable-elaborate
              • Vl-sequence-elaborate
              • Vl-property-elaborate
              • Vl-modportlist-elaborate
              • Vl-modport-port-elaborate
              • Vl-modinstlist-elaborate
              • Vl-letdecllist-elaborate
              • Vl-interfaceport-elaborate
              • Vl-initiallist-elaborate
              • Vl-gateinst-elaborate
              • Vl-fundecllist-elaborate
              • Vl-clkdecllist-elaborate
              • Vl-assignlist-elaborate
              • Vl-assign-elaborate-aux
              • Vl-arguments-elaborate
              • Vl-alwayslist-elaborate
              • Vl-regularport-elaborate
              • Vl-portlist-elaborate
              • Vl-finallist-elaborate
              • Vl-dpiimport-elaborate
              • Vl-clkassign-elaborate
              • Vl-bindlist-elaborate
              • Vl-aliaslist-elaborate
              • Vl-warn-about-negative-indices
              • Vl-udplist-elaborate
              • Vl-propport-elaborate
              • Vl-modinst-elaborate
              • Vl-udp-elaborate
              • Vl-port-elaborate
              • Vl-plainarg-elaborate
              • Vl-namedarg-elaborate
              • Vl-modport-elaborate
              • Vl-gclkdecl-elaborate
              • Vl-elabtask-elaborate
              • Vl-clkskew-elaborate
              • Vl-assign-elaborate
              • Vl-always-elaborate-aux
              • Vl-always-elaborate
              • Vl-alias-elaborate
              • Vl-initial-elaborate
              • Vl-bind-elaborate
              • Vl-final-elaborate
              • Vl-fundecl-paramdecls-for-const-args
              • Vl-fundecl-body-with-const-args
              • Vl-exprlist-args-to-4vec-consts
              • Sv::svex-constval
            • Addnames
            • Annotate
            • Clean-warnings
            • Eliminitial
            • Custom-transform-hooks
            • Problem-modules
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Elabindex

    Vl-scope->elabkey

    Signature
    (vl-scope->elabkey scope) → key
    Arguments
    scope — Guard (vl-scope-p scope).
    Returns
    key — Type (and (iff (vl-elabkey-p key) key) (vl-maybe-elabkey-p key)).

    Definitions and Theorems

    Function: vl-scope->elabkey

    (defun vl-scope->elabkey (scope)
      (declare (xargs :guard (vl-scope-p scope)))
      (let ((__function__ 'vl-scope->elabkey))
        (declare (ignorable __function__))
        (b* ((name (vl-scope->id scope))
             (type (vl-scope->scopetype scope)))
          (case type
                ((:vl-module :vl-interface)
                 (and (stringp name)
                      (vl-elabkey-def name)))
                ((:vl-fundecl :vl-taskdecl :vl-genblock)
                 (cond ((stringp name) (vl-elabkey-item name))
                       ((integerp name)
                        (vl-elabkey-index name))))
                ((:vl-genarray :vl-genloop)
                 (and (stringp name)
                      (vl-elabkey-item name)))
                (:vl-genarrayblock (and (integerp name)
                                        (vl-elabkey-index name)))
                (:vl-package (and (stringp name)
                                  (vl-elabkey-package name)))
                (:vl-class (and (stringp name)
                                (vl-elabkey-class name)))
                (otherwise nil)))))

    Theorem: return-type-of-vl-scope->elabkey

    (defthm return-type-of-vl-scope->elabkey
      (b* ((key (vl-scope->elabkey scope)))
        (and (iff (vl-elabkey-p key) key)
             (vl-maybe-elabkey-p key)))
      :rule-classes :rewrite)

    Theorem: vl-scope->elabkey-of-vl-scope-fix-scope

    (defthm vl-scope->elabkey-of-vl-scope-fix-scope
      (equal (vl-scope->elabkey (vl-scope-fix scope))
             (vl-scope->elabkey scope)))

    Theorem: vl-scope->elabkey-vl-scope-equiv-congruence-on-scope

    (defthm vl-scope->elabkey-vl-scope-equiv-congruence-on-scope
      (implies (vl-scope-equiv scope scope-equiv)
               (equal (vl-scope->elabkey scope)
                      (vl-scope->elabkey scope-equiv)))
      :rule-classes :congruence)