From 7cfdf56c3ada3783c1c043fde94a6051e0b79b5d Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 1 Jun 2020 13:46:17 -0400 Subject: [PATCH] That was weird. For some reason it wasn't generating any ports --- src/soc/regfile/formal/proof_regfile.py | 8 ++++---- src/soc/regfile/regfile.py | 4 +++- 2 files changed, 7 insertions(+), 5 deletions(-) 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: -- 2.30.2