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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #4 from Michael Nolan <mtnolan2640 at 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.