From 5aa978d7a9348514d3d949bc243b957dd487d02a Mon Sep 17 00:00:00 2001 From: Jean THOMAS Date: Mon, 20 Jul 2020 16:34:26 +0200 Subject: [PATCH] Adding test for tXXDController --- gram/common.py | 10 ++++++++++ gram/test/test_common.py | 15 ++++++++++++++- 2 files changed, 24 insertions(+), 1 deletion(-) 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 -- 2.30.2