From b7ecdeca26d6ae241ab438d9c1c9ee0df4f1f649 Mon Sep 17 00:00:00 2001 From: Jean THOMAS Date: Fri, 10 Jul 2020 16:09:38 +0200 Subject: [PATCH] Fix formal checks for RefreshTimer --- gram/core/refresher.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/gram/core/refresher.py b/gram/core/refresher.py index 91d1d76..9101c8e 100644 --- a/gram/core/refresher.py +++ b/gram/core/refresher.py @@ -146,8 +146,8 @@ class RefreshSequencer(Elaboratable): if platform == "formal": m.d.comb += [ - Assert(countEqZero.implies(count == 0)), - Assert(countDiffZero.implies(count != 0)) + Assert(countEqZero == (count == 0)), + Assert(countDiffZero == (count != 0)), ] return m @@ -162,6 +162,9 @@ class RefreshTimer(Elaboratable): """ def __init__(self, trefi): + # TODO: we don't pass formal verification for trefi = 1 + assert trefi != 1 + self.wait = Signal() self.done = Signal() self.count = Signal(range(trefi), reset=trefi-1) @@ -172,8 +175,6 @@ class RefreshTimer(Elaboratable): trefi = self._trefi - done = Signal() - with m.If(self.wait & (self.count != 0)): m.d.sync += self.count.eq(self.count-1) @@ -186,7 +187,7 @@ class RefreshTimer(Elaboratable): ] if platform == "formal": - m.d.comb += Assert(self.done.implies(self.count == 0)) + m.d.comb += Assert(self.done == (self.count == 0)) return m -- 2.30.2