Add sync Assert for _wrports 'wen' signal in proof_regfile.py, proof

still not working

diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py
index 38f18479c007e86e3e7c8a57c528d708a51dd2e5..dbb9330d2e68ba9f1f941487b9e094942643d71a 100644 (file)
--- a/src/soc/regfile/formal/proof_regfile.py
+++ b/src/soc/regfile/formal/proof_regfile.py
@@ -18,6 +18,7 @@ class Driver(Register):
     def elaborate(self, platform):
         m = super().elaborate(platform)
         comb = m.d.comb
+        sync = m.d.sync
 
         width     = self.width
         writethru = self.writethru
@@ -40,6 +41,10 @@ class Driver(Register):
             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)
+
         return m