pfv.Interface: add support for skipping instructions.

The `pfv.skip` signal is used to handle cases where the DUT does not
actually execute an instruction (e.g. a no-op), which may prevent some
side-effects (e.g. GPR accesses) from being observable.

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   ),

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),
             ]

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),
             ]
 

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]

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()),