[libre-riscv-dev] [Bug 335] New: Formal Correctness Proof for Branch pipeline

[libre-riscv-dev] [Bug 335] New: Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

            Bug ID: 335
           Summary: Formal Correctness Proof for Branch pipeline
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Mac OS
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: lkcl@lkcl.net
          Reporter: lkcl@lkcl.net
                CC: libre-riscv-dev@lists.libre-riscv.org
   NLnet milestone: ---

a formal correctness proof is needed for the branch pipeline.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
 total budget (EUR)|0                           |300
  for completion of|                            |
       task and all|                            |
           subtasks|                            |
           Assignee|lkcl@lkcl.net               |mtnolan2640@gmail.com
    NLnet milestone|---                         |NLNet.2019.10.Formal
             Blocks|                            |313
    parent task for|                            |195
  budget allocation|                            |


Referenced Bugs:

https://bugs.libre-soc.org/show_bug.cgi?id=313
[Bug 313] Create Branch Pipeline for POWER9
-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #1 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #2 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
just did my usual makes-me-happy variable name munging

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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]):

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #4 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #6 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
                # 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?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
>                 comb += Assert(dut.o.ctr.data != BO[2])

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

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #8 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #9 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #10 from Michael Nolan <mtnolan2640@gmail.com> ---
(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).

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #11 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev