diff --git a/cores/microwatt/microwatt/core.py b/cores/microwatt/microwatt/core.py index cbef745..afd5d70 100644 --- a/cores/microwatt/microwatt/core.py +++ b/cores/microwatt/microwatt/core.py @@ -236,6 +236,7 @@ class MicrowattWrapper(Elaboratable): ("o", "pfv_out.intr" , self.pfv.intr ), ("o", "pfv_out.cia" , self.pfv.cia ), ("o", "pfv_out.nia" , self.pfv.nia ), + ("o", "pfv_out.skip" , self.pfv.skip ), ("o", "pfv_out.ra" , self.pfv.ra ), ("o", "pfv_out.rb" , self.pfv.rb ), ("o", "pfv_out.rs" , self.pfv.rs ), diff --git a/power_fv/check/gpr.py b/power_fv/check/gpr.py index 3c6acc4..5aebbdb 100644 --- a/power_fv/check/gpr.py +++ b/power_fv/check/gpr.py @@ -66,7 +66,7 @@ class GPRTestbench(Elaboratable): m.d.comb += gpr_conflict.curr.eq(1) m.d.sync += gpr_conflict.prev.eq(dut.pfv.order < spec_order) - with m.If(dut.pfv.stb & (dut.pfv.order < spec_order)): + with m.If(dut.pfv.stb & (dut.pfv.order < spec_order) & ~dut.pfv.skip): with m.If(gpr_write.any()): m.d.sync += gpr_written.prev.eq(1) with m.If(gpr_write.ra): @@ -82,6 +82,7 @@ class GPRTestbench(Elaboratable): m.d.comb += [ Assume(dut.pfv.stb), Assume(dut.pfv.order == spec_order), + Assume(~dut.pfv.skip), Assert(~gpr_conflict.curr), Assert(~gpr_conflict.prev), ] diff --git a/power_fv/check/insn/__init__.py b/power_fv/check/insn/__init__.py index 13cc934..2eec96f 100644 --- a/power_fv/check/insn/__init__.py +++ b/power_fv/check/insn/__init__.py @@ -58,6 +58,7 @@ class InsnTestbench(Elaboratable): m.d.comb += [ Assume(dut.pfv.stb), Assume(dut.pfv.insn == spec.pfv.insn), + Assume(~dut.pfv.skip), Assert(dut.pfv.intr == spec.pfv.intr), ] diff --git a/power_fv/check/storage.py b/power_fv/check/storage.py index 64bcbab..45ac8cf 100644 --- a/power_fv/check/storage.py +++ b/power_fv/check/storage.py @@ -49,6 +49,12 @@ class DataStorageTestbench(Elaboratable, metaclass=ABCMeta): m.d.comb += storage.connect(dut) + with m.If(dut.pfv.stb & dut.pfv.skip): + m.d.comb += [ + Assert(~dut.pfv.mem.r_mask.any()), + Assert(~dut.pfv.mem.w_mask.any()), + ] + with m.If(dut.pfv.stb & (dut.pfv.mem.addr == storage.addr)): for i, byte_written in enumerate(written): byte_shadow = shadow[i*8:i*8+8] diff --git a/power_fv/pfv.py b/power_fv/pfv.py index d5adbff..51dde7b 100644 --- a/power_fv/pfv.py +++ b/power_fv/pfv.py @@ -59,6 +59,7 @@ class Interface(Record): ("intr" , unsigned( 1)), ("cia" , unsigned(64)), ("nia" , unsigned(64)), + ("skip" , unsigned( 1)), ("ra", gprf_port_layout()), ("rb", gprf_port_layout()),