blob: 300657df8f2b2660cf84aee342234a41732bf2c7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
default Order dec
$include <prelude.sail>
val "reg_deref" : forall ('a: Type). register('a) -> 'a effect {rreg}
register R0 : bits(32)
register R1 : bits(32)
register R2 : bits(32)
register R3 : bits(32)
let GPRs = [ref R3, ref R2, ref R1, ref R0]
$property
function prop() -> bool = {
R0 = 0xDEAD_BEEF;
reg_deref(GPRs[0]) == 0xDEAD_BEEF
}
|
