(In reply to Michael Nolan from https://bugs.libre-soc.org/show_bug.cgi?id=313#38)
> I have a formal proof for branches now, I handled the CRs in a similar way
> to the CR unit so I know the CR handling is good.

great.  i notice the "not doing 32 bit" right now.

just did my usual makes-me-happy variable name munging

mmm... what about when op.lk is zero?

when op.lk is zero, we don't want dut.o.lr.ok to be set.

there's four cases to be covered

* rec.lk true, LK true
* rec.lk false, LK true
* rec.lk true, LK false
* rec.lk false, LK false

i belive dut.o.lr.ok should only be set when rec.lk is true and LK is true

however if i put "Assert lr_ok.ok == 0" the proof fails, indicating
a potential problem?


--- a/src/soc/fu/branch/formal/proof_main_stage.py
+++ b/src/soc/fu/branch/formal/proof_main_stage.py
@@ -129,6 +129,8 @@ class Driver(Elaboratable):
                     with m.If(LK & rec.lk):
                         comb += Assert(lr_o.data == (cia + 4)[0:64])
                         comb += Assert(lr_o.ok == 1)
+                    with m.Else():
+                        comb += Assert(lr_o.ok == rec.lk)
 
                 # Check that CTR is decremented
                 with m.If(~BO[2]):

(In reply to Luke Kenneth Casson Leighton from comment #3)
> mmm... what about when op.lk is zero?
> 
> when op.lk is zero, we don't want dut.o.lr.ok to be set.
> 
> there's four cases to be covered
> 
> * rec.lk true, LK true
> * rec.lk false, LK true
> * rec.lk true, LK false
> * rec.lk false, LK false
> 
> i belive dut.o.lr.ok should only be set when rec.lk is true and LK is true
> 
> however if i put "Assert lr_ok.ok == 0" the proof fails, indicating
> a potential problem?
> 
> 
> --- a/src/soc/fu/branch/formal/proof_main_stage.py
> +++ b/src/soc/fu/branch/formal/proof_main_stage.py
> @@ -129,6 +129,8 @@ class Driver(Elaboratable):
>                      with m.If(LK & rec.lk):
>                          comb += Assert(lr_o.data == (cia + 4)[0:64])
>                          comb += Assert(lr_o.ok == 1)
> +                    with m.Else():
> +                        comb += Assert(lr_o.ok == rec.lk)
>  
>                  # Check that CTR is decremented
>                  with m.If(~BO[2]):

Ah, it looks like power_decoder2 already handles this for us. It only sets dec2.e.lk if the instruction has the lk flag set in the table, and LK is set in the instruction field.

(In reply to Michael Nolan from comment #4)

> Ah, it looks like power_decoder2 already handles this for us. It only sets
> dec2.e.lk if the instruction has the lk flag set in the table, and LK is set
> in the instruction field.

yyeah i think that was me, doing something random (which i now don't
quite follow, but i did at the time).  this should be commented.

also it occurs to me that similar things need to be done to check that
{insert_data_thing}.ok == 0 at appropriate points, because the plan is to 
actually use those in the CompUnits, to set the "REQUEST_WRITE" flags.

if for example ctr.ok is set to 1 when it should not be, the CTR SPR
would get corrupted data sent to the register file.

                # Check that CTR is decremented
                with m.If(~BO[2]):
                    comb += Assert(dut.o.ctr.data == ctr_next)


i think... that one needs...

                comb += Assert(dut.o.ctr.data != BO[2])

does that look right?

>                 comb += Assert(dut.o.ctr.data != BO[2])

wait...             comb += Assert(dut.o.ctr.ok != BO[2])

commit 6c74707101355960956055ee586e81c26914d2f0 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Fri May 22 19:59:59 2020 +0100

    test branch ctr ok flag

hm i feel the need to assert that when the cases are not being enabled,
the registers not in use (not changed) should be Asserted 0
(self.o.{something}.ok == 0)

this because if they are not zero they will cause a request for a
register port write at the MultiCompUnit, which, because their data
(self.o.{something}.data) was not initialised, would cause regfile
corruption.

(In reply to Luke Kenneth Casson Leighton from comment #9)
> hm i feel the need to assert that when the cases are not being enabled,
> the registers not in use (not changed) should be Asserted 0
> (self.o.{something}.ok == 0)
> 
> this because if they are not zero they will cause a request for a
> register port write at the MultiCompUnit, which, because their data
> (self.o.{something}.data) was not initialised, would cause regfile
> corruption.

Good idea - done. Caught a bug where a regular branch would write to ctr if the branch immediate was just right (or wrong).

(In reply to Michael Nolan from comment #10)
> (In reply to Luke Kenneth Casson Leighton from comment #9)
> > hm i feel the need to assert that when the cases are not being enabled,
> > the registers not in use (not changed) should be Asserted 0
> > (self.o.{something}.ok == 0)
> > 
> > this because if they are not zero they will cause a request for a
> > register port write at the MultiCompUnit, which, because their data
> > (self.o.{something}.data) was not initialised, would cause regfile
> > corruption.
> 
> Good idea - done. Caught a bug where a regular branch would write to ctr if
> the branch immediate was just right (or wrong).

these are not fully showing up because we do not have writes to regfile(s) yet.  if we put together the regfiles and a quick link to the pipelines through the CompUnits interface, we pretty much have a working CPU done and can catch these things, because SPRs,  XER, etc will all be spuriously modified.

reopening: proof needs modifying as cia has moved to an immediate

commit 5e73a60c7beb52480dcf73469f597aa28b845227 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Wed Jul 22 11:41:44 2020 +0100

    fix branch main_stage proof, add ctr 32-bit, fix BCREG

commit 17849f9dd18fdb7564e299763e261b8a2c5ee7ad
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Wed Jul 22 11:14:32 2020 +0100

    rework branch proof to use br_input_record