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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon Jul 20 22:31:10 BST 2020


--- Comment #10 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #6)
> that's a bug, yay!  spec - in the pseudo-code - is this:
>     MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
>     MSR[3] <- (MSR[3] & SRR1[3])

Where do I find this and similar relevant pseudocode?  I've looked through the
wiki without success.  I've found a POWER9 ISA manual online, but it lacks
anything like the detail given above.  I've checked out the OpenPOWER ISA spec
3.0b that is linked from the wiki, and ... I have to admit I'm deeply flustered
by my inability to locate useful information in that document.

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

More information about the libre-soc-bugs mailing list