Build an arbitrary expression of some particular width.
Function:
(defun vl-default-n-bit-expr (n) (declare (xargs :guard (posp n))) (let ((__function__ 'vl-default-n-bit-expr)) (declare (ignorable __function__)) (let ((n (mbe :logic (pos-fix n) :exec n))) (make-vl-atom :guts (make-vl-constint :value 0 :origwidth n :origtype :vl-unsigned) :finalwidth n :finaltype :vl-unsigned))))
Theorem:
(defthm vl-expr-p-of-vl-default-n-bit-expr (b* ((expr (vl-default-n-bit-expr n))) (vl-expr-p expr)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-default-n-bit-expr (equal (vl-expr->finalwidth (vl-default-n-bit-expr n)) (pos-fix n)))
Theorem:
(defthm vl-expr-widthsfixed-p-of-vl-default-n-bit-expr (vl-expr-widthsfixed-p (vl-default-n-bit-expr n)))
Theorem:
(defthm vl-default-n-bit-expr-of-pos-fix-n (equal (vl-default-n-bit-expr (pos-fix n)) (vl-default-n-bit-expr n)))
Theorem:
(defthm vl-default-n-bit-expr-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-default-n-bit-expr n) (vl-default-n-bit-expr n-equiv))) :rule-classes :congruence)