From c582e3154174755e4016669b7c5b2944a9f4d63f Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 16 Apr 2022 17:36:04 -0300 Subject: [PATCH] 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. --- src/soc/regfile/sram_wrapper.py | 4 ++++ 1 file changed, 4 insertions(+) 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 -- 2.30.2