That was weird. For some reason it wasn't generating any ports

diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py
index dc1c34c81e2acfcee9638a2d3f495d3cee147d60..27b4fb977d543dbffdf5ff3092acab70d47acb50 100644 (file)
--- a/src/soc/regfile/formal/proof_regfile.py
+++ b/src/soc/regfile/formal/proof_regfile.py
@@ -14,6 +14,9 @@ from soc.regfile.regfile import Register
 class Driver(Register):
     def __init__(self, writethru=True):
         super().__init__(8, writethru)
+        for i in range(1): # just do one for now
+            self.read_port(f"{i}")
+            self.write_port(f"{i}")
 
     def elaborate(self, platform):
         m = super().elaborate(platform)
@@ -26,9 +29,6 @@ class Driver(Register):
         _wrports  = self._wrports
         reg       = self.reg
 
-        for i in range(1): # just do one for now
-            self.read_port(f"{i}")
-            self.write_port(f"{i}")
 
         comb += _wrports[0].data_i.eq(AnyConst(8))
         comb += _wrports[0].wen.eq(AnyConst(1))
@@ -66,7 +66,7 @@ class Driver(Register):
             comb += Assume(rst == 0)
 
             # If there is no read, then data_o should be 0
-            with m.If(_rdports[0].ren):
+            with m.If(_rdports[0].ren == 0):
                 comb += Assert(_rdports[0].data_o == 0)
 
             # If there is a read request

diff --git a/src/soc/regfile/regfile.py b/src/soc/regfile/regfile.py
index c7ee9a5dbbcf76bee7b5b2ba53bcd5305e67c4ff..b255b7a51e42fcba19f99d638b9ee4c55b3afc28 100644 (file)
--- a/src/soc/regfile/regfile.py
+++ b/src/soc/regfile/regfile.py
@@ -56,7 +56,7 @@ class Register(Elaboratable):
 
         # read ports. has write-through detection (returns data written)
         for rp in self._rdports:
-            with m.If(rp.ren):
+            with m.If(rp.ren == 1):
                 if self.writethru:
                     wr_detect = Signal(reset_less=False)
                     m.d.comb += wr_detect.eq(0)
@@ -68,6 +68,8 @@ class Register(Elaboratable):
                         m.d.comb += rp.data_o.eq(reg)
                 else:
                     m.d.comb += rp.data_o.eq(reg)
+            with m.Else():
+                m.d.comb += rp.data_o.eq(0)
 
         # write ports, delayed by 1 cycle
         for wp in self._wrports: