From a155905d24017e0976c3745f3d21aee16432c75f Mon Sep 17 00:00:00 2001 From: Jean THOMAS Date: Mon, 6 Jul 2020 13:12:13 +0200 Subject: [PATCH] Make RefreshTimer fully synchronous (#24) --- gram/core/refresher.py | 22 ++++++++++++---------- gram/test/test_core_refresher.py | 10 +++++++++- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/gram/core/refresher.py b/gram/core/refresher.py index 816d819..3673908 100644 --- a/gram/core/refresher.py +++ b/gram/core/refresher.py @@ -164,7 +164,7 @@ class RefreshTimer(Elaboratable): def __init__(self, trefi): self.wait = Signal() self.done = Signal() - self.count = Signal(range(trefi)) + self.count = Signal(range(trefi), reset=trefi-1) self._trefi = trefi def elaborate(self, platform): @@ -173,18 +173,20 @@ class RefreshTimer(Elaboratable): trefi = self._trefi done = Signal() - count = Signal(range(trefi), reset=trefi-1) - with m.If(self.wait & ~self.done): - m.d.sync += count.eq(count-1) + with m.If(self.wait & (self.count != 0)): + m.d.sync += self.count.eq(self.count-1) + + with m.If(self.count == 1): + m.d.sync += self.done.eq(1) with m.Else(): - m.d.sync += count.eq(count.reset) + m.d.sync += [ + self.count.eq(self.count.reset), + self.done.eq(0), + ] - m.d.comb += [ - done.eq(count == 0), - self.done.eq(done), - self.count.eq(count) - ] + if platform == "formal": + m.d.comb += Assert(self.done.implies(self.count == 0)) return m diff --git a/gram/test/test_core_refresher.py b/gram/test/test_core_refresher.py index 34b692c..500db2c 100644 --- a/gram/test/test_core_refresher.py +++ b/gram/test/test_core_refresher.py @@ -2,7 +2,7 @@ from nmigen import * from nmigen.hdl.ast import Past from nmigen.asserts import Assert, Assume -from gram.core.refresher import RefreshExecuter, RefreshSequencer, RefreshPostponer, Refresher +from gram.core.refresher import RefreshExecuter, RefreshSequencer, RefreshTimer, RefreshPostponer, Refresher from gram.compat import * from utils import * @@ -31,6 +31,14 @@ class RefreshSequencerTestCase(FHDLTestCase): dut = RefreshSequencer(abits=14, babits=3, trp=5, trfc=5, postponing=1) self.assertFormal(dut, mode="bmc", depth=4) +class RefreshTimerTestCase(FHDLTestCase): + def test_formal(self): + def generic_test(tREFI): + dut = RefreshTimer(tREFI) + self.assertFormal(dut, mode="bmc", depth=4) + + [generic_test(_) for _ in [1, 5, 10]] + class RefreshPostponerTestCase(FHDLTestCase): def test_init(self): m = Module() -- 2.30.2