Bug 306

python3 alu/formal/proof_main_stage.py ..
----------------------------------------------------------------------
Ran 2 tests in 312.563s

wooow :)

(In reply to Luke Kenneth Casson Leighton from comment #1)
> python3 alu/formal/proof_main_stage.py ..
> ----------------------------------------------------------------------
> Ran 2 tests in 312.563s
> 
> wooow :)

Yeah, adding shifts to the proof *really* slowed it down

* OP_EXTS proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=32d9da2bd849d3ae9b59bdec7a4add0c35908922

* OP_CMP and OP_CMPEQB proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=ca79ab18a7fa9bdabeca860448d79b5d11dc222f

hmm

the same thing we noted in Branch, for CMPEQB is also not being picked up n the main_stage.py

https://libre-soc.org/openpower/isa/comparefixed/

cmpeqb is only supposed to alter the CR, not the main register RT.

the formal proof is not picking that up.

  70         comb += Assume(a[32:64] == 0)
  71         comb += Assume(b[32:64] == 0)

michael in the alu proof should those be conditional? with m.If(op.is_32bit)?

(In reply to Luke Kenneth Casson Leighton from comment #5)
>   70         comb += Assume(a[32:64] == 0)
>   71         comb += Assume(b[32:64] == 0)
> 
> michael in the alu proof should those be conditional? with m.If(op.is_32bit)?

oh, yep. Fixed.

(In reply to Michael Nolan from comment #6)
> (In reply to Luke Kenneth Casson Leighton from comment #5)
> >   70         comb += Assume(a[32:64] == 0)
> >   71         comb += Assume(b[32:64] == 0)
> > 
> > michael in the alu proof should those be conditional? with m.If(op.is_32bit)?
> 
> oh, yep. Fixed.

star.

assigning to Samuel for review of formal_main_stage.py up to this point:

        # Assert that op gets copied from the input to output
        for rec_sig in rec.ports():
            name = rec_sig.name
            dut_sig = getattr(dut.o.ctx.op, name)
            comb += Assert(dut_sig == rec_sig)

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;hb=HEAD#l56

from commit git diff 685b7 769a8, samuel did this:

+        # Output context is the same as the input context.
+        comb += Assert(dut.o.ctx != dut.i.ctx)

this is the reasonable expectation: both are Records.  should it be
ok to Assert that one Record's contents equals the contents of another?

a bug in cmp was found

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/main_stage.py;h=b2d2279cf80dec3670d70e5b65359c92a9794acf;hb=29d0566fd104ab8b9ffd0c460fc7c588a72a340b#l50

the proof needs updating to match

(In reply to Luke Kenneth Casson Leighton from comment #10)
> a bug in cmp was found
> 
> https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/main_stage.py;
> h=b2d2279cf80dec3670d70e5b65359c92a9794acf;
> hb=29d0566fd104ab8b9ffd0c460fc7c588a72a340b#l50
> 
> the proof needs updating to match

Can you explain the bug?  I see a link to line 50 of the main_stage.py file, but without more context, I don't know what I'm looking to fix in the proof.  Thanks.

(In reply to Samuel A. Falvo II from comment #11)

> Can you explain the bug?  I see a link to line 50 of the main_stage.py file,
> but without more context, I don't know what I'm looking to fix in the proof.
> Thanks.

ah sorry i should have recorded the diff-commit rather than a link to the line.
the "L" field was previously being completely ignored.

so where for example the pseudocode says this:

* cmp BF,L,RA,RB

    if L = 0 then
        a <-  EXTS((RA)[32:63] )
        b <- EXTS((RB)[32:63])
    else
        a <- (RA)
        b <- (RB)


we were in fact simply doing this:


* cmp BF,L,RA,RB

    a <- (RA)
    b <- (RB)


because this was in the proof *and* the HDL and there was no corresponding unit test to catch it, the bug went unnoticed for several months.