Bug 335 - Formal Correctness Proof for Branch pipeline
Summary: Formal Correctness Proof for Branch pipeline
Status: IN_PROGRESS
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Mac OS
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on: 435
Blocks: 313
  Show dependency treegraph
 
Reported: 2020-05-21 14:04 BST by Luke Kenneth Casson Leighton
Modified: 2020-12-06 13:14 GMT (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 400
budget (EUR) for this task, excluding subtasks' budget: 400
parent task for budget allocation: 195
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
"lkcl"={amount=300, submitted=2020-12-06} "donated"={amount=100, submitted=2020-12-06}


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-05-21 14:04:53 BST
a formal correctness proof is needed for the branch pipeline.

* OP_B     - done
* OP_BC    - done
* OP_BCREG - done
Comment 1 Luke Kenneth Casson Leighton 2020-05-22 19:24:55 BST
(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.
Comment 2 Luke Kenneth Casson Leighton 2020-05-22 19:29:56 BST
just did my usual makes-me-happy variable name munging
Comment 3 Luke Kenneth Casson Leighton 2020-05-22 19:35:18 BST
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]):
Comment 4 Michael Nolan 2020-05-22 19:42:36 BST
(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.
Comment 5 Luke Kenneth Casson Leighton 2020-05-22 19:47:39 BST
(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.
Comment 6 Luke Kenneth Casson Leighton 2020-05-22 19:50:26 BST
                # 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?
Comment 7 Luke Kenneth Casson Leighton 2020-05-22 19:50:55 BST
>                 comb += Assert(dut.o.ctr.data != BO[2])

wait...             comb += Assert(dut.o.ctr.ok != BO[2])
Comment 8 Luke Kenneth Casson Leighton 2020-05-22 20:00:21 BST
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
Comment 9 Luke Kenneth Casson Leighton 2020-05-24 19:33:28 BST
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.
Comment 10 Michael Nolan 2020-05-24 20:20:03 BST
(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).
Comment 11 Luke Kenneth Casson Leighton 2020-05-25 01:22:11 BST
(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.
Comment 12 Luke Kenneth Casson Leighton 2020-07-21 21:24:09 BST
reopening: proof needs modifying as cia has moved to an immediate
Comment 13 Luke Kenneth Casson Leighton 2020-07-22 11:48:32 BST
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