diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-05-03 13:48:56 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-05-03 13:48:56 -0700 |
| commit | e884e955feed337100c791c705f65de709ec4a4b (patch) | |
| tree | 51cd04bc948e1ffb4e3ef598fcff278bfd0b5ddf /model/riscv_sys_control.sail | |
| parent | 7904e06ebb9106d58bbe026e169b792042a76ddc (diff) | |
| download | sail-riscv-e884e955feed337100c791c705f65de709ec4a4b.zip sail-riscv-e884e955feed337100c791c705f65de709ec4a4b.tar.gz sail-riscv-e884e955feed337100c791c705f65de709ec4a4b.tar.bz2 | |
Enable some asserts.
Diffstat (limited to 'model/riscv_sys_control.sail')
| -rw-r--r-- | model/riscv_sys_control.sail | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 41fe13a..d37ffc9 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -187,7 +187,7 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits * allows for example the M_Timer to be delegated to the U-mode. */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { - //assert(haveUsrMode()); + assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); let effective_pending = mip.bits() & mie.bits(); if effective_pending == EXTZ(0b0) then None() /* fast path */ else { @@ -227,7 +227,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege * Absence of U-mode implies absence of S-mode. */ if (~ (haveUsrMode())) | ((~ (haveSupMode())) & (~ (haveNExt()))) then { - //assert(priv == Machine); + assert(priv == Machine, "invalid current privilege"); let enabled_pending = mip.bits() & mie.bits(); match findPendingInterrupt(enabled_pending) { Some(i) => let r = (i, Machine) in Some(r), @@ -307,7 +307,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, mcause) }, Supervisor => { - //assert (haveSupMode()); + assert (haveSupMode(), "no supervisor mode present for delegation"); scause->IsInterrupt() = intr; scause->Cause() = EXTZ(c); @@ -331,7 +331,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, scause) }, User => { - //assert(haveUsrMode()); + assert(haveUsrMode(), "no user mode present for delegation"); ucause->IsInterrupt() = intr; ucause->Cause() = EXTZ(c); |