• 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
          • Scopestack
          • Hid-tools
          • Filtering-by-name
          • Vl-interface-mocktype
          • Stripping-functions
          • Genblob
          • Expr-tools
          • Extract-vl-types
          • Hierarchy
          • Range-tools
          • Finding-by-name
            • Fast-finding-by-name
              • Vl-interfaceportlist-alist
              • Vl-genelementlist-alist
              • Vl-vardecllist-alist
              • Vl-portdecllist-alist
              • Vl-paramdecllist-alist
                • Vl-interfacelist-alist
                • Vl-gateinstlist-alist
                • Vl-fundecllist-alist
                • Vl-dpiimportlist-alist
                • Vl-typedeflist-alist
                • Vl-taskdecllist-alist
                • Vl-programlist-alist
                • Vl-packagelist-alist
                • Vl-modulelist-alist
                • Vl-modportlist-alist
                • Vl-modinstlist-alist
                • Vl-genvarlist-alist
                • Vl-configlist-alist
                • Vl-classlist-alist
                • Vl-udplist-alist
                • Vl-vardecl-alist
                • Vl-typedef-alist
                • Vl-taskdecl-alist
                • Vl-program-alist
                • Vl-portdecl-alist
                • Vl-paramdecl-alist
                • Vl-package-alist
                • Vl-module-alist
                • Vl-modport-alist
                • Vl-modinst-alist
                • Vl-interfaceport-alist
                • Vl-interface-alist
                • Vl-genvar-alist
                • Vl-genelement-alist
                • Vl-gateinst-alist
                • Vl-fundecl-alist
                • Vl-dpiimport-alist
                • Vl-config-alist
                • Vl-class-alist
                • Vl-udp-alist
              • Vl-find-interfaceport
              • Vl-find-portdecl
              • Vl-find-taskdecl
              • Vl-find-paramdecl
              • Vl-find-interface
              • Vl-find-gateinst
              • Vl-find-dpiimport
              • 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-genvar
              • Vl-find-config
              • Vl-find-class
              • Vl-find-udp
              • Vl-modalist
              • Vl-make-portdecl-alist
              • Vl-fast-find-module
              • Vl-fast-find-portdecl
            • Stmt-tools
            • Modnamespace
            • Flat-warnings
            • Reordering-by-name
            • Datatype-tools
            • Syscalls
            • Allexprs
            • Lvalues
            • Port-tools
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Fast-finding-by-name

    Vl-paramdecllist-alist

    Extend an alist by binding the names of vl-paramdecls to their definitions.

    Signature
    (vl-paramdecllist-alist x acc) → alist
    Arguments
    x — Guard (vl-paramdecllist-p x).
    Returns
    alist — Type (equal (vl-paramdecl-alist-p alist) (vl-paramdecl-alist-p acc)).

    This can be used as an alternative to vl-find-paramdecl when you need to perform a lot of lookups.

    Definitions and Theorems

    Function: vl-paramdecllist-alist

    (defun vl-paramdecllist-alist (x acc)
      (declare (xargs :guard (vl-paramdecllist-p x)))
      (let ((__function__ 'vl-paramdecllist-alist))
        (declare (ignorable __function__))
        (if (atom x)
            acc
          (cons (cons (vl-paramdecl->name (car x))
                      (vl-paramdecl-fix (car x)))
                (vl-paramdecllist-alist (cdr x) acc)))))

    Theorem: return-type-of-vl-paramdecllist-alist

    (defthm return-type-of-vl-paramdecllist-alist
      (b* ((alist (vl-paramdecllist-alist x acc)))
        (equal (vl-paramdecl-alist-p alist)
               (vl-paramdecl-alist-p acc)))
      :rule-classes :rewrite)

    Theorem: lookup-in-vl-paramdecllist-alist-acc-elim

    (defthm lookup-in-vl-paramdecllist-alist-acc-elim
     (implies
       (syntaxp (not (equal acc ''nil)))
       (equal (hons-assoc-equal name (vl-paramdecllist-alist x acc))
              (or (hons-assoc-equal name (vl-paramdecllist-alist x nil))
                  (hons-assoc-equal name acc)))))

    Theorem: lookup-in-vl-paramdecllist-alist-fast

    (defthm lookup-in-vl-paramdecllist-alist-fast
      (implies
           (stringp name)
           (equal (hons-assoc-equal name (vl-paramdecllist-alist x nil))
                  (let ((val (vl-find-paramdecl name x)))
                    (and val (cons name val))))))

    Theorem: vl-paramdecllist-alist-of-vl-paramdecllist-fix-x

    (defthm vl-paramdecllist-alist-of-vl-paramdecllist-fix-x
      (equal (vl-paramdecllist-alist (vl-paramdecllist-fix x)
                                     acc)
             (vl-paramdecllist-alist x acc)))

    Theorem: vl-paramdecllist-alist-vl-paramdecllist-equiv-congruence-on-x

    (defthm
          vl-paramdecllist-alist-vl-paramdecllist-equiv-congruence-on-x
      (implies (vl-paramdecllist-equiv x x-equiv)
               (equal (vl-paramdecllist-alist x acc)
                      (vl-paramdecllist-alist x-equiv acc)))
      :rule-classes :congruence)