(vl-sign-extend-constint value origwidth finalwidth) returns a new value, which is the
sign extension of the
When the MSB is true we need to add the appropriate number of 1 bits. There are probably any number of ways to do this. My method is relatively simple:
|---- finalwidth -------------| |-- origwidth --| value == 0000...0000 1bb...bbbbbbbbbbb (logior) mask == 1111...1111 000...00000000000 ---------------------------------------------------------- result == 1111...1111 1bb...bbbbbbbbbbb
Function:
(defun vl-sign-extend-constint (value origwidth finalwidth) (declare (xargs :guard (and (natp value) (posp origwidth) (posp finalwidth)))) (declare (xargs :guard (and (< value (expt 2 origwidth)) (< origwidth finalwidth)))) (let ((__function__ 'vl-sign-extend-constint)) (declare (ignorable __function__)) (b* ((msb (logbitp (1- origwidth) value)) ((unless msb) value) (finalwidth-many-ones (- (expt 2 finalwidth) 1)) (origwidth-many-ones (- (expt 2 origwidth) 1)) (mask (logxor finalwidth-many-ones origwidth-many-ones)) (result (logior mask value))) result)))
Theorem:
(defthm natp-of-vl-sign-extend-constint (implies (and (force (natp value)) (force (posp origwidth)) (syntaxp (or (not (quotep origwidth)) (< (unquote origwidth) 10000))) (force (< value (expt 2 origwidth))) (force (posp finalwidth)) (force (< origwidth finalwidth))) (natp (vl-sign-extend-constint value origwidth finalwidth))) :rule-classes :type-prescription)
Theorem:
(defthm upper-bound-of-vl-sign-extend-constint (implies (and (force (natp value)) (force (posp origwidth)) (syntaxp (or (not (quotep origwidth)) (< (unquote origwidth) 10000))) (force (< value (expt 2 origwidth))) (force (posp finalwidth)) (force (< origwidth finalwidth))) (< (vl-sign-extend-constint value origwidth finalwidth) (expt 2 finalwidth))) :rule-classes ((:rewrite) (:linear)))