From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Tue, 14 Jul 2020 19:59:59 +0000 (+0100)
Subject: cookie-cut setup from alu proof_main_stage.py
X-Git-Tag: div_pipeline~35
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ead389c3edc78ec2af354a3f713788ac8c0ce6a2;p=soc.git

cookie-cut setup from alu proof_main_stage.py
---

diff --git a/src/soc/fu/spr/formal/proof_main_stage.py b/src/soc/fu/spr/formal/proof_main_stage.py
index 0c7d5231..457f89a1 100644
--- a/src/soc/fu/spr/formal/proof_main_stage.py
+++ b/src/soc/fu/spr/formal/proof_main_stage.py
@@ -6,18 +6,17 @@ Links:
 * https://bugs.libre-soc.org/show_bug.cgi?id=418
 """
 
-from os import getenv
-
-from unittest import skipUnless
-
 from nmigen import (Elaboratable, Module)
-from nmigen.asserts import Assert
+from nmigen.asserts import Assert, AnyConst, Assume
 from nmigen.cli import rtlil
 
 from nmutil.formaltest import FHDLTestCase
 
 from soc.fu.spr.main_stage import SPRMainStage
 from soc.fu.spr.pipe_data import SPRPipeSpec
+from soc.fu.spr.spr_input_record import CompSPROpSubset
+from soc.decoder.power_enums import MicrOp
+import unittest
 
 
 class Driver(Elaboratable):
@@ -30,16 +29,48 @@ class Driver(Elaboratable):
         m = Module()
         comb = m.d.comb
 
-        dut = SPRMainStage(SPRPipeSpec(id_wid=2))
+        # cookie-cutting most of this from alu formal proof_main_stage.py
+
+        rec = CompSPROpSubset()
+        # Setup random inputs for dut.op
+        for p in rec.ports():
+            width = p.width
+            comb += p.eq(AnyConst(width))
+
+        pspec = SPRPipeSpec(id_wid=2)
+        m.submodules.dut = dut = SPRMainStage(pspec)
+
+        # convenience variables
+        a = dut.i.a
+        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)),
+                 ca_in.eq(AnyConst(0b11)),
+                 so_in.eq(AnyConst(1))]
+
+        comb += dut.i.ctx.op.eq(rec)
 
-        # Output context is the same as the input context.
-        comb += Assert(dut.o.ctx != dut.i.ctx)
+        # Assert that op gets copied from the input to output
+        for rec_sig in rec.ports():
+            name = rec_sig.name
+            dut_sig = getattr(dut.o.ctx.op, name)
+            comb += Assert(dut_sig == rec_sig)
 
         return m
 
 
 class SPRMainStageTestCase(FHDLTestCase):
-    @skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
+    #don't worry about it - tests are run manually anyway.  fail is fine.
+    #@skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
     def test_formal(self):
         self.assertFormal(Driver(), mode="bmc", depth=100)
         self.assertFormal(Driver(), mode="cover", depth=100)