		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-dissect-pair

Signature
(vl-lucid-dissect-pair key val reportcard st typos) → (mv reportcard typos)
Arguments: key — Guard (vl-lucidkey-p key).; val — Guard (vl-lucidval-p val).; reportcard — Guard (vl-reportcard-p reportcard).; st — Guard (vl-lucidstate-p st).; typos — Guard (vl-typocandidates-p typos).
Returns: reportcard — Type (vl-reportcard-p reportcard).; typos — Type (vl-typocandidates-p typos).

Definitions and Theorems

Function: vl-lucid-dissect-pair

(defun vl-lucid-dissect-pair (key val reportcard st typos)
 (declare (xargs :guard (and (vl-lucidkey-p key)
                             (vl-lucidval-p val)
                             (vl-reportcard-p reportcard)
                             (vl-lucidstate-p st)
                             (vl-typocandidates-p typos))))
 (let ((__function__ 'vl-lucid-dissect-pair))
  (declare (ignorable __function__))
  (b*
   ((reportcard (vl-reportcard-fix reportcard))
    (typos (vl-typocandidates-fix typos))
    ((vl-lucidstate st))
    ((vl-lucidkey key))
    ((vl-lucidval val))
    (topname (vl-scopestack->topname key.scopestack))
    (sequential-udp-p
     (b*
      ((dfn
        (and
           (stringp topname)
           (vl-scopestack-find-definition topname key.scopestack))))
      (and (eq (tag dfn) :vl-module)
           (consp (assoc-equal "VL_SEQUENTIAL_UDP"
                               (vl-module->atts dfn))))))
    ((when sequential-udp-p)
     (mv reportcard typos))
    ((when val.errors)
     (b*
      ((w
        (make-vl-warning
         :type :vl-lucid-error
         :msg
         "Error computing use/set information for ~s0.  Debugging details: ~x1."
         :args (list (with-local-ps (vl-pp-lucidkey key))
                     val.errors)
         :fatalp nil
         :fn __function__)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos))))
   (case
    (tag key.item)
    (:vl-fundecl
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Function ~w0 is never used. (~s1)"
         :args
         (list
              (vl-fundecl->name key.item)
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-genvar
     (b*
      ((usedp (consp val.used))
       (setp (consp val.set))
       ((when (and usedp setp))
        (mv reportcard typos))
       (name (vl-genvar->name key.item))
       (path (with-local-ps (vl-pp-scopestack-path key.scopestack)))
       (w
        (cond
         ((and (not usedp) (not setp))
          (make-vl-warning
              :type :vl-lucid-spurious
              :msg "Genvar ~w0 is never used or set anywhere. (~s1)"
              :args (list name path key.item)
              :fn __function__
              :fatalp nil))
         ((and usedp (not setp))
          (make-vl-warning :type :vl-lucid-unset
                           :msg "Genvar ~w0 is never set. (~s1)"
                           :args (list name path key.item)
                           :fn __function__
                           :fatalp nil))
         (t (make-vl-warning :type :vl-lucid-unused
                             :msg "Genvar ~w0 is never used. (~s1)"
                             :args (list name path key.item)
                             :fn __function__
                             :fatalp nil)))))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-modport
     (b*
      (((unless st.modportsp)
        (mv reportcard typos))
       ((when (vl-lucid-some-solo-occp val.used))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Modport ~s0 is never used. (~s1)"
         :args
         (list
              (vl-modport->name key.item)
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-dpiimport
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "DPI imported function ~w0 is never used. (~s1)"
         :args
         (list
              (vl-dpiimport->name key.item)
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-taskdecl
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Task ~w0 is never used. (~s1)"
         :args
         (list
              (vl-taskdecl->name key.item)
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-typedef
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Type ~w0 is never used. (~s1)"
         :args
         (list
              (vl-typedef->name key.item)
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-vardecl
     (b*
      (((mv warnings possible-typop)
        (vl-lucid-dissect-var-main
             key.scopestack key.item
             val.used val.set st.db st.generatesp))
       (typos (if possible-typop
                  (vl-add-typo-candidate key.scopestack
                                         (vl-vardecl->name key.item)
                                         typos)
                typos)))
      (mv (vl-extend-reportcard-list topname warnings reportcard)
          typos)))
    (:vl-paramdecl
       (b* (((unless st.paramsp)
             (mv reportcard typos))
            ((mv warnings ?possible-typop)
             (vl-lucid-dissect-var-main
                  key.scopestack key.item
                  val.used val.set st.db st.generatesp)))
         (mv (vl-extend-reportcard-list topname warnings reportcard)
             typos)))
    (:vl-interfaceport
     (b*
      (((when (or val.used val.set))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-spurious
         :msg "Interface port ~w0 is never mentioned. (~s1)"
         :args
         (list
              (vl-interfaceport->name key.item)
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (:vl-modinst
     (b*
      (((vl-modinst key.item))
       (mod (vl-scopestack-find-definition
                 key.item.modname key.scopestack))
       ((unless (eq (tag mod) :vl-interface))
        (mv reportcard typos))
       ((when (or val.used val.set))
        (mv reportcard typos))
       (w
        (make-vl-warning
         :type :vl-lucid-spurious
         :msg "Interface ~w0 is never mentioned. (~s1)"
         :args
         (list
              key.item.instname
              (with-local-ps (vl-pp-scopestack-path key.scopestack))
              key.item)
         :fn __function__
         :fatalp nil)))
      (mv (vl-extend-reportcard topname w reportcard)
          typos)))
    (otherwise (mv reportcard typos))))))

Theorem: vl-reportcard-p-of-vl-lucid-dissect-pair.reportcard

(defthm vl-reportcard-p-of-vl-lucid-dissect-pair.reportcard
  (b* (((mv ?reportcard ?typos)
        (vl-lucid-dissect-pair key val reportcard st typos)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-typocandidates-p-of-vl-lucid-dissect-pair.typos

(defthm vl-typocandidates-p-of-vl-lucid-dissect-pair.typos
  (b* (((mv ?reportcard ?typos)
        (vl-lucid-dissect-pair key val reportcard st typos)))
    (vl-typocandidates-p typos))
  :rule-classes :rewrite)

Theorem: vl-lucid-dissect-pair-of-vl-lucidkey-fix-key

(defthm vl-lucid-dissect-pair-of-vl-lucidkey-fix-key
  (equal (vl-lucid-dissect-pair (vl-lucidkey-fix key)
                                val reportcard st typos)
         (vl-lucid-dissect-pair key val reportcard st typos)))

Theorem: vl-lucid-dissect-pair-vl-lucidkey-equiv-congruence-on-key

(defthm vl-lucid-dissect-pair-vl-lucidkey-equiv-congruence-on-key
 (implies
  (vl-lucidkey-equiv key key-equiv)
  (equal (vl-lucid-dissect-pair key val reportcard st typos)
         (vl-lucid-dissect-pair key-equiv val reportcard st typos)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-lucidval-fix-val

(defthm vl-lucid-dissect-pair-of-vl-lucidval-fix-val
  (equal (vl-lucid-dissect-pair key (vl-lucidval-fix val)
                                reportcard st typos)
         (vl-lucid-dissect-pair key val reportcard st typos)))

Theorem: vl-lucid-dissect-pair-vl-lucidval-equiv-congruence-on-val

(defthm vl-lucid-dissect-pair-vl-lucidval-equiv-congruence-on-val
 (implies
  (vl-lucidval-equiv val val-equiv)
  (equal (vl-lucid-dissect-pair key val reportcard st typos)
         (vl-lucid-dissect-pair key val-equiv reportcard st typos)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-reportcard-fix-reportcard

(defthm vl-lucid-dissect-pair-of-vl-reportcard-fix-reportcard
  (equal
       (vl-lucid-dissect-pair key val (vl-reportcard-fix reportcard)
                              st typos)
       (vl-lucid-dissect-pair key val reportcard st typos)))

Theorem: vl-lucid-dissect-pair-vl-reportcard-equiv-congruence-on-reportcard

(defthm
 vl-lucid-dissect-pair-vl-reportcard-equiv-congruence-on-reportcard
 (implies
  (vl-reportcard-equiv reportcard reportcard-equiv)
  (equal (vl-lucid-dissect-pair key val reportcard st typos)
         (vl-lucid-dissect-pair key val reportcard-equiv st typos)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-lucidstate-fix-st

(defthm vl-lucid-dissect-pair-of-vl-lucidstate-fix-st
 (equal (vl-lucid-dissect-pair key
                               val reportcard (vl-lucidstate-fix st)
                               typos)
        (vl-lucid-dissect-pair key val reportcard st typos)))

Theorem: vl-lucid-dissect-pair-vl-lucidstate-equiv-congruence-on-st

(defthm vl-lucid-dissect-pair-vl-lucidstate-equiv-congruence-on-st
 (implies
  (vl-lucidstate-equiv st st-equiv)
  (equal (vl-lucid-dissect-pair key val reportcard st typos)
         (vl-lucid-dissect-pair key val reportcard st-equiv typos)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-typocandidates-fix-typos

(defthm vl-lucid-dissect-pair-of-vl-typocandidates-fix-typos
  (equal (vl-lucid-dissect-pair key val reportcard
                                st (vl-typocandidates-fix typos))
         (vl-lucid-dissect-pair key val reportcard st typos)))

Theorem: vl-lucid-dissect-pair-vl-typocandidates-equiv-congruence-on-typos

(defthm
  vl-lucid-dissect-pair-vl-typocandidates-equiv-congruence-on-typos
 (implies
  (vl-typocandidates-equiv typos typos-equiv)
  (equal (vl-lucid-dissect-pair key val reportcard st typos)
         (vl-lucid-dissect-pair key val reportcard st typos-equiv)))
 :rule-classes :congruence)