blob: 4205db10b544750c6b1c1e9d313d0247030194dd (
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(64)
register R2 : bits(64)
$property
function prop('sz: range(0, 64)) -> bool = {
let z: bits('sz) = sail_zeros(sz);
let x: bits('sz + 64) = R1 @ z;
let y: bits(64 + 'sz) = R2 @ z;
let padding = sail_zeros(64) @ 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
}
|
