From ec0cd34b2e83933e19859986b86af51ccbc98492 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Sun, 24 May 2020 19:30:56 +0100 Subject: [PATCH] comment and add links to branch formal proof --- src/soc/fu/branch/formal/proof_main_stage.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py index ca8271f0..666f9377 100644 --- a/src/soc/fu/branch/formal/proof_main_stage.py +++ b/src/soc/fu/branch/formal/proof_main_stage.py @@ -1,5 +1,10 @@ # Proof of correctness for partitioned equal signal combiner # Copyright (C) 2020 Michael Nolan +""" +Links: +* https://bugs.libre-soc.org/show_bug.cgi?id=335 +* https://libre-soc.org/openpower/isa/branch/ +""" from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, signed, Array) @@ -93,6 +98,8 @@ class Driver(Elaboratable): comb += Assume(~rec.is_32bit) with m.Switch(rec.insn_type): + + #### b #### with m.Case(InternalOp.OP_B): # Extract target address LI = i_fields.LI[0:-1] @@ -114,6 +121,7 @@ class Driver(Elaboratable): with m.Else(): comb += Assert(lr_o.ok == 0) + #### bc #### with m.Case(InternalOp.OP_BC): # Assert that branches are conditional comb += Assert(nia_o.ok == (cond_ok & ctr_ok)) @@ -135,6 +143,8 @@ class Driver(Elaboratable): # Check that CTR is decremented with m.If(~BO[2]): comb += Assert(dut.o.ctr.data == ctr_next) + + #### bctar/bcctr/bclr #### with m.Case(InternalOp.OP_BCREG): # assert that the condition is good comb += Assert(nia_o.ok == (cond_ok & ctr_ok)) @@ -153,7 +163,6 @@ class Driver(Elaboratable): comb += Assert(dut.o.ctr.data == ctr_next) comb += Assert(dut.o.ctr.ok != BO[2]) - return m -- 2.30.2