blob: 857f7f3306e29f49ddb1564834ed295b59b54084 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
default Order dec
$include <prelude.sail>
register R1 : bits(32)
register R2 : bits(32)
$property
function prop('sz: range(0, 32)) -> bool = {
let z: bits('sz) = sail_zeros(sz);
let x: bits('sz + 32) = R1 @ z;
let y: bits(32 + 'sz) = R2 @ z;
let padding = sail_zeros(32) @ sail_zeros(sz);
// A and B must be equal
let A = x @ y;
let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y);
A == B
}
|
