From 133771e295ad523cb6c829a003f48ffdf30a3c65 Mon Sep 17 00:00:00 2001
From: colepoirier <colepoirier@gmail.com>
Date: Wed, 27 May 2020 18:11:25 -0700
Subject: [PATCH] Add sync Assert for _wrports 'wen' signal in
 proof_regfile.py, proof still not working

---
 src/soc/regfile/formal/proof_regfile.py | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py
index 38f18479..dbb9330d 100644
--- 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
 
 
-- 
2.30.2