From: Jean THOMAS <git0@pub.jeanthomas.me>
Date: Fri, 10 Jul 2020 14:09:38 +0000 (+0200)
Subject: Fix formal checks for RefreshTimer
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b7ecdeca26d6ae241ab438d9c1c9ee0df4f1f649;p=gram.git

Fix formal checks for RefreshTimer
---

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