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
|
default Order dec
$include <prelude.sail>
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
register R0 : bits(64)
register R1 : bits(64)
register R2 : bits(64)
register R3 : bits(64)
let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
type regno('r: Int) -> Bool = 0 <= 'r <= 3
val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
(int('r), bits('d)) -> unit effect {wreg}
function set_R(r, data) = {
let R = GPRs[r];
(*R)['d - 1 .. 0] = data
}
val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
(implicit('d), int('r)) -> bits('d) effect {rreg}
function get_R(datasize, r) = {
let R = GPRs[r];
reg_deref(R)[datasize - 1 .. 0]
}
overload R = {set_R, get_R}
function main() -> unit = {
R(0) = 0xCAFE_CAFE_0000_0000;
R(0) = 0xFFFF_FFFF;
print_bits("R = ", R(0) : bits(64));
print_bits("R = ", R(0) : bits(32))
}
|
