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
|
default Order dec
$include <prelude.sail>
register R0 : bits(32)
register R1 : bits(32)
register R2 : bits(32)
register R3 : bits(32)
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
let GPRs = [ref R3, ref R2, ref R1, ref R0]
function wGPR(n: range(0, 3), v: bits(32)) -> unit = {
(*GPRs[n]) = v
}
function rGPR(n: range(0, 3)) -> bits(32) = {
reg_deref(GPRs[n])
}
overload R = {wGPR, rGPR}
$property
function prop() -> bool = {
R(0) = 0x1234_5679;
R(0) == 0x1234_5678
}
|
