Accumulate lsb's into acc, which produces an MSB-ordered list.
Function:
(defun vl-msb-bitslice-constint-aux (len value acc) (declare (xargs :guard (and (natp len) (natp value)))) (let ((__function__ 'vl-msb-bitslice-constint-aux)) (declare (ignorable __function__)) (mbe :logic (revappend (vl-lsb-bitslice-constint-aux len value) acc) :exec (b* (((when (zp len)) acc) (floor2 (mbe :logic (floor value 2) :exec (ash value -1))) (mod2 (mbe :logic (mod value 2) :exec (logand value 1))) (bit (if (eql mod2 0) |*sized-1'b0*| |*sized-1'b1*|))) (vl-msb-bitslice-constint-aux (mbe :logic (- (nfix len) 1) :exec (- len 1)) floor2 (cons bit acc))))))
Theorem:
(defthm vl-msb-bitslice-constint-aux-of-nfix-len (equal (vl-msb-bitslice-constint-aux (nfix len) value acc) (vl-msb-bitslice-constint-aux len value acc)))
Theorem:
(defthm vl-msb-bitslice-constint-aux-nat-equiv-congruence-on-len (implies (acl2::nat-equiv len len-equiv) (equal (vl-msb-bitslice-constint-aux len value acc) (vl-msb-bitslice-constint-aux len-equiv value acc))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-constint-aux-of-nfix-value (equal (vl-msb-bitslice-constint-aux len (nfix value) acc) (vl-msb-bitslice-constint-aux len value acc)))
Theorem:
(defthm vl-msb-bitslice-constint-aux-nat-equiv-congruence-on-value (implies (acl2::nat-equiv value value-equiv) (equal (vl-msb-bitslice-constint-aux len value acc) (vl-msb-bitslice-constint-aux len value-equiv acc))) :rule-classes :congruence)