[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 #2 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
here is the pseudocode pages for the ops implemented in TRAP.

https://libre-soc.org/openpower/isa/fixedtrap/
https://libre-soc.org/openpower/isa/sprset/
https://libre-soc.org/openpower/isa/system/

if you look closely at the regs they use (and set) you will notice that td/tw,
sc, rfid, mtmsr and mfmsr all have very similar register usage profiles, hence
why we put them all in the same pipeline.

in fact sc does basically nearly the exact same thing as an unconditional trap,
just with an address 0xc00 instead of 0x700

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