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

@@ -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()):

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_mask : out std_ulogic_vector(63 downto 0);
-        pfv_srr1_w_data : out std_ulogic_vector(63 downto 0);
+        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)
         );
 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;

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}),

power_fv/checks/cons/all.py

@@ -1,5 +1,5 @@
-from .unique import *
+from .unique  import *
-from .ia_fwd import *
+from .ia_fwd  import *
-from .gpr    import *
+from .gpr     import *
-from .cr     import *
+from .cr      import *
-from .spr    import *
+from .spr.all import *

power_fv/checks/cons/spr.py

@@ -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

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

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

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.r_mask & spec_lr_r_mask) == spec_lr_r_mask),
-                Assert(self.pfv.lr.w_stb == spec_lr_w_stb),
+                Assert(self.pfv.lr.w_mask == spec_lr_w_mask),
-                Assert(self.pfv.lr.w_stb.implies(self.pfv.lr.w_data == spec_lr_w_data)),
+                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.r_mask & spec_ctr_r_mask) == spec_ctr_r_mask),
-                Assert(self.pfv.ctr.w_stb == spec_ctr_w_stb),
+                Assert(self.pfv.ctr.w_mask == spec_ctr_w_mask),
-                Assert(self.pfv.ctr.w_stb.implies(self.pfv.ctr.w_data == spec_ctr_w_data)),
+                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 += [
+            m.d.sync += Assert((self.pfv.tar.r_mask & spec_tar_r_mask) == spec_tar_r_mask)
-                Assert(self.pfv.tar.r_stb == spec_tar_r_stb),
-            ]
 
         return m
 

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",
             )
         ]