diff --git a/cores/microwatt/checks.pfv b/cores/microwatt/checks.pfv index 1e8b5ce..81ce8da 100644 --- a/cores/microwatt/checks.pfv +++ b/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 diff --git a/cores/microwatt/microwatt/__main__.py b/cores/microwatt/microwatt/__main__.py index b492503..a5be109 100644 --- a/cores/microwatt/microwatt/__main__.py +++ b/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): diff --git a/cores/microwatt/microwatt/check/__init__.py b/cores/microwatt/microwatt/check/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/cores/microwatt/microwatt/check/storage.py b/cores/microwatt/microwatt/check/storage.py new file mode 100644 index 0000000..09a8482 --- /dev/null +++ b/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 diff --git a/power_fv/check/storage.py b/power_fv/check/storage.py new file mode 100644 index 0000000..64bcbab --- /dev/null +++ b/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