Refactor to facilitate integration with CLIs and config files.

* Checks are now split in two modules: checks.cons for consistency
  checks, checks.insn for instructions.

* Checks are derived from PowerFVCheck and have a shorthand (e.g.
  "insn_b"). PowerFVCheck holds a mapping between its subclasses and
  their shorthands.

* Instruction checks definitions have been simplified to one-liners,
  and grouped into a single file.

* A Trigger class has been added to define testbench triggers.

cores/microwatt/run.py

@@ -1,11 +1,11 @@
 import argparse
-import importlib
 import os
 import multiprocessing
 
 from amaranth import *
 
-from power_fv.tb import Testbench
+from power_fv.checks import *
+from power_fv.checks.all import *
 from power_fv.build import SymbiYosysPlatform
 
 from _wrapper import MicrowattWrapper
@@ -58,22 +58,23 @@ def microwatt_files():
     yield top_filename, top_contents
 
 
-def run_check(module_name, pre, post):
-    module = importlib.import_module(f".{module_name}", package="power_fv.checks")
-    check  = module.Check()
-    cpu    = MicrowattWrapper()
-    top    = Testbench(check, cpu, t_pre=pre, t_post=post)
+def run_check(*args):
+    check_name, tb_args = args
+
+    check = PowerFVCheck.registry[check_name]()
+    dut   = MicrowattWrapper()
+    tb    = check.get_testbench(dut, **tb_args)
 
     platform = SymbiYosysPlatform()
     for filename, contents in microwatt_files():
         platform.add_file(filename, contents)
 
-    top_name  = "{}_tb".format(module_name)
-    build_dir = "build/{}".format(top_name)
+    tb_name   = "{}_tb".format(check_name)
+    build_dir = "build/{}".format(tb_name)
 
     platform.build(
-        top       = top,
-        name      = top_name,
+        top       = tb,
+        name      = tb_name,
         build_dir = build_dir,
         mode      = "bmc",
         ghdl_opts = "--std=08",
@@ -92,28 +93,26 @@ if __name__ == "__main__":
     args = parser.parse_args()
 
     checks = [
-        # name           pre   post
-        ("unique",       12,   15),
-        ("ia_fwd",       None, 15),
-        ("gpr",          None, 15),
-        ("cr",           None, 15),
-        ("spr",          None, 15),
-
-        ("insn_b",       None, 15),
-        ("insn_ba",      None, 15),
-        ("insn_bl",      None, 15),
-        ("insn_bla",     None, 15),
-        ("insn_bc",      None, 15),
-        ("insn_bca",     None, 15),
-        ("insn_bcl",     None, 15),
-        ("insn_bcla",    None, 15),
-
-        ("insn_bclr",    None, 15),
-        ("insn_bclrl",   None, 15),
-        ("insn_bcctr",   None, 15),
-        ("insn_bcctrl",  None, 15),
-        ("insn_bctar",   None, 15),
-        ("insn_bctarl",  None, 15),
+        ("cons_unique",  {"post": 15, "pre": 12}),
+        ("cons_ia_fwd",  {"post": 15}),
+        ("cons_gpr",     {"post": 15}),
+        ("cons_cr",      {"post": 15}),
+        ("cons_spr",     {"post": 15}),
+
+        ("insn_b",       {"post": 15}),
+        ("insn_ba",      {"post": 15}),
+        ("insn_bl",      {"post": 15}),
+        ("insn_bla",     {"post": 15}),
+        ("insn_bc",      {"post": 15}),
+        ("insn_bca",     {"post": 15}),
+        ("insn_bcl",     {"post": 15}),
+        ("insn_bcla",    {"post": 15}),
+        ("insn_bclr",    {"post": 15}),
+        ("insn_bclrl",   {"post": 15}),
+        ("insn_bcctr",   {"post": 15}),
+        ("insn_bcctrl",  {"post": 15}),
+        ("insn_bctar",   {"post": 15}),
+        ("insn_bctarl",  {"post": 15}),
     ]
 
     with multiprocessing.Pool(processes=args.jobs) as pool:

power_fv/build/plat.py

@@ -116,7 +116,7 @@ class SymbiYosysPlatform(TemplatedPlatform):
         if not isinstance(top, tb.Testbench):
             raise TypeError("Top-level must be an instance of power_fv.tb.Testbench")
 
-        skip  = str(top.t_post)
-        depth = str(top.t_post + 1)
+        depth = str(top.bmc_depth)
+        skip  = str(top.bmc_depth - 1)
 
         return super().build(top, mode=mode, depth=depth, skip=skip, **kwargs)

power_fv/checks/__init__.py

@@ -1,5 +1,12 @@
-from .cr     import *
-from .gpr    import *
-from .ia_fwd import *
-from .spr    import *
-from .unique import *
+class PowerFVCheck:
+    registry = {}
+    name     = None
+
+    def __init_subclass__(cls, name):
+        if name in cls.registry:
+            raise ValueError("Check name {!r} is already registered".format(name))
+        cls.registry[name] = cls
+        cls.name = name
+
+    def get_testbench(self, dut, *args, **kwargs):
+        raise NotImplementedError

power_fv/checks/all.py

@@ -0,0 +1,2 @@
+from .cons.all import *
+from .insn.all import *

power_fv/checks/cons/all.py

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

power_fv/checks/cons/cr.py

@@ -1,23 +1,24 @@
 from amaranth import *
 from amaranth.asserts import *
 
-from .. import pfv
+from .. import PowerFVCheck
+from ... import pfv, tb
 
 
-__all__ = ["Check"]
+__all__ = ["CRSpec", "CRCheck"]
 
 
-class Check(Elaboratable):
-    """Condition Register check.
+class CRSpec(Elaboratable):
+    """Condition Register consistency specification.
 
-    Checks that reads from CR fields are consistent with the last value that was written to them.
+    Checks that reads from CR fields return the last value that was written to them.
     """
-    def __init__(self):
+    def __init__(self, post):
         self.pfv  = pfv.Interface()
-        self.trig = Record([
-            ("pre",  1),
-            ("post", 1),
-        ])
+        self.post = tb.Trigger(cycle=post)
+
+    def triggers(self):
+        yield self.post
 
     def elaborate(self, platform):
         m = Module()
@@ -56,7 +57,7 @@ class Check(Elaboratable):
                         cr_field.shadow .eq(cr_field.pfv.w_data),
                     ]
 
-        with m.If(self.trig.post):
+        with m.If(self.post.stb):
             m.d.sync += [
                 Assume(Past(self.pfv.stb)),
                 Assume(Past(self.pfv.order) == spec_order),
@@ -68,3 +69,10 @@ class Check(Elaboratable):
                         m.d.sync += Assert(Past(cr_field.pfv.r_data) == Past(cr_field.shadow))
 
         return m
+
+
+class CRCheck(PowerFVCheck, name="cons_cr"):
+    def get_testbench(self, dut, post):
+        tb_spec = CRSpec(post)
+        tb_top  = tb.Testbench(tb_spec, dut)
+        return tb_top

power_fv/checks/cons/gpr.py

@@ -1,26 +1,27 @@
 from amaranth import *
 from amaranth.asserts import *
 
-from .. import pfv
+from .. import PowerFVCheck
+from ... import pfv, tb
 
 
-__all__ = ["Check"]
+__all__ = ["GPRSpec", "GPRCheck"]
 
 
-class Check(Elaboratable):
-    """General Purpose Registers check.
+class GPRSpec(Elaboratable):
+    """GPR consistency specification.
 
     Checks that:
-      * reads from a GPR are consistent with the last value that was written to it;
+      * reads from a GPR return the last value that was written to it;
       * writes to multiple GPRs by a single instruction (e.g. load with update) do not target the
         same register.
     """
-    def __init__(self):
+    def __init__(self, post):
         self.pfv  = pfv.Interface()
-        self.trig = Record([
-            ("pre",  1),
-            ("post", 1),
-        ])
+        self.post = tb.Trigger(cycle=post)
+
+    def triggers(self):
+        yield self.post
 
     def elaborate(self, platform):
         m = Module()
@@ -58,7 +59,7 @@ class Check(Elaboratable):
                 with m.Else():
                     m.d.sync += gpr_shadow.eq(self.pfv.rt.w_data)
 
-        with m.If(self.trig.post):
+        with m.If(self.post.stb):
             m.d.sync += [
                 Assume(Past(self.pfv.stb)),
                 Assume(Past(self.pfv.order) == spec_order),
@@ -75,3 +76,10 @@ class Check(Elaboratable):
                     m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rt.r_data))
 
         return m
+
+
+class GPRCheck(PowerFVCheck, name="cons_gpr"):
+    def get_testbench(self, dut, post):
+        tb_spec = GPRSpec(post)
+        tb_top  = tb.Testbench(tb_spec, dut)
+        return tb_top

power_fv/checks/cons/ia_fwd.py

@@ -1,24 +1,25 @@
 from amaranth import *
 from amaranth.asserts import *
 
-from .. import pfv
+from .. import PowerFVCheck
+from ... import pfv, tb
 
 
-__all__ = ["Check"]
+__all__ = ["IAForwardSpec", "IAForwardCheck"]
 
 
-class Check(Elaboratable):
-    """IA forward check.
+class IAForwardSpec(Elaboratable):
+    """IA forward specification.
 
-    Given two instructions retiring in order, check that the NIA of the first matches the CIA
+    Given two instructions retiring in order, the NIA of the first must match the CIA
     of the second.
     """
-    def __init__(self):
+    def __init__(self, post):
         self.pfv  = pfv.Interface()
-        self.trig = Record([
-            ("pre",  1),
-            ("post", 1),
-        ])
+        self.post = tb.Trigger(cycle=post)
+
+    def triggers(self):
+        yield self.post
 
     def elaborate(self, platform):
         m = Module()
@@ -33,7 +34,7 @@ class Check(Elaboratable):
                 pred_nia.eq(self.pfv.nia)
             ]
 
-        with m.If(self.trig.post):
+        with m.If(self.post.stb):
             m.d.sync += [
                 Assume(self.pfv.stb),
                 Assume(self.pfv.order == pred_order + 1),
@@ -42,3 +43,10 @@ class Check(Elaboratable):
             ]
 
         return m
+
+
+class IAForwardCheck(PowerFVCheck, name="cons_ia_fwd"):
+    def get_testbench(self, dut, post):
+        tb_spec = IAForwardSpec(post)
+        tb_top  = tb.Testbench(tb_spec, dut)
+        return tb_top

power_fv/checks/cons/spr.py

@@ -3,24 +3,25 @@ from collections import OrderedDict
 from amaranth import *
 from amaranth.asserts import *
 
-from .. import pfv
+from .. import PowerFVCheck
+from ... import pfv, tb
 
 
-__all__ = ["Check"]
+__all__ = ["SPRSpec", "SPRCheck"]
 
 
-class Check(Elaboratable):
-    """Special Purpose Registers check.
+class SPRSpec(Elaboratable):
+    """SPR consistency specification.
 
-    Checks that reads from supported SPRs are consistent with the last value that was written to
+    Checks that reads from supported SPRs are the last value that was written to
     them.
     """
-    def __init__(self):
+    def __init__(self, post):
         self.pfv  = pfv.Interface()
-        self.trig = Record([
-            ("pre",  1),
-            ("post", 1),
-        ])
+        self.post = tb.Trigger(cycle=post)
+
+    def triggers(self):
+        yield self.post
 
     def elaborate(self, platform):
         m = Module()
@@ -46,7 +47,7 @@ class Check(Elaboratable):
                         spr.shadow .eq(pfv_spr.w_data),
                     ]
 
-        with m.If(self.trig.post):
+        with m.If(self.post.stb):
             m.d.sync += [
                 Assume(Past(self.pfv.stb)),
                 Assume(Past(self.pfv.order) == spec_order),
@@ -59,3 +60,10 @@ class Check(Elaboratable):
                     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/unique.py

@@ -0,0 +1,49 @@
+from amaranth import *
+from amaranth.asserts import *
+
+from .. import PowerFVCheck
+from ... import pfv, tb
+
+
+__all__ = ["UniquenessSpec", "UniquenessCheck"]
+
+
+class UniquenessSpec(Elaboratable):
+    """Uniqueness specification.
+
+    A core cannot retire two instructions that share the same `pfv.order` identifier.
+    """
+    def __init__(self, pre, post):
+        self.pfv  = pfv.Interface()
+        self.pre  = tb.Trigger(cycle=pre)
+        self.post = tb.Trigger(cycle=post)
+
+    def triggers(self):
+        yield from (self.pre, self.post)
+
+    def elaborate(self, platform):
+        m = Module()
+
+        spec_order = AnyConst(self.pfv.order.shape())
+        duplicate  = Signal()
+
+        with m.If(self.pre.stb):
+            m.d.sync += [
+                Assume(self.pfv.stb),
+                Assume(spec_order == self.pfv.order),
+                Assume(~duplicate),
+            ]
+        with m.Elif(self.pfv.stb & (self.pfv.order == spec_order)):
+            m.d.sync += duplicate.eq(1)
+
+        with m.If(self.post.stb):
+            m.d.sync += Assert(~duplicate)
+
+        return m
+
+
+class UniquenessCheck(PowerFVCheck, name="cons_unique"):
+    def get_testbench(self, dut, pre, post):
+        tb_spec = UniquenessSpec(pre, post)
+        tb_top  = tb.Testbench(tb_spec, dut)
+        return tb_top

power_fv/checks/insn/_branch.py

@@ -1,33 +1,32 @@
 from amaranth import *
 from amaranth.asserts import *
 
-from .. import pfv
-from ..insn import *
-from ..utils import iea_mask
+from .. import PowerFVCheck
+from ... import pfv, tb
+from ...utils import iea_mask
 
+from ._fmt  import *
+from ._insn import *
 
-__all__ = ["Check"]
 
+__all__ = ["BranchSpec", "BranchCheck"]
 
-class Check(Elaboratable):
-    _insn_cls = None
 
-    def __init_subclass__(cls, *, insn_cls):
-        cls._insn_cls = insn_cls
+class BranchSpec(Elaboratable):
+    def __init__(self, insn_cls, post):
+        self.insn_cls = insn_cls
+        self.pfv      = pfv.Interface()
+        self.post     = tb.Trigger(cycle=post)
 
-    def __init__(self):
-        self.pfv  = pfv.Interface()
-        self.trig = Record([
-            ("pre",  1),
-            ("post", 1),
-        ])
+    def triggers(self):
+        yield self.post
 
     def elaborate(self, platform):
         m = Module()
 
-        spec_insn = self._insn_cls()
+        spec_insn = self.insn_cls()
 
-        with m.If(self.trig.post):
+        with m.If(self.post.stb):
             m.d.sync += [
                 Assume(self.pfv.stb),
                 Assume(self.pfv.insn[32:] == spec_insn),
@@ -37,7 +36,7 @@ class Check(Elaboratable):
         msr_w_sf = Signal()
         m.d.comb += msr_w_sf.eq(self.pfv.msr.w_data[63])
 
-        if isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+        if isinstance(spec_insn, (Instruction_B, Instruction_XL_bc)):
             bo_valid_patterns = [
                 "001--",
                 "011--",
@@ -57,7 +56,7 @@ class Check(Elaboratable):
             bo_invalid = Signal()
             m.d.comb += bo_invalid.eq(~spec_insn.bo.matches(*bo_valid_patterns))
 
-            with m.If(self.trig.post):
+            with m.If(self.post.stb):
                 m.d.sync += Assert(bo_invalid.implies(self.pfv.intr))
 
         # NIA
@@ -73,7 +72,7 @@ class Check(Elaboratable):
                 offset.eq(spec_insn.li)
             ]
 
-        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_bc)):
             cond_bit = Signal()
             ctr_any  = Signal()
             cond_ok  = Signal()
@@ -116,7 +115,7 @@ class Check(Elaboratable):
 
         m.d.comb += spec_nia.eq(iea_mask(target, msr_w_sf))
 
-        with m.If(self.trig.post & ~self.pfv.intr):
+        with m.If(self.post.stb & ~self.pfv.intr):
             m.d.sync += Assert(self.pfv.nia == spec_nia)
 
         # CR
@@ -125,12 +124,12 @@ class Check(Elaboratable):
 
         if isinstance(spec_insn, Instruction_I):
             m.d.comb += spec_cr_r_stb.eq(0)
-        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_bc)):
             m.d.comb += spec_cr_r_stb[::-1].bit_select(spec_insn.bi[2:], width=1).eq(1)
         else:
             assert False
 
-        with m.If(self.trig.post & ~self.pfv.intr):
+        with m.If(self.post.stb & ~self.pfv.intr):
             for i, spec_cr_r_stb_bit in enumerate(spec_cr_r_stb):
                 pfv_cr_r_stb_bit = self.pfv.cr.r_stb[i]
                 m.d.sync += Assert(spec_cr_r_stb_bit.implies(pfv_cr_r_stb_bit))
@@ -143,7 +142,7 @@ class Check(Elaboratable):
 
         if isinstance(spec_insn, (Instruction_I, Instruction_B)):
             m.d.comb += spec_lr_r_stb.eq(0)
-        elif isinstance(spec_insn, (Instruction_XL_b)):
+        elif isinstance(spec_insn, (Instruction_XL_bc)):
             if isinstance(spec_insn, (BCLR, BCLRL)):
                 m.d.comb += spec_lr_r_stb.eq(1)
             else:
@@ -159,7 +158,7 @@ class Check(Elaboratable):
             spec_lr_w_data.eq(iea_mask(cia_4, msr_w_sf)),
         ]
 
-        with m.If(self.trig.post & ~self.pfv.intr):
+        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),
@@ -176,7 +175,7 @@ class Check(Elaboratable):
             m.d.comb += spec_ctr_r_stb.eq(0)
         elif isinstance(spec_insn, Instruction_B):
             m.d.comb += spec_ctr_r_stb.eq(~spec_insn.bo[4-2])
-        elif isinstance(spec_insn, Instruction_XL_b):
+        elif isinstance(spec_insn, Instruction_XL_bc):
             if isinstance(spec_insn, (BCCTR, BCCTRL)):
                 m.d.comb += spec_ctr_r_stb.eq(1)
             else:
@@ -188,7 +187,7 @@ class Check(Elaboratable):
             m.d.comb += spec_ctr_w_stb.eq(0)
         elif isinstance(spec_insn, Instruction_B):
             m.d.comb += spec_ctr_w_stb.eq(~spec_insn.bo[4-2])
-        elif isinstance(spec_insn, Instruction_XL_b):
+        elif isinstance(spec_insn, Instruction_XL_bc):
             if isinstance(spec_insn, (BCCTR, BCCTRL)):
                 m.d.comb += spec_ctr_w_stb.eq(0)
             else:
@@ -198,7 +197,7 @@ class Check(Elaboratable):
 
         m.d.comb += spec_ctr_w_data.eq(self.pfv.ctr.r_data - 1)
 
-        with m.If(self.trig.post & ~self.pfv.intr):
+        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),
@@ -211,7 +210,7 @@ class Check(Elaboratable):
 
         if isinstance(spec_insn, (Instruction_I, Instruction_B)):
             m.d.comb += spec_tar_r_stb.eq(0)
-        elif isinstance(spec_insn, (Instruction_XL_b)):
+        elif isinstance(spec_insn, (Instruction_XL_bc)):
             if isinstance(spec_insn, (BCTAR, BCTARL)):
                 m.d.comb += spec_tar_r_stb.eq(1)
             else:
@@ -219,9 +218,20 @@ class Check(Elaboratable):
         else:
             assert False
 
-        with m.If(self.trig.post & ~self.pfv.intr):
+        with m.If(self.post.stb & ~self.pfv.intr):
             m.d.sync += [
                 Assert(self.pfv.tar.r_stb == spec_tar_r_stb),
             ]
 
         return m
+
+
+class BranchCheck(PowerFVCheck, name=None):
+    def __init_subclass__(cls, name, insn_cls):
+        super().__init_subclass__(name)
+        cls.insn_cls = insn_cls
+
+    def get_testbench(self, dut, post):
+        tb_spec = BranchSpec(self.insn_cls, post)
+        tb_top  = tb.Testbench(tb_spec, dut)
+        return tb_top

power_fv/checks/insn/_fmt.py

@@ -3,6 +3,9 @@ from amaranth.asserts import AnyConst
 from amaranth.hdl.ast import ValueCastable
 
 
+__all__ = ["Instruction_I", "Instruction_B", "Instruction_XL_bc"]
+
+
 class Instruction_I(ValueCastable):
     po = None
     li = None
@@ -45,7 +48,7 @@ class Instruction_B(ValueCastable):
         return Cat(self.lk, self.aa, self.bd, self.bi, self.bo, self.po)
 
 
-class Instruction_XL_b(ValueCastable):
+class Instruction_XL_bc(ValueCastable):
     po = None
     bo = None
     bi = None
@@ -68,21 +71,3 @@ class Instruction_XL_b(ValueCastable):
     @ValueCastable.lowermethod
     def as_value(self):
         return Cat(self.lk, self.xo, self.bh, self._0, self.bi, self.bo, self.po)
-
-
-class B      (Instruction_I, po=18, aa=0, lk=0): pass
-class BA     (Instruction_I, po=18, aa=1, lk=0): pass
-class BL     (Instruction_I, po=18, aa=0, lk=1): pass
-class BLA    (Instruction_I, po=18, aa=1, lk=1): pass
-
-class BC     (Instruction_B, po=16, aa=0, lk=0): pass
-class BCA    (Instruction_B, po=16, aa=1, lk=0): pass
-class BCL    (Instruction_B, po=16, aa=0, lk=1): pass
-class BCLA   (Instruction_B, po=16, aa=1, lk=1): pass
-
-class BCLR   (Instruction_XL_b, po=19, xo= 16, lk=0): pass
-class BCLRL  (Instruction_XL_b, po=19, xo= 16, lk=1): pass
-class BCCTR  (Instruction_XL_b, po=19, xo=528, lk=0): pass
-class BCCTRL (Instruction_XL_b, po=19, xo=528, lk=1): pass
-class BCTAR  (Instruction_XL_b, po=19, xo=560, lk=0): pass
-class BCTARL (Instruction_XL_b, po=19, xo=560, lk=1): pass

power_fv/checks/insn/_insn.py

@@ -0,0 +1,20 @@
+from . import _fmt
+
+# Branches
+
+class B      (_fmt.Instruction_I, po=18, aa=0, lk=0): pass
+class BA     (_fmt.Instruction_I, po=18, aa=1, lk=0): pass
+class BL     (_fmt.Instruction_I, po=18, aa=0, lk=1): pass
+class BLA    (_fmt.Instruction_I, po=18, aa=1, lk=1): pass
+
+class BC     (_fmt.Instruction_B, po=16, aa=0, lk=0): pass
+class BCA    (_fmt.Instruction_B, po=16, aa=1, lk=0): pass
+class BCL    (_fmt.Instruction_B, po=16, aa=0, lk=1): pass
+class BCLA   (_fmt.Instruction_B, po=16, aa=1, lk=1): pass
+
+class BCLR   (_fmt.Instruction_XL_bc, po=19, xo= 16, lk=0): pass
+class BCLRL  (_fmt.Instruction_XL_bc, po=19, xo= 16, lk=1): pass
+class BCCTR  (_fmt.Instruction_XL_bc, po=19, xo=528, lk=0): pass
+class BCCTRL (_fmt.Instruction_XL_bc, po=19, xo=528, lk=1): pass
+class BCTAR  (_fmt.Instruction_XL_bc, po=19, xo=560, lk=0): pass
+class BCTARL (_fmt.Instruction_XL_bc, po=19, xo=560, lk=1): pass

power_fv/checks/insn/all.py

@@ -0,0 +1,21 @@
+from . import _insn
+from ._branch import BranchCheck
+
+# Branches
+
+class B      (BranchCheck, name="insn_b",      insn_cls=_insn.B,    ): pass
+class BA     (BranchCheck, name="insn_ba",     insn_cls=_insn.BA    ): pass
+class BL     (BranchCheck, name="insn_bl",     insn_cls=_insn.BL    ): pass
+class BLA    (BranchCheck, name="insn_bla",    insn_cls=_insn.BLA   ): pass
+
+class BC     (BranchCheck, name="insn_bc",     insn_cls=_insn.BC    ): pass
+class BCA    (BranchCheck, name="insn_bca",    insn_cls=_insn.BCA   ): pass
+class BCL    (BranchCheck, name="insn_bcl",    insn_cls=_insn.BCL   ): pass
+class BCLA   (BranchCheck, name="insn_bcla",   insn_cls=_insn.BCLA  ): pass
+
+class BCLR   (BranchCheck, name="insn_bclr",   insn_cls=_insn.BCLR  ): pass
+class BCLRL  (BranchCheck, name="insn_bclrl",  insn_cls=_insn.BCLRL ): pass
+class BCCTR  (BranchCheck, name="insn_bcctr",  insn_cls=_insn.BCCTR ): pass
+class BCCTRL (BranchCheck, name="insn_bcctrl", insn_cls=_insn.BCCTRL): pass
+class BCTAR  (BranchCheck, name="insn_bctar",  insn_cls=_insn.BCTAR ): pass
+class BCTARL (BranchCheck, name="insn_bctarl", insn_cls=_insn.BCTARL): pass

power_fv/checks/insn_b.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.B):
-    pass

power_fv/checks/insn_ba.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BA):
-    pass

power_fv/checks/insn_bc.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BC):
-    pass

power_fv/checks/insn_bca.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCA):
-    pass

power_fv/checks/insn_bcctr.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCCTR):
-    pass

power_fv/checks/insn_bcctrl.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCCTRL):
-    pass

power_fv/checks/insn_bcl.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCL):
-    pass

power_fv/checks/insn_bcla.py

@@ -1,10 +0,0 @@
-from . import _branch
-
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCLA):
-    pass

power_fv/checks/insn_bclr.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCLR):
-    pass

power_fv/checks/insn_bclrl.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCLRL):
-    pass

power_fv/checks/insn_bctar.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCTAR):
-    pass

power_fv/checks/insn_bctarl.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BCTARL):
-    pass

power_fv/checks/insn_bl.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BL):
-    pass

power_fv/checks/insn_bla.py

@@ -1,9 +0,0 @@
-from . import _branch
-from .. import insn
-
-
-__all__ = ["Check"]
-
-
-class Check(_branch.Check, insn_cls=insn.BLA):
-    pass

power_fv/checks/unique.py

@@ -1,40 +0,0 @@
-from amaranth import *
-from amaranth.asserts import *
-
-from .. import pfv
-
-
-__all__ = ["Check"]
-
-
-class Check(Elaboratable):
-    """Uniqueness check.
-
-    Check that the core cannot retire two instructions with the same `pfv.order` identifier.
-    """
-    def __init__(self):
-        self.pfv  = pfv.Interface()
-        self.trig = Record([
-            ("pre",  1),
-            ("post", 1),
-        ])
-
-    def elaborate(self, platform):
-        m = Module()
-
-        spec_order = AnyConst(self.pfv.order.shape())
-        duplicate  = Signal()
-
-        with m.If(self.trig.pre):
-            m.d.sync += [
-                Assume(self.pfv.stb),
-                Assume(spec_order == self.pfv.order),
-                Assume(~duplicate),
-            ]
-        with m.Elif(self.pfv.stb & (self.pfv.order == spec_order)):
-            m.d.sync += duplicate.eq(1)
-
-        with m.If(self.trig.post):
-            m.d.sync += Assert(~duplicate)
-
-        return m

power_fv/tb.py

@@ -1,51 +1,78 @@
+from collections import OrderedDict
+
 from amaranth import *
 from amaranth.asserts import *
+from amaranth.utils import bits_for
+
 
+__all__ = ["Trigger", "Testbench"]
 
-__all__ = ["Testbench"]
 
+class Trigger:
+    def __init__(self, cycle, name=None, src_loc_at=0):
+        if not isinstance(cycle, int) or cycle < 0:
+            raise ValueError("Clock cycle must be a non-negative integer, not {!r}"
+                             .format(cycle))
 
-def _check_triggers(t_start, t_pre, t_post):
-    if not isinstance(t_start, int) or t_start <= 0:
-        raise ValueError("t_start must be a positive integer, not {!r}"
-                         .format(t_start))
-    if not isinstance(t_post, int) or t_post < t_start:
-        raise ValueError("t_post must be an integer greater than or equal to t_start ({}), not {!r}"
-                         .format(t_start, t_post))
-    if not isinstance(t_pre, int) or t_pre > t_post or t_pre < t_start:
-        raise ValueError("t_pre must be an integer between t_start and t_post (i.e. [{},{}]), "
-                         "not {!r}".format(t_start, t_post, t_pre))
+        self.stb   = Signal(name=name, src_loc_at=1 + src_loc_at)
+        self.cycle = cycle
 
 
 class Testbench(Elaboratable):
-    def __init__(self, check, dut, *, t_start=1, t_pre=None, t_post=20):
-        if t_pre is None and t_post is not None:
-            t_pre = t_post
+    def __init__(self, spec, dut, start=0):
+        self.spec  = spec
+        self.dut   = dut
+        self.start = Trigger(cycle=start)
+
+        self._triggers  = OrderedDict()
+        self._bmc_depth = None
+        self._frozen    = False
+
+        self.add_trigger(self.start)
+        for trigger in spec.triggers():
+            self.add_trigger(trigger)
+
+    def freeze(self):
+        if not self._frozen:
+            self._bmc_depth = max(t.cycle for t in self.triggers()) + 1
+            self._frozen    = True
 
-        _check_triggers(t_start, t_pre, t_post)
+    def add_trigger(self, trigger):
+        if self._frozen:
+            raise ValueError("Testbench is frozen.")
+        if not isinstance(trigger, Trigger):
+            raise TypeError("Trigger must be an instance of Trigger, not {!r}"
+                            .format(trig))
+        self._triggers[id(trigger)] = trigger
 
-        self.check   = check
-        self.dut     = dut
-        self.t_start = t_start
-        self.t_pre   = t_pre
-        self.t_post  = t_post
+    def triggers(self):
+        yield from self._triggers.values()
+
+    @property
+    def bmc_depth(self):
+        self.freeze()
+        return self._bmc_depth
 
     def elaborate(self, platform):
         m = Module()
 
-        timer = Signal(range(self.t_post + 2), reset=1)
+        cycle = Signal(range(self.bmc_depth), reset=0)
+
+        with m.If(cycle < self.bmc_depth):
+            m.d.sync += cycle.eq(cycle + 1)
+
+        for trigger in self.triggers():
+            m.d.comb += trigger.stb.eq(cycle == trigger.cycle)
+
+        spec_rst = Signal(reset=1)
 
-        with m.If(timer <= self.t_post):
-            m.d.sync += timer.eq(timer + 1)
+        with m.If(self.start.stb):
+            m.d.sync += spec_rst.eq(0)
 
-        m.submodules.check = ResetInserter(timer < self.t_start)(self.check)
-        m.submodules.dut   = self.dut
+        m.submodules.spec = ResetInserter(spec_rst)(self.spec)
+        m.submodules.dut  = self.dut
 
-        m.d.comb += [
-            self.check.pfv.eq(self.dut.pfv),
-            self.check.trig.pre .eq(timer == self.t_pre),
-            self.check.trig.post.eq(timer == self.t_post),
-        ]
+        m.d.comb += self.spec.pfv.eq(self.dut.pfv)
 
         m.d.comb += Assume(ResetSignal() == Initial())