pulp-platform / ara

The PULP Ara is a 64-bit Vector Unit, compatible with the RISC-V Vector Extension Version 1.0, working as a coprocessor to CORE-V's CVA6 core
Other
366 stars 129 forks source link

The hazards of different LMULs have not been considered in their entirety. #239

Open WEIhabi opened 1 year ago

WEIhabi commented 1 year ago

It was mentioned earlier https://github.com/pulp-platform/ara/issues/111 that a different LMUL might affect hazard, and the response given by the development team was to utilize stalling when the LMUL is changed (WAIT_STATE in the ara_dispatcher) to avoid this situation.

However, when we verified it using formal verification, we found the following errors.

image image image image image

When the first incoming instruction vslideup.vx,vl=144,EW16,LMUL=2,vs2=v0,vd=6,vm=1,stride=128 Next instruction is vadd vl=16,EW16,LMUL=1/2,vs1=v11, vs2=v7,vd=v31,vadd.vv v31, v7, v11

The original slideup instruction that would have written vd=6 would have written to v7 (because stride and LMUL=2), but the next vadd instruction would have already taken out the data from the source register, v7, and done the math. This causes the vadd instruction, which is supposed to stall and wait for v7 to be written back before taking out the data, to get the data that has not yet been written back beforehand, causing an error.

The main reason for this failure is that the stall mechanism in ara_dispatcher is not well thought out (only LMUL[2]=0 && LMUL_old > LMUL_new are taken into account).

To complete the above consider that it might be possible to rewrite it as follows:

if ((!vtype_q.vlmul[2] && (vtype_d.vlmul[2:0] < vtype_q.vlmul[2:0])) || (vtype_q.vlmul[2] && (vtype_d.vlmul[2:0] > vtype_q.vlmul[2:0])))
                  state_d = WAIT_IDLE;
end
mp-17 commented 1 year ago

Hello @WEIhabi, thanks for your extensive verification effort. Very appreciated. You are right, we did not take into account fractional LMULs when LMUL_new > LMUL_old. I will fix this in the next round of fixes.

Thanks again, Matteo