summaryrefslogtreecommitdiff
path: root/test/smt/shift_or_concat4_2.unsat.sail
blob: 43a1b1989c3b56bec5f675eaace7797ace751ab3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
default Order dec

$include <prelude.sail>

register R1 : bits(4)
register R2 : bits(4)

$property
function prop((): unit) -> bool = {
  let w = 4;
  let x = sail_zero_extend(R1, 8);
  let x = sail_shiftleft(x, w);
  let y = or_vec(x, sail_zero_extend(R2, 8));
  let z = R1 @ R2;
  y == z
}