• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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-bindcontext-fix
              • Vl-bindcontext-p
              • Vl-bindcontext-equiv
              • Vl-bindcontext->shortdescription
            • 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

• Vl-bindcontext

Vl-bindcontext-p

Recognizer for vl-bindcontext.

Signature

(vl-bindcontext-p x) → *

Definitions and Theorems

Function: vl-bindcontext-p

(defun vl-bindcontext-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-bindcontext-p))
    (declare (ignorable __function__))
    (common-lisp::case (tag x)
      ((:vl-interface) (vl-interface-p x))
      ((:vl-module) (vl-module-p x))
      (otherwise (vl-design-p x)))))

Theorem: consp-when-vl-bindcontext-p

(defthm consp-when-vl-bindcontext-p
  (implies (vl-bindcontext-p x) (consp x))
  :rule-classes :compound-recognizer)

Theorem: vl-bindcontext-p-when-vl-interface-p

(defthm vl-bindcontext-p-when-vl-interface-p
  (implies (vl-interface-p x)
           (vl-bindcontext-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-bindcontext-p-when-vl-module-p

(defthm vl-bindcontext-p-when-vl-module-p
  (implies (vl-module-p x)
           (vl-bindcontext-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-bindcontext-p-when-vl-design-p

(defthm vl-bindcontext-p-when-vl-design-p
  (implies (vl-design-p x)
           (vl-bindcontext-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-interface-p-by-tag-when-vl-bindcontext-p

(defthm vl-interface-p-by-tag-when-vl-bindcontext-p
  (implies (and (or (equal (tag x) :vl-interface))
                (vl-bindcontext-p x))
           (vl-interface-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-module-p-by-tag-when-vl-bindcontext-p

(defthm vl-module-p-by-tag-when-vl-bindcontext-p
  (implies (and (or (equal (tag x) :vl-module))
                (vl-bindcontext-p x))
           (vl-module-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-design-p-by-tag-when-vl-bindcontext-p

(defthm vl-design-p-by-tag-when-vl-bindcontext-p
  (implies (and (or (equal (tag x) :vl-design))
                (vl-bindcontext-p x))
           (vl-design-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-bindcontext-p-when-invalid-tag

(defthm vl-bindcontext-p-when-invalid-tag
  (implies (and (not (equal (tag x) :vl-interface))
                (not (equal (tag x) :vl-module))
                (not (equal (tag x) :vl-design)))
           (not (vl-bindcontext-p x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: tag-when-vl-bindcontext-p-forward

(defthm tag-when-vl-bindcontext-p-forward
  (implies (vl-bindcontext-p x)
           (or (equal (tag x) :vl-interface)
               (equal (tag x) :vl-module)
               (equal (tag x) :vl-design)))
  :rule-classes ((:forward-chaining)))