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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
/* address ranges */
// TODO: handle PMP grain > 4 (i.e. G > 0).
// TODO: handle the 34-bit paddr32 on RV32
/* [min, max) of the matching range. */
type pmp_addr_range = option((xlenbits, xlenbits))
function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = {
match pmpAddrMatchType_of_bits(cfg.A()) {
OFF => None(),
TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) },
NA4 => { // TODO: I find the spec unclear for entries marked NA4 and G = 1.
// (for G >= 2, it is the same as NAPOT). In particular, it affects
// whether pmpaddr[0] is always read as 0.
let lo = pmpaddr << 2;
Some((lo, lo + 4))
},
NAPOT => { let mask = pmpaddr ^ (pmpaddr + 1); // generate 1s in signifying bits
let lo = pmpaddr & (~ (mask));
let len = mask + 1;
Some((lo << 2, (lo + len) << 2))
}
}
}
/* permission checks */
val pmpCheckRWX: (Pmpcfg_ent, AccessType(ext_access_type)) -> bool
function pmpCheckRWX(ent, acc) = {
match acc {
Read(Data) => ent.R() == true,
Write(Data) => ent.W() == true,
ReadWrite(Data) => ent.R() == true & ent.W() == true,
Execute() => ent.X() == true
}
}
// this needs to be called with the effective current privilege.
val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
function pmpCheckPerms(ent, acc, priv) = {
match priv {
Machine => if ent.L() == true
then pmpCheckRWX(ent, acc)
else true,
_ => pmpCheckRWX(ent, acc)
}
}
/* matching logic */
enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match}
function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> pmpAddrMatch = {
match rng {
None() => PMP_NoMatch,
Some((lo, hi)) => if hi <_u lo /* to handle mis-configuration */
then PMP_NoMatch
else {
if (addr + width <_u lo) | (hi <_u addr)
then PMP_NoMatch
else if (lo <=_u addr) & (addr + width <=_u hi)
then PMP_Match
else PMP_PartialMatch
}
}
}
enum pmpMatch = {PMP_Success, PMP_Continue, PMP_Fail}
function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege,
ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmpMatch = {
let rng = pmpAddrRange(ent, pmpaddr, prev_pmpaddr);
match pmpMatchAddr(addr, width, rng) {
PMP_NoMatch => PMP_Continue,
PMP_PartialMatch => PMP_Fail,
PMP_Match => if pmpCheckPerms(ent, acc, priv)
then PMP_Success
else PMP_Fail
}
}
/* priority checks */
function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
let check : bool =
match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp1cfg, pmpaddr1, pmpaddr0) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp2cfg, pmpaddr2, pmpaddr1) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp3cfg, pmpaddr3, pmpaddr2) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp4cfg, pmpaddr4, pmpaddr3) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp5cfg, pmpaddr5, pmpaddr4) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp6cfg, pmpaddr6, pmpaddr5) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp7cfg, pmpaddr7, pmpaddr6) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp8cfg, pmpaddr8, pmpaddr7) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp9cfg, pmpaddr9, pmpaddr8) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp10cfg, pmpaddr10, pmpaddr9) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp11cfg, pmpaddr11, pmpaddr10) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp12cfg, pmpaddr12, pmpaddr11) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp13cfg, pmpaddr13, pmpaddr12) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp14cfg, pmpaddr14, pmpaddr13) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue =>
match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) {
PMP_Success => true,
PMP_Fail => false,
PMP_Continue => match priv {
Machine => true,
_ => false
}
}}}}}}}}}}}}}}}};
if check
then None()
else match acc {
Read(Data) => Some(E_Load_Access_Fault),
Write(Data) => Some(E_SAMO_Access_Fault),
ReadWrite(Data) => Some(E_SAMO_Access_Fault),
Execute() => Some(E_Fetch_Access_Fault)
}
}
function init_pmp() -> unit = {
pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF));
pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF));
pmp2cfg = update_A(pmp2cfg, pmpAddrMatchType_to_bits(OFF));
pmp3cfg = update_A(pmp3cfg, pmpAddrMatchType_to_bits(OFF));
pmp4cfg = update_A(pmp4cfg, pmpAddrMatchType_to_bits(OFF));
pmp5cfg = update_A(pmp5cfg, pmpAddrMatchType_to_bits(OFF));
pmp6cfg = update_A(pmp6cfg, pmpAddrMatchType_to_bits(OFF));
pmp7cfg = update_A(pmp7cfg, pmpAddrMatchType_to_bits(OFF));
pmp8cfg = update_A(pmp8cfg, pmpAddrMatchType_to_bits(OFF));
pmp9cfg = update_A(pmp9cfg, pmpAddrMatchType_to_bits(OFF));
pmp10cfg = update_A(pmp10cfg, pmpAddrMatchType_to_bits(OFF));
pmp11cfg = update_A(pmp11cfg, pmpAddrMatchType_to_bits(OFF));
pmp12cfg = update_A(pmp12cfg, pmpAddrMatchType_to_bits(OFF));
pmp13cfg = update_A(pmp13cfg, pmpAddrMatchType_to_bits(OFF));
pmp14cfg = update_A(pmp14cfg, pmpAddrMatchType_to_bits(OFF));
pmp15cfg = update_A(pmp15cfg, pmpAddrMatchType_to_bits(OFF))
}
|
