(vl-always->svex-latch-warnings write-masks read-masks) → warnings
Function:
(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:
(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:
(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:
(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:
(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:
(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)