Reduce amount of combinatorial statements to improve frequency (#24)

diff --git a/gram/core/refresher.py b/gram/core/refresher.py
index adf289edf0bee58d4dc020f6671ab1d905c9432b..816d81911b7ec77fd7b0d1dde7aa52a46678aa66 100644 (file)
--- a/gram/core/refresher.py
+++ b/gram/core/refresher.py
@@ -7,6 +7,7 @@
 
 from nmigen import *
 from nmigen.utils import log2_int
+from nmigen.asserts import Assert, Assume
 
 from gram.core.multiplexer import *
 from gram.compat import Timeline
@@ -113,18 +114,42 @@ class RefreshSequencer(Elaboratable):
             self.we.eq(executer.we),
         ]
 
+        countEqZero = Signal(reset=(self._postponing <= 1))
+        countDiffZero = Signal(reset=(self._postponing > 1))
+
         count = Signal(range(self._postponing), reset=self._postponing-1)
         with m.If(self.start):
-            m.d.sync += count.eq(count.reset)
+            m.d.sync += [
+                count.eq(count.reset),
+                countEqZero.eq(self._postponing <= 1),
+                countDiffZero.eq(self._postponing > 1),
+            ]
         with m.Elif(executer.done):
             with m.If(count != 0):
                 m.d.sync += count.eq(count-1)
 
+            with m.If(count == 1):
+                m.d.sync += [
+                    countEqZero.eq(1),
+                    countDiffZero.eq(0),
+                ]
+            with m.Else():
+                m.d.sync += [
+                    countEqZero.eq(0),
+                    countDiffZero.eq(1),
+                ]
+
         m.d.comb += [
-            executer.start.eq(self.start | (count != 0)),
-            self.done.eq(executer.done & (count == 0)),
+            executer.start.eq(self.start | countDiffZero),
+            self.done.eq(executer.done & countEqZero),
         ]
 
+        if platform == "formal":
+            m.d.comb += [
+                Assert(countEqZero.implies(count == 0)),
+                Assert(countDiffZero.implies(count != 0))
+            ]
+
         return m
 
 # RefreshTimer -------------------------------------------------------------------------------------

diff --git a/gram/test/test_core_refresher.py b/gram/test/test_core_refresher.py
index 5ef6f818cb71dc187fd1cc6116d8c0891c0d9ecf..34b692cf7f120be29a645df5d0d1ba8f82a15947 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, RefreshPostponer, Refresher
+from gram.core.refresher import RefreshExecuter, RefreshSequencer, RefreshPostponer, Refresher
 from gram.compat import *
 from utils import *
 
@@ -26,6 +26,11 @@ class RefreshExecuterTestCase(FHDLTestCase):
         generic_test(20, 20, 5, 5)
         generic_test(20, 20, 100, 5)
 
+class RefreshSequencerTestCase(FHDLTestCase):
+    def test_formal(self):
+        dut = RefreshSequencer(abits=14, babits=3, trp=5, trfc=5, postponing=1)
+        self.assertFormal(dut, mode="bmc", depth=4)
+
 class RefreshPostponerTestCase(FHDLTestCase):
     def test_init(self):
         m = Module()
@@ -106,4 +111,3 @@ class RefresherTestCase(FHDLTestCase):
             runSimulation(m, process, "test_refresher.vcd")
 
         [generic_test(_) for _ in [1, 2, 4, 8]]
-