Skip to content

Commit 1776d88

Browse files
trdthgtrdthg
committed
Add VU and VS privilege level
- Add VirtualUser and VirtualSupervisor to the existing Privilege enum - Add virt_mode - Rename priv_level to nom_priv_bits - Add mapping between Privilege and (nom_priv_bits, priv_mode) - Add placeholder to all match cur_privilege statements, mark VS and VU branches as unimplemented - Add TODO comments for places where VS/VUs need to be handled
1 parent c204a16 commit 1776d88

10 files changed

+136
-75
lines changed

‎model/riscv_insts_base.sail

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -521,14 +521,17 @@ mapping clause encdec = ECALL()
521521
<-> 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
522522

523523
function clause execute ECALL() = {
524-
let t : sync_exception =
525-
struct { trap = match (cur_privilege) {
526-
User => E_U_EnvCall(),
527-
Supervisor => E_S_EnvCall(),
528-
Machine => E_M_EnvCall()
529-
},
530-
excinfo = (None() : option(xlenbits)),
531-
ext = None() };
524+
let t : sync_exception = struct {
525+
trap = match (cur_privilege) {
526+
User => E_U_EnvCall(),
527+
Supervisor => E_S_EnvCall(),
528+
Machine => E_M_EnvCall(),
529+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
530+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
531+
},
532+
excinfo = (None() : option(xlenbits)),
533+
ext = None(),
534+
};
532535
Trap(cur_privilege, CTL_TRAP(t), PC)
533536
}
534537

@@ -563,7 +566,9 @@ function clause execute SRET() = {
563566
let sret_illegal : bool = match cur_privilege {
564567
User => true,
565568
Supervisor => not(currentlyEnabled(Ext_S)) | mstatus[TSR] == 0b1,
566-
Machine => not(currentlyEnabled(Ext_S))
569+
Machine => not(currentlyEnabled(Ext_S)),
570+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
571+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
567572
};
568573
if sret_illegal
569574
then Illegal_Instruction()
@@ -600,7 +605,9 @@ function clause execute WFI() =
600605
Supervisor => if mstatus[TW] == 0b1
601606
then Illegal_Instruction()
602607
else Enter_Wait(WAIT_WFI),
603-
User => Illegal_Instruction()
608+
User => Illegal_Instruction(),
609+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
610+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
604611
}
605612

606613
mapping clause assembly = WFI() <-> "wfi"
@@ -624,7 +631,9 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
624631
0b1 => Illegal_Instruction(),
625632
0b0 => { flush_TLB(asid, addr); RETIRE_SUCCESS },
626633
},
627-
Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS }
634+
Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS },
635+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
636+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
628637
}
629638
}
630639

‎model/riscv_insts_svinval.sail

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ mapping clause encdec = SFENCE_W_INVAL()
3232
function clause execute SFENCE_W_INVAL() = {
3333
if cur_privilege == User
3434
then Illegal_Instruction()
35+
// TODO: VU-mode raises a virtual-instruction exception
3536
else RETIRE_SUCCESS // Implemented as no-op as all memory operations are visible immediately the current Sail model
3637
}
3738

@@ -48,7 +49,12 @@ mapping clause encdec = SFENCE_INVAL_IR()
4849
function clause execute SFENCE_INVAL_IR() = {
4950
if cur_privilege == User
5051
then Illegal_Instruction()
52+
// TODO: VU-mode raises a virtual-instruction exception
5153
else RETIRE_SUCCESS // Implemented as no-op as all memory operations are visible immediately in current Sail model
5254
}
5355

5456
mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir"
57+
58+
/* ****************************************************************** */
59+
60+
// TODO: Implement HINVAL.VVMA amd HINVAL.GVMA

‎model/riscv_insts_zicbom.sail

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,10 +50,13 @@ enum checked_cbop = {CBOP_ILLEGAL, CBOP_ILLEGAL_VIRTUAL, CBOP_INVAL_FLUSH, CBOP_
5050
// Select the cbop to perform based on the privilege.
5151
function cbop_priv_check(p: Privilege) -> checked_cbop = {
5252
let mCBIE : cbie = encdec_cbie(menvcfg[CBIE]);
53+
// TODO: check henvcfg after hyppervisor is implemented
5354
let sCBIE : cbie = if currentlyEnabled(Ext_S)
5455
then encdec_cbie(senvcfg[CBIE])
5556
else encdec_cbie(menvcfg[CBIE]);
5657
match (p, mCBIE, sCBIE) {
58+
(VirtualUser, _, _) => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
59+
(VirtualSupervisor, _, _) => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
5760
(Machine, _, _ ) => CBOP_INVAL_INVAL,
5861
(_, CBIE_ILLEGAL, _ ) => CBOP_ILLEGAL, // (priv_mode != M) && mCBIE == 00
5962
(User, _, CBIE_ILLEGAL ) => CBOP_ILLEGAL, // (priv_mode == U) && sCBIE == 00

‎model/riscv_smcntrpmf.sail

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ function legalize_smcntrpmf(c : CountSmcntrpmf, value : bits(64)) -> CountSmcntr
1515
MINH = v[MINH],
1616
SINH = if currentlyEnabled(Ext_S) then v[SINH] else 0b0,
1717
UINH = if currentlyEnabled(Ext_U) then v[UINH] else 0b0,
18-
// VSINH = v[VSINH],
19-
// VUINH = v[VUINH],
18+
VSINH = if currentlyEnabled(Ext_H) then v[VSINH] else 0b0,
19+
VUINH = if currentlyEnabled(Ext_H) then v[VUINH] else 0b0,
2020
]
2121
}
2222

@@ -48,10 +48,11 @@ function clause write_CSR((0x722, value) if xlen == 32) = { minstretcfg = legali
4848
function counter_priv_filter_bit(reg : CountSmcntrpmf, priv : Privilege) -> bits(1) =
4949
// When all xINH bits are zero, event counting is enabled in all modes.
5050
match priv {
51-
Machine => reg[MINH],
52-
Supervisor => reg[SINH],
53-
User => reg[UINH],
54-
// TODO: VSINH, VUINH when those modes are defined
51+
Machine => reg[MINH],
52+
Supervisor => reg[SINH],
53+
VirtualSupervisor => reg[VSINH],
54+
User => reg[UINH],
55+
VirtualUser => reg[VUINH],
5556
}
5657

5758
function should_inc_mcycle(priv : Privilege) -> bool =

‎model/riscv_sscofpmf.sail

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,8 @@ function get_scountovf(priv : Privilege) -> bits(32) = {
7272
Machine => overflow,
7373
Supervisor => overflow & mcounteren.bits,
7474
User => internal_error(__FILE__, __LINE__, "scountovf not readable from User mode"),
75+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
76+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
7577
}
7678
}
7779

‎model/riscv_sys_control.sail

Lines changed: 52 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
/* CSR access control */
1212

1313
function csrAccess(csr : csreg) -> csrRW = csr[11..10]
14-
function csrPriv(csr : csreg) -> priv_level = csr[9..8]
14+
function csrPriv(csr : csreg) -> nom_priv_bits = csr[9..8]
1515

1616
// Check that the CSR access is made with sufficient privilege.
1717
function check_CSR_priv(csr : csreg, p : Privilege) -> bool =
@@ -21,15 +21,19 @@ function check_CSR_priv(csr : csreg, p : Privilege) -> bool =
2121
function check_CSR_access(csr : csreg, isWrite : bool) -> bool =
2222
not(isWrite & (csrAccess(csr) == 0b11))
2323

24+
// TODO: check VS/VU-mode if hypervisor enabled
2425
function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
2526
not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1)
2627

2728
// There are several features that are controlled by machine/supervisor enable
2829
// bits (m/senvcfg, m/scounteren, etc.). This abstracts that logic.
30+
// TODO: check hcounteren if hypervisor enabled
2931
function feature_enabled_for_priv(p : Privilege, machine_enable_bit : bit, supervisor_enable_bit : bit) -> bool = match p {
3032
Machine => true,
3133
Supervisor => machine_enable_bit == bitone,
3234
User => machine_enable_bit == bitone & (not(currentlyEnabled(Ext_S)) | supervisor_enable_bit == bitone),
35+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
36+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
3337
}
3438

3539
// Return true if the counter is enabled OR the CSR is not a counter.
@@ -46,8 +50,13 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = {
4650
function check_Stimecmp(csr : csreg, p : Privilege) -> bool = {
4751
// Check if it is not stimecmp.
4852
if csr != 0x14D & csr != 0x15D then return true;
49-
50-
p == Machine | (p == Supervisor & mcounteren[TM] == 0b1 & menvcfg[STCE] == 0b1)
53+
match p {
54+
Machine => true,
55+
Supervisor => mcounteren[TM] == 0b1 & menvcfg[STCE] == 0b1,
56+
User => false,
57+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
58+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
59+
}
5160
}
5261

5362
/* Seed may only be accessed if we are doing a write, and access has been
@@ -64,6 +73,8 @@ function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = {
6473
Machine => true,
6574
Supervisor => false, /* TODO: base this on mseccfg */
6675
User => false, /* TODO: base this on mseccfg */
76+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
77+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
6778
}
6879
}
6980
}
@@ -105,6 +116,7 @@ val valid_reservation = pure {interpreter: "Platform.valid_reservation", c: "val
105116
function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
106117
let idx = num_of_ExceptionType(e);
107118
let super = bit_to_bool(medeleg.bits[idx]);
119+
// TODO: check VS/VU-mode if hypervisor extension enabled
108120
let deleg = if currentlyEnabled(Ext_S) & super then Supervisor else Machine;
109121
/* We cannot transition to a less-privileged mode. */
110122
if privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
@@ -133,6 +145,7 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
133145
*
134146
* This is used when the hart is in the Active state.
135147
*/
148+
// TODO: check hip/hie if hypervisor enabled.
136149
function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
137150
// mideleg can only be non-zero if we support Supervisor mode.
138151
assert(currentlyEnabled(Ext_S) | mideleg.bits == zeros());
@@ -216,6 +229,8 @@ function track_trap(p : Privilege) -> unit = {
216229
csr_write_callback("sepc", sepc);
217230
},
218231
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
232+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
233+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
219234
};
220235
}
221236

@@ -230,54 +245,60 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
230245

231246
match (del_priv) {
232247
Machine => {
233-
mcause[IsInterrupt] = bool_to_bits(intr);
234-
mcause[Cause] = zero_extend(c);
248+
mcause[IsInterrupt] = bool_to_bits(intr);
249+
mcause[Cause] = zero_extend(c);
235250

236-
mstatus[MPIE] = mstatus[MIE];
237-
mstatus[MIE] = 0b0;
238-
mstatus[MPP] = privLevel_to_bits(cur_privilege);
239-
mtval = tval(info);
240-
mepc = pc;
251+
mstatus[MPIE] = mstatus[MIE];
252+
mstatus[MIE] = 0b0;
253+
mstatus[MPP] = privLevel_to_bits(cur_privilege);
254+
mtval = tval(info);
255+
mepc = pc;
241256

242-
cur_privilege = del_priv;
257+
cur_privilege = del_priv;
243258

244-
handle_trap_extension(del_priv, pc, ext);
259+
handle_trap_extension(del_priv, pc, ext);
245260

246-
track_trap(del_priv);
261+
track_trap(del_priv);
247262

248-
prepare_trap_vector(del_priv, mcause)
263+
prepare_trap_vector(del_priv, mcause)
249264
},
250265
Supervisor => {
251-
assert (currentlyEnabled(Ext_S), "no supervisor mode present for delegation");
266+
assert (currentlyEnabled(Ext_S), "no supervisor mode present for delegation");
252267

253-
scause[IsInterrupt] = bool_to_bits(intr);
254-
scause[Cause] = zero_extend(c);
268+
scause[IsInterrupt] = bool_to_bits(intr);
269+
scause[Cause] = zero_extend(c);
255270

256-
mstatus[SPIE] = mstatus[SIE];
257-
mstatus[SIE] = 0b0;
258-
mstatus[SPP] = match cur_privilege {
259-
User => 0b0,
260-
Supervisor => 0b1,
261-
Machine => internal_error(__FILE__, __LINE__, "invalid privilege for s-mode trap")
262-
};
263-
stval = tval(info);
264-
sepc = pc;
271+
mstatus[SPIE] = mstatus[SIE];
272+
mstatus[SIE] = 0b0;
273+
mstatus[SPP] = match cur_privilege {
274+
User => 0b0,
275+
Supervisor => 0b1,
276+
Machine => internal_error(__FILE__, __LINE__, "invalid privilege for s-mode trap"),
277+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
278+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
279+
};
280+
stval = tval(info);
281+
sepc = pc;
265282

266-
cur_privilege = del_priv;
283+
cur_privilege = del_priv;
267284

268-
handle_trap_extension(del_priv, pc, ext);
285+
handle_trap_extension(del_priv, pc, ext);
269286

270-
track_trap(del_priv);
287+
track_trap(del_priv);
271288

272-
prepare_trap_vector(del_priv, scause)
289+
prepare_trap_vector(del_priv, scause)
273290
},
274291
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
292+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
293+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
275294
};
276295
}
277296

278297
function exception_handler(cur_priv : Privilege, ctl : ctl_result,
279298
pc: xlenbits) -> xlenbits = {
280299
match (cur_priv, ctl) {
300+
(VirtualUser, _) => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
301+
(VirtualSupervisor, _) => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
281302
(_, CTL_TRAP(e)) => {
282303
let del_priv = exception_delegatee(e.trap, cur_priv);
283304
if get_config_print_platform()
@@ -289,7 +310,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
289310
let prev_priv = cur_privilege;
290311
mstatus[MIE] = mstatus[MPIE];
291312
mstatus[MPIE] = 0b1;
292-
cur_privilege = privLevel_of_bits(mstatus[MPP]);
313+
cur_privilege = privLevel_of_bits(mstatus[MPP], 0b0); // TODO: use mstatus[MPV] if hypervisor enabled
293314
mstatus[MPP] = privLevel_to_bits(if currentlyEnabled(Ext_U) then User else Machine);
294315
if cur_privilege != Machine
295316
then mstatus[MPRV] = 0b0;

‎model/riscv_sys_exceptions.sail

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,12 @@ function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -
2020
/* used for traps and ECALL */
2121
function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
2222
let tvec : Mtvec = match p {
23-
Machine => mtvec,
24-
Supervisor => stvec,
25-
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
26-
};
23+
Machine => mtvec,
24+
Supervisor => stvec,
25+
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
26+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
27+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
28+
};
2729
match tvec_addr(tvec, cause) {
2830
Some(epc) => epc,
2931
None() => internal_error(__FILE__, __LINE__, "Invalid tvec mode")
@@ -40,18 +42,22 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
4042
val get_xepc : Privilege -> xlenbits
4143
function get_xepc(p) =
4244
match p {
43-
Machine => align_pc(mepc),
44-
Supervisor => align_pc(sepc),
45-
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
45+
Machine => align_pc(mepc),
46+
Supervisor => align_pc(sepc),
47+
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
48+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
49+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
4650
}
4751

4852
val set_xepc : (Privilege, xlenbits) -> xlenbits
4953
function set_xepc(p, value) = {
5054
let target = legalize_xepc(value);
5155
match p {
52-
Machine => mepc = target,
53-
Supervisor => sepc = target,
54-
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
56+
Machine => mepc = target,
57+
Supervisor => sepc = target,
58+
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
59+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
60+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
5561
};
5662
target
5763
}

‎model/riscv_sys_regs.sail

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ function virtual_memory_supported() -> bool = {
150150
function lowest_supported_privLevel() -> Privilege =
151151
if currentlyEnabled(Ext_U) then User else Machine
152152

153-
function have_privLevel(priv : priv_level) -> bool =
153+
function have_privLevel(priv : nom_priv_bits) -> bool =
154154
match priv {
155155
0b00 => currentlyEnabled(Ext_U),
156156
0b01 => currentlyEnabled(Ext_S),
@@ -198,7 +198,7 @@ bitfield Mstatus : bits(64) = {
198198

199199
function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege =
200200
if t != InstructionFetch() & m[MPRV] == 0b1
201-
then privLevel_of_bits(m[MPP])
201+
then privLevel_of_bits(m[MPP], 0b0) // TODO: use m[MPP] if hypervisor enabled
202202
else priv
203203

204204
function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
@@ -296,7 +296,9 @@ function cur_architecture() -> Architecture = {
296296
match cur_privilege {
297297
Machine => misa[MXL],
298298
Supervisor => get_mstatus_SXL(mstatus),
299-
User => get_mstatus_UXL(mstatus)
299+
User => get_mstatus_UXL(mstatus),
300+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
301+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
300302
};
301303
architecture(a)
302304
}
@@ -390,6 +392,8 @@ function is_fiom_active() -> bool = {
390392
Machine => false,
391393
Supervisor => menvcfg[FIOM] == 0b1,
392394
User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1,
395+
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
396+
VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
393397
}
394398
}
395399

0 commit comments

Comments
 (0)