Adding test for tXXDController

diff --git a/gram/common.py b/gram/common.py
index abe181d1cc8f5b502e0d72ecd97801a2e6e1992e..80fe39ffffb45b6dc71e3d3a2420572f9adbb543 100644 (file)
--- 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 bfc144765e5e32a5025bfeddd969d1abc8559982..a051f1a8f4638ab62544ded114369fecef2ce4a0 100644 (file)
--- 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