Make RefreshTimer fully synchronous (#24)

diff --git a/gram/core/refresher.py b/gram/core/refresher.py
index 816d81911b7ec77fd7b0d1dde7aa52a46678aa66..36739080fa3c3250265e635db5d0a0d22de421c9 100644 (file)
--- 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 34b692cf7f120be29a645df5d0d1ba8f82a15947..500db2c3690dc6905312fc7f736270f28d1821ab 100644 (file)
--- 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()