		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-scopestack-find-item/ss/path

Signature
(vl-scopestack-find-item/ss/path name ss) → (mv item item-ss elabpath)
Arguments: name — Guard (stringp name).; ss — Guard (vl-scopestack-p ss).
Returns: item — Type (iff (vl-scopeitem-p item) item).; item-ss — Type (vl-scopestack-p item-ss).; elabpath — Reversed instructions to get from the SS to the item location.
Type (vl-elabtraversal-p elabpath).

Definitions and Theorems

Function: vl-scopestack-find-item/ss/path

(defun vl-scopestack-find-item/ss/path (name ss)
 (declare (xargs :guard (and (stringp name)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-scopestack-find-item/ss/path))
  (declare (ignorable __function__))
  (b*
   (((mv item context-ss pkg-name)
     (vl-scopestack-find-item/context name ss))
    (elabpath (vl-scopestack-find-elabpath ss context-ss pkg-name))
    ((unless pkg-name)
     (mv item context-ss elabpath))
    (design (vl-scopestack->design context-ss))
    (pkg
     (and
       design
       (cdr (hons-get pkg-name
                      (vl-design-scope-package-alist-top design)))))
    (item-ss
        (and pkg
             (vl-scopestack-push pkg (vl-scopestack-init design)))))
   (mv item item-ss elabpath))))

Theorem: return-type-of-vl-scopestack-find-item/ss/path.item

(defthm return-type-of-vl-scopestack-find-item/ss/path.item
  (b* (((mv ?item ?item-ss ?elabpath)
        (vl-scopestack-find-item/ss/path name ss)))
    (iff (vl-scopeitem-p item) item))
  :rule-classes :rewrite)

Theorem: vl-scopestack-p-of-vl-scopestack-find-item/ss/path.item-ss

(defthm vl-scopestack-p-of-vl-scopestack-find-item/ss/path.item-ss
  (b* (((mv ?item ?item-ss ?elabpath)
        (vl-scopestack-find-item/ss/path name ss)))
    (vl-scopestack-p item-ss))
  :rule-classes :rewrite)

Theorem: vl-elabtraversal-p-of-vl-scopestack-find-item/ss/path.elabpath

(defthm
     vl-elabtraversal-p-of-vl-scopestack-find-item/ss/path.elabpath
  (b* (((mv ?item ?item-ss ?elabpath)
        (vl-scopestack-find-item/ss/path name ss)))
    (vl-elabtraversal-p elabpath))
  :rule-classes :rewrite)

Theorem: tag-of-vl-scopestack-find-item/ss/path-forward

(defthm tag-of-vl-scopestack-find-item/ss/path-forward
  (b* (((mv item ?item-ss ?item-path)
        (vl-scopestack-find-item/ss/path name ss)))
    (implies item
             (or (equal (tag item) :vl-modinst)
                 (equal (tag item) :vl-gateinst)
                 (equal (tag item) :vl-genloop)
                 (equal (tag item) :vl-genif)
                 (equal (tag item) :vl-gencase)
                 (equal (tag item) :vl-genbegin)
                 (equal (tag item) :vl-genarray)
                 (equal (tag item) :vl-genbase)
                 (equal (tag item) :vl-genvar)
                 (equal (tag item) :vl-interfaceport)
                 (equal (tag item) :vl-paramdecl)
                 (equal (tag item) :vl-vardecl)
                 (equal (tag item) :vl-fundecl)
                 (equal (tag item) :vl-taskdecl)
                 (equal (tag item) :vl-typedef)
                 (equal (tag item) :vl-dpiimport)
                 (equal (tag item) :vl-modport))))
  :rule-classes ((:forward-chaining)))

Theorem: vl-scopestack-find-item/ss/path-of-str-fix-name

(defthm vl-scopestack-find-item/ss/path-of-str-fix-name
  (equal (vl-scopestack-find-item/ss/path (str-fix name)
                                          ss)
         (vl-scopestack-find-item/ss/path name ss)))

Theorem: vl-scopestack-find-item/ss/path-streqv-congruence-on-name

(defthm vl-scopestack-find-item/ss/path-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-scopestack-find-item/ss/path name ss)
                  (vl-scopestack-find-item/ss/path name-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-scopestack-find-item/ss/path-of-vl-scopestack-fix-ss

(defthm vl-scopestack-find-item/ss/path-of-vl-scopestack-fix-ss
  (equal
       (vl-scopestack-find-item/ss/path name (vl-scopestack-fix ss))
       (vl-scopestack-find-item/ss/path name ss)))

Theorem: vl-scopestack-find-item/ss/path-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-scopestack-find-item/ss/path-vl-scopestack-equiv-congruence-on-ss
 (implies (vl-scopestack-equiv ss ss-equiv)
          (equal (vl-scopestack-find-item/ss/path name ss)
                 (vl-scopestack-find-item/ss/path name ss-equiv)))
 :rule-classes :congruence)