[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 #3 from Luke Kenneth Casson Leighton <lkcl at 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.