From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Thu, 28 May 2020 10:10:17 +0000 (+0100)
Subject: hmm....
X-Git-Tag: div_pipeline~776
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c82cf2bb2525eccfccc2105a506e55590bb9fd57;p=soc.git

hmm....
---

diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py
index dbb9330d..e0dc910f 100644
--- a/src/soc/regfile/formal/proof_regfile.py
+++ b/src/soc/regfile/formal/proof_regfile.py
@@ -12,8 +12,8 @@ from soc.regfile.regfile import Register
 
 
 class Driver(Register):
-    def __init__(self):
-        super().__init__(8)
+    def __init__(self, writethru=True):
+        super().__init__(8, writethru)
 
     def elaborate(self, platform):
         m = super().elaborate(platform)
@@ -30,20 +30,27 @@ class Driver(Register):
             self.read_port(f"{i}")
             self.write_port(f"{i}")
 
-        comb += reg.eq(AnyConst(8))
-
-        for i in range(len(_rdports)):
-            with m.If(_rdports[i].ren & writethru):
-                with m.If(_wrports[i].wen):
-                    comb += Assert(_rdports[i].data_o == _wrports[i].data_i)
+        sync += reg.eq(AnyConst(8))
+
+        if writethru:
+            for i in range(len(_rdports)):
+                with m.If(_rdports[i].ren):
+                    with m.If(_wrports[i].wen):
+                        pass
+                        #comb += Assert(_rdports[i].data_o == _wrports[i].data_i)
+                    with m.Else():
+                        pass
+                        #comb += Assert(_rdports[i].data_o == reg)
                 with m.Else():
-                    comb += Assert(_rdports[i].data_o == reg)
-            with m.Else():
-                comb += Assert(_rdports[i].data_o == reg)
-
-        for i in range(len(_wrports)):
-            with m.If(Past(_wrports[i].wen)):
-                sync += Assert(reg == _wrports[i].data_i)
+                    #comb += Assert(_rdports[i].data_o == reg)
+                    pass
+
+            for i in range(len(_wrports)):
+                with m.If(Past(_wrports[i].wen)):
+                    #comb += Assert(reg == _wrports[i].data_i)
+                    pass
+        else:
+            pass
 
         return m