X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Ffu%2Falu%2Fformal%2Fproof_main_stage.py;h=c1e71536d65546794734e336a5b77948285a9b5b;hb=5e1c13282694de2e986ea6703bd4dba888c28f66;hp=f102fc2b1726ed4d87b9a7415f09b9c7c9438423;hpb=6e30af026706829d5af7820c4bd23111aeb012e9;p=soc.git

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index f102fc2b..c1e71536 100644
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -1,15 +1,21 @@
-# Proof of correctness for partitioned equal signal combiner
+# Proof of correctness for ALU pipeline, main stage
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+"""
+Links:
+* https://bugs.libre-soc.org/show_bug.cgi?id=306
+* https://bugs.libre-soc.org/show_bug.cgi?id=305
+* https://bugs.libre-soc.org/show_bug.cgi?id=343
+"""
 
 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
                     signed)
 from nmigen.asserts import Assert, AnyConst, Assume, Cover
-from nmigen.test.utils import FHDLTestCase
+from nmutil.formaltest import FHDLTestCase
 from nmigen.cli import rtlil
 
-from soc.alu.main_stage import ALUMainStage
-from soc.alu.pipe_data import ALUPipeSpec
-from soc.alu.alu_input_record import CompALUOpSubset
+from soc.fu.alu.main_stage import ALUMainStage
+from soc.fu.alu.pipe_data import ALUPipeSpec
+from soc.fu.alu.alu_input_record import CompALUOpSubset
 from soc.decoder.power_enums import InternalOp
 import unittest
 
@@ -26,28 +32,31 @@ class Driver(Elaboratable):
         comb = m.d.comb
 
         rec = CompALUOpSubset()
-        recwidth = 0
         # Setup random inputs for dut.op
         for p in rec.ports():
             width = p.width
-            recwidth += width
             comb += p.eq(AnyConst(width))
 
-        pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
+        pspec = ALUPipeSpec(id_wid=2)
         m.submodules.dut = dut = ALUMainStage(pspec)
 
         # convenience variables
         a = dut.i.a
         b = dut.i.b
-        carry_in = dut.i.carry_in
-        so_in = dut.i.so
-        carry_out = dut.o.carry_out
-        o = dut.o.o
+        ca_in = dut.i.xer_ca[0]   # CA carry in
+        ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
+        so_in = dut.i.xer_so      # SO sticky overflow
+
+        ca_o = dut.o.xer_ca.data[0]   # CA carry out
+        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.data
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
                  b.eq(AnyConst(64)),
-                 carry_in.eq(AnyConst(1)),
+                 ca_in.eq(AnyConst(0b11)),
                  so_in.eq(AnyConst(1))]
 
         comb += dut.i.ctx.op.eq(rec)
@@ -64,10 +73,64 @@ class Driver(Elaboratable):
         comb += a_signed.eq(a)
         comb += a_signed_32.eq(a[0:32])
 
+        # do not check MSBs of a/b in 32-bit mode
+        with m.If(rec.is_32bit):
+            comb += Assume(a[32:64] == 0)
+            comb += Assume(b[32:64] == 0)
+
+        # Data.ok checking.  these only to be valid when there is a change
+        # in the output that needs to go into a regfile
+        o_ok = Signal()
+        cr0_ok = Signal()
+        ov_ok = Signal()
+        ca_ok = Signal()
+        comb += cr0_ok.eq(0)
+        comb += ov_ok.eq(0)
+        comb += ca_ok.eq(0)
+
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_ADD):
-                comb += Assert(Cat(o, carry_out) == (a + b + carry_in))
+
+                # check result of 65-bit add-with-carry
+                comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
+
+                # CA32 - XXX note this fails! replace with ca_in and it works
+                comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
+
+                # From microwatt execute1.vhdl line 130, calc_ov() function
+                comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
+                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]:
+                    with m.If(rec.data_len == i):
+                        # 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])
+
+            with m.Case(InternalOp.OP_CMPEQB):
+                src1 = a[0:8]
+                eqs = Signal(8)
+                for i in range(8):
+                    comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
+                comb += Assert(dut.o.cr0.data[2] == eqs.any())
+                comb += cr0_ok.eq(1)
+
+        # 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)
+        comb += Assert(dut.o.xer_ov.ok == ov_ok)
+        comb += Assert(dut.o.xer_ca.ok == ca_ok)
 
         return m
 
@@ -80,7 +143,7 @@ class ALUTestCase(FHDLTestCase):
     def test_ilang(self):
         dut = Driver()
         vl = rtlil.convert(dut, ports=[])
-        with open("main_stage.il", "w") as f:
+        with open("alu_main_stage.il", "w") as f:
             f.write(vl)