From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 1 Jun 2020 17:46:17 +0000 (-0400)
Subject: That was weird. For some reason it wasn't generating any ports
X-Git-Tag: div_pipeline~680
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7cfdf56c3ada3783c1c043fde94a6051e0b79b5d;p=soc.git

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 dc1c34c8..27b4fb97 100644
--- 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 c7ee9a5d..b255b7a5 100644
--- 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: