Check whether an always block looks like a combinational block that we can support.
(vl-always-check-cblock always vars scary warnings) → (mv okp warnings)
Function:
(defun vl-always-check-cblock (always vars scary warnings) (declare (xargs :guard (and (vl-always-p always) (vl-vardecllist-p vars) (string-listp scary) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-always-check-cblock)) (declare (ignorable __function__)) (b* ((stmt (vl-always->stmt always)) (type (vl-always->type always)) ((when (or (eq type :vl-always-latch) (eq type :vl-always-ff))) (mv nil (ok))) ((mv okp ctrl body) (cond ((eq type :vl-always-comb) (mv t nil stmt)) ((and (eq type :vl-always) (vl-timingstmt-p stmt)) (mv t (vl-timingstmt->ctrl stmt) (vl-timingstmt->body stmt))) (t (mv nil nil stmt)))) ((unless okp) (mv nil (ok))) ((unless (or (eq type :vl-always-comb) (vl-star-control-p ctrl) (vl-classic-control-p ctrl))) (mv nil (ok))) ((unless (vl-stmt-cblock-p body)) (mv nil (ok))) (lvalues (mergesort (vl-idexprlist->names (vl-stmt-cblock-lvalexprs body)))) (paths-okp (vl-cblock-pathcheck lvalues body)) ((when (and (not paths-okp) (not (eq type :vl-always-comb)))) (mv nil (ok))) (warnings (if (and (not paths-okp) (eq type :vl-always-comb)) (warn :type :vl-tricky-always-comb :msg "~a0: always block does not obviously write to all of ~ its registers in every if/else branch." :args (list always)) (ok))) ((mv sens-okp warnings) (if (eq type :vl-always-comb) (mv t (ok)) (vl-check-sensitivity-list ctrl body always warnings))) ((unless sens-okp) (mv nil warnings)) (scary-writes (intersect lvalues (redundant-mergesort scary))) ((when scary-writes) (mv nil (fatal :type :vl-bad-always :msg "~a0: cowardly refusing to synthesize this as a ~ combinational always block, because registers ~ are written to by other always blocks, which is ~ very scary: ~&1." :args (list always scary-writes)))) (warn (vl-always-check-regs lvalues vars always)) ((when warn) (mv nil (cons warn warnings))) (non-vars (difference lvalues (mergesort (vl-vardecllist->names vars)))) ((when non-vars) (mv nil (fatal :type :vl-bad-always :msg "~a0: can't synthesize this always block because ~ it writes to non-variables: ~&1." :args (list always non-vars))))) (mv t warnings))))
Theorem:
(defthm booleanp-of-vl-always-check-cblock.okp (b* (((mv ?okp ?warnings) (vl-always-check-cblock always vars scary warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-always-check-cblock.warnings (b* (((mv ?okp ?warnings) (vl-always-check-cblock always vars scary warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)