File: new_bitfields.sail

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (56 lines) | stat: -rw-r--r-- 1,106 bytes parent folder | download
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
default Order dec

$include <prelude.sail>

// We have a few variations of the same bitfield:

bitfield B : bits(32) = {
  Field0: (31..16 @ 7..0),
  Field1: 15..8
}

bitfield B2 : bits(32) = {
  Field0: 31..16 @ 7..0,
  Field1: 15..8
}

bitfield B3 : bits(32) = {
  Field0: 31..16 @ 7..0,
  Field1: 15..8,
}

bitfield B4 : bits(32) = {
  Field0: 31..16 @ 7..4 @ 3..0,
  Field1: 15..8,
}

bitfield B5 : bits(32) = {
  Field0: (31..16) @ 7..4 @ 3..0,
  Field1: 15..8,
}

bitfield B6 : bits(32) = {
  Field0: ((31..16) @ 7..4) @ 3..0,
  Field1: 15..8,
}

register R : B

function main() -> unit = {
  R[Field1] = 0x00;
  R[Field0] = 0x4711FF;
  assert(R[Field1] == 0x00);
  assert(R[Field0] == 0x4711FF);
  print_bits("R.bits=", R.bits);
  assert(R.bits == 0x471100FF);
  R = [R with Field0 = 0xFF0077];
  assert(R[Field1] == 0x00);
  assert(R[Field0] == 0xFF0077);
  print_bits("R.bits=", R.bits);
  assert(R.bits == 0xFF000077);
  R = [R with Field1 = 0x47, Field0 = 0x000011];
  assert(R[Field1] == 0x47);
  assert(R[Field0] == 0x000011);
  print_bits("R.bits=", R.bits);
  assert(R.bits == 0x00004711)
}