[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 #12 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #10)
> (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?

https://libre-soc.org/openpower/isa/

i believe i add the links at the top of each source file.

i added the ones to  proof_main_stage.py a few days ago?

>  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. 

actually the pseudocode is taken directly from the v3.0B spec, using pdf2txt
and a *lot* of hand editing of the resultant dog's dinner mess.

> 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.

i use xpdf, and its search capability is pretty quick given it's a 1500 page
document.

start at the top and search "rfid" or "twi" and the sections which describe
each instruction come up pretty quickly.

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