• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
          • Scopestack
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
          • Allexprs
          • Hid-tools
          • Vl-consteval
          • Range-tools
          • Lvalexprs
          • Hierarchy
          • Finding-by-name
            • Fast-finding-by-name
            • Vl-find-interfaceport
            • Vl-find-portdecl
            • Vl-find-taskdecl
            • Vl-find-paramdecl
            • Vl-find-interface
            • Vl-find-gateinst
            • Vl-find-vardecl
            • Vl-find-typedef
            • Vl-find-program
            • Vl-find-package
            • Vl-find-module
            • Vl-find-modport
            • Vl-find-modinst
            • Vl-find-genelement
            • Vl-find-fundecl
            • Vl-find-config
            • Vl-modalist
            • Vl-find-udp
            • Vl-make-portdecl-alist
            • Vl-fast-find-module
              • Vl-fast-find-portdecl
            • Expr-tools
            • Expr-slicing
            • Stripping-functions
            • Stmt-tools
            • Modnamespace
            • Vl-parse-expr-from-str
            • Welltyped
            • Reordering-by-name
            • Flat-warnings
            • Genblob
            • Expr-building
            • Datatype-tools
            • Syscalls
            • Relocate
            • Expr-cleaning
            • Namemangle
            • Caremask
            • Port-tools
            • Lvalues
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Finding-by-name

    Vl-fast-find-module

    Legacy. vl-modalist-optimized version of vl-find-module.

    Signature
    (vl-fast-find-module name mods modalist) → *
    Arguments
    name — Guard (stringp name).
    mods — Guard (vl-modulelist-p mods).
    modalist — Guard (equal modalist (vl-modalist mods)).

    Definitions and Theorems

    Function: vl-fast-find-module$inline

    (defun vl-fast-find-module$inline (name mods modalist)
      (declare (xargs :guard (and (stringp name)
                                  (vl-modulelist-p mods)
                                  (equal modalist (vl-modalist mods)))))
      (let ((__function__ 'vl-fast-find-module))
        (declare (ignorable __function__))
        (mbe :logic (vl-find-module (string-fix name) mods)
             :exec (cdr (hons-get name modalist)))))

    Theorem: vl-fast-find-module$inline-of-str-fix-name

    (defthm vl-fast-find-module$inline-of-str-fix-name
      (equal (vl-fast-find-module$inline (str-fix name)
                                         mods modalist)
             (vl-fast-find-module$inline name mods modalist)))

    Theorem: vl-fast-find-module$inline-streqv-congruence-on-name

    (defthm vl-fast-find-module$inline-streqv-congruence-on-name
     (implies
          (streqv name name-equiv)
          (equal (vl-fast-find-module$inline name mods modalist)
                 (vl-fast-find-module$inline name-equiv mods modalist)))
     :rule-classes :congruence)

    Theorem: vl-fast-find-module$inline-of-vl-modulelist-fix-mods

    (defthm vl-fast-find-module$inline-of-vl-modulelist-fix-mods
      (equal (vl-fast-find-module$inline name (vl-modulelist-fix mods)
                                         modalist)
             (vl-fast-find-module$inline name mods modalist)))

    Theorem: vl-fast-find-module$inline-vl-modulelist-equiv-congruence-on-mods

    (defthm
      vl-fast-find-module$inline-vl-modulelist-equiv-congruence-on-mods
     (implies
          (vl-modulelist-equiv mods mods-equiv)
          (equal (vl-fast-find-module$inline name mods modalist)
                 (vl-fast-find-module$inline name mods-equiv modalist)))
     :rule-classes :congruence)