• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • 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-bindelim-find-global-target

Signature

(vl-bindelim-find-global-target x itbl ss warnings) 
  → 
(mv name warnings)

Arguments

x — Guard (vl-bind-p x).

itbl — Guard (vl-bindelim-insttable-p itbl).

ss — Guard (vl-scopestack-p ss).

warnings — Guard (vl-warninglist-p warnings).

Returns

name — Type (maybe-stringp name).

warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-bindelim-find-global-target

(defun vl-bindelim-find-global-target (x itbl ss warnings)
 (declare (xargs :guard (and (vl-bind-p x)
                             (vl-bindelim-insttable-p itbl)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-bindelim-find-global-target))
  (declare (ignorable __function__))
  (b*
   ((itbl (vl-bindelim-insttable-fix itbl))
    ((vl-bind x) (vl-bind-fix x))
    ((when (and x.scope (atom x.addto)))
     (mv x.scope (ok)))
    ((unless (consp x.addto))
     (mv
      (raise
       "Programming error -- scopeless bind should always have addto: ~x0"
       x)
      (ok)))
    ((unless (atom (cdr x.addto)))
     (mv
      nil
      (fatal
       :type :vl-bindelim-fail
       :msg
       "~a0: bind statement isn't supported (multiple instances, ~
                         not sure if it's global.)"
       :args (list x))))
    (addto (first x.addto))
    ((unless (vl-idexpr-p addto))
     (mv
      nil
      (fatal
       :type :vl-bindelim-fail
       :msg
       "~a0: bind statement isn't supported because the ~
                        add-to expression, ~a1, isn't just an identifier."
       :args (list x addto))))
    (target-inst (vl-scopestack-find-item (vl-idexpr->name addto)
                                          ss))
    ((unless (mbe :logic (vl-modinst-p target-inst)
                  :exec (eq (tag target-inst) :vl-modinst)))
     (mv
      nil
      (fatal
       :type :vl-bad-bind
       :msg
       "~a0: trying to add instances to ~a1, which isn't ~
                         a module instance.  (~a2)"
       :args (list x addto (tag target-inst)))))
    ((vl-modinst target-inst))
    ((when (and x.scope
                (not (equal x.scope target-inst.modname))))
     (mv
      nil
      (fatal
       :type :vl-bad-bind
       :msg
       "~a0: bind statement says that ~a1 is an ~
                         instance of ~a2, but actually it is an ~
                         instance of ~a3."
       :args (list x addto x.scope target-inst.modname))))
    (inst-infos (cdr (hons-get target-inst.modname itbl)))
    ((unless (consp inst-infos))
     (mv
      (raise
       "Programming error -- the bindelim insttable says ~
                    there are no instance of ~x0, but we found one: ~x1. ~
                    How can this be?"
       target-inst.modname target-inst)
      (ok)))
    ((unless (atom (cdr inst-infos)))
     (mv
      nil
      (fatal
       :type :vl-bindelim-fail
       :msg
       "~a0: bind statement isn't supported because there ~
                         are multiple instances of ~s1 in the design, ~
                         including at least at ~a2 and ~a3."
       :args
       (list
          x target-inst.modname
          (vl-modinst->loc
               (vl-bindelim-institem->inst (first inst-infos)))
          (vl-modinst->loc
               (vl-bindelim-institem->inst (second inst-infos)))))))
    ((vl-bindelim-institem info1)
     (car inst-infos))
    ((unless (equal info1.inst target-inst))
     (mv
      (raise
       "Programming error -- the bindelim insttable says ~
                    there's exactly one instance of ~x0, but we found ~x1 ~
                    and it's different than ~x2."
       target-inst.modname target-inst info1)
      (ok)))
    ((when info1.genp)
     (mv
      nil
      (fatal
       :type :vl-bindelim-fail
       :msg
       "~a0: bind statement isn't supported because it ~
                         refers to an instance that is inside a generate ~
                         block, so we aren't sure this is a globally unique ~
                         instance."
       :args (list x)))))
   (mv target-inst.modname (ok)))))

Theorem: maybe-stringp-of-vl-bindelim-find-global-target.name

(defthm maybe-stringp-of-vl-bindelim-find-global-target.name
  (b* (((mv ?name ?warnings)
        (vl-bindelim-find-global-target x itbl ss warnings)))
    (maybe-stringp name))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-bindelim-find-global-target.warnings

(defthm vl-warninglist-p-of-vl-bindelim-find-global-target.warnings
  (b* (((mv ?name ?warnings)
        (vl-bindelim-find-global-target x itbl ss warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-bindelim-find-global-target-of-vl-bind-fix-x

(defthm vl-bindelim-find-global-target-of-vl-bind-fix-x
  (equal (vl-bindelim-find-global-target (vl-bind-fix x)
                                         itbl ss warnings)
         (vl-bindelim-find-global-target x itbl ss warnings)))

Theorem: vl-bindelim-find-global-target-vl-bind-equiv-congruence-on-x

(defthm vl-bindelim-find-global-target-vl-bind-equiv-congruence-on-x
 (implies
  (vl-bind-equiv x x-equiv)
  (equal (vl-bindelim-find-global-target x itbl ss warnings)
         (vl-bindelim-find-global-target x-equiv itbl ss warnings)))
 :rule-classes :congruence)

Theorem: vl-bindelim-find-global-target-of-vl-bindelim-insttable-fix-itbl

(defthm
   vl-bindelim-find-global-target-of-vl-bindelim-insttable-fix-itbl
 (equal
  (vl-bindelim-find-global-target x (vl-bindelim-insttable-fix itbl)
                                  ss warnings)
  (vl-bindelim-find-global-target x itbl ss warnings)))

Theorem: vl-bindelim-find-global-target-vl-bindelim-insttable-equiv-congruence-on-itbl

(defthm
 vl-bindelim-find-global-target-vl-bindelim-insttable-equiv-congruence-on-itbl
 (implies
  (vl-bindelim-insttable-equiv itbl itbl-equiv)
  (equal (vl-bindelim-find-global-target x itbl ss warnings)
         (vl-bindelim-find-global-target x itbl-equiv ss warnings)))
 :rule-classes :congruence)

Theorem: vl-bindelim-find-global-target-of-vl-scopestack-fix-ss

(defthm vl-bindelim-find-global-target-of-vl-scopestack-fix-ss
  (equal
       (vl-bindelim-find-global-target x itbl (vl-scopestack-fix ss)
                                       warnings)
       (vl-bindelim-find-global-target x itbl ss warnings)))

Theorem: vl-bindelim-find-global-target-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-bindelim-find-global-target-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-bindelim-find-global-target x itbl ss warnings)
         (vl-bindelim-find-global-target x itbl ss-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-bindelim-find-global-target-of-vl-warninglist-fix-warnings

(defthm
      vl-bindelim-find-global-target-of-vl-warninglist-fix-warnings
  (equal (vl-bindelim-find-global-target
              x itbl ss (vl-warninglist-fix warnings))
         (vl-bindelim-find-global-target x itbl ss warnings)))

Theorem: vl-bindelim-find-global-target-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-bindelim-find-global-target-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal (vl-bindelim-find-global-target x itbl ss warnings)
         (vl-bindelim-find-global-target x itbl ss warnings-equiv)))
 :rule-classes :congruence)