From a413025fcb7a51777ab9adf43216042339113955 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Tue, 31 May 2022 22:48:59 +0200 Subject: [PATCH] Update SPR interface and split consistency check. * Use bitmasks to describe SPR accesses at the field granularity. * Use separate checks for each SPR, instead of covering them all at once. Users may run them in the same batch, and know which SPR passes or fails its check. --- cores/microwatt/_wrapper.py | 34 ++++++------ cores/microwatt/microwatt_top.vhdl | 70 ++++++++++++------------- cores/microwatt/run.py | 7 ++- power_fv/checks/cons/all.py | 10 ++-- power_fv/checks/cons/spr.py | 69 ------------------------- power_fv/checks/cons/spr/__init__.py | 0 power_fv/checks/cons/spr/_storage.py | 77 ++++++++++++++++++++++++++++ power_fv/checks/cons/spr/all.py | 9 ++++ power_fv/checks/insn/_branch.py | 42 ++++++++++----- power_fv/pfv.py | 16 ++++-- 10 files changed, 190 insertions(+), 144 deletions(-) delete mode 100644 power_fv/checks/cons/spr.py create mode 100644 power_fv/checks/cons/spr/__init__.py create mode 100644 power_fv/checks/cons/spr/_storage.py create mode 100644 power_fv/checks/cons/spr/all.py diff --git a/cores/microwatt/_wrapper.py b/cores/microwatt/_wrapper.py index 6555c27..f34a933 100644 --- a/cores/microwatt/_wrapper.py +++ b/cores/microwatt/_wrapper.py @@ -126,40 +126,40 @@ class MicrowattWrapper(Elaboratable): ("o", "pfv_cr_w_stb", self.pfv.cr.w_stb), ("o", "pfv_cr_w_data", self.pfv.cr.w_data), - ("o", "pfv_lr_r_stb", self.pfv.lr.r_stb), + ("o", "pfv_msr_r_mask", self.pfv.msr.r_mask), + ("o", "pfv_msr_r_data", self.pfv.msr.r_data), + ("o", "pfv_msr_w_mask", self.pfv.msr.w_mask), + ("o", "pfv_msr_w_data", self.pfv.msr.w_data), + + ("o", "pfv_lr_r_mask", self.pfv.lr.r_mask), ("o", "pfv_lr_r_data", self.pfv.lr.r_data), - ("o", "pfv_lr_w_stb", self.pfv.lr.w_stb), + ("o", "pfv_lr_w_mask", self.pfv.lr.w_mask), ("o", "pfv_lr_w_data", self.pfv.lr.w_data), - ("o", "pfv_ctr_r_stb", self.pfv.ctr.r_stb), + ("o", "pfv_ctr_r_mask", self.pfv.ctr.r_mask), ("o", "pfv_ctr_r_data", self.pfv.ctr.r_data), - ("o", "pfv_ctr_w_stb", self.pfv.ctr.w_stb), + ("o", "pfv_ctr_w_mask", self.pfv.ctr.w_mask), ("o", "pfv_ctr_w_data", self.pfv.ctr.w_data), - ("o", "pfv_xer_r_stb", self.pfv.xer.r_stb), + ("o", "pfv_xer_r_mask", self.pfv.xer.r_mask), ("o", "pfv_xer_r_data", self.pfv.xer.r_data), - ("o", "pfv_xer_w_stb", self.pfv.xer.w_stb), + ("o", "pfv_xer_w_mask", self.pfv.xer.w_mask), ("o", "pfv_xer_w_data", self.pfv.xer.w_data), - ("o", "pfv_tar_r_stb", self.pfv.tar.r_stb), + ("o", "pfv_tar_r_mask", self.pfv.tar.r_mask), ("o", "pfv_tar_r_data", self.pfv.tar.r_data), - ("o", "pfv_tar_w_stb", self.pfv.tar.w_stb), + ("o", "pfv_tar_w_mask", self.pfv.tar.w_mask), ("o", "pfv_tar_w_data", self.pfv.tar.w_data), - ("o", "pfv_srr0_r_stb", self.pfv.srr0.r_stb), + ("o", "pfv_srr0_r_mask", self.pfv.srr0.r_mask), ("o", "pfv_srr0_r_data", self.pfv.srr0.r_data), - ("o", "pfv_srr0_w_stb", self.pfv.srr0.w_stb), + ("o", "pfv_srr0_w_mask", self.pfv.srr0.w_mask), ("o", "pfv_srr0_w_data", self.pfv.srr0.w_data), - ("o", "pfv_srr1_r_stb", self.pfv.srr1.r_stb), + ("o", "pfv_srr1_r_mask", self.pfv.srr1.r_mask), ("o", "pfv_srr1_r_data", self.pfv.srr1.r_data), - ("o", "pfv_srr1_w_stb", self.pfv.srr1.w_stb), + ("o", "pfv_srr1_w_mask", self.pfv.srr1.w_mask), ("o", "pfv_srr1_w_data", self.pfv.srr1.w_data), - - ("o", "pfv_msr_r_stb", self.pfv.msr.r_stb), - ("o", "pfv_msr_r_data", self.pfv.msr.r_data), - ("o", "pfv_msr_w_stb", self.pfv.msr.w_stb), - ("o", "pfv_msr_w_data", self.pfv.msr.w_data), ) with m.If(Initial()): diff --git a/cores/microwatt/microwatt_top.vhdl b/cores/microwatt/microwatt_top.vhdl index 78b9969..29374e9 100644 --- a/cores/microwatt/microwatt_top.vhdl +++ b/cores/microwatt/microwatt_top.vhdl @@ -64,40 +64,40 @@ entity toplevel is pfv_cr_w_stb : out std_ulogic_vector( 7 downto 0); pfv_cr_w_data : out std_ulogic_vector(31 downto 0); - pfv_lr_r_stb : out std_ulogic; + pfv_msr_r_mask : out std_ulogic_vector(63 downto 0); + pfv_msr_r_data : out std_ulogic_vector(63 downto 0); + pfv_msr_w_mask : out std_ulogic_vector(63 downto 0); + pfv_msr_w_data : out std_ulogic_vector(63 downto 0); + + pfv_lr_r_mask : out std_ulogic_vector(63 downto 0); pfv_lr_r_data : out std_ulogic_vector(63 downto 0); - pfv_lr_w_stb : out std_ulogic; + pfv_lr_w_mask : out std_ulogic_vector(63 downto 0); pfv_lr_w_data : out std_ulogic_vector(63 downto 0); - pfv_ctr_r_stb : out std_ulogic; + pfv_ctr_r_mask : out std_ulogic_vector(63 downto 0); pfv_ctr_r_data : out std_ulogic_vector(63 downto 0); - pfv_ctr_w_stb : out std_ulogic; + pfv_ctr_w_mask : out std_ulogic_vector(63 downto 0); pfv_ctr_w_data : out std_ulogic_vector(63 downto 0); - pfv_xer_r_stb : out std_ulogic; + pfv_xer_r_mask : out std_ulogic_vector(63 downto 0); pfv_xer_r_data : out std_ulogic_vector(63 downto 0); - pfv_xer_w_stb : out std_ulogic; + pfv_xer_w_mask : out std_ulogic_vector(63 downto 0); pfv_xer_w_data : out std_ulogic_vector(63 downto 0); - pfv_tar_r_stb : out std_ulogic; + pfv_tar_r_mask : out std_ulogic_vector(63 downto 0); pfv_tar_r_data : out std_ulogic_vector(63 downto 0); - pfv_tar_w_stb : out std_ulogic; + pfv_tar_w_mask : out std_ulogic_vector(63 downto 0); pfv_tar_w_data : out std_ulogic_vector(63 downto 0); - pfv_srr0_r_stb : out std_ulogic; + pfv_srr0_r_mask : out std_ulogic_vector(63 downto 0); pfv_srr0_r_data : out std_ulogic_vector(63 downto 0); - pfv_srr0_w_stb : out std_ulogic; + pfv_srr0_w_mask : out std_ulogic_vector(63 downto 0); pfv_srr0_w_data : out std_ulogic_vector(63 downto 0); - pfv_srr1_r_stb : out std_ulogic; + pfv_srr1_r_mask : out std_ulogic_vector(63 downto 0); pfv_srr1_r_data : out std_ulogic_vector(63 downto 0); - pfv_srr1_w_stb : out std_ulogic; - pfv_srr1_w_data : out std_ulogic_vector(63 downto 0); - - pfv_msr_r_stb : out std_ulogic; - pfv_msr_r_data : out std_ulogic_vector(63 downto 0); - pfv_msr_w_stb : out std_ulogic; - pfv_msr_w_data : out std_ulogic_vector(63 downto 0) + pfv_srr1_w_mask : out std_ulogic_vector(63 downto 0); + pfv_srr1_w_data : out std_ulogic_vector(63 downto 0) ); end entity toplevel; @@ -171,39 +171,39 @@ begin pfv_cr_w_stb <= pfv.cr.w_stb; pfv_cr_w_data <= pfv.cr.w_data; - pfv_lr_r_stb <= pfv.lr.r_stb; + pfv_msr_r_mask <= pfv.msr.r_mask; + pfv_msr_r_data <= pfv.msr.r_data; + pfv_msr_w_mask <= pfv.msr.w_mask; + pfv_msr_w_data <= pfv.msr.w_data; + + pfv_lr_r_mask <= pfv.lr.r_mask; pfv_lr_r_data <= pfv.lr.r_data; - pfv_lr_w_stb <= pfv.lr.w_stb; + pfv_lr_w_mask <= pfv.lr.w_mask; pfv_lr_w_data <= pfv.lr.w_data; - pfv_ctr_r_stb <= pfv.ctr.r_stb; + pfv_ctr_r_mask <= pfv.ctr.r_mask; pfv_ctr_r_data <= pfv.ctr.r_data; - pfv_ctr_w_stb <= pfv.ctr.w_stb; + pfv_ctr_w_mask <= pfv.ctr.w_mask; pfv_ctr_w_data <= pfv.ctr.w_data; - pfv_xer_r_stb <= pfv.xer.r_stb; + pfv_xer_r_mask <= pfv.xer.r_mask; pfv_xer_r_data <= pfv.xer.r_data; - pfv_xer_w_stb <= pfv.xer.w_stb; + pfv_xer_w_mask <= pfv.xer.w_mask; pfv_xer_w_data <= pfv.xer.w_data; - pfv_tar_r_stb <= pfv.tar.r_stb; + pfv_tar_r_mask <= pfv.tar.r_mask; pfv_tar_r_data <= pfv.tar.r_data; - pfv_tar_w_stb <= pfv.tar.w_stb; + pfv_tar_w_mask <= pfv.tar.w_mask; pfv_tar_w_data <= pfv.tar.w_data; - pfv_srr0_r_stb <= pfv.srr0.r_stb; + pfv_srr0_r_mask <= pfv.srr0.r_mask; pfv_srr0_r_data <= pfv.srr0.r_data; - pfv_srr0_w_stb <= pfv.srr0.w_stb; + pfv_srr0_w_mask <= pfv.srr0.w_mask; pfv_srr0_w_data <= pfv.srr0.w_data; - pfv_srr1_r_stb <= pfv.srr1.r_stb; + pfv_srr1_r_mask <= pfv.srr1.r_mask; pfv_srr1_r_data <= pfv.srr1.r_data; - pfv_srr1_w_stb <= pfv.srr1.w_stb; + pfv_srr1_w_mask <= pfv.srr1.w_mask; pfv_srr1_w_data <= pfv.srr1.w_data; - pfv_msr_r_stb <= pfv.msr.r_stb; - pfv_msr_r_data <= pfv.msr.r_data; - pfv_msr_w_stb <= pfv.msr.w_stb; - pfv_msr_w_data <= pfv.msr.w_data; - end architecture behave; diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index 40ed198..56de7eb 100644 --- a/cores/microwatt/run.py +++ b/cores/microwatt/run.py @@ -97,7 +97,12 @@ if __name__ == "__main__": ("cons_ia_fwd", {"post": 15}), ("cons_gpr", {"post": 15}), ("cons_cr", {"post": 15}), - ("cons_spr", {"post": 15}), + ("cons_lr", {"post": 15}), + ("cons_ctr", {"post": 15}), + ("cons_xer", {"post": 15}), + ("cons_tar", {"post": 15}), + ("cons_srr0", {"post": 15}), + ("cons_srr1", {"post": 15}), ("insn_b", {"post": 15}), ("insn_ba", {"post": 15}), diff --git a/power_fv/checks/cons/all.py b/power_fv/checks/cons/all.py index ad0aaae..e819cf8 100644 --- a/power_fv/checks/cons/all.py +++ b/power_fv/checks/cons/all.py @@ -1,5 +1,5 @@ -from .unique import * -from .ia_fwd import * -from .gpr import * -from .cr import * -from .spr import * +from .unique import * +from .ia_fwd import * +from .gpr import * +from .cr import * +from .spr.all import * diff --git a/power_fv/checks/cons/spr.py b/power_fv/checks/cons/spr.py deleted file mode 100644 index 37d0452..0000000 --- a/power_fv/checks/cons/spr.py +++ /dev/null @@ -1,69 +0,0 @@ -from collections import OrderedDict - -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - - -__all__ = ["SPRSpec", "SPRCheck"] - - -class SPRSpec(Elaboratable): - """SPR consistency specification. - - Checks that reads from supported SPRs are the last value that was written to - them. - """ - def __init__(self, post): - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spr_map = OrderedDict() - - for spr_name in ("lr", "ctr", "xer", "tar"): - spr = Record([ - ("written", 1), - ("shadow", 64), - ], name=spr_name) - spr_map[spr_name] = spr - - spec_order = AnyConst(self.pfv.order.width) - - with m.If(self.pfv.stb & (self.pfv.order <= spec_order)): - for spr_name, spr in spr_map.items(): - pfv_spr = getattr(self.pfv, spr_name) - - with m.If(pfv_spr.w_stb): - m.d.sync += [ - spr.written.eq(1), - spr.shadow .eq(pfv_spr.w_data), - ] - - with m.If(self.post.stb): - m.d.sync += [ - Assume(Past(self.pfv.stb)), - Assume(Past(self.pfv.order) == spec_order), - ] - - for spr_name, spr in spr_map.items(): - pfv_spr = getattr(self.pfv, spr_name) - - with m.If(spr.written & Past(pfv_spr.r_stb)): - m.d.sync += Assert(Past(spr.shadow) == Past(pfv_spr.r_data)) - - return m - - -class SPRCheck(PowerFVCheck, name="cons_spr"): - def get_testbench(self, dut, post): - tb_spec = SPRSpec(post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/cons/spr/__init__.py b/power_fv/checks/cons/spr/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/power_fv/checks/cons/spr/_storage.py b/power_fv/checks/cons/spr/_storage.py new file mode 100644 index 0000000..44967cf --- /dev/null +++ b/power_fv/checks/cons/spr/_storage.py @@ -0,0 +1,77 @@ +from collections import OrderedDict + +from amaranth import * +from amaranth.asserts import * + +from ... import PowerFVCheck +from .... import pfv, tb + + +__all__ = ["SPRSpec", "SPRCheck"] + + +class StorageSPRSpec(Elaboratable): + """Storage SPR specification. + + Checks that reads from supported SPRs return the last value that was written to them. + """ + def __init__(self, spr_name, spr_reset, post): + self.spr_name = spr_name + self.spr_reset = spr_reset + + self.pfv = pfv.Interface() + self.post = tb.Trigger(cycle=post) + + def triggers(self): + yield self.post + + @property + def pfv_spr(self): + return getattr(self.pfv, self.spr_name) + + def elaborate(self, platform): + m = Module() + + spr = Record([ + ("written", 1), + ("shadow", self.pfv_spr.r_data.width), + ], name=self.spr_name) + + spec_order = AnyConst(self.pfv.order.width) + + with m.If(Initial()): + m.d.sync += Assume(spr.shadow == self.spr_reset) + + with m.If(self.pfv.stb & (self.pfv.order <= spec_order)): + with m.If(self.pfv_spr.w_mask.any()): + m.d.sync += [ + spr.written.eq(1), + spr.shadow .eq((spr.shadow & ~self.pfv_spr.w_mask) | (self.pfv_spr.w_data & self.pfv_spr.w_mask)), + ] + + with m.If(self.post.stb): + m.d.sync += [ + Assume(Past(self.pfv.stb)), + Assume(Past(self.pfv.order) == spec_order), + ] + + with m.If(spr.written): + p_spr_r_mask = Past(self.pfv_spr.r_mask) + p_spr_r_data = Past(self.pfv_spr.r_data) + p_spr_shadow = Past(spr.shadow) + m.d.sync += Assert((p_spr_r_data & p_spr_r_mask) == (p_spr_shadow & p_spr_r_mask)) + + m.d.sync += Assume(spr.written & Past(self.pfv_spr.r_mask).any()) # FIXME rm + + return m + + +class StorageSPRCheck(PowerFVCheck, name="_cons_spr_storage"): + def __init_subclass__(cls, name, spr_name): + super().__init_subclass__(name) + cls.spr_name = spr_name + + def get_testbench(self, dut, post, spr_reset=0): + tb_spec = StorageSPRSpec(self.spr_name, spr_reset, post) + tb_top = tb.Testbench(tb_spec, dut) + return tb_top diff --git a/power_fv/checks/cons/spr/all.py b/power_fv/checks/cons/spr/all.py new file mode 100644 index 0000000..89fb27b --- /dev/null +++ b/power_fv/checks/cons/spr/all.py @@ -0,0 +1,9 @@ +from ._storage import StorageSPRCheck + + +class LR (StorageSPRCheck, name="cons_lr", spr_name="lr" ): pass +class CTR (StorageSPRCheck, name="cons_ctr", spr_name="ctr" ): pass +class XER (StorageSPRCheck, name="cons_xer", spr_name="xer" ): pass +class TAR (StorageSPRCheck, name="cons_tar", spr_name="tar" ): pass +class SRR0 (StorageSPRCheck, name="cons_srr0", spr_name="srr0"): pass +class SRR1 (StorageSPRCheck, name="cons_srr1", spr_name="srr1"): pass diff --git a/power_fv/checks/insn/_branch.py b/power_fv/checks/insn/_branch.py index 13aeb2c..1bd8cdf 100644 --- a/power_fv/checks/insn/_branch.py +++ b/power_fv/checks/insn/_branch.py @@ -30,11 +30,11 @@ class BranchSpec(Elaboratable): m.d.sync += [ Assume(self.pfv.stb), Assume(self.pfv.insn[32:] == spec_insn), - Assert(self.pfv.msr.w_stb), + Assert(self.pfv.msr.w_mask[63 - 0]), # MSR.SF ] msr_w_sf = Signal() - m.d.comb += msr_w_sf.eq(self.pfv.msr.w_data[63]) + m.d.comb += msr_w_sf.eq(self.pfv.msr.w_data[63 - 0]) if isinstance(spec_insn, (Instruction_B, Instruction_XL_bc)): bo_valid_patterns = [ @@ -138,6 +138,9 @@ class BranchSpec(Elaboratable): spec_lr_r_stb = Signal() spec_lr_w_stb = Signal() + + spec_lr_r_mask = Signal(64) + spec_lr_w_mask = Signal(64) spec_lr_w_data = Signal(64) if isinstance(spec_insn, (Instruction_I, Instruction_B)): @@ -150,25 +153,31 @@ class BranchSpec(Elaboratable): else: assert False + m.d.comb += spec_lr_w_stb.eq(spec_insn.lk) + cia_4 = Signal(unsigned(64)) m.d.comb += cia_4.eq(self.pfv.cia + 4) m.d.comb += [ - spec_lr_w_stb .eq(spec_insn.lk), + spec_lr_r_mask.eq(Repl(spec_lr_r_stb, 64)), + spec_lr_w_mask.eq(Repl(spec_lr_w_stb, 64)), spec_lr_w_data.eq(iea_mask(cia_4, msr_w_sf)), ] with m.If(self.post.stb & ~self.pfv.intr): m.d.sync += [ - Assert(self.pfv.lr.r_stb == spec_lr_r_stb), - Assert(self.pfv.lr.w_stb == spec_lr_w_stb), - Assert(self.pfv.lr.w_stb.implies(self.pfv.lr.w_data == spec_lr_w_data)), + Assert((self.pfv.lr.r_mask & spec_lr_r_mask) == spec_lr_r_mask), + Assert(self.pfv.lr.w_mask == spec_lr_w_mask), + Assert((self.pfv.lr.w_data & spec_lr_w_mask) == (spec_lr_w_data & spec_lr_w_mask)), ] # CTR spec_ctr_r_stb = Signal() spec_ctr_w_stb = Signal() + + spec_ctr_r_mask = Signal(64) + spec_ctr_w_mask = Signal(64) spec_ctr_w_data = Signal(64) if isinstance(spec_insn, Instruction_I): @@ -195,18 +204,23 @@ class BranchSpec(Elaboratable): else: assert False - m.d.comb += spec_ctr_w_data.eq(self.pfv.ctr.r_data - 1) + m.d.comb += [ + spec_ctr_r_mask.eq(Repl(spec_ctr_r_stb, 64)), + spec_ctr_w_mask.eq(Repl(spec_ctr_w_stb, 64)), + spec_ctr_w_data.eq(self.pfv.ctr.r_data - 1), + ] with m.If(self.post.stb & ~self.pfv.intr): m.d.sync += [ - Assert(self.pfv.ctr.r_stb == spec_ctr_r_stb), - Assert(self.pfv.ctr.w_stb == spec_ctr_w_stb), - Assert(self.pfv.ctr.w_stb.implies(self.pfv.ctr.w_data == spec_ctr_w_data)), + Assert((self.pfv.ctr.r_mask & spec_ctr_r_mask) == spec_ctr_r_mask), + Assert(self.pfv.ctr.w_mask == spec_ctr_w_mask), + Assert((self.pfv.ctr.w_data & spec_ctr_w_mask) == (spec_ctr_w_data & spec_ctr_w_mask)), ] # TAR - spec_tar_r_stb = Signal() + spec_tar_r_stb = Signal() + spec_tar_r_mask = Signal(64) if isinstance(spec_insn, (Instruction_I, Instruction_B)): m.d.comb += spec_tar_r_stb.eq(0) @@ -218,10 +232,10 @@ class BranchSpec(Elaboratable): else: assert False + m.d.comb += spec_tar_r_mask.eq(Repl(spec_tar_r_stb, 64)) + with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert(self.pfv.tar.r_stb == spec_tar_r_stb), - ] + m.d.sync += Assert((self.pfv.tar.r_mask & spec_tar_r_mask) == spec_tar_r_mask) return m diff --git a/power_fv/pfv.py b/power_fv/pfv.py index 9f98a35..9f1022d 100644 --- a/power_fv/pfv.py +++ b/power_fv/pfv.py @@ -66,13 +66,24 @@ class Interface(Record): ]), ] + # MSR + + layout += [ + ("msr", [ + ("r_mask", 64), + ("r_data", 64), + ("w_mask", 64), + ("w_data", 64), + ]), + ] + # SPRs layout += [ (spr_name, [ - ("r_stb", 1), + ("r_mask", 64), ("r_data", 64), - ("w_stb", 1), + ("w_mask", 64), ("w_data", 64), ]) for spr_name in ( "lr", @@ -81,7 +92,6 @@ class Interface(Record): "xer", "srr0", "srr1", - "msr", ) ]