summaryrefslogtreecommitdiff
path: root/src/test/vectors.sail
blob: 353444e5b883ead61073650a3b2ba31b1dc63886 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
let (bit[32]) v = 0b101
let (bit[4]) v2 = [0,1,0,0]
register (bit[32]) i

let (bit[10]) v3 = 0b0101010111
register (bit[10]) slice_check

register nat match_success

let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check,slice_check]

function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1
and decode x = match_success := x

function bit main _ = {

  slice_check := v3;
  slice_check := v3[1..10];
  slice_check := v3[5..10];

  gpr_small[1] := v3;
  slice_check := gpr_small[1];
 
  i := [bitzero, bitzero, bitone, bitzero];

  (* literal match *)
  switch v {
    case 0b101 -> match_success := 1
    case _ -> match_success := v
  };

  switch i {
    case [bitzero, bitzero, bitone, bitzero] -> match_success := 1
    case _ -> match_success := i
  };

  decode(i);

  (* concatenation *)
  switch i {
    case ([bitzero] : [bitzero, bitone] : [bitzero]) -> match_success := 1
    case _ -> match_success := i
  };
  switch i {
    (* check order of concatenation *)
    case ([bitzero] : [bitone] : [bitzero] : [bitzero]) -> match_success := 99
    case ([bitzero] : [bitzero] : [bitone] : [bitzero]) -> match_success := 1
    case _ -> match_success := i
  };

  (* indexed match *)
  switch i {
    case [0=bitzero, 1=bitzero, 2=bitone, 3=bitzero] -> match_success := 1
    case _ -> match_success := i
  };

  (* slice update *)
  i[0] := bitzero;
  i[2 .. 3] := [bitone, bitone];

  (* slice access of literal *)
  v[0];
}