From: Jean THOMAS <git0@pub.jeanthomas.me>
Date: Mon, 20 Jul 2020 14:34:26 +0000 (+0200)
Subject: Adding test for tXXDController
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5aa978d7a9348514d3d949bc243b957dd487d02a;p=gram.git

Adding test for tXXDController
---

diff --git a/gram/common.py b/gram/common.py
index abe181d..80fe39f 100644
--- a/gram/common.py
+++ b/gram/common.py
@@ -10,6 +10,7 @@ from operator import add
 from collections import OrderedDict
 
 from nmigen import *
+from nmigen.asserts import Assert, Assume
 from nmigen.hdl.rec import *
 from nmigen.utils import log2_int
 
@@ -272,6 +273,15 @@ class tXXDController(Elaboratable):
                 m.d.sync += count.eq(count-1)
                 with m.If(count == 1):
                     m.d.sync += self.ready.eq(1)
+
+        if platform == "formal":
+            if self._txxd is not None and self._txxd > 0:
+                hasSeenValid = Signal()
+                with m.If(self.valid):
+                    m.d.sync += hasSeenValid.eq(1)
+
+                m.d.sync += Assert((hasSeenValid & (count == 0)).implies(self.ready == 1))
+
         return m
 
 
diff --git a/gram/test/test_common.py b/gram/test/test_common.py
index bfc1447..a051f1a 100644
--- a/gram/test/test_common.py
+++ b/gram/test/test_common.py
@@ -1,7 +1,8 @@
+#nmigen: UnusedElaboratable=no
 from nmigen import *
 from nmigen.hdl.ast import Past
 
-from gram.common import DQSPattern
+from gram.common import DQSPattern, tXXDController
 from utils import *
 
 class DQSPatternTestCase(FHDLTestCase):
@@ -28,3 +29,15 @@ class DQSPatternTestCase(FHDLTestCase):
             self.assertEqual((yield dut.o), 0b01010101)
 
         runSimulation(m, process, "test_dqspattern_async.vcd")
+
+class tXXDControllerTestCase(FHDLTestCase):
+    def test_formal(self):
+        def generic_test(txxd):
+            dut = tXXDController(txxd)
+            self.assertFormal(dut, mode="bmc", depth=4)
+
+        generic_test(None)
+        generic_test(0)
+        generic_test(1)
+        generic_test(5)
+        generic_test(10)
\ No newline at end of file