• 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
            • 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-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
    • Basic-bind-elim

    Vl-interface-apply-binddelta

    Signature
    (vl-interface-apply-binddelta x delta) → new-x
    Arguments
    x — Guard (vl-interface-p x).
    delta — Guard (vl-binddelta-p delta).
    Returns
    new-x — Type (vl-interface-p new-x).

    Definitions and Theorems

    Function: vl-interface-apply-binddelta

    (defun vl-interface-apply-binddelta (x delta)
      (declare (xargs :guard (and (vl-interface-p x)
                                  (vl-binddelta-p delta))))
      (let ((__function__ 'vl-interface-apply-binddelta))
        (declare (ignorable __function__))
        (b* (((vl-interface x) (vl-interface-fix x))
             (delta (vl-binddelta-fix delta))
             (intents (cdr (hons-get x.name delta)))
             ((unless intents) x)
             (new-insts (vl-bindintentlist->modinsts intents)))
          (change-vl-interface
               x
               :modinsts (append-without-guard x.modinsts new-insts)))))

    Theorem: vl-interface-p-of-vl-interface-apply-binddelta

    (defthm vl-interface-p-of-vl-interface-apply-binddelta
      (b* ((new-x (vl-interface-apply-binddelta x delta)))
        (vl-interface-p new-x))
      :rule-classes :rewrite)

    Theorem: vl-interface-apply-binddelta-of-vl-interface-fix-x

    (defthm vl-interface-apply-binddelta-of-vl-interface-fix-x
      (equal (vl-interface-apply-binddelta (vl-interface-fix x)
                                           delta)
             (vl-interface-apply-binddelta x delta)))

    Theorem: vl-interface-apply-binddelta-vl-interface-equiv-congruence-on-x

    (defthm
        vl-interface-apply-binddelta-vl-interface-equiv-congruence-on-x
      (implies (vl-interface-equiv x x-equiv)
               (equal (vl-interface-apply-binddelta x delta)
                      (vl-interface-apply-binddelta x-equiv delta)))
      :rule-classes :congruence)

    Theorem: vl-interface-apply-binddelta-of-vl-binddelta-fix-delta

    (defthm vl-interface-apply-binddelta-of-vl-binddelta-fix-delta
      (equal (vl-interface-apply-binddelta x (vl-binddelta-fix delta))
             (vl-interface-apply-binddelta x delta)))

    Theorem: vl-interface-apply-binddelta-vl-binddelta-equiv-congruence-on-delta

    (defthm
     vl-interface-apply-binddelta-vl-binddelta-equiv-congruence-on-delta
     (implies (vl-binddelta-equiv delta delta-equiv)
              (equal (vl-interface-apply-binddelta x delta)
                     (vl-interface-apply-binddelta x delta-equiv)))
     :rule-classes :congruence)