blob: 5fed8ad6f28b5087b3e807341d3f40268a8b2d39 (
plain)
1
2
3
4
5
6
7
8
|
val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
(bits('N), int('S)) -> (bits('N), bit) effect pure
function LSR_C (x, shift) = {
result : bits('N) = x >> shift;
carry_out : bit = if shift > 'N then bitzero else x[shift - 1];
return((result, carry_out))
}
|
