From 5c9bc3e68c9067c1da569b1ba3f94329a6cc0577 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Mon, 16 May 2022 17:56:48 +0200 Subject: [PATCH] cores/microwatt: add support for concurrent execution of formal checks. --- cores/microwatt/README.md | 48 ++------------------ cores/microwatt/run.py | 95 ++++++++++++++++++++++----------------- power_fv/checks/cr.py | 12 ++--- power_fv/checks/gpr.py | 20 +++++---- power_fv/checks/ia_fwd.py | 44 +++--------------- power_fv/checks/spr.py | 64 +++++--------------------- power_fv/checks/unique.py | 42 ++++------------- power_fv/tb.py | 6 +-- 8 files changed, 105 insertions(+), 226 deletions(-) diff --git a/cores/microwatt/README.md b/cores/microwatt/README.md index f0afbe5..b0750ce 100644 --- a/cores/microwatt/README.md +++ b/cores/microwatt/README.md @@ -12,58 +12,18 @@ git clone git@git.openpower.foundation:jfng/microwatt -b powerfv ## Usage +### Enter/exit the Python virtualenv + ``` -# Enter virtual environment poetry shell python ./run.py --help -# Exit virtual environment exit ``` -## Example - -Let's try the [uniqueness check](https://git.openpower.foundation/cores/power-fv/src/branch/main/power_fv/checks/unique.py) on Microwatt. - -First, we find the minimal number of clock cycles needed to observe at least two retired instructions: - -``` -python run.py unique --mode=cover --post=15 -``` -``` -SBY 15:28:31 [unique_cover_tb] engine_0: ## 0:00:29 Reached cover statement at /home/jf/src/power-fv/power_fv/checks/unique.py:64 ($12) in step 10. -SBY 15:28:31 [unique_cover_tb] engine_0: ## 0:00:29 Writing trace to VCD file: engine_0/trace0.vcd -SBY 15:28:53 [unique_cover_tb] engine_0: ## 0:00:51 Writing trace to Verilog testbench: engine_0/trace0_tb.v -SBY 15:28:53 [unique_cover_tb] engine_0: ## 0:00:51 Writing trace to constraints file: engine_0/trace0.smtc -SBY 15:28:53 [unique_cover_tb] engine_0: ## 0:00:51 Checking cover reachability in step 10.. -SBY 15:28:55 [unique_cover_tb] engine_0: ## 0:00:52 Checking cover reachability in step 11.. -SBY 15:29:09 [unique_cover_tb] engine_0: ## 0:01:07 Reached cover statement at /home/jf/src/power-fv/power_fv/checks/unique.py:65 ($15) in step 11. -SBY 15:29:09 [unique_cover_tb] engine_0: ## 0:01:07 Writing trace to VCD file: engine_0/trace1.vcd -SBY 15:29:33 [unique_cover_tb] engine_0: ## 0:01:31 Writing trace to Verilog testbench: engine_0/trace1_tb.v -SBY 15:29:33 [unique_cover_tb] engine_0: ## 0:01:31 Writing trace to constraints file: engine_0/trace1.smtc -``` - -It takes at least 10 clock cycles to observe one retired instruction, and at least 11 for two instructions. +### Run the checks locally -In BMC mode, let's set the pre-condition trigger to 10 cycles, and the post-condition to 12. We should really use higher values to cover a larger state space, but we just want to minimize execution time for this demo. - -``` -python ./run.py unique --mode=bmc --pre=10 --post=12 -``` ``` -SBY 16:14:26 [unique_bmc_tb] engine_0: starting process "cd unique_bmc_tb; yosys-smtbmc --presat --unroll --noprogress -t 12:13 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" -SBY 16:14:26 [unique_bmc_tb] engine_0: ## 0:00:00 Solver: yices -SBY 16:14:37 [unique_bmc_tb] engine_0: ## 0:00:11 Skipping step 0.. -# ... -SBY 16:14:42 [unique_bmc_tb] engine_0: ## 0:00:16 Skipping step 11.. -SBY 16:14:43 [unique_bmc_tb] engine_0: ## 0:00:16 Checking assumptions in step 12.. -SBY 16:15:12 [unique_bmc_tb] engine_0: ## 0:00:46 Checking assertions in step 12.. -SBY 16:15:13 [unique_bmc_tb] engine_0: ## 0:00:46 Status: passed -SBY 16:15:13 [unique_bmc_tb] engine_0: finished (returncode=0) -SBY 16:15:13 [unique_bmc_tb] engine_0: Status returned by engine: pass -SBY 16:15:13 [unique_bmc_tb] summary: Elapsed clock time [H:MM:SS (secs)]: 0:01:07 (67) -SBY 16:15:13 [unique_bmc_tb] summary: Elapsed process time [H:MM:SS (secs)]: 0:01:09 (69) -SBY 16:15:13 [unique_bmc_tb] summary: engine_0 (smtbmc) returned pass -SBY 16:15:13 [unique_bmc_tb] DONE (PASS, rc=0) +python run.py --jobs=$(nproc) ``` diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index 9383b8c..34fbf16 100644 --- a/cores/microwatt/run.py +++ b/cores/microwatt/run.py @@ -1,43 +1,18 @@ import argparse +import importlib import os +import multiprocessing from amaranth import * -from amaranth.asserts import * -from power_fv import pfv -from power_fv.checks import * from power_fv.tb import Testbench from power_fv.build import SymbiYosysPlatform from _wrapper import MicrowattWrapper -if __name__ == "__main__": - parser = argparse.ArgumentParser() - parser.add_argument("check", help="check", type=str, choices=("unique", "ia_fwd", "gpr", "cr", "spr")) - parser.add_argument("--mode", help="mode", type=str, choices=("cover", "bmc"), default="bmc") - parser.add_argument("--pre", help="pre-condition step, in clock cycles (default: 15)", type=int, default=15) - parser.add_argument("--post", help="post-condition step, in clock cycles (default: 15)", type=int, default=15) - - args = parser.parse_args() - - check = None - if args.check == "unique": - check = UniquenessCheck() if args.mode == "bmc" else UniquenessCover() - if args.check == "ia_fwd": - check = IAForwardCheck() if args.mode == "bmc" else IAForwardCover() - if args.check == "gpr": - check = GPRCheck() - if args.check == "cr": - check = CRCheck() - if args.check == "spr": - check = SPRCheck() if args.mode == "bmc" else SPRCover() - - cpu = MicrowattWrapper() - testbench = Testbench(check, cpu, t_pre=args.pre, t_post=args.post) - platform = SymbiYosysPlatform() - - microwatt_files = [ +def microwatt_files(): + _filenames = ( "cache_ram.vhdl", "common.vhdl", "control.vhdl", @@ -64,28 +39,66 @@ if __name__ == "__main__": "nonrandom.vhdl", "plru.vhdl", "pmu.vhdl", + "powerfv_types.vhdl", + "powerfv.vhdl", "ppc_fx_insns.vhdl", "register_file.vhdl", "rotator.vhdl", "utils.vhdl", "wishbone_types.vhdl", "writeback.vhdl", + ) - "powerfv_types.vhdl", - "powerfv.vhdl", - ] + for filename in _filenames: + contents = open(os.path.join(os.curdir, "microwatt", filename), "r").read() + yield filename, contents + + top_filename = "microwatt_top.vhdl" + top_contents = open(os.path.join(os.curdir, top_filename), "r").read() + yield top_filename, top_contents - for filename in microwatt_files: - file = open(os.path.join(os.curdir, "microwatt", filename), "r") - platform.add_file(filename, file.read()) - platform.add_file("microwatt_top.vhdl", open(os.path.join(os.curdir, "microwatt_top.vhdl"), "r")) +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) - platform.build(testbench, - name = f"{args.check}_{args.mode}_tb", - build_dir = f"build/{args.check}_{args.mode}", - mode = args.mode, + 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) + + platform.build( + top = top, + name = top_name, + build_dir = build_dir, + mode = "bmc", ghdl_opts = "--std=08", - # TODO: investigate why combinatorial loops appear with `prep -flatten -nordff` prep_opts = "-nordff", ) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("-j", "--jobs", + help="Number of worker processes (default: os.cpu_count())", + type=int, + default=os.cpu_count(), + ) + + args = parser.parse_args() + + checks = [ + # name pre post + ("unique", 12, 15), + ("ia_fwd", None, 15), + ("gpr", None, 15), + ("cr", None, 15), + ("spr", None, 15), + ] + + with multiprocessing.Pool(processes=args.jobs) as pool: + pool.starmap(run_check, checks) diff --git a/power_fv/checks/cr.py b/power_fv/checks/cr.py index 70ae907..978ccbc 100644 --- a/power_fv/checks/cr.py +++ b/power_fv/checks/cr.py @@ -4,18 +4,20 @@ from amaranth.asserts import * from .. import pfv -__all__ = ["CRCheck"] +__all__ = ["Check"] -class CRCheck(Elaboratable): +class Check(Elaboratable): """Condition Register check. Checks that reads from CR fields are consistent with the last value that was written to them. """ def __init__(self): - self.pre = Signal() - self.post = Signal() self.pfv = pfv.Interface() + self.trig = Record([ + ("pre", 1), + ("post", 1), + ]) def elaborate(self, platform): m = Module() @@ -54,7 +56,7 @@ class CRCheck(Elaboratable): cr_field.shadow .eq(cr_field.pfv.w_data), ] - with m.If(self.post): + with m.If(self.trig.post): m.d.sync += [ Assume(Past(self.pfv.stb)), Assume(Past(self.pfv.order) == spec_order), diff --git a/power_fv/checks/gpr.py b/power_fv/checks/gpr.py index ac3156b..f0cd5e4 100644 --- a/power_fv/checks/gpr.py +++ b/power_fv/checks/gpr.py @@ -4,10 +4,10 @@ from amaranth.asserts import * from .. import pfv -__all__ = ["GPRCheck"] +__all__ = ["Check"] -class GPRCheck(Elaboratable): +class Check(Elaboratable): """General Purpose Registers check. Checks that reads from GPRs are consistent with the last value that was written to them. @@ -15,9 +15,11 @@ class GPRCheck(Elaboratable): with update) do not target the same register. """ def __init__(self): - self.pre = Signal() - self.post = Signal() self.pfv = pfv.Interface() + self.trig = Record([ + ("pre", 1), + ("post", 1), + ]) def elaborate(self, platform): m = Module() @@ -55,19 +57,19 @@ class GPRCheck(Elaboratable): with m.Else(): m.d.sync += gpr_shadow.eq(self.pfv.rt.w_data) - with m.If(self.post): + with m.If(self.trig.post): m.d.sync += [ Assume(Past(self.pfv.stb)), Assume(Past(self.pfv.order) == spec_order), Assert(gpr_written.implies(~gpr_conflict)), ] - with m.If(Past(gpr_ra_read)): + with m.If(gpr_written & Past(gpr_ra_read)): m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.ra.r_data)) - with m.If(Past(gpr_rb_read)): + with m.If(gpr_written & Past(gpr_rb_read)): m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rb.r_data)) - with m.If(Past(gpr_rs_read)): + with m.If(gpr_written & Past(gpr_rs_read)): m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rs.r_data)) - with m.If(Past(gpr_rt_read)): + with m.If(gpr_written & Past(gpr_rt_read)): m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rt.r_data)) return m diff --git a/power_fv/checks/ia_fwd.py b/power_fv/checks/ia_fwd.py index e76a7d8..13e76f0 100644 --- a/power_fv/checks/ia_fwd.py +++ b/power_fv/checks/ia_fwd.py @@ -4,19 +4,21 @@ from amaranth.asserts import * from .. import pfv -__all__ = ["IAForwardCheck", "IAForwardCover"] +__all__ = ["Check"] -class IAForwardCheck(Elaboratable): +class Check(Elaboratable): """IA forward check. Given two instructions retiring in order, check that the NIA of the first matches the CIA of the second. """ def __init__(self): - self.pre = Signal() - self.post = Signal() self.pfv = pfv.Interface() + self.trig = Record([ + ("pre", 1), + ("post", 1), + ]) def elaborate(self, platform): m = Module() @@ -31,7 +33,7 @@ class IAForwardCheck(Elaboratable): pred_nia.eq(self.pfv.nia) ] - with m.If(self.post): + with m.If(self.trig.post): m.d.sync += [ Assume(self.pfv.stb), Assume(self.pfv.order == pred_order + 1), @@ -40,35 +42,3 @@ class IAForwardCheck(Elaboratable): ] return m - - -class IAForwardCover(Elaboratable): - def __init__(self): - self.pre = Signal() - self.post = Signal() - self.pfv = pfv.Interface() - - def elaborate(self, platform): - m = Module() - - insn_count = Signal(range(4)) - pred_branch = Signal() - - with m.If(self.pfv.stb): - m.d.sync += [ - insn_count .eq(insn_count + 1), - pred_branch.eq(self.pfv.nia != (self.pfv.cia + 4)), - ] - - cover_1 = Signal() - cover_2 = Signal() - - m.d.comb += [ - cover_1.eq((insn_count > 1) & pred_branch), - cover_2.eq(cover_1 & self.pfv.stb), - - Cover(cover_1), - Cover(cover_2), - ] - - return m diff --git a/power_fv/checks/spr.py b/power_fv/checks/spr.py index 1c62225..c4e5be0 100644 --- a/power_fv/checks/spr.py +++ b/power_fv/checks/spr.py @@ -4,19 +4,21 @@ from amaranth.asserts import * from .. import pfv -__all__ = ["SPRCheck", "SPRCover"] +__all__ = ["Check"] -class SPRCheck(Elaboratable): +class Check(Elaboratable): """Special Purpose Registers check. Checks that reads from supported SPRs are consistent with the last value that was written to them. """ def __init__(self): - self.pre = Signal() - self.post = Signal() self.pfv = pfv.Interface() + self.trig = Record([ + ("pre", 1), + ("post", 1), + ]) def elaborate(self, platform): m = Module() @@ -54,62 +56,18 @@ class SPRCheck(Elaboratable): tar_shadow .eq(self.pfv.tar.w_data), ] - with m.If(self.post): + with m.If(self.trig.post): m.d.sync += [ Assume(Past(self.pfv.stb)), Assume(Past(self.pfv.order) == spec_order), ] - with m.If(Past(self.pfv.lr.r_stb)): + with m.If(lr_written & Past(self.pfv.lr.r_stb)): m.d.sync += Assert(Past(lr_shadow) == Past(self.pfv.lr.r_data)) - with m.If(Past(self.pfv.ctr.r_stb)): + with m.If(ctr_written & Past(self.pfv.ctr.r_stb)): m.d.sync += Assert(Past(ctr_shadow) == Past(self.pfv.ctr.r_data)) - with m.If(Past(self.pfv.xer.r_stb)): + with m.If(xer_written & Past(self.pfv.xer.r_stb)): m.d.sync += Assert(Past(xer_shadow) == Past(self.pfv.xer.r_data)) - with m.If(Past(self.pfv.tar.r_stb)): + with m.If(tar_written & Past(self.pfv.tar.r_stb)): m.d.sync += Assert(Past(tar_shadow) == Past(self.pfv.tar.r_data)) return m - - -class SPRCover(Elaboratable): - def __init__(self): - self.pre = Signal() - self.post = Signal() - self.pfv = pfv.Interface() - - def elaborate(self, platform): - m = Module() - - insn_count = Signal(range(4)) - lr_written = Signal() - ctr_written = Signal() - xer_written = Signal() - tar_written = Signal() - - with m.If(self.pfv.stb): - m.d.sync += [ - insn_count .eq(insn_count + 1), - lr_written .eq(self.pfv.lr .w_stb), - ctr_written.eq(self.pfv.ctr.w_stb), - xer_written.eq(self.pfv.xer.w_stb), - tar_written.eq(self.pfv.tar.w_stb), - ] - - cover_1 = Signal() - cover_2 = Signal() - cover_3 = Signal() - cover_4 = Signal() - - m.d.comb += [ - cover_1.eq((insn_count > 1) & lr_written), - cover_2.eq((insn_count > 1) & ctr_written), - cover_3.eq((insn_count > 1) & xer_written), - cover_4.eq((insn_count > 1) & tar_written), - - Cover(cover_1), - Cover(cover_2), - Cover(cover_3), - Cover(cover_4), - ] - - return m diff --git a/power_fv/checks/unique.py b/power_fv/checks/unique.py index 483a86b..a01cfb6 100644 --- a/power_fv/checks/unique.py +++ b/power_fv/checks/unique.py @@ -4,18 +4,20 @@ from amaranth.asserts import * from .. import pfv -__all__ = ["UniquenessCheck", "UniquenessCover"] +__all__ = ["Check"] -class UniquenessCheck(Elaboratable): +class Check(Elaboratable): """Uniqueness check. Check that the core cannot retire two instructions with the same `pfv.order` identifier. """ def __init__(self): - self.pre = Signal() - self.post = Signal() self.pfv = pfv.Interface() + self.trig = Record([ + ("pre", 1), + ("post", 1), + ]) def elaborate(self, platform): m = Module() @@ -23,7 +25,7 @@ class UniquenessCheck(Elaboratable): spec_order = AnyConst(self.pfv.order.shape()) duplicate = Signal() - with m.If(self.pre): + with m.If(self.trig.pre): m.d.sync += [ Assume(self.pfv.stb), Assume(spec_order == self.pfv.order), @@ -32,35 +34,7 @@ class UniquenessCheck(Elaboratable): with m.Elif(self.pfv.stb & (self.pfv.order == spec_order)): m.d.sync += duplicate.eq(1) - with m.If(self.post): + with m.If(self.trig.post): m.d.sync += Assert(~duplicate) return m - - -class UniquenessCover(Elaboratable): - def __init__(self): - self.pre = Signal() - self.post = Signal() - self.pfv = pfv.Interface() - - def elaborate(self, platform): - m = Module() - - insn_count = Signal(range(4)) - - with m.If(self.pfv.stb): - m.d.sync += insn_count.eq(insn_count + 1) - - cover_1 = Signal() - cover_2 = Signal() - - m.d.comb += [ - cover_1.eq(insn_count == 1), - cover_2.eq(insn_count == 2), - - Cover(cover_1), - Cover(cover_2), - ] - - return m diff --git a/power_fv/tb.py b/power_fv/tb.py index 81f1561..dd6d3a0 100644 --- a/power_fv/tb.py +++ b/power_fv/tb.py @@ -42,9 +42,9 @@ class Testbench(Elaboratable): m.submodules.dut = self.dut m.d.comb += [ - self.check.pre .eq(timer == self.t_pre), - self.check.post.eq(timer == self.t_post), - self.check.pfv .eq(self.dut.pfv), + 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 += Assume(ResetSignal() == Initial())