Add instruction storage check.

cores/microwatt/checks.pfv

@@ -5,7 +5,8 @@ check causal   --depth=15
 check liveness --depth=20 --skip=12 --bus-fairness
 check insn     --depth=17 --exclude=brh,brw,setbc,setbcr,setnbc,setnbcr
 
-check microwatt:storage:data --depth=15
+check microwatt:storage:insn --depth=20
+check microwatt:storage:data --depth=20
 
 build --build-dir=./build --src-dir=./src
 exit

cores/microwatt/microwatt/check/storage.py

@@ -4,16 +4,75 @@ from amaranth.utils import log2_int
 
 from amaranth_soc import wishbone
 
-from power_fv.check.storage import DataStorageCheck, DataStorageTestbench, DataStorageModel
+from power_fv.check.storage import *
 
 from ..core import *
 
 
 __all__ = [
+    "InsnStorageCheck_Microwatt", "InsnStorageTestbench_Microwatt", "InsnStorageModel_Microwatt",
     "DataStorageCheck_Microwatt", "DataStorageTestbench_Microwatt", "DataStorageModel_Microwatt",
 ]
 
 
+class InsnStorageCheck_Microwatt(InsnStorageCheck, name=("microwatt", "storage", "insn")):
+    def __init__(self, *, depth, skip, core, **kwargs):
+        if not isinstance(core, MicrowattCore):
+            raise TypeError("Core must be an instance of MicrowattCore, not {!r}"
+                            .format(core))
+        super().__init__(depth=depth, skip=skip, core=core, **kwargs)
+
+    def testbench(self):
+        return InsnStorageTestbench_Microwatt(self)
+
+
+class InsnStorageTestbench_Microwatt(InsnStorageTestbench):
+    def storage(self):
+        return InsnStorageModel_Microwatt()
+
+
+class InsnStorageModel_Microwatt(InsnStorageModel, Elaboratable):
+    def __init__(self):
+        self.addr  = Signal(64)
+        self.data  = Signal(32)
+        self._ibus = wishbone.Interface(addr_width=29, data_width=64, granularity=8,
+                                        features=("stall",))
+
+    def connect(self, dut):
+        assert isinstance(dut, MicrowattWrapper)
+        assert dut.wb_insn.addr_width  == self._ibus.addr_width
+        assert dut.wb_insn.data_width  == self._ibus.data_width
+        assert dut.wb_insn.granularity == self._ibus.granularity
+
+        return self._ibus.eq(dut.wb_insn)
+
+    def elaborate(self, platform):
+        m = Module()
+
+        with m.If(self._ibus.cyc & self._ibus.stb):
+            m.d.comb += Assume(self._ibus.stall == ~self._ibus.ack)
+
+        with m.If(self._ibus.ack):
+            m.d.comb += [
+                Assume(self._ibus.cyc & Past(self._ibus.cyc)),
+                Assume(self._ibus.stb & Past(self._ibus.stb)),
+                Assume(~Past(self._ibus.ack)),
+            ]
+
+        m.d.comb += [
+            self.addr.eq(Cat(AnyConst(32), Const(0, 32))),
+            self.data.eq(AnyConst(32)),
+        ]
+
+        with m.If(self._ibus.cyc & self._ibus.stb & self._ibus.ack & ~ResetSignal("sync")):
+            with m.If(self.addr == Cat(Const(0b000, 3), self._ibus.adr)):
+                m.d.comb += Assume(self._ibus.dat_r[:32] == self.data)
+            with m.If(self.addr == Cat(Const(0b100, 3), self._ibus.adr)):
+                m.d.comb += Assume(self._ibus.dat_r[32:] == self.data)
+
+        return m
+
+
 class DataStorageCheck_Microwatt(DataStorageCheck, name=("microwatt", "storage", "data")):
     def __init__(self, *, depth, skip, core, **kwargs):
         if not isinstance(core, MicrowattCore):
@@ -53,15 +112,18 @@ class DataStorageModel_Microwatt(DataStorageModel, Elaboratable):
         m.d.comb += [
             dbus_read .eq(self._dbus.cyc & self._dbus.stb & self._dbus.ack),
             dbus_write.eq(self._dbus.cyc & self._dbus.stb & self._dbus.ack & self._dbus.we),
-
-            Assume(self._dbus.ack.implies(Past(self._dbus.cyc) & self._dbus.cyc)),
-            Assume(self._dbus.ack.implies(Past(self._dbus.stb) & self._dbus.stb)),
-            Assume(self._dbus.ack.implies(~Past(self._dbus.ack))),
         ]
 
         with m.If(self._dbus.cyc & self._dbus.stb):
             m.d.comb += Assume(self._dbus.stall == ~self._dbus.ack)
 
+        with m.If(self._dbus.ack):
+            m.d.comb += [
+                Assume(self._dbus.cyc & Past(self._dbus.cyc)),
+                Assume(self._dbus.stb & Past(self._dbus.stb)),
+                Assume(~Past(self._dbus.ack)),
+            ]
+
         addr_lsb = log2_int(len(self._dbus.sel))
         addr_hit = Signal()
         value    = Signal(64)

power_fv/check/storage.py

@@ -6,12 +6,66 @@ from amaranth.asserts import *
 from power_fv.check import PowerFVCheck
 
 
-__all__ = ["DataStorageCheck", "DataStorageModel", "DataStorageTestbench"]
+__all__ = [
+    "InsnStorageCheck", "InsnStorageModel", "InsnStorageTestbench",
+    "DataStorageCheck", "DataStorageModel", "DataStorageTestbench",
+]
 
 
 # TODO: add support for restricting addresses to non-cachable/write-through regions.
 
 
+class InsnStorageCheck(PowerFVCheck):
+    pass
+
+
+class InsnStorageModel(metaclass=ABCMeta):
+    @abstractmethod
+    def connect(self, dut):
+        raise NotImplementedError
+
+    @abstractmethod
+    def elaborate(self, platform):
+        raise NotImplementedError
+
+
+class InsnStorageTestbench(Elaboratable, metaclass=ABCMeta):
+    def __init__(self, check):
+        if not isinstance(check, InsnStorageCheck):
+            raise TypeError("Check must be an instance of InsnStorageCheck, not {!r}"
+                            .format(check))
+        self.check = check
+        self.name  = "storage_insn_tb"
+
+    @abstractmethod
+    def storage(self):
+        raise NotImplementedError
+
+    def elaborate(self, platform):
+        m = Module()
+
+        m.submodules.dut     = dut     = self.check.dut
+        m.submodules.storage = storage = self.storage()
+
+        insn_po  = Signal(6)
+        prefixed = Signal()
+
+        m.d.comb += [
+            storage.connect(dut),
+
+            insn_po .eq(dut.pfv.insn[63-5:64-0]),
+            prefixed.eq(insn_po == 1),
+        ]
+
+        with m.If(dut.pfv.stb & ~dut.pfv.intr):
+            with m.If(dut.pfv.cia == storage.addr):
+                m.d.comb += Assert(dut.pfv.insn[32:] == storage.data)
+            with m.If(prefixed & (dut.pfv.cia + 4 == storage.addr)):
+                m.d.comb += Assert(dut.pfv.insn[:32] == storage.data)
+
+        return m
+
+
 class DataStorageCheck(PowerFVCheck):
     pass
 
@@ -73,3 +127,4 @@ class DataStorageTestbench(Elaboratable, metaclass=ABCMeta):
                     m.d.comb += Assert(byte_r_data == byte_shadow)
 
         return m
+