• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • 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
            • Basic-bind-elim
              • Vl-modulelist-apply-binddelta
              • Vl-interfacelist-apply-binddelta
              • Vl-bindelim-main
              • Vl-bindelim-bindlist
              • Vl-bindelim-find-global-target
              • Vl-interfacelist-bindelim
              • Vl-modulelist-bindelim
              • Vl-interface-bindelim
              • Vl-module-bindelim
              • Vl-bindelim-institem
              • Vl-warn-bindintentlist-undefined
              • Vl-warn-bindintent-undefined
              • Vl-interfacelist-bindelim-insttable
              • Vl-modulelist-bindelim-insttable
              • Vl-warn-binddelta-undefined
              • Vl-interface-bindelim-insttable
              • Vl-interface-apply-binddelta
              • Vl-design-bindelim-pass2
              • Vl-bindelim-modinstlist-add-atts
              • Vl-module-bindelim-insttable
              • Vl-module-apply-binddelta
              • Vl-bindelim-modinst-add-atts
              • Vl-design-bindelim-pass1
              • Vl-bindcontext
              • Vl-bindintent->modinsts
              • Vl-bindelim-insttable
                • Vl-bindelim-insttable-p
                • Vl-bindelim-insttable-fix
                • Vl-bindelim-extend-insttable
                  • Vl-bindelim-insttable-equiv
                  • Vl-bindelim-create-insttable
                  • Vl-genblob-bindelim-insttable
                • Vl-bindintentlist->modinsts
                • Vl-binddelta
                • Vl-design-bindelim
                • Vl-bindelim-institemlist
              • 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-bindelim-insttable

    Vl-bindelim-extend-insttable

    Straightforward extension of the vl-bindelim-insttable with a bunch of instances from some context.

    Signature
    (vl-bindelim-extend-insttable x ctx genp bindp itbl) 
      → 
    new-itbl
    Arguments
    x — Guard (vl-modinstlist-p x).
    ctx — Guard (vl-bindcontext-p ctx).
    genp — Guard (booleanp genp).
    bindp — Guard (booleanp bindp).
    itbl — Guard (vl-bindelim-insttable-p itbl).
    Returns
    new-itbl — Type (vl-bindelim-insttable-p new-itbl).

    Definitions and Theorems

    Function: vl-bindelim-extend-insttable

    (defun vl-bindelim-extend-insttable (x ctx genp bindp itbl)
      (declare (xargs :guard (and (vl-modinstlist-p x)
                                  (vl-bindcontext-p ctx)
                                  (booleanp genp)
                                  (booleanp bindp)
                                  (vl-bindelim-insttable-p itbl))))
      (let ((__function__ 'vl-bindelim-extend-insttable))
        (declare (ignorable __function__))
        (b* ((x (vl-modinstlist-fix x))
             (itbl (vl-bindelim-insttable-fix itbl))
             ((when (atom x)) itbl)
             ((vl-modinst inst1) (first x))
             (item (make-vl-bindelim-institem :ctx ctx
                                              :inst inst1
                                              :genp genp
                                              :bindp bindp))
             (prev-items (cdr (hons-get inst1.modname itbl)))
             (new-items (cons item prev-items))
             (itbl (hons-acons inst1.modname new-items itbl)))
          (vl-bindelim-extend-insttable (rest x)
                                        ctx genp bindp itbl))))

    Theorem: vl-bindelim-insttable-p-of-vl-bindelim-extend-insttable

    (defthm vl-bindelim-insttable-p-of-vl-bindelim-extend-insttable
      (b*
       ((new-itbl (vl-bindelim-extend-insttable x ctx genp bindp itbl)))
       (vl-bindelim-insttable-p new-itbl))
      :rule-classes :rewrite)

    Theorem: vl-bindelim-extend-insttable-of-vl-modinstlist-fix-x

    (defthm vl-bindelim-extend-insttable-of-vl-modinstlist-fix-x
      (equal (vl-bindelim-extend-insttable (vl-modinstlist-fix x)
                                           ctx genp bindp itbl)
             (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

    Theorem: vl-bindelim-extend-insttable-vl-modinstlist-equiv-congruence-on-x

    (defthm
      vl-bindelim-extend-insttable-vl-modinstlist-equiv-congruence-on-x
     (implies
       (vl-modinstlist-equiv x x-equiv)
       (equal
            (vl-bindelim-extend-insttable x ctx genp bindp itbl)
            (vl-bindelim-extend-insttable x-equiv ctx genp bindp itbl)))
     :rule-classes :congruence)

    Theorem: vl-bindelim-extend-insttable-of-vl-bindcontext-fix-ctx

    (defthm vl-bindelim-extend-insttable-of-vl-bindcontext-fix-ctx
      (equal (vl-bindelim-extend-insttable x (vl-bindcontext-fix ctx)
                                           genp bindp itbl)
             (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

    Theorem: vl-bindelim-extend-insttable-vl-bindcontext-equiv-congruence-on-ctx

    (defthm
     vl-bindelim-extend-insttable-vl-bindcontext-equiv-congruence-on-ctx
     (implies
       (vl-bindcontext-equiv ctx ctx-equiv)
       (equal
            (vl-bindelim-extend-insttable x ctx genp bindp itbl)
            (vl-bindelim-extend-insttable x ctx-equiv genp bindp itbl)))
     :rule-classes :congruence)

    Theorem: vl-bindelim-extend-insttable-of-bool-fix-genp

    (defthm vl-bindelim-extend-insttable-of-bool-fix-genp
      (equal (vl-bindelim-extend-insttable x ctx (acl2::bool-fix genp)
                                           bindp itbl)
             (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

    Theorem: vl-bindelim-extend-insttable-iff-congruence-on-genp

    (defthm vl-bindelim-extend-insttable-iff-congruence-on-genp
     (implies
       (iff genp genp-equiv)
       (equal
            (vl-bindelim-extend-insttable x ctx genp bindp itbl)
            (vl-bindelim-extend-insttable x ctx genp-equiv bindp itbl)))
     :rule-classes :congruence)

    Theorem: vl-bindelim-extend-insttable-of-bool-fix-bindp

    (defthm vl-bindelim-extend-insttable-of-bool-fix-bindp
     (equal
         (vl-bindelim-extend-insttable x ctx genp (acl2::bool-fix bindp)
                                       itbl)
         (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

    Theorem: vl-bindelim-extend-insttable-iff-congruence-on-bindp

    (defthm vl-bindelim-extend-insttable-iff-congruence-on-bindp
     (implies
       (iff bindp bindp-equiv)
       (equal
            (vl-bindelim-extend-insttable x ctx genp bindp itbl)
            (vl-bindelim-extend-insttable x ctx genp bindp-equiv itbl)))
     :rule-classes :congruence)

    Theorem: vl-bindelim-extend-insttable-of-vl-bindelim-insttable-fix-itbl

    (defthm
         vl-bindelim-extend-insttable-of-vl-bindelim-insttable-fix-itbl
      (equal (vl-bindelim-extend-insttable
                  x ctx genp
                  bindp (vl-bindelim-insttable-fix itbl))
             (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

    Theorem: vl-bindelim-extend-insttable-vl-bindelim-insttable-equiv-congruence-on-itbl

    (defthm
     vl-bindelim-extend-insttable-vl-bindelim-insttable-equiv-congruence-on-itbl
     (implies
       (vl-bindelim-insttable-equiv itbl itbl-equiv)
       (equal
            (vl-bindelim-extend-insttable x ctx genp bindp itbl)
            (vl-bindelim-extend-insttable x ctx genp bindp itbl-equiv)))
     :rule-classes :congruence)