(vl-expr-simp-unary-bitnot x args) → new-x
Function:
(defun vl-expr-simp-unary-bitnot (x args) (declare (xargs :guard (and (vl-expr-p x) (vl-exprlist-p args)))) (declare (xargs :guard (and (not (vl-atom-p x)) (equal (vl-nonatom->op x) :vl-unary-bitnot) (equal (len args) 1)))) (let ((__function__ 'vl-expr-simp-unary-bitnot)) (declare (ignorable __function__)) (b* ((arg (first args)) ((when (and (not (vl-atom-p arg)) (eq (vl-nonatom->op arg) :vl-unary-bitnot))) (first (vl-nonatom->args arg))) ((when (and (vl-atom-p arg) (vl-expr-resolved-p arg) (or (eql (vl-resolved->val arg) 1) (eql (vl-resolved->val arg) 0)) (equal (vl-expr->finalwidth x) 1) (equal (vl-expr->finaltype x) :vl-unsigned))) (b* ((curr (vl-resolved->val arg)) (ans (if (eql curr 0) |*sized-1'b1*| |*sized-1'b0*|))) (vl-cw-ps-seq (vl-cw "NC Rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (not (vl-atom-p arg)) (eq (vl-nonatom->op arg) :vl-qmark))) (b* (((list a b c) (vl-nonatom->args arg)) (~b (make-vl-nonatom :op :vl-unary-bitnot :args (list b) :finalwidth (vl-expr->finalwidth b) :finaltype (vl-expr->finaltype b))) (~c (make-vl-nonatom :op :vl-unary-bitnot :args (list c) :finalwidth (vl-expr->finalwidth c) :finaltype (vl-expr->finaltype c))) (ans (change-vl-nonatom arg :args (list a ~b ~c)))) (vl-cw-ps-seq (vl-cw "QM Rewrite ~a0 to ~a1!~%" x ans)) ans)) ((when (and (not (vl-atom-p arg)) (eq (vl-nonatom->op arg) :vl-binary-bitand))) (b* (((list a b) (vl-nonatom->args arg)) (~a (make-vl-nonatom :op :vl-unary-bitnot :args (list a) :finalwidth (vl-expr->finalwidth a) :finaltype (vl-expr->finaltype a))) (~b (make-vl-nonatom :op :vl-unary-bitnot :args (list b) :finalwidth (vl-expr->finalwidth b) :finaltype (vl-expr->finaltype b))) (ans (change-vl-nonatom arg :op :vl-binary-bitor :args (list ~a ~b)))) (vl-cw-ps-seq (vl-cw "DMA Rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (not (vl-atom-p arg)) (eq (vl-nonatom->op arg) :vl-binary-bitor))) (b* (((list a b) (vl-nonatom->args arg)) (~a (make-vl-nonatom :op :vl-unary-bitnot :args (list a) :finalwidth (vl-expr->finalwidth a) :finaltype (vl-expr->finaltype a))) (~b (make-vl-nonatom :op :vl-unary-bitnot :args (list b) :finalwidth (vl-expr->finalwidth b) :finaltype (vl-expr->finaltype b))) (ans (change-vl-nonatom arg :op :vl-binary-bitand :args (list ~a ~b)))) (vl-cw-ps-seq (vl-cw "DMO Rewrite ~a0 to ~a1~%" x ans)) ans))) (change-vl-nonatom x :args args))))
Theorem:
(defthm vl-expr-p-of-vl-expr-simp-unary-bitnot (b* ((new-x (vl-expr-simp-unary-bitnot x args))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-simp-unary-bitnot-of-vl-expr-fix-x (equal (vl-expr-simp-unary-bitnot (vl-expr-fix x) args) (vl-expr-simp-unary-bitnot x args)))
Theorem:
(defthm vl-expr-simp-unary-bitnot-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-simp-unary-bitnot x args) (vl-expr-simp-unary-bitnot x-equiv args))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-simp-unary-bitnot-of-vl-exprlist-fix-args (equal (vl-expr-simp-unary-bitnot x (vl-exprlist-fix args)) (vl-expr-simp-unary-bitnot x args)))
Theorem:
(defthm vl-expr-simp-unary-bitnot-vl-exprlist-equiv-congruence-on-args (implies (vl-exprlist-equiv args args-equiv) (equal (vl-expr-simp-unary-bitnot x args) (vl-expr-simp-unary-bitnot x args-equiv))) :rule-classes :congruence)