		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-multidrive-detect

Signature
(vl-lucid-multidrive-detect ss item set genp) → warnings
Arguments: ss — Guard (vl-scopestack-p ss).; item — Guard (or (vl-paramdecl-p item) (vl-vardecl-p item)).; set — Guard (vl-lucidocclist-p set).; genp — Consider occurrences from generates?.
Guard (booleanp genp).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lucid-multidrive-detect

(defun vl-lucid-multidrive-detect (ss item set genp)
 (declare (xargs :guard (and (vl-scopestack-p ss)
                             (or (vl-paramdecl-p item)
                                 (vl-vardecl-p item))
                             (vl-lucidocclist-p set)
                             (booleanp genp))))
 (let ((__function__ 'vl-lucid-multidrive-detect))
  (declare (ignorable __function__))
  (b*
   ((ss (vl-scopestack-fix ss))
    (set (vl-lucidocclist-fix set))
    ((when (or (atom set) (atom (cdr set))))
     nil)
    (set (vl-lucidocclist-drop-initials set))
    (set (vl-lucidocclist-merge-blocks set))
    (set (vl-lucidocclist-drop-bad-modinsts set))
    (set (vl-lucidocclist-drop-foreign-writes set ss))
    (set (if genp set
           (vl-lucidocclist-drop-generates set)))
    (set (vl-lucidocclist-remove-tails set))
    ((when (or (atom set) (atom (cdr set))))
     nil)
    ((when (and (eq (tag item) :vl-vardecl)
                (not (member (vl-vardecl->nettype item)
                             '(nil :vl-wire :vl-uwire)))))
     nil)
    ((when (vl-lucidocclist-some-transistory-p set))
     nil)
    ((mv simple-p ?valid-bits)
     (vl-lucid-valid-bits-for-decl item ss))
    ((unless simple-p) nil)
    ((when (vl-inside-interface-p ss)) nil)
    ((when (vl-inside-blockscope-p ss)) nil)
    ((when (vl-custom-suppress-multidrive-p ss item set))
     nil)
    (name (if (eq (tag item) :vl-vardecl)
              (vl-vardecl->name item)
            (vl-paramdecl->name item)))
    (solos (vl-lucid-collect-solo-occs set))
    ((when (and (consp solos) (consp (cdr solos))))
     (list (make-vl-warning
                :type :vl-lucid-multidrive
                :msg "~w0 has multiple drivers:~%~s1"
                :args (list name
                            (vl-lucid-multidrive-summary solos))
                :fn __function__)))
    (resolved (vl-lucid-collect-resolved-slices set))
    (allbits (vl-lucid-slices-append-bits resolved))
    ((when (and (consp solos) (consp allbits)))
     (list
      (make-vl-warning
       :type :vl-lucid-multidrive
       :msg "~w0 has multiple drivers:~%~s1"
       :args
       (list
        name
        (with-local-ps
             (vl-indent 4)
             (vl-print " - Full: ")
             (vl-pp-ctxelement-summary
                  (vl-context1->elem (vl-lucidocc->ctx (car solos)))
                  :withloc t)
             (vl-println "")
             (vl-lucid-pp-multibits (mergesort allbits)
                                    resolved)))
       :fn __function__)))
    (dupes (duplicated-members allbits))
    ((unless (consp dupes)) nil))
   (list
    (make-vl-warning
       :type :vl-lucid-multidrive
       :msg "~w0 has multiple drivers on some bits:~%~s1"
       :args
       (list name
             (with-local-ps (vl-lucid-pp-multibits (mergesort dupes)
                                                   resolved)))
       :fn __function__)))))

Theorem: vl-warninglist-p-of-vl-lucid-multidrive-detect

(defthm vl-warninglist-p-of-vl-lucid-multidrive-detect
  (b* ((warnings (vl-lucid-multidrive-detect ss item set genp)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-lucid-multidrive-detect-of-vl-scopestack-fix-ss

(defthm vl-lucid-multidrive-detect-of-vl-scopestack-fix-ss
  (equal (vl-lucid-multidrive-detect (vl-scopestack-fix ss)
                                     item set genp)
         (vl-lucid-multidrive-detect ss item set genp)))

Theorem: vl-lucid-multidrive-detect-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-lucid-multidrive-detect-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-lucid-multidrive-detect ss item set genp)
              (vl-lucid-multidrive-detect ss-equiv item set genp)))
  :rule-classes :congruence)

Theorem: vl-lucid-multidrive-detect-of-vl-lucidocclist-fix-set

(defthm vl-lucid-multidrive-detect-of-vl-lucidocclist-fix-set
  (equal
       (vl-lucid-multidrive-detect ss item (vl-lucidocclist-fix set)
                                   genp)
       (vl-lucid-multidrive-detect ss item set genp)))

Theorem: vl-lucid-multidrive-detect-vl-lucidocclist-equiv-congruence-on-set

(defthm
 vl-lucid-multidrive-detect-vl-lucidocclist-equiv-congruence-on-set
 (implies
      (vl-lucidocclist-equiv set set-equiv)
      (equal (vl-lucid-multidrive-detect ss item set genp)
             (vl-lucid-multidrive-detect ss item set-equiv genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-multidrive-detect-of-bool-fix-genp

(defthm vl-lucid-multidrive-detect-of-bool-fix-genp
 (equal
      (vl-lucid-multidrive-detect ss item set (acl2::bool-fix genp))
      (vl-lucid-multidrive-detect ss item set genp)))

Theorem: vl-lucid-multidrive-detect-iff-congruence-on-genp

(defthm vl-lucid-multidrive-detect-iff-congruence-on-genp
  (implies
       (iff genp genp-equiv)
       (equal (vl-lucid-multidrive-detect ss item set genp)
              (vl-lucid-multidrive-detect ss item set genp-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-lucidocclist-merge-blocks: Combine together the writes to a variable that occur in the same always block.