From 5ea3ed47fee23d01fc4a8a110ff90929a287802d Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 22 Jul 2020 13:53:43 +0100 Subject: [PATCH] comments, add page spec numbers for branch ops into proof --- src/soc/fu/branch/formal/proof_main_stage.py | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py index ebf19006..fcb214a3 100644 --- a/src/soc/fu/branch/formal/proof_main_stage.py +++ b/src/soc/fu/branch/formal/proof_main_stage.py @@ -107,15 +107,15 @@ class Driver(Elaboratable): with m.Else(): comb += ctr_m.eq(ctr) - # CTR combpare with 0 + # CTR (32/64 bit) compare with 0 ctr_ok = Signal() comb += ctr_ok.eq(BO[2] | ((ctr_m != 0) ^ BO[1])) - # Sorry, not bothering with 32 bit right now - with m.Switch(rec.insn_type): - #### b #### + ### + # b - v3.0B p37 + ### with m.Case(MicrOp.OP_B): # Extract target address LI = i_fields.LI[0:-1] @@ -140,7 +140,9 @@ class Driver(Elaboratable): # Assert that ctr is not written to comb += Assert(dut.o.ctr.ok == 0) - #### bc #### + #### + # bc - v3.0B p37-38 + #### with m.Case(MicrOp.OP_BC): # Assert that branches are conditional comb += Assert(nia_o.ok == (cond_ok & ctr_ok)) @@ -166,7 +168,9 @@ class Driver(Elaboratable): with m.Else(): comb += Assert(dut.o.ctr.ok == 0) - #### bctar/bcctr/bclr #### + ################## + # bctar/bcctr/bclr - v3.0B p38-39 + ################## with m.Case(MicrOp.OP_BCREG): # assert that the condition is good comb += Assert(nia_o.ok == (cond_ok & ctr_ok)) -- 2.30.2