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

i meant as a smaller program rather than a much larger one.  i wrote a small
mask-printing test a few weeks ago, ran for loops from 0 to 63 and it was very
instructive.

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

it shouldn't.  or, microwatt has already taken it into consideration in the
design of rotator.py and how it is called from sr main_stage.py


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

no absolutely not.  the reason is because the CSV files come directly from
microwatt decode1.vhdl, the code was written by a team with *over 25* years
experience *each* in PowerISA, and we can trust they they know what they are
doing.

the way that microwatt (and libresoc) works is that the immediates are placed
into the RB input, as the second operand.

we therefore *lose and do not need* to even know that the instruction was an
immediate or a register variant.

all that the pipeline needs to know is: RA, RB and for this pipeline RS as
well.

however some operations also need mb and me fields so that is why rotator.py
takes extra parameters.


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

take a look at shift rot main_stage.py.  

you will see that rotator is called with some pretty clear decoding and
identification of the instructions

* left mask needed
* right mask needed
* is arithmetic 
* left_or_right

something like that.

but really: you really *do not* need to know it was an immediate variant or
not.  that has definitely been encoded into RB (and in the case of LDST into RA
as a zero).  look at DecodeInB in power_decode2 .py search for "imm_out" then
crossreference the CONST_xxx against the CSV files in isatables to see what is
going on.

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