From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Sat, 18 Jul 2020 01:00:05 +0000 (-0700)
Subject: Failing test: fast1/fast2 vs srr0/srr1? on trap pipe
X-Git-Tag: semi_working_ecp5~697^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3378a4459ce839a14f1b5cd25580ac18a0c68681;p=soc.git

Failing test: fast1/fast2 vs srr0/srr1? on trap pipe
---

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index 10fa29ff..2526f11c 100644
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -19,6 +19,7 @@ from soc.decoder.power_enums import MicrOp
 
 from soc.fu.trap.main_stage import TrapMainStage
 from soc.fu.trap.pipe_data import TrapPipeSpec
+from soc.fu.trap.trap_input_record import CompTrapOpSubset
 
 
 def is_ok(sig, value):
@@ -48,6 +49,19 @@ def full_function_bits(msr):
     return Cat(msr[0:16], zeros16_21, msr[22:27], zeros27_30, msr[31:64])
 
 
+def is_full_function_ok(out, inp):
+    """
+    Answers with a list of assertions that ONLY covers the full function
+    MSR bits.  It ignores the remaining bits.
+    """
+    return [
+        Assert(out.data[0:16] == inp[0:16]),
+#       Assert(out.data[22:27] == inp[22:27]),
+#       Assert(out.data[31:64] == inp[31:64]),
+        Assert(out.ok),
+    ]
+
+
 class Driver(Elaboratable):
     """
     """
@@ -56,6 +70,7 @@ class Driver(Elaboratable):
         m = Module()
         comb = m.d.comb
 
+        rec = CompTrapOpSubset()
         pspec = TrapPipeSpec(id_wid=2)
 
         m.submodules.dut = dut = TrapMainStage(pspec)
@@ -63,6 +78,8 @@ class Driver(Elaboratable):
         # frequently used aliases
         op = dut.i.ctx.op
 
+        comb += op.eq(rec)
+
         # start of properties
         with m.Switch(op.insn_type):
             with m.Case(MicrOp.OP_SC):
@@ -71,6 +88,11 @@ class Driver(Elaboratable):
                     is_ok(dut.o.srr0, dut.i.cia + 4),
                     is_ok(dut.o.srr1, full_function_bits(dut.i.msr)),
                 ]
+            with m.Case(MicrOp.OP_RFID):
+                comb += [
+                    is_ok(dut.o.nia, Cat(Const(0, 2), dut.i.srr0[2:])),
+                    is_full_function_ok(dut.o.msr, dut.i.srr1),
+                ]
 
         comb += dut.i.ctx.matches(dut.o.ctx)