[OpenRISC] Error found in mor1kx cache lru

[OpenRISC] Error found in mor1kx cache lru

[Stafford Horne]

+CC list

Hi Harshita,

Thanks for reporting, could you also open a github issue with the
same details at:

 https://github.com/openrisc/mor1kx/issues

-Stafford

On Wed, May 26, 2021 at 02:52:11PM +0530, Harshitha S wrote:

> 
>      NUMWAYS = 4
>      current = 6'b110100;
>      access  = 4'b0010;
>    
>     This current history is:
>    
>       0<1 0<2 0<3 1<2 1<3 2<3
>       0   0   1   0   1   1
>     
>      History of access => 3>0>1>2
>      Access request is for 1, then expected order is 1>3>0>2.
>      Expected values of lru_post = 1 and lru_pre = 2
>  
> Initial expand matrix based on current history
> 
>         0     1      2      3         0 1 2 3
>    0    1    (0<1)  (0<2)  (0<3)    0 1 0 0 1
>    1  (1<0)    1    (1<2)  (1<3) => 1 1 1 0 1
>    2  (2<0)  (2<1)    1    (2<3)    2 1 1 1 1
>    3  (3<0)  (3<1)  (3<2)    1      3 0 0 0 1
> 
> lru_pre is AND of bits in a row
> 
> When request access=4'b0010 then 1st row of expand matrix is 
> replaced with zeros and 1st column of expand matrix is replaced 
> with 1.
> 
>      
>      
> The matrix changes accordingly
>       
>          0 1 2 3      0 1 2 3
>        0 1 0 0 1    0 1 1 0 1
>        1 1 1 0 1 => 1 0 1 0 0
>        2 1 1 1 1    2 1 1 1 1
>        3 0 0 0 1    3 0 1 0 1
> 
> lru_post is product of bits in a column
> 
> update = 6'b100101
> 
> This means updated history is
> 
>  0<1 0<2 0<3 1<2 1<3 2<3
>   1   0   1   0   0   1
> 
> This is what we interpret from output 1>3>0>2 and its same as our expectation.
> 
>    

[OpenRISC] Error found in mor1kx cache lru

[Harshitha S]

Sure, I will do that.

On Wed, 26 May, 2021, 5:45 PM Stafford Horne, <shorne@gmail.com> wrote:

> +CC list
>
> Hi Harshita,
>
> Thanks for reporting, could you also open a github issue with the
> same details at:
>
>  https://github.com/openrisc/mor1kx/issues
>
> -Stafford
>
> On Wed, May 26, 2021 at 02:52:11PM +0530, Harshitha S wrote:
>
> >
> >      NUMWAYS = 4
> >      current = 6'b110100;
> >      access  = 4'b0010;
> >
> >     This current history is:
> >
> >       0<1 0<2 0<3 1<2 1<3 2<3
> >       0   0   1   0   1   1
> >
> >      History of access => 3>0>1>2
> >      Access request is for 1, then expected order is 1>3>0>2.
> >      Expected values of lru_post = 1 and lru_pre = 2
> >
> > Initial expand matrix based on current history
> >
> >         0     1      2      3         0 1 2 3
> >    0    1    (0<1)  (0<2)  (0<3)    0 1 0 0 1
> >    1  (1<0)    1    (1<2)  (1<3) => 1 1 1 0 1
> >    2  (2<0)  (2<1)    1    (2<3)    2 1 1 1 1
> >    3  (3<0)  (3<1)  (3<2)    1      3 0 0 0 1
> >
> > lru_pre is AND of bits in a row
> >
> > When request access=4'b0010 then 1st row of expand matrix is
> > replaced with zeros and 1st column of expand matrix is replaced
> > with 1.
> >
> >
> >
> > The matrix changes accordingly
> >
> >          0 1 2 3      0 1 2 3
> >        0 1 0 0 1    0 1 1 0 1
> >        1 1 1 0 1 => 1 0 1 0 0
> >        2 1 1 1 1    2 1 1 1 1
> >        3 0 0 0 1    3 0 1 0 1
> >
> > lru_post is product of bits in a column
> >
> > update = 6'b100101
> >
> > This means updated history is
> >
> >  0<1 0<2 0<3 1<2 1<3 2<3
> >   1   0   1   0   0   1
> >
> > This is what we interpret from output 1>3>0>2 and its same as our
> expectation.
> >
> >
>
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.librecores.org/pipermail/openrisc/attachments/20210526/83e417f4/attachment.htm>

[OpenRISC] Error found in mor1kx cache lru

[Stafford Horne]

Hi All,

The github issue was added here:

https://github.com/openrisc/mor1kx/issues/119

Harshita thanks for you investigation and starting early on GSoC you
are already getting into some interesting parts.

On Wed, May 26, 2021 at 6:21 PM Harshitha S
<harshithasridhar172000@gmail.com> wrote:
>
> Hello Sir,
>
> I'm Harshitha, I was looking into the formal verification of mor1kx's cache LRU module and I found a bug there.
>
> I was expecting that the variable access request would be the new lru_post value, but it's not the case. lru_post is calculated as AND of rows but I think it has to be considered as AND of columns. I considered the same example as per your description, wrote a test bench to verify it. I got different update variable values that the code functionally executes. I corrected the code by modifying the lru_post computation, then I was able to get the access same as the lru_post.

I think its not correct, the lru_post is the least recently used from
history.  The access request is the "most recently used", so it will
not be in lru_post.

>
> I came across another unusual thing. In the code snippet where the expand matrix is updated, the row number for exchange is not computed before because of which the last row of the expand matrix is considered as one bit less by the formal tool. You can check the expand_error image for this error where the third row of the matrix has only 3 bits instead of 4.  I tried to precompute the row number for exchange then I didn't face this error. You can look into no_expand_error  where this issue was resolved.
>

That sounds strange, can you post a PR for this change?  or a patch
using 'git diff` its easier to explain code changes using patches.

> I request you to look into this error. Let me know what you think.
>
> Regards
> -Harshitha
>