convert ALU to output Data on int reg
authorLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Sun, 24 May 2020 13:07:02 +0000 (14:07 +0100)
committerLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Sun, 24 May 2020 13:07:02 +0000 (14:07 +0100)
src/soc/fu/alu/formal/proof_main_stage.py
src/soc/fu/alu/main_stage.py
src/soc/fu/alu/test/test_pipe_caller.py

index b63e958e89905e6df1446a07e0da5d419b2e13d7..4ef8ef978f0d812cb37828e47c67310599599031 100644 (file)
@@ -45,7 +45,7 @@ class Driver(Elaboratable):
         ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
         ov_o = dut.o.xer_ov.data[0]   # OV overflow
         ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
-        o = dut.o.o
+        o = dut.o.o.data
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -70,6 +70,9 @@ class Driver(Elaboratable):
         comb += Assume(a[32:64] == 0)
         comb += Assume(b[32:64] == 0)
 
+        o_ok = Signal()
+        comb += o_ok.eq(1) # will be set to zero if no op takes place
+
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_ADD):
@@ -101,6 +104,12 @@ class Driver(Elaboratable):
                     comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
                 comb += Assert(dut.o.cr0[2] == eqs.any())
 
+            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)
+
         return m
 
 
index d65acf55ab8f322be97dd69f0a9a518df2269072..ec892a13022389864f6645f0ed30d3cd6c907d91 100644 (file)
@@ -46,6 +46,8 @@ 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
 
@@ -56,12 +58,12 @@ class ALUMainStage(PipeModBase):
                 # however we have a trick: instead of adding either 2x 64-bit
                 # MUXes to invert a and b, or messing with a 64-bit output,
                 # swap +ve and -ve test in the *output* stage using an XOR gate
-                comb += o.eq(add_o[1:-1])
+                comb += o.data.eq(add_o[1:-1])
 
             #### add ####
             with m.Case(InternalOp.OP_ADD):
                 # bit 0 is not part of the result, top bit is the carry-out
-                comb += o.eq(add_o[1:-1])
+                comb += o.data.eq(add_o[1:-1])
 
                 # see microwatt OP_ADD code
                 # https://bugs.libre-soc.org/show_bug.cgi?id=319#c5
@@ -73,11 +75,11 @@ class ALUMainStage(PipeModBase):
             #### exts (sign-extend) ####
             with m.Case(InternalOp.OP_EXTS):
                 with m.If(op.data_len == 1):
-                    comb += o.eq(exts(a, 8, 64))
+                    comb += o.data.eq(exts(a, 8, 64))
                 with m.If(op.data_len == 2):
-                    comb += o.eq(exts(a, 16, 64))
+                    comb += o.data.eq(exts(a, 16, 64))
                 with m.If(op.data_len == 4):
-                    comb += o.eq(exts(a, 32, 64))
+                    comb += o.data.eq(exts(a, 32, 64))
 
             #### cmpeqb ####
             with m.Case(InternalOp.OP_CMPEQB):
@@ -88,6 +90,9 @@ class ALUMainStage(PipeModBase):
                     comb += eqs[i].eq(src1 == b[8*i:8*(i+1)])
                 comb += cr0.data.eq(Cat(Const(0, 2), eqs.any(), Const(0, 1)))
 
+            with m.Default():
+                comb += o.ok.eq(0)
+
         ###### sticky overflow and context, both pass-through #####
 
         comb += self.o.xer_so.data.eq(self.i.xer_so)
index 6a1277eff95708a869b50ff68a7af9c9458c3a80..be966d3324819ac8d8fc58dc794ed0f7bbd38338 100644 (file)
@@ -220,7 +220,7 @@ class TestRunner(FHDLTestCase):
                         yield
                         vld = yield alu.n.valid_o
                     yield
-                    alu_out = yield alu.n.data_o.o
+                    alu_out = yield alu.n.data_o.o.data
                     out_reg_valid = yield pdecode2.e.write_reg.ok
                     if out_reg_valid:
                         write_reg_idx = yield pdecode2.e.write_reg.data