blob: 1cb8f11a06a7d1d8f3b61b950d1e1e832a1c0242 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
default Order dec
$include <prelude.sail>
register R1 : bits(32)
register R2 : bits(32)
$property
function prop((): unit) -> bool = {
let x = sail_zero_extend(R1, 64);
let x = sail_shiftleft(x, 32);
let y = or_vec(x, sail_zero_extend(R2, 64));
let z = R1 @ R2;
y == z
}
|
