From 9c4e820c036fea825a7f90e8d289a95fb71d3890 Mon Sep 17 00:00:00 2001 From: Jean THOMAS Date: Mon, 6 Jul 2020 12:49:37 +0200 Subject: [PATCH] Reduce amount of combinatorial statements to improve frequency (#24) --- gram/core/refresher.py | 31 ++++++++++++++++++++++++++++--- gram/test/test_core_refresher.py | 8 ++++++-- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/gram/core/refresher.py b/gram/core/refresher.py index adf289e..816d819 100644 --- 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 5ef6f81..34b692c 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, 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]] - -- 2.30.2