@@ -79,19 +79,6 @@ function pmpMatchAddr(
79
79
}
80
80
}
81
81
82
- enum pmpMatch = {PMP_Success , PMP_Continue , PMP_Fail }
83
-
84
- function pmpMatchEntry (addr : physaddr , width : xlenbits , acc : AccessType (ext_access_type ), priv : Privilege ,
85
- ent : Pmpcfg_ent , pmpaddr : xlenbits , prev_pmpaddr : xlenbits ) -> pmpMatch = {
86
- match pmpMatchAddr (addr , width , ent , pmpaddr , prev_pmpaddr ) {
87
- PMP_NoMatch => PMP_Continue ,
88
- PMP_PartialMatch => PMP_Fail ,
89
- PMP_Match => if pmpCheckRWX (ent , acc ) | (priv == Machine & not (pmpLocked (ent )))
90
- then PMP_Success
91
- else PMP_Fail
92
- }
93
- }
94
-
95
82
/* priority checks */
96
83
97
84
function accessToFault (acc : AccessType (ext_access_type )) -> ExceptionType =
@@ -112,12 +99,17 @@ function pmpCheck forall 'n, 0 < 'n <= max_mem_access . (
112
99
let width : xlenbits = to_bits (width );
113
100
114
101
foreach (i from 0 to 63 ) {
115
- let prev_pmpaddr = (if i > 0 then pmpReadAddrReg (i - 1 ) else zeros ());
116
- match pmpMatchEntry (addr , width , acc , priv , pmpcfg_n [i ], pmpReadAddrReg (i ), prev_pmpaddr ) {
117
- PMP_Success => { return None (); },
118
- PMP_Fail => { return Some (accessToFault (acc )); },
119
- PMP_Continue => (),
120
- }
102
+ let prev_pmpaddr = if i > 0 then pmpReadAddrReg (i - 1 ) else zeros ();
103
+
104
+ match pmpMatchAddr (addr , width , pmpcfg_n [i ], pmpReadAddrReg (i ), prev_pmpaddr ) {
105
+ PMP_NoMatch => (),
106
+ PMP_PartialMatch => return Some (accessToFault (acc )),
107
+ PMP_Match => return (
108
+ if pmpCheckRWX (cfg , acc ) | (priv == Machine & not (pmpLocked (cfg )))
109
+ then None ()
110
+ else Some (accessToFault (acc ))
111
+ ),
112
+ };
121
113
};
122
114
if priv == Machine then None () else Some (accessToFault (acc ))
123
115
}
0 commit comments