[Libre-soc-dev] [OpenPOWER-HDL-Cores] bug in microwatt stfsu and stfdu

[Paul Mackerras]

On Wed, May 19, 2021 at 11:19:24AM +0100, Luke Kenneth Casson Leighton wrote:

> v3.0B book I chapter 4 page 145 section 4.6.3 states:
> 
> stfs FRS,D(RA)
> 
>    if RA = 0 then b <- 0
>     else           b <- (RA)
>     EA <- + EXTS(D)
> 
> but stfsu states simply:
> 
>     EA <- (RA) + EXTS(D)
> 
> thus we conclude that Major 53 is *wrong*, in1 should simply be RA *not*
> RA_OR_ZERO.
> 
> now that i'm looking at it, stfdu is also wrong.
> 
> stfsx is *correct*.  stfs is correct.  stfd is correct.  stfdux is
> *wrong*.  stfdx is correct.
> 
> basically needs a full review.  in the above *i'm assuming the spec is
> correct*.

Writing down for future reference what we discussed on the call:

The spec says, for the update-form floating-point loads and stores
({l,st}f[sd]u{,x}) that if RA=0 the instruction form is invalid.
The RTL doesn't specify the behaviour of invalid forms, which is why
it doesn't have the RA = 0 case which the non-update forms have.

Section 1.9.2 "Invalid Instruction Forms" says that executing an
invalid instruction form will either cause an illegal instruction
interrupt or yield boundedly undefined results.  "Boundedly undefined"
means a result that could have been obtained by executing a finite
sequence of instructions in the same processor state (defined in
section 1.3.1, more precisely than that quick summary).

My recollection is that I did some experiments with POWER9 and worked
out that for update-form loads and stores with RA = 0, it doesn't
cause an illegal instruction interrupt and it does use the value 0
rather than the contents of R0.  That's why microwatt has RA_OR_ZERO
in the decode table.

The 1000 test sequences in the microwatt repo and the sequences
generated by the simple_random program include invalid instruction
forms.  Getting those invalid forms to match P9 behaviour is necessary
for the results to match up - which they do.

Paul.