From ec073b9a94cdf8d3bc5ecd36d259047d8bc85fd3 Mon Sep 17 00:00:00 2001 From: Jean THOMAS Date: Wed, 8 Jul 2020 15:33:41 +0200 Subject: [PATCH] Fix bugs in _AntiStarvation --- gram/core/multiplexer.py | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/gram/core/multiplexer.py b/gram/core/multiplexer.py index b813b80..ffe47f9 100644 --- a/gram/core/multiplexer.py +++ b/gram/core/multiplexer.py @@ -11,6 +11,7 @@ from functools import reduce from operator import or_, and_ from nmigen import * +from nmigen.asserts import Assert, Assume from gram.common import * import gram.stream as stream @@ -211,21 +212,30 @@ class _Steerer(Elaboratable): class _AntiStarvation(Elaboratable): def __init__(self, timeout): self.en = Signal() - self.max_time = Signal() + self.max_time = Signal(reset=1) + self._timeout = timeout def elaborate(self, platform): m = Module() - if timeout > 0: - t = timeout - 1 - time = Signal(range(t+1)) - m.d.comb += max_time.eq(time == 0) - with m.If(~en): - m.d.sync += time.eq(t) - with m.Elif(~max_time): - m.d.sync += time.eq(time - 1) + if self._timeout > 0: + time = Signal(range(self._timeout)) + with m.If(~self.en): + m.d.sync += time.eq(self._timeout-1) + with m.If(time == 1): + m.d.sync += self.max_time.eq(1) + with m.Else(): + m.d.sync += self.max_time.eq(0) + with m.Elif(time != 0): + m.d.sync += [ + time.eq(time-1), + self.max_time.eq(0), + ] else: - m.d.comb += max_time.eq(0) + m.d.comb += self.max_time.eq(0) + + if platform == "formal" and self._timeout > 0: + m.d.comb += Assert(self.max_time.implies(time == 0)) return m -- 2.30.2