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
|
default Order dec
$include <prelude.sail>
$include <exception_basic.sail>
enum pred = {
P_false,
P_true
}
mapping decenc_p : bits(2) <-> pred = {
0b00 <-> P_true,
0b01 <-> P_false
}
scattered union ast
val encdec : ast <-> bits(16)
union clause ast = ABS : (pred, bits(10))
mapping clause encdec =
ABS(decenc_p(0b0 @ p), rd @ rs)
<-> 0b10011 @ p : bits(1) @ rd : bits(5) @ rs : bits(5)
function fetch(_: unit) -> bits(16) = {
0b10011 @ 0xFF @ 0b111
}
val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
function main () = {
let bin = fetch();
let ast = encdec(bin);
let bin' = encdec(ast);
assert(bin == bin');
print_bits("bin = ", bin);
print_bits("bin' = ", bin')
}
|
