From 81de08a20bb8ecf07f0cf6d84d1bc0e75f6ad57f Mon Sep 17 00:00:00 2001
From: "Samuel A. Falvo II" <kc5tja@arrl.net>
Date: Fri, 17 Jul 2020 17:04:33 -0700
Subject: [PATCH] FV props for SC instruction

---
 src/soc/fu/trap/formal/proof_main_stage.py | 48 +++++++++++++++++++++-
 1 file changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index 89a0ebbb..7d8655bf 100644
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -9,16 +9,50 @@ Links:
 
 import unittest
 
-from nmigen import Elaboratable, Module
+from nmigen import (
+    Cat,
+    Const,
+    Elaboratable, 
+    Module, 
+)
 from nmigen.asserts import Assert, AnyConst
 from nmigen.cli import rtlil
 
 from nmutil.formaltest import FHDLTestCase
 
+from soc.decoder.power_enums import MicrOp
+
 from soc.fu.trap.main_stage import TrapMainStage
 from soc.fu.trap.pipe_data import TrapPipeSpec
 
 
+def is_ok(sig, value):
+    """
+    Answers with a list of assertions that checks for valid data on
+    a pipeline stage output.  sig.data must have the anticipated value,
+    and sig.ok must be asserted.  The `value` is constrained to the width
+    of the sig.data field it's verified against, so it's safe to add, etc.
+    offsets to Nmigen signals without having to worry about inequalities from
+    differing signal widths.
+    """
+    return [
+        Assert(sig.data == value[0:len(sig.data)]),
+        Assert(sig.ok),
+    ]
+
+
+def full_function_bits(msr):
+    """
+    Answers with a numeric constant signal with all "full functional"
+    bits filled in, but all partial functional bits zeroed out.
+
+    See src/soc/fu/trap/main_stage.py:msr_copy commentary for details.
+    """
+    zeros16_21 = Const(0, (22 - 16))
+    zeros27_30 = Const(0, (31 - 27))
+    return Cat(msr[0:16], zeros16_21, msr[22:27], zeros27_30, msr[31:64])
+
+
 class Driver(Elaboratable):
     """
     """
@@ -31,6 +65,18 @@ class Driver(Elaboratable):
 
         m.submodules.dut = dut = TrapMainStage(pspec)
 
+        # frequently used aliases
+        op = dut.i.ctx.op
+
+        # start of properties
+        with m.Switch(op.insn_type):
+            with m.Case(MicrOp.OP_SC):
+                comb += [
+                    is_ok(dut.o.nia, Const(0xC00)),
+                    is_ok(dut.o.srr0, dut.i.cia + 4),
+                    is_ok(dut.o.srr1, full_function_bits(dut.i.msr)),
+                ]
+
         comb += dut.i.ctx.matches(dut.o.ctx)
 
         return m
-- 
2.30.2