Add data storage check.

This check is implemented in two parts:
- an implementation-dependant DataStorageModel, which is connected to
  the DUT and emulates bus accesses to a r/w memory.
- a DataStorageTestbench, which checks that a load from a given address
  returns the last value that was stored to it.

cores/microwatt/checks.pfv

@@ -3,5 +3,7 @@ check cia    --depth=15
 check gpr    --depth=15
 check insn   --depth=15
 
+check microwatt:storage:data --depth=15
+
 build --build-dir=./build --src-dir=./src
 exit

cores/microwatt/microwatt/__main__.py

@@ -2,6 +2,7 @@ from pathlib import PurePath
 from power_fv.session import PowerFVSession
 
 from .core import MicrowattCore
+from .check.storage import *
 
 
 class MicrowattSession(PowerFVSession, core_cls=MicrowattCore):

cores/microwatt/microwatt/check/storage.py

@@ -0,0 +1,82 @@
+from amaranth import *
+from amaranth.asserts import *
+from amaranth.utils import log2_int
+
+from amaranth_soc import wishbone
+
+from power_fv.check.storage import DataStorageCheck, DataStorageTestbench, DataStorageModel
+
+from ..core import *
+
+
+__all__ = [
+    "DataStorageCheck_Microwatt", "DataStorageTestbench_Microwatt", "DataStorageModel_Microwatt",
+]
+
+
+class DataStorageCheck_Microwatt(DataStorageCheck, name=("microwatt", "storage", "data")):
+    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 DataStorageTestbench_Microwatt(self)
+
+
+class DataStorageTestbench_Microwatt(DataStorageTestbench):
+    def storage(self):
+        return DataStorageModel_Microwatt()
+
+
+class DataStorageModel_Microwatt(DataStorageModel, Elaboratable):
+    def __init__(self):
+        self.addr  = Signal(64)
+        self._dbus = wishbone.Interface(addr_width=29, data_width=64, granularity=8,
+                                        features=("stall",))
+
+    def connect(self, dut):
+        assert isinstance(dut, MicrowattWrapper)
+        assert dut.wb_data.addr_width  == self._dbus.addr_width
+        assert dut.wb_data.data_width  == self._dbus.data_width
+        assert dut.wb_data.granularity == self._dbus.granularity
+
+        return self._dbus.eq(dut.wb_data)
+
+    def elaborate(self, platform):
+        m = Module()
+
+        dbus_read  = Signal()
+        dbus_write = Signal()
+
+        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)
+
+        addr_lsb = log2_int(len(self._dbus.sel))
+        addr_hit = Signal()
+        value    = Signal(64)
+
+        m.d.comb += [
+            self.addr.eq(Cat(AnyConst(32), Const(0, 32))),
+            addr_hit.eq(self._dbus.adr == self.addr[addr_lsb:32]),
+        ]
+
+        with m.If(dbus_read & addr_hit & ~ResetSignal("sync")):
+            m.d.comb += Assume(self._dbus.dat_r == value)
+
+        with m.If(dbus_write & addr_hit):
+            for i, sel_bit in enumerate(self._dbus.sel):
+                with m.If(sel_bit):
+                    m.d.sync += value[i*8:i*8+8].eq(self._dbus.dat_w[i*8:i*8+8])
+
+        return m

power_fv/check/storage.py

@@ -0,0 +1,69 @@
+from abc import ABCMeta, abstractmethod
+
+from amaranth import *
+from amaranth.asserts import *
+
+from power_fv.check import PowerFVCheck
+
+
+__all__ = ["DataStorageCheck", "DataStorageModel", "DataStorageTestbench"]
+
+
+# TODO: add support for restricting addresses to non-cachable/write-through regions.
+
+
+class DataStorageCheck(PowerFVCheck):
+    pass
+
+
+class DataStorageModel(metaclass=ABCMeta):
+    @abstractmethod
+    def connect(self, dut):
+        raise NotImplementedError
+
+    @abstractmethod
+    def elaborate(self, platform):
+        raise NotImplementedError
+
+
+class DataStorageTestbench(Elaboratable, metaclass=ABCMeta):
+    def __init__(self, check):
+        if not isinstance(check, DataStorageCheck):
+            raise TypeError("Check must be an instance of DataStorageCheck, not {!r}"
+                            .format(check))
+        self.check = check
+        self.name  = "storage_data_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()
+
+        written = Signal(64 // 8)
+        shadow  = Signal(64)
+
+        m.d.comb += storage.connect(dut)
+
+        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]
+                byte_w_stb  = dut.pfv.mem.w_mask[i]
+                byte_w_data = dut.pfv.mem.w_data[i*8:i*8+8]
+                byte_r_stb  = dut.pfv.mem.r_mask[i]
+                byte_r_data = dut.pfv.mem.r_data[i*8:i*8+8]
+
+                with m.If(byte_w_stb):
+                    m.d.sync += [
+                        byte_written.eq(1),
+                        byte_shadow .eq(byte_w_data),
+                    ]
+
+                with m.If(byte_r_stb & byte_written):
+                    m.d.comb += Assert(byte_r_data == byte_shadow)
+
+        return m