Check if the sensitivity list is okay for a combinational block.
(vl-check-sensitivity-list ctrl body ctx warnings) → (mv okp warnings)
Function:
(defun vl-check-sensitivity-list (ctrl body ctx warnings) (declare (xargs :guard (and (vl-delayoreventcontrol-p ctrl) (vl-stmt-p body) (vl-always-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (or (vl-star-control-p ctrl) (vl-classic-control-p ctrl)) (vl-stmt-cblock-p body)))) (let ((__function__ 'vl-check-sensitivity-list)) (declare (ignorable __function__)) (b* (((when (vl-star-control-p ctrl)) (mv t (ok))) (sens-exprs (vl-classic-control->exprs ctrl)) (sens-names (vl-idexprlist->names sens-exprs)) (warnings (if (not (duplicated-members sens-names)) (ok) (warn :type :vl-warn-sensitivity-list :msg "~a0: sensitivity list has multiple occurrences of ~&1." :args (list ctx (duplicated-members sens-names))))) (used-rvals (vl-stmt-cblock-rvalexprs body)) (used-names (vl-exprlist-names used-rvals)) (sens (mergesort sens-names)) (used (mergesort used-names)) (unnecessary-in-sens (difference sens used)) (missing-from-sens (difference used sens)) (warnings (if (not unnecessary-in-sens) (ok) (warn :type :vl-warn-sensitivity-list :msg "~a0: sensitivity list unnecessarily mentions ~&1." :args (list ctx unnecessary-in-sens)))) (warnings (if (not missing-from-sens) (ok) (fatal :type :vl-sensitivity-list-fail :msg "~a0: sensitivity list omits ~&1." :args (list ctx missing-from-sens)))) (lvalues (vl-idexprlist->names (vl-stmt-cblock-lvalexprs body))) (bad-lvalues (intersect (mergesort lvalues) sens)) (warnings (if (not bad-lvalues) (ok) (fatal :type :vl-bad-always :msg "~a0: found assignments to registers in the sensitivity ~ list; we don't support this and it might indicate loops: ~&1." :args (list ctx bad-lvalues)))) (okp (and (not bad-lvalues) (not missing-from-sens)))) (mv okp warnings))))
Theorem:
(defthm booleanp-of-vl-check-sensitivity-list.okp (b* (((mv ?okp ?warnings) (vl-check-sensitivity-list ctrl body ctx warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-check-sensitivity-list.warnings (b* (((mv ?okp ?warnings) (vl-check-sensitivity-list ctrl body ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)