		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-check-uses-are-spurious-instances

Signature
(vl-lucid-check-uses-are-spurious-instances name used db clk) → (mv just-passed-to-a-spurious-instance warnings)
Arguments: name — Guard (stringp name).; used — Guard (vl-lucidocclist-p used).; db — Guard (vl-luciddb-p db).; clk — Guard (natp clk).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lucid-check-uses-are-spurious-instances

(defun vl-lucid-check-uses-are-spurious-instances (name used db clk)
 (declare (xargs :guard (and (stringp name)
                             (vl-lucidocclist-p used)
                             (vl-luciddb-p db)
                             (natp clk))))
 (let ((__function__ 'vl-lucid-check-uses-are-spurious-instances))
  (declare (ignorable __function__))
  (b*
   (((when (atom used)) (mv t nil))
    (name (string-fix name))
    (db (vl-luciddb-fix db))
    ((mv rest-just-passed warnings)
     (vl-lucid-check-uses-are-spurious-instances name (cdr used)
                                                 db clk))
    ((unless rest-just-passed)
     (mv nil warnings))
    (occ (car used))
    ((vl-lucidctx ctx)
     (vl-lucidocc->ctx occ))
    ((unless (and (eq (tag ctx.elem) :vl-modinst)
                  ctx.portname))
     (mv nil warnings))
    (modname (vl-modinst->modname ctx.elem))
    (mod (vl-scopestack-find-definition modname ctx.ss))
    ((unless (and mod
                  (member (tag mod)
                          '(:vl-module :vl-interface))))
     (mv
      nil
      (warn
       :type :vl-lucid-programming-error
       :msg
       "Confused -- it seems ~s0 is used in instance ~s1 (path:
                        ~s2) but can't find module/interface ~s3"
       :args (list name (vl-modinst->instname ctx.elem)
                   (vl-scopestack->path ctx.ss)
                   modname))))
    (key-ss
     (vl-normalize-scopestack
         (vl-scopestack-push mod (vl-scopestack->toplevel ctx.ss))))
    (key-item (vl-scopestack-find-item ctx.portname key-ss))
    ((unless key-item)
     (mv
      nil
      (warn
       :type :vl-lucid-programming-error
       :msg
       "Confused -- it seems ~s0 is connected to port ~s1 of instance ~s2 (path:
                        ~s3) but can't find a declaration of that name in ~s4"
       :args (list name ctx.portname
                   (vl-modinst->instname ctx.elem)
                   (vl-scopestack->path ctx.ss)
                   modname))))
    (key (make-vl-lucidkey :item key-item
                           :scopestack key-ss))
    (lookup (cdr (hons-get key db)))
    ((unless (and lookup
                  (consp (vl-lucidval->used lookup))))
     (mv t nil))
    ((when (zp clk))
     (mv
      nil
      (warn
       :type :vl-lucid-spurious-instances-loop
       :msg
       "Recursion limit ran out when looking for spurious instances for ~s0"
       :args (list name)))))
   (vl-lucid-check-uses-are-spurious-instances
        ctx.portname (vl-lucidval->used lookup)
        db (1- clk)))))

Theorem: vl-warninglist-p-of-vl-lucid-check-uses-are-spurious-instances.warnings

(defthm
 vl-warninglist-p-of-vl-lucid-check-uses-are-spurious-instances.warnings
 (b*
  (((mv ?just-passed-to-a-spurious-instance
        ?warnings)
    (vl-lucid-check-uses-are-spurious-instances name used db clk)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-lucid-check-uses-are-spurious-instances-of-str-fix-name

(defthm vl-lucid-check-uses-are-spurious-instances-of-str-fix-name
 (equal
     (vl-lucid-check-uses-are-spurious-instances (str-fix name)
                                                 used db clk)
     (vl-lucid-check-uses-are-spurious-instances name used db clk)))

Theorem: vl-lucid-check-uses-are-spurious-instances-streqv-congruence-on-name

(defthm
 vl-lucid-check-uses-are-spurious-instances-streqv-congruence-on-name
 (implies
  (streqv name name-equiv)
  (equal
       (vl-lucid-check-uses-are-spurious-instances name used db clk)
       (vl-lucid-check-uses-are-spurious-instances
            name-equiv used db clk)))
 :rule-classes :congruence)

Theorem: vl-lucid-check-uses-are-spurious-instances-of-vl-lucidocclist-fix-used

(defthm
 vl-lucid-check-uses-are-spurious-instances-of-vl-lucidocclist-fix-used
 (equal
     (vl-lucid-check-uses-are-spurious-instances
          name (vl-lucidocclist-fix used)
          db clk)
     (vl-lucid-check-uses-are-spurious-instances name used db clk)))

Theorem: vl-lucid-check-uses-are-spurious-instances-vl-lucidocclist-equiv-congruence-on-used

(defthm
 vl-lucid-check-uses-are-spurious-instances-vl-lucidocclist-equiv-congruence-on-used
 (implies
  (vl-lucidocclist-equiv used used-equiv)
  (equal
       (vl-lucid-check-uses-are-spurious-instances name used db clk)
       (vl-lucid-check-uses-are-spurious-instances
            name used-equiv db clk)))
 :rule-classes :congruence)

Theorem: vl-lucid-check-uses-are-spurious-instances-of-vl-luciddb-fix-db

(defthm
    vl-lucid-check-uses-are-spurious-instances-of-vl-luciddb-fix-db
 (equal
     (vl-lucid-check-uses-are-spurious-instances
          name used (vl-luciddb-fix db)
          clk)
     (vl-lucid-check-uses-are-spurious-instances name used db clk)))

Theorem: vl-lucid-check-uses-are-spurious-instances-vl-luciddb-equiv-congruence-on-db

(defthm
 vl-lucid-check-uses-are-spurious-instances-vl-luciddb-equiv-congruence-on-db
 (implies
  (vl-luciddb-equiv db db-equiv)
  (equal
       (vl-lucid-check-uses-are-spurious-instances name used db clk)
       (vl-lucid-check-uses-are-spurious-instances
            name used db-equiv clk)))
 :rule-classes :congruence)

Theorem: vl-lucid-check-uses-are-spurious-instances-of-nfix-clk

(defthm vl-lucid-check-uses-are-spurious-instances-of-nfix-clk
 (equal
     (vl-lucid-check-uses-are-spurious-instances
          name used db (nfix clk))
     (vl-lucid-check-uses-are-spurious-instances name used db clk)))

Theorem: vl-lucid-check-uses-are-spurious-instances-nat-equiv-congruence-on-clk

(defthm
 vl-lucid-check-uses-are-spurious-instances-nat-equiv-congruence-on-clk
 (implies
  (acl2::nat-equiv clk clk-equiv)
  (equal
       (vl-lucid-check-uses-are-spurious-instances name used db clk)
       (vl-lucid-check-uses-are-spurious-instances
            name used db clk-equiv)))
 :rule-classes :congruence)