From: Cesar Strauss Date: Sat, 16 Apr 2022 20:36:04 +0000 (-0300) Subject: Enable read port for non-transparent memories X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c582e3154174755e4016669b7c5b2944a9f4d63f;p=soc.git Enable read port for non-transparent memories For some reason, the reset value (=1) of the port enable is not recognized by the formal engine, even if the simulation is fine with it. --- diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py index 297a935f..cba1ec21 100644 --- a/src/soc/regfile/sram_wrapper.py +++ b/src/soc/regfile/sram_wrapper.py @@ -599,6 +599,10 @@ class DualPortRegfile(Elaboratable): lvt_mem = Memory(width=self.we_width, depth=depth) lvt_wr = lvt_mem.write_port(granularity=1) lvt_rd = lvt_mem.read_port(transparent=self.transparent) + if not self.transparent: + # for some reason, formal proofs don't recognize the default + # reset value for this signal + m.d.comb += lvt_rd.en.eq(1) m.submodules.lvt_wr = lvt_wr m.submodules.lvt_rd = lvt_rd # generate and wire the phases for the phased memories