From 3e8a8d1921a136451e282b375a2d35a868d84f01 Mon Sep 17 00:00:00 2001 From: colepoirier Date: Thu, 28 May 2020 14:58:03 -0700 Subject: [PATCH] Added Initial() synchronous check with draft truth table for rp.ren and wp.wen of Register() in proof_regfile --- src/soc/regfile/formal/proof_regfile.py | 51 ++++++++++++++++--------- 1 file changed, 34 insertions(+), 17 deletions(-) diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py index e0dc910f..cbfa0c96 100644 --- a/src/soc/regfile/formal/proof_regfile.py +++ b/src/soc/regfile/formal/proof_regfile.py @@ -32,25 +32,42 @@ class Driver(Register): 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) + rst = ResetSignal() + + init = Initial() + + # Most likely incorrect 4-way truth table + # + # rp.ren wp.wen rp.data_o reg + # 0 0 rp.data_o reg + # 0 1 rp.data_o wp.data_i + # 1 0 reg reg + # 1 1 wp.data_i wp.data_i + + with m.If(init): + comb += Assume(rst == 1) + + with m.Else(): + comb += Assume(rst == 0) + 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(): - pass #comb += Assert(_rdports[i].data_o == reg) - with m.Else(): - #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 + 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