		Search-engine friendly clone of the ACL2 documentation.

Vl-svstmt.lisp

Vl-always->svex-latch-warnings

Signature
(vl-always->svex-latch-warnings write-masks read-masks) → warnings
Arguments: write-masks — Guard (sv::4vmask-alist-p write-masks).; read-masks — Guard (sv::svex-mask-alist-p read-masks).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-always->svex-latch-warnings

(defun vl-always->svex-latch-warnings (write-masks read-masks)
 (declare (xargs :guard (and (sv::4vmask-alist-p write-masks)
                             (sv::svex-mask-alist-p read-masks))))
 (let ((__function__ 'vl-always->svex-latch-warnings))
  (declare (ignorable __function__))
  (b*
   ((warnings nil)
    (write-masks (sv::4vmask-alist-fix write-masks))
    ((when (atom write-masks)) (ok))
    ((cons var wmask) (car write-masks))
    (var (sv::svar-fix var))
    (wmask (sv::4vmask-fix wmask))
    (rmask (sv::svex-mask-lookup (sv::make-svex-var :name var)
                                 read-masks))
    (overlap (bitops::sparseint-bitand wmask rmask))
    (warnings
     (if (bitops::sparseint-equal overlap 0)
         warnings
      (warn
       :type :vl-always-comb-looks-like-latch
       :msg
       "Variable ~a0 was both read and written (or not ~
                               always updated) in an always_comb block.  ~
                               Verilog simulators may treat this variable as ~
                               a latch.  Overlap of read and write bits: ~s1"
       :args (list var
                   (if (< (bitops::sparseint-length overlap)
                          40000)
                       (str::hexify (bitops::sparseint-val overlap))
                     "<more than 10000 digits>")))))
    ((wmv warnings)
     (vl-always->svex-latch-warnings (cdr write-masks)
                                     read-masks)))
   warnings)))

Theorem: vl-warninglist-p-of-vl-always->svex-latch-warnings

(defthm vl-warninglist-p-of-vl-always->svex-latch-warnings
 (b* ((warnings
           (vl-always->svex-latch-warnings write-masks read-masks)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-always->svex-latch-warnings-of-4vmask-alist-fix-write-masks

(defthm
     vl-always->svex-latch-warnings-of-4vmask-alist-fix-write-masks
 (equal
  (vl-always->svex-latch-warnings (sv::4vmask-alist-fix write-masks)
                                  read-masks)
  (vl-always->svex-latch-warnings write-masks read-masks)))

Theorem: vl-always->svex-latch-warnings-4vmask-alist-equiv-congruence-on-write-masks

(defthm
 vl-always->svex-latch-warnings-4vmask-alist-equiv-congruence-on-write-masks
 (implies
  (sv::4vmask-alist-equiv write-masks write-masks-equiv)
  (equal
     (vl-always->svex-latch-warnings write-masks read-masks)
     (vl-always->svex-latch-warnings write-masks-equiv read-masks)))
 :rule-classes :congruence)

Theorem: vl-always->svex-latch-warnings-of-svex-mask-alist-fix-read-masks

(defthm
   vl-always->svex-latch-warnings-of-svex-mask-alist-fix-read-masks
  (equal (vl-always->svex-latch-warnings
              write-masks
              (sv::svex-mask-alist-fix read-masks))
         (vl-always->svex-latch-warnings write-masks read-masks)))

Theorem: vl-always->svex-latch-warnings-svex-mask-alist-equiv-congruence-on-read-masks

(defthm
 vl-always->svex-latch-warnings-svex-mask-alist-equiv-congruence-on-read-masks
 (implies
  (sv::svex-mask-alist-equiv read-masks read-masks-equiv)
  (equal
     (vl-always->svex-latch-warnings write-masks read-masks)
     (vl-always->svex-latch-warnings write-masks read-masks-equiv)))
 :rule-classes :congruence)