[Libre-soc-bugs] [Bug 421] TRAP pipeline formal correctness proof needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=421

--- Comment #25 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
samuel: regarding system call (sc) LEV, this is in the spec:

setting of the MSR is affected by the contents of the
LEV field. LEV values greater than 1 are reserved. Bits
0:5 of the LEV field (instruction bits 20:25) are treated
as a reserved field.

    Programming Note
If LEV=1 the hypervisor is invoked. This is the only
way that executing an instruction can cause hyper-
visor state to be entered.

note: like microwatt, we are *not* supporting hypervisor mode (yet).
we're code-tracking microwatt, so the proof needs to cover what
parts of the spec that *microwatt* implements, rather than "purely
and strictly the spec".

-- 
You are receiving this mail because:
You are on the CC list for the bug.