From c82cf2bb2525eccfccc2105a506e55590bb9fd57 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Thu, 28 May 2020 11:10:17 +0100 Subject: [PATCH] hmm.... --- src/soc/regfile/formal/proof_regfile.py | 37 +++++++++++++++---------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py index dbb9330d..e0dc910f 100644 --- a/src/soc/regfile/formal/proof_regfile.py +++ b/src/soc/regfile/formal/proof_regfile.py @@ -12,8 +12,8 @@ from soc.regfile.regfile import Register class Driver(Register): - def __init__(self): - super().__init__(8) + def __init__(self, writethru=True): + super().__init__(8, writethru) def elaborate(self, platform): m = super().elaborate(platform) @@ -30,20 +30,27 @@ class Driver(Register): self.read_port(f"{i}") self.write_port(f"{i}") - comb += reg.eq(AnyConst(8)) - - for i in range(len(_rdports)): - with m.If(_rdports[i].ren & writethru): - with m.If(_wrports[i].wen): - comb += Assert(_rdports[i].data_o == _wrports[i].data_i) + sync += reg.eq(AnyConst(8)) + + if writethru: + for i in range(len(_rdports)): + with m.If(_rdports[i].ren): + with m.If(_wrports[i].wen): + pass + #comb += Assert(_rdports[i].data_o == _wrports[i].data_i) + with m.Else(): + pass + #comb += Assert(_rdports[i].data_o == reg) with m.Else(): - comb += Assert(_rdports[i].data_o == reg) - with m.Else(): - comb += Assert(_rdports[i].data_o == reg) - - for i in range(len(_wrports)): - with m.If(Past(_wrports[i].wen)): - sync += Assert(reg == _wrports[i].data_i) + #comb += Assert(_rdports[i].data_o == reg) + pass + + for i in range(len(_wrports)): + with m.If(Past(_wrports[i].wen)): + #comb += Assert(reg == _wrports[i].data_i) + pass + else: + pass return m -- 2.30.2