[Libre-soc-bugs] [Bug 340] formal proof of POWER9 SHIFTROT pipeline needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #8 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #7)
> ok suggestion there is to write some short program that actually prints out
> the values.

I'm not sure how this would help, as that would just tell me the same
information that GTKWave is reporting, no?

The other question I had, upon further reflection, is that we have three types
of RLC instructions, but one of them (rlwimi) has different behavior.  Once
this masking bug is resolved, this will become another failure in the proofs. 
To work around this, I need to actually check the major opcode (m_fields.OPCD).
 I have *not* implemented that yet, but will shortly.  Should we assign a
different OP_RLCxxx token for rlwimi because of this?  Or, is there some other
field I should check that tells me whether or not I should OR-in the (a &
~mask) part of the result?

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