Should only be called on good cblocks.
(vl-cblock-synth x vars delta) → (mv delta cvtregs)
Function:
(defun vl-cblock-synth (x vars delta) (declare (xargs :guard (and (vl-always-p x) (vl-vardecllist-p vars) (vl-delta-p delta)))) (let ((__function__ 'vl-cblock-synth)) (declare (ignorable __function__)) (b* ((stmt (vl-always->stmt x)) (type (vl-always->type x)) ((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 nil)))) ((unless okp) (raise "Not a valid cblock: ~x0." x) (mv delta nil)) ((unless (and (or (eq type :vl-always-comb) (vl-star-control-p ctrl) (vl-classic-control-p ctrl)) (vl-stmt-cblock-p body))) (raise "Not a valid cblock: ~x0." x) (mv delta nil)) ((mv body delta) (vl-stmt-stmttemps body delta x)) ((unless (vl-stmt-cblock-p body)) (raise "Somehow stmttemps screwed up the body?" x) (mv delta nil)) (lvalues (mergesort (vl-idexprlist->names (vl-stmt-cblock-lvalexprs body)))) (assigns (vl-cblock-make-assigns lvalues vars body x)) (delta (change-vl-delta delta :assigns (append assigns (vl-delta->assigns delta))))) (mv delta lvalues))))
Theorem:
(defthm vl-delta-p-of-vl-cblock-synth.delta (implies (and (force (vl-always-p x)) (force (vl-vardecllist-p vars)) (force (vl-delta-p delta))) (b* (((mv ?delta ?cvtregs) (vl-cblock-synth x vars delta))) (vl-delta-p delta))) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-cblock-synth.cvtregs (b* (((mv ?delta ?cvtregs) (vl-cblock-synth x vars delta))) (string-listp cvtregs)) :rule-classes :rewrite)