From 9ea58a47a9897ba11daae73c6c92141037f164e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Tue, 24 May 2022 16:26:27 +0200 Subject: [PATCH] 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 | 65 +++++++++-------- power_fv/build/plat.py | 4 +- power_fv/checks/__init__.py | 17 +++-- power_fv/checks/all.py | 2 + power_fv/checks/cons/all.py | 5 ++ power_fv/checks/{ => cons}/cr.py | 30 +++++--- power_fv/checks/{ => cons}/gpr.py | 30 +++++--- power_fv/checks/{ => cons}/ia_fwd.py | 30 +++++--- power_fv/checks/{ => cons}/spr.py | 30 +++++--- power_fv/checks/cons/unique.py | 49 +++++++++++++ power_fv/checks/insn/__init__.py | 0 power_fv/checks/{ => insn}/_branch.py | 68 ++++++++++-------- power_fv/{insn.py => checks/insn/_fmt.py} | 23 ++---- power_fv/checks/insn/_insn.py | 20 ++++++ power_fv/checks/insn/all.py | 21 ++++++ power_fv/checks/insn_b.py | 9 --- power_fv/checks/insn_ba.py | 9 --- power_fv/checks/insn_bc.py | 9 --- power_fv/checks/insn_bca.py | 9 --- power_fv/checks/insn_bcctr.py | 9 --- power_fv/checks/insn_bcctrl.py | 9 --- power_fv/checks/insn_bcl.py | 9 --- power_fv/checks/insn_bcla.py | 10 --- power_fv/checks/insn_bclr.py | 9 --- power_fv/checks/insn_bclrl.py | 9 --- power_fv/checks/insn_bctar.py | 9 --- power_fv/checks/insn_bctarl.py | 9 --- power_fv/checks/insn_bl.py | 9 --- power_fv/checks/insn_bla.py | 9 --- power_fv/checks/unique.py | 40 ----------- power_fv/tb.py | 87 +++++++++++++++-------- 31 files changed, 319 insertions(+), 329 deletions(-) create mode 100644 power_fv/checks/all.py create mode 100644 power_fv/checks/cons/all.py rename power_fv/checks/{ => cons}/cr.py (75%) rename power_fv/checks/{ => cons}/gpr.py (82%) rename power_fv/checks/{ => cons}/ia_fwd.py (55%) rename power_fv/checks/{ => cons}/spr.py (69%) create mode 100644 power_fv/checks/cons/unique.py create mode 100644 power_fv/checks/insn/__init__.py rename power_fv/checks/{ => insn}/_branch.py (82%) rename power_fv/{insn.py => checks/insn/_fmt.py} (66%) create mode 100644 power_fv/checks/insn/_insn.py create mode 100644 power_fv/checks/insn/all.py delete mode 100644 power_fv/checks/insn_b.py delete mode 100644 power_fv/checks/insn_ba.py delete mode 100644 power_fv/checks/insn_bc.py delete mode 100644 power_fv/checks/insn_bca.py delete mode 100644 power_fv/checks/insn_bcctr.py delete mode 100644 power_fv/checks/insn_bcctrl.py delete mode 100644 power_fv/checks/insn_bcl.py delete mode 100644 power_fv/checks/insn_bcla.py delete mode 100644 power_fv/checks/insn_bclr.py delete mode 100644 power_fv/checks/insn_bclrl.py delete mode 100644 power_fv/checks/insn_bctar.py delete mode 100644 power_fv/checks/insn_bctarl.py delete mode 100644 power_fv/checks/insn_bl.py delete mode 100644 power_fv/checks/insn_bla.py delete mode 100644 power_fv/checks/unique.py diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index ce04d8d..c54df20 100644 --- a/cores/microwatt/run.py +++ b/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: diff --git a/power_fv/build/plat.py b/power_fv/build/plat.py index d07671c..6994f8f 100644 --- a/power_fv/build/plat.py +++ b/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) diff --git a/power_fv/checks/__init__.py b/power_fv/checks/__init__.py index 506fc6a..2941bd1 100644 --- a/power_fv/checks/__init__.py +++ b/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 diff --git a/power_fv/checks/all.py b/power_fv/checks/all.py new file mode 100644 index 0000000..eee112e --- /dev/null +++ b/power_fv/checks/all.py @@ -0,0 +1,2 @@ +from .cons.all import * +from .insn.all import * diff --git a/power_fv/checks/cons/all.py b/power_fv/checks/cons/all.py new file mode 100644 index 0000000..ad0aaae --- /dev/null +++ b/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 * diff --git a/power_fv/checks/cr.py b/power_fv/checks/cons/cr.py similarity index 75% rename from power_fv/checks/cr.py rename to power_fv/checks/cons/cr.py index f5eb977..c289fa1 100644 --- a/power_fv/checks/cr.py +++ b/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 diff --git a/power_fv/checks/gpr.py b/power_fv/checks/cons/gpr.py similarity index 82% rename from power_fv/checks/gpr.py rename to power_fv/checks/cons/gpr.py index 0f98de4..302e667 100644 --- a/power_fv/checks/gpr.py +++ b/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 diff --git a/power_fv/checks/ia_fwd.py b/power_fv/checks/cons/ia_fwd.py similarity index 55% rename from power_fv/checks/ia_fwd.py rename to power_fv/checks/cons/ia_fwd.py index 13e76f0..a96a8cb 100644 --- a/power_fv/checks/ia_fwd.py +++ b/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 diff --git a/power_fv/checks/spr.py b/power_fv/checks/cons/spr.py similarity index 69% rename from power_fv/checks/spr.py rename to power_fv/checks/cons/spr.py index 2e0529f..37d0452 100644 --- a/power_fv/checks/spr.py +++ b/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 diff --git a/power_fv/checks/cons/unique.py b/power_fv/checks/cons/unique.py new file mode 100644 index 0000000..92edce2 --- /dev/null +++ b/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 diff --git a/power_fv/checks/insn/__init__.py b/power_fv/checks/insn/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/power_fv/checks/_branch.py b/power_fv/checks/insn/_branch.py similarity index 82% rename from power_fv/checks/_branch.py rename to power_fv/checks/insn/_branch.py index 28668aa..ed1b19a 100644 --- a/power_fv/checks/_branch.py +++ b/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 diff --git a/power_fv/insn.py b/power_fv/checks/insn/_fmt.py similarity index 66% rename from power_fv/insn.py rename to power_fv/checks/insn/_fmt.py index cc802f1..1d898bb 100644 --- a/power_fv/insn.py +++ b/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 diff --git a/power_fv/checks/insn/_insn.py b/power_fv/checks/insn/_insn.py new file mode 100644 index 0000000..ed17c90 --- /dev/null +++ b/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 diff --git a/power_fv/checks/insn/all.py b/power_fv/checks/insn/all.py new file mode 100644 index 0000000..95d17e0 --- /dev/null +++ b/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 diff --git a/power_fv/checks/insn_b.py b/power_fv/checks/insn_b.py deleted file mode 100644 index 5a3a830..0000000 --- a/power_fv/checks/insn_b.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.B): - pass diff --git a/power_fv/checks/insn_ba.py b/power_fv/checks/insn_ba.py deleted file mode 100644 index 03b4ddc..0000000 --- a/power_fv/checks/insn_ba.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BA): - pass diff --git a/power_fv/checks/insn_bc.py b/power_fv/checks/insn_bc.py deleted file mode 100644 index 470e64b..0000000 --- a/power_fv/checks/insn_bc.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BC): - pass diff --git a/power_fv/checks/insn_bca.py b/power_fv/checks/insn_bca.py deleted file mode 100644 index ba31123..0000000 --- a/power_fv/checks/insn_bca.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCA): - pass diff --git a/power_fv/checks/insn_bcctr.py b/power_fv/checks/insn_bcctr.py deleted file mode 100644 index cdc0790..0000000 --- a/power_fv/checks/insn_bcctr.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCCTR): - pass diff --git a/power_fv/checks/insn_bcctrl.py b/power_fv/checks/insn_bcctrl.py deleted file mode 100644 index 9cdc80b..0000000 --- a/power_fv/checks/insn_bcctrl.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCCTRL): - pass diff --git a/power_fv/checks/insn_bcl.py b/power_fv/checks/insn_bcl.py deleted file mode 100644 index 4d287f2..0000000 --- a/power_fv/checks/insn_bcl.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCL): - pass diff --git a/power_fv/checks/insn_bcla.py b/power_fv/checks/insn_bcla.py deleted file mode 100644 index 960d28e..0000000 --- a/power_fv/checks/insn_bcla.py +++ /dev/null @@ -1,10 +0,0 @@ -from . import _branch - -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCLA): - pass diff --git a/power_fv/checks/insn_bclr.py b/power_fv/checks/insn_bclr.py deleted file mode 100644 index a6e639f..0000000 --- a/power_fv/checks/insn_bclr.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCLR): - pass diff --git a/power_fv/checks/insn_bclrl.py b/power_fv/checks/insn_bclrl.py deleted file mode 100644 index 236ea26..0000000 --- a/power_fv/checks/insn_bclrl.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCLRL): - pass diff --git a/power_fv/checks/insn_bctar.py b/power_fv/checks/insn_bctar.py deleted file mode 100644 index df26f1e..0000000 --- a/power_fv/checks/insn_bctar.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCTAR): - pass diff --git a/power_fv/checks/insn_bctarl.py b/power_fv/checks/insn_bctarl.py deleted file mode 100644 index 908056c..0000000 --- a/power_fv/checks/insn_bctarl.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BCTARL): - pass diff --git a/power_fv/checks/insn_bl.py b/power_fv/checks/insn_bl.py deleted file mode 100644 index 05fe1c1..0000000 --- a/power_fv/checks/insn_bl.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BL): - pass diff --git a/power_fv/checks/insn_bla.py b/power_fv/checks/insn_bla.py deleted file mode 100644 index a34d516..0000000 --- a/power_fv/checks/insn_bla.py +++ /dev/null @@ -1,9 +0,0 @@ -from . import _branch -from .. import insn - - -__all__ = ["Check"] - - -class Check(_branch.Check, insn_cls=insn.BLA): - pass diff --git a/power_fv/checks/unique.py b/power_fv/checks/unique.py deleted file mode 100644 index a01cfb6..0000000 --- a/power_fv/checks/unique.py +++ /dev/null @@ -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 diff --git a/power_fv/tb.py b/power_fv/tb.py index dd6d3a0..75672ec 100644 --- a/power_fv/tb.py +++ b/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())