(vl-edgesynth-assignstmt-clklift x edgetable) → stmt
Function:
(defun vl-edgesynth-assignstmt-clklift (x edgetable) (declare (xargs :guard (and (and (vl-stmt-p x) (vl-assignstmt-p x) (vl-edgesynth-stmt-p x)) (vl-edgetable-p edgetable)))) (let ((__function__ 'vl-edgesynth-assignstmt-clklift)) (declare (ignorable __function__)) (b* (((vl-assignstmt x) x) ((mv c a b) (vl-qmark-p x.expr)) ((unless (and c (eql (vl-expr->finalwidth c) 1))) x) ((mv type guts) (vl-edgesynth-classify-iftest c edgetable)) ((when (eq type :clock)) (make-vl-ifstmt :condition guts :truebranch (change-vl-assignstmt x :expr a) :falsebranch (change-vl-assignstmt x :expr b))) ((when (eq type :nclock)) (make-vl-ifstmt :condition guts :truebranch (change-vl-assignstmt x :expr b) :falsebranch (change-vl-assignstmt x :expr a)))) x)))
Theorem:
(defthm vl-edgesynth-stmt-p-of-vl-edgesynth-assignstmt-clklift (implies (and (force (if (vl-stmt-p x) (if (vl-assignstmt-p$inline x) (vl-edgesynth-stmt-p x) 'nil) 'nil)) (force (vl-edgetable-p edgetable))) (b* ((stmt (vl-edgesynth-assignstmt-clklift x edgetable))) (vl-edgesynth-stmt-p stmt))) :rule-classes :rewrite)