From 749184e96407f2ca00cb1e60f6fc1eaf140f859d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Tue, 26 Jul 2022 12:56:17 +0200 Subject: [PATCH] Add instruction storage check. --- cores/microwatt/checks.pfv | 3 +- cores/microwatt/microwatt/check/storage.py | 72 ++++++++++++++++++++-- power_fv/check/storage.py | 57 ++++++++++++++++- 3 files changed, 125 insertions(+), 7 deletions(-) diff --git a/cores/microwatt/checks.pfv b/cores/microwatt/checks.pfv index d9ca600..1d3aec7 100644 --- a/cores/microwatt/checks.pfv +++ b/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 diff --git a/cores/microwatt/microwatt/check/storage.py b/cores/microwatt/microwatt/check/storage.py index 09a8482..c31248c 100644 --- a/cores/microwatt/microwatt/check/storage.py +++ b/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) diff --git a/power_fv/check/storage.py b/power_fv/check/storage.py index 45ac8cf..0f469a5 100644 --- a/power_fv/check/storage.py +++ b/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 +