Assert that ctr is only written when needed

diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py
index 666f937724221b40616da1a66323e03029e1fa0a..2ff11b68ff945cd5915dd8ff5b6664e7266507aa 100644 (file)
--- a/src/soc/fu/branch/formal/proof_main_stage.py
+++ b/src/soc/fu/branch/formal/proof_main_stage.py
@@ -121,6 +121,9 @@ class Driver(Elaboratable):
                 with m.Else():
                     comb += Assert(lr_o.ok == 0)
 
+                # Assert that ctr is not written to
+                comb += Assert(dut.o.ctr.ok == 0)
+
             #### bc ####
             with m.Case(InternalOp.OP_BC):
                 # Assert that branches are conditional
@@ -143,7 +146,9 @@ class Driver(Elaboratable):
                 # Check that CTR is decremented
                 with m.If(~BO[2]):
                     comb += Assert(dut.o.ctr.data == ctr_next)
-
+                    comb += Assert(dut.o.ctr.ok == 1)
+                with m.Else():
+                    comb += Assert(dut.o.ctr.ok == 0)
             #### bctar/bcctr/bclr ####
             with m.Case(InternalOp.OP_BCREG):
                 # assert that the condition is good
@@ -161,7 +166,9 @@ class Driver(Elaboratable):
                 # Check that CTR is decremented
                 with m.If(~BO[2]):
                     comb += Assert(dut.o.ctr.data == ctr_next)
-                comb += Assert(dut.o.ctr.ok != BO[2])
+                    comb += Assert(dut.o.ctr.ok == 1)
+                with m.Else():
+                    comb += Assert(dut.o.ctr.ok == 0)
 
         return m
 

diff --git a/src/soc/fu/branch/main_stage.py b/src/soc/fu/branch/main_stage.py
index cf7d48f45809cd2f48bf65a18855cff0f1995e1f..03c65118efd401b5ba6807413c668b84da29aa68 100644 (file)
--- a/src/soc/fu/branch/main_stage.py
+++ b/src/soc/fu/branch/main_stage.py
@@ -88,6 +88,10 @@ class BranchMainStage(PipeModBase):
         cr_bit = Signal(reset_less=True)
         comb += cr_bit.eq(cr_bits[BI])
 
+        # Whether ctr is written to on a conditional branch
+        ctr_write = Signal(reset_less=True)
+        comb += ctr_write.eq(0)
+
         # Whether the conditional branch should be taken
         bc_taken = Signal(reset_less=True)
         with m.If(BO[2]):
@@ -97,7 +101,7 @@ class BranchMainStage(PipeModBase):
             ctr_n = Signal(64, reset_less=True)
             comb += ctr_n.eq(ctr - 1)
             comb += ctr_o.data.eq(ctr_n)
-            comb += ctr_o.ok.eq(1)
+            comb += ctr_write.eq(1)
             # take either all 64 bits or only 32 of post-incremented counter
             ctr_m = Signal(64, reset_less=True)
             with m.If(op.is_32bit):
@@ -126,10 +130,12 @@ class BranchMainStage(PipeModBase):
                 BD = b_fields.BD[0:-1]
                 comb += br_imm_addr.eq(br_ext(BD))
                 comb += br_taken.eq(bc_taken)
+                comb += ctr_o.ok.eq(ctr_write)
             #### branch conditional reg ####
             with m.Case(InternalOp.OP_BCREG):
                 comb += br_imm_addr.eq(spr1) # SPR1 is set by decode unit
                 comb += br_taken.eq(bc_taken)
+                comb += ctr_o.ok.eq(ctr_write)
 
         # output next instruction address
         comb += nia_o.data.eq(br_addr)