From 3896655e24bd2f2220382ded91a4920208fae318 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Sun, 24 May 2020 15:16:28 -0400 Subject: [PATCH] Assert that ctr is only written when needed --- src/soc/fu/branch/formal/proof_main_stage.py | 11 +++++++++-- src/soc/fu/branch/main_stage.py | 8 +++++++- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py index 666f9377..2ff11b68 100644 --- 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 cf7d48f4..03c65118 100644 --- 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) -- 2.30.2