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

index 9497dd1b083fc544005d02a7ff0ac49acf693594..cb6a0690abffec00c13ab2c20e1db219bf4728fc 100644 (file)
@@ -51,7 +51,7 @@ class Driver(Elaboratable):
         b = dut.i.b
         carry_in = dut.i.xer_ca[0]
         carry_in32 = dut.i.xer_ca[1]
-        o = dut.o.o
+        o = dut.o.o.data
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -73,26 +73,29 @@ class Driver(Elaboratable):
         comb += a_signed.eq(a)
         comb += a_signed_32.eq(a[0:32])
 
+        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_AND):
-                comb += Assert(dut.o.o == a & b)
+                comb += Assert(o == a & b)
             with m.Case(InternalOp.OP_OR):
-                comb += Assert(dut.o.o == a | b)
+                comb += Assert(o == a | b)
             with m.Case(InternalOp.OP_XOR):
-                comb += Assert(dut.o.o == a ^ b)
+                comb += Assert(o == a ^ b)
 
             with m.Case(InternalOp.OP_POPCNT):
                 with m.If(rec.data_len == 8):
-                    comb += Assert(dut.o.o == self.popcount(a, 64))
+                    comb += Assert(o == self.popcount(a, 64))
                 with m.If(rec.data_len == 4):
 
                     for i in range(2):
-                        comb += Assert(dut.o.o[i*32:(i+1)*32] ==
+                        comb += Assert(o[i*32:(i+1)*32] ==
                                        self.popcount(a[i*32:(i+1)*32], 32))
                 with m.If(rec.data_len == 1):
                     for i in range(8):
-                        comb += Assert(dut.o.o[i*8:(i+1)*8] ==
+                        comb += Assert(o[i*8:(i+1)*8] ==
                                        self.popcount(a[i*8:(i+1)*8], 8))
 
             with m.Case(InternalOp.OP_PRTY):
@@ -100,15 +103,16 @@ class Driver(Elaboratable):
                     result = 0
                     for i in range(8):
                         result = result ^ a[i*8]
-                    comb += Assert(dut.o.o == result)
+                    comb += Assert(o == result)
                 with m.If(rec.data_len == 4):
                     result_low = 0
                     result_high = 0
                     for i in range(4):
                         result_low = result_low ^ a[i*8]
                         result_high = result_high ^ a[i*8 + 32]
-                    comb += Assert(dut.o.o[0:32] == result_low)
-                    comb += Assert(dut.o.o[32:64] == result_high)
+                    comb += Assert(o[0:32] == result_low)
+                    comb += Assert(o[32:64] == result_high)
+
             with m.Case(InternalOp.OP_CNTZ):
                 XO = dut.fields.FormX.XO[0:-1]
                 with m.If(rec.is_32bit):
@@ -120,10 +124,10 @@ class Driver(Elaboratable):
                         comb += peo.eq(pe32.o)
                     with m.If(XO[-1]): # cnttzw
                         comb += pe32.i.eq(a[0:32])
-                        comb += Assert(dut.o.o == peo)
+                        comb += Assert(o == peo)
                     with m.Else(): # cntlzw
                         comb += pe32.i.eq(a[0:32][::-1])
-                        comb += Assert(dut.o.o == peo)
+                        comb += Assert(o == peo)
                 with m.Else():
                     m.submodules.pe64 = pe64 = PriorityEncoder(64)
                     peo64 = Signal(7)
@@ -133,11 +137,24 @@ class Driver(Elaboratable):
                         comb += peo64.eq(pe64.o)
                     with m.If(XO[-1]): # cnttzd
                         comb += pe64.i.eq(a[0:64])
-                        comb += Assert(dut.o.o == peo64)
+                        comb += Assert(o == peo64)
                     with m.Else(): # cntlzd
                         comb += pe64.i.eq(a[0:64][::-1])
-                        comb += Assert(dut.o.o == peo64)
+                        comb += Assert(o == peo64)
+
+            with m.Case(InternalOp.OP_CMPB):
+                # TODO
+                pass
+
+            with m.Case(InternalOp.OP_BPERM):
+                # TODO
+                pass
+
+            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 b40c91fdd85af11a0a2fb6b3f5c15432a91b5600..f85acebe29bfcae8e95f13756753457ac2f4614e 100644 (file)
@@ -43,6 +43,8 @@ class LogicalMainStage(PipeModBase):
         comb = m.d.comb
         op, a, b, o = self.i.ctx.op, self.i.a, self.i.b, self.o.o
 
+        comb += o.ok.eq(1) # overridden if no op activates
+
         ##########################
         # main switch for logic ops AND, OR and XOR, cmpb, parity, and popcount
 
@@ -50,11 +52,11 @@ class LogicalMainStage(PipeModBase):
 
             ###### AND, OR, XOR #######
             with m.Case(InternalOp.OP_AND):
-                comb += o.eq(a & b)
+                comb += o.data.eq(a & b)
             with m.Case(InternalOp.OP_OR):
-                comb += o.eq(a | b)
+                comb += o.data.eq(a | b)
             with m.Case(InternalOp.OP_XOR):
-                comb += o.eq(a ^ b)
+                comb += o.data.eq(a ^ b)
 
             ###### cmpb #######
             with m.Case(InternalOp.OP_CMPB):
@@ -62,7 +64,7 @@ class LogicalMainStage(PipeModBase):
                 for i in range(8):
                     slc = slice(i*8, (i+1)*8)
                     l.append(Repl(a[slc] == b[slc], 8))
-                comb += o.eq(Cat(*l))
+                comb += o.data.eq(Cat(*l))
 
             ###### popcount #######
             with m.Case(InternalOp.OP_POPCNT):
@@ -94,7 +96,7 @@ class LogicalMainStage(PipeModBase):
                         comb += o[i*32:(i+1)*32].eq(pc32[i])
                 with m.Else():
                     # popcntd - put 1x 6-bit answer into output
-                    comb += o.eq(popcnt[0])
+                    comb += o.data.eq(popcnt[0])
 
             ###### parity #######
             with m.Case(InternalOp.OP_PRTY):
@@ -104,7 +106,7 @@ class LogicalMainStage(PipeModBase):
                 comb += par0.eq(Cat(a[0], a[8], a[16], a[24]).xor())
                 comb += par1.eq(Cat(a[32], a[40], a[48], a[56]).xor())
                 with m.If(op.data_len[3] == 1):
-                    comb += o.eq(par0 ^ par1)
+                    comb += o.data.eq(par0 ^ par1)
                 with m.Else():
                     comb += o[0].eq(par0)
                     comb += o[32].eq(par1)
@@ -126,14 +128,17 @@ class LogicalMainStage(PipeModBase):
 
                 m.submodules.clz = clz = CLZ(64)
                 comb += clz.sig_in.eq(cntz_i)
-                comb += o.eq(Mux(op.is_32bit, clz.lz-32, clz.lz))
+                comb += o.data.eq(Mux(op.is_32bit, clz.lz-32, clz.lz))
 
             ###### bpermd #######
             with m.Case(InternalOp.OP_BPERM):
                 m.submodules.bpermd = bpermd = Bpermd(64)
                 comb += bpermd.rs.eq(a)
                 comb += bpermd.rb.eq(b)
-                comb += o.eq(bpermd.ra)
+                comb += o.data.eq(bpermd.ra)
+
+            with m.Default():
+                comb += o.ok.eq(0)
 
         ###### context, pass-through #####