[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

Samuel A. Falvo II <kc5tja at arrl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|CONFIRMED                   |IN_PROGRESS

--- Comment #31 from Samuel A. Falvo II <kc5tja at arrl.net> ---
I've completed implementing the properties for the trap pipeline; however,
there seems to be an irreconcilable issue with the trap pipeline.  For some
reason, during the execution of MTMSRD, (IBM) bit 30 of MSR remains in the
wrong state, and I've not been able to figure out why.  I've double-checked the
properties against the documented specs in the V3.0B specs (page 978); I've
also reviewed the code in main_stage.py.  I can't locate the discrepency.  I
will need someone else to take over from here.

Everything else, so far at least, seems to run OK.

Can someone please double-check and advise?  Thanks.

(I'm going to move this task to complete in my wiki page; but, if needed, I'll
move it back to in progress.)

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