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
|
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
/* address ranges */
// [min, max) of the matching range, in units of 4 bytes.
type pmp_addr_range_in_words = option((xlenbits, xlenbits))
function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range_in_words = {
match pmpAddrMatchType_of_bits(cfg[A]) {
OFF => None(),
TOR => { Some ((prev_pmpaddr, pmpaddr)) },
NA4 => {
// NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg().
assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1.");
let lo = pmpaddr;
Some((lo, lo + 4))
},
NAPOT => {
// Example pmpaddr: 0b00010101111
// ^--- last 0 dictates region size & alignment
let mask = pmpaddr ^ (pmpaddr + 1);
// pmpaddr + 1: 0b00010110000
// mask: 0b00000011111
// ~mask: 0b11111100000
let lo = pmpaddr & (~ (mask));
// mask + 1: 0b00000100000
let len = mask + 1;
Some((lo, (lo + len)))
}
}
}
/* permission checks */
val pmpCheckRWX: (Pmpcfg_ent, AccessType(ext_access_type)) -> bool
function pmpCheckRWX(ent, acc) = {
match acc {
Read(_) => ent[R] == 0b1,
Write(_) => ent[W] == 0b1,
ReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1,
Execute() => ent[X] == 0b1
}
}
// 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 pmpLocked(ent)
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_in_words) -> pmpAddrMatch = {
match rng {
None() => PMP_NoMatch,
Some((lo, hi)) => {
// Convert to integers.
let addr = unsigned(addr);
let width = unsigned(width);
// These are in units of 4 bytes.
let lo = unsigned(lo) * 4;
let hi = unsigned(hi) * 4;
if hi <= lo /* to handle mis-configuration */
then PMP_NoMatch
else {
if (addr + width <= lo) | (hi <= addr)
then PMP_NoMatch
else if (lo <= addr) & (addr + width <= 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 accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType =
match acc {
Read(_) => E_Load_Access_Fault(),
Write(_) => E_SAMO_Access_Fault(),
ReadWrite(_) => E_SAMO_Access_Fault(),
Execute() => E_Fetch_Access_Fault(),
}
function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: int('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
foreach (i from 0 to 63) {
let prev_pmpaddr = (if i > 0 then pmpReadAddrReg(i - 1) else zeros());
match pmpMatchEntry(addr, width, acc, priv, pmpcfg_n[i], pmpReadAddrReg(i), prev_pmpaddr) {
PMP_Success => { return None(); },
PMP_Fail => { return Some(accessToFault(acc)); },
PMP_Continue => (),
}
};
if priv == Machine then None() else Some(accessToFault(acc))
}
function init_pmp() -> unit = {
assert(
sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64,
"sys_pmp_count() must be 0, 16, or 64"
);
foreach (i from 0 to 63) {
// On reset the PMP register's A and L bits are set to 0 unless the plaform
// mandates a different value.
pmpcfg_n[i] = [pmpcfg_n[i] with A = pmpAddrMatchType_to_bits(OFF), L = 0b0];
};
}
|
