4vec-rsh
Right ``arithmetic'' shift of 4vecs.
- Signature
(4vec-rsh amt src) → shifted
- Arguments
- amt — Shift amount.
Guard (4vec-p amt).
- src — Source operand.
Guard (4vec-p src).
- Returns
- shifted — Type (4vec-p shifted).
In the usual case, amt is a 2vec, i.e., its bits are
all good Boolean values. In this case:
- If amt is non-negative then we ``arithmetically'' shift src to
the right by amt-many places. This doesn't affect the infinitely-repeated
most significant bit of src. That is, if src is negative to begin
with, i.e., its upper bits are all 1s, then the resulting, shifted value will
also be a negative number whose upper bits are all 1s. If src has upper
bits Z, then the shifted result will also have upper bits that are all Zs,
etc.
- If amt is negative, then we shift src to the left instead
of to the right, shifting in 0s from below. Note that this behavior
differs from the (very strange) semantics of Verilog/SystemVerilog,
where shift amounts are always treated as unsigned.
In cases where amt has any X or Z bits, the result is just all
Xes.
Definitions and Theorems
Function: 4vec-rsh
(defun 4vec-rsh (amt src)
(declare (xargs :guard (and (4vec-p amt) (4vec-p src))))
(let ((__function__ '4vec-rsh))
(declare (ignorable __function__))
(if (2vec-p amt)
(4vec-shift-core (- (2vec->val amt))
src)
(4vec-x))))
Theorem: 4vec-p-of-4vec-rsh
(defthm 4vec-p-of-4vec-rsh
(b* ((shifted (4vec-rsh amt src)))
(4vec-p shifted))
:rule-classes :rewrite)
Theorem: 4vec-rsh-of-2vecx-fix-amt
(defthm 4vec-rsh-of-2vecx-fix-amt
(equal (4vec-rsh (2vecx-fix amt) src)
(4vec-rsh amt src)))
Theorem: 4vec-rsh-2vecx-equiv-congruence-on-amt
(defthm 4vec-rsh-2vecx-equiv-congruence-on-amt
(implies (2vecx-equiv amt amt-equiv)
(equal (4vec-rsh amt src)
(4vec-rsh amt-equiv src)))
:rule-classes :congruence)
Theorem: 4vec-rsh-of-4vec-fix-src
(defthm 4vec-rsh-of-4vec-fix-src
(equal (4vec-rsh amt (4vec-fix src))
(4vec-rsh amt src)))
Theorem: 4vec-rsh-4vec-equiv-congruence-on-src
(defthm 4vec-rsh-4vec-equiv-congruence-on-src
(implies (4vec-equiv src src-equiv)
(equal (4vec-rsh amt src)
(4vec-rsh amt src-equiv)))
:rule-classes :congruence)
