OP_CMPEQB also requesting change of output reg (stop that)

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 08e742597d965234eb0bf523a8c14d8aff6f40cd..c668228071e2b93710829bfcb458c93934d81efd 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -84,7 +84,6 @@ class Driver(Elaboratable):
         cr0_ok = Signal()
         ov_ok = Signal()
         ca_ok = Signal()
-        comb += o_ok.eq(1) # will be set to zero if no op takes place
         comb += cr0_ok.eq(0)
         comb += ov_ok.eq(0)
         comb += ca_ok.eq(0)
@@ -104,6 +103,7 @@ class Driver(Elaboratable):
                 comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
                 comb += ov_ok.eq(1)
                 comb += ca_ok.eq(1)
+                comb += o_ok.eq(1)
 
             with m.Case(InternalOp.OP_EXTS):
                 for i in [1, 2, 4]:
@@ -111,12 +111,12 @@ class Driver(Elaboratable):
                         # main part, then sign-bit replicated up
                         comb += Assert(o[0:i*8] == a[0:i*8])
                         comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
+                comb += o_ok.eq(1)
 
             with m.Case(InternalOp.OP_CMP):
                 # CMP is defined as not taking in carry
                 comb += Assume(ca_in == 0)
                 comb += Assert(o == (a+b)[0:64])
-                comb += o_ok.eq(0) # must not change output reg
 
             with m.Case(InternalOp.OP_CMPEQB):
                 src1 = a[0:8]
@@ -126,9 +126,6 @@ class Driver(Elaboratable):
                 comb += Assert(dut.o.cr0.data[2] == eqs.any())
                 comb += cr0_ok.eq(1)
 
-            with m.Default():
-                comb += o_ok.eq(0)
-
         # check that data ok was only enabled when op actioned
         comb += Assert(dut.o.o.ok == o_ok)
         comb += Assert(dut.o.cr0.ok == cr0_ok)

diff --git a/src/soc/fu/alu/main_stage.py b/src/soc/fu/alu/main_stage.py
index 1d0f34326f04cbc47a21de9eb32722ec42733695..fc8eb1f0a3bdda9bdd8820bc3a78264c06367bd9 100644 (file)
--- a/src/soc/fu/alu/main_stage.py
+++ b/src/soc/fu/alu/main_stage.py
@@ -48,8 +48,6 @@ class ALUMainStage(PipeModBase):
             comb += add_b.eq(Cat(Const(1, 1), b, Const(0, 1)))
             comb += add_o.eq(add_a + add_b)
 
-        comb += o.ok.eq(1) # overridden to 0 if op not handled
-
         ##########################
         # main switch-statement for handling arithmetic operations
 
@@ -76,6 +74,7 @@ class ALUMainStage(PipeModBase):
                 comb += ov_o.data[0].eq((add_o[-2] != a[-1]) & (a[-1] == b[-1]))
                 comb += ov_o.data[1].eq((add_o[32] != a[31]) & (a[31] == b[31]))
                 comb += ov_o.ok.eq(1)
+                comb += o.ok.eq(1) # output register
 
             #### exts (sign-extend) ####
             with m.Case(InternalOp.OP_EXTS):
@@ -85,6 +84,7 @@ class ALUMainStage(PipeModBase):
                     comb += o.data.eq(exts(a, 16, 64))
                 with m.If(op.data_len == 4):
                     comb += o.data.eq(exts(a, 32, 64))
+                comb += o.ok.eq(1) # output register
 
             #### cmpeqb ####
             with m.Case(InternalOp.OP_CMPEQB):
@@ -96,9 +96,7 @@ class ALUMainStage(PipeModBase):
                 comb += o.data[0].eq(eqs.any())
                 comb += cr0.data.eq(Cat(Const(0, 2), eqs.any(), Const(0, 1)))
                 comb += cr0.ok.eq(1)
-
-            with m.Default():
-                comb += o.ok.eq(0)
+                comb += o.ok.eq(0) # use o.data but do *not* actually output
 
         ###### sticky overflow and context, both pass-through #####