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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
default Order dec
$include <prelude.sail>
type xlen : Int = 32
type xlen_bytes : Int = 4
type xlenbits : Type = bits(xlen)
type regno ('n : Int), 0 <= 'n < 32 = atom('n)
type regbits = bits(5)
val regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
function regbits_to_regno b = unsigned(b)
enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
/* Architectural state */
register R1 : xlenbits
register R2 : xlenbits
register R3 : xlenbits
register R4 : xlenbits
register R5 : xlenbits
register R6 : xlenbits
register R7 : xlenbits
register R8 : xlenbits
register R9 : xlenbits
register R10 : xlenbits
register R11 : xlenbits
register R12 : xlenbits
register R13 : xlenbits
register R14 : xlenbits
register R15 : xlenbits
register R16 : xlenbits
register R17 : xlenbits
register R18 : xlenbits
register R19 : xlenbits
register R20 : xlenbits
register R21 : xlenbits
register R22 : xlenbits
register R23 : xlenbits
register R24 : xlenbits
register R25 : xlenbits
register R26 : xlenbits
register R27 : xlenbits
register R28 : xlenbits
register R29 : xlenbits
register R30 : xlenbits
register R31 : xlenbits
/* Getters and setters for X registers (special case for zeros register, x0) */
val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
function rX(r) = {
if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
else if r == 1 then R1
else if r == 2 then R2
else if r == 3 then R3
else if r == 4 then R4
else if r == 5 then R5
else if r == 6 then R6
else if r == 7 then R7
else if r == 8 then R8
else if r == 9 then R9
else if r == 10 then R10
else if r == 11 then R11
else if r == 12 then R12
else if r == 13 then R13
else if r == 14 then R14
else if r == 15 then R15
else if r == 16 then R16
else if r == 17 then R17
else if r == 18 then R18
else if r == 19 then R19
else if r == 20 then R20
else if r == 21 then R21
else if r == 22 then R22
else if r == 23 then R23
else if r == 24 then R24
else if r == 25 then R25
else if r == 26 then R26
else if r == 27 then R27
else if r == 28 then R28
else if r == 29 then R29
else if r == 30 then R30
else R31
}
val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
function wX(r, v) = {
if r == 0 then ()
else if r == 1 then R1 = v
else if r == 2 then R2 = v
else if r == 3 then R3 = v
else if r == 4 then R4 = v
else if r == 5 then R5 = v
else if r == 6 then R6 = v
else if r == 7 then R7 = v
else if r == 8 then R8 = v
else if r == 9 then R9 = v
else if r == 10 then R10 = v
else if r == 11 then R11 = v
else if r == 12 then R12 = v
else if r == 13 then R13 = v
else if r == 14 then R14 = v
else if r == 15 then R15 = v
else if r == 16 then R16 = v
else if r == 17 then R17 = v
else if r == 18 then R18 = v
else if r == 19 then R19 = v
else if r == 20 then R20 = v
else if r == 21 then R21 = v
else if r == 22 then R22 = v
else if r == 23 then R23 = v
else if r == 24 then R24 = v
else if r == 25 then R25 = v
else if r == 26 then R26 = v
else if r == 27 then R27 = v
else if r == 28 then R28 = v
else if r == 29 then R29 = v
else if r == 30 then R30 = v
else R31 = v
}
val rX_bits : bits(5) -> xlenbits effect {rreg}
function rX_bits(r) = rX(regbits_to_regno(r))
val wX_bits : (bits(5), xlenbits) -> unit effect {wreg}
function wX_bits(r,v) = wX(regbits_to_regno(r), v)
overload X = {rX, wX, rX_bits, wX_bits}
scattered union ast
union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
val decode : bits(32) -> option(ast) effect pure
val execute : ast -> unit effect {rmem, rreg, wreg}
function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
= Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
let rs1_val = X(rs1) in
let imm_ext : xlenbits = sail_sign_extend(imm, sizeof(xlen)) in
let result = rs1_val + imm_ext in
X(rd) = result
function clause decode _ = None()
$property
function prop(imm: bits(12), rs1: regbits, rd: regbits) -> bool = {
let v = X(rs1);
match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
Some(instr) => {
execute(instr);
X(rd) == v + sail_sign_extend(imm, sizeof(xlen))
},
_ => false
}
}
|
