diff --git a/cores/microwatt/README.md b/cores/microwatt/README.md index 3852f27..f0afbe5 100644 --- a/cores/microwatt/README.md +++ b/cores/microwatt/README.md @@ -4,18 +4,17 @@ - [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin) +Get Microwatt: + ``` -git clone https://github.com/antonblanchard/microwatt -cd microwatt; -git apply ../0001-WIP.patch -cd - +git clone git@git.openpower.foundation:jfng/microwatt -b powerfv ``` ## Usage ``` # Enter virtual environment -poetry shell # Activate virtual environment +poetry shell python ./run.py --help @@ -25,38 +24,46 @@ exit ## Example -In `run.py`, we check that Microwatt is able to retire one instruction. +Let's try the [uniqueness check](https://git.openpower.foundation/cores/power-fv/src/branch/main/power_fv/checks/unique.py) on Microwatt. -Let's find the minimal number of clock cycles to reach this state: +First, we find the minimal number of clock cycles needed to observe at least two retired instructions: ``` -python run.py --mode=cover --pre=20 --post=20 +python run.py unique --mode=cover --post=15 ``` ``` -SBY 13:58:23 [smoke_tb] engine_0: ## 0:00:29 Reached cover statement at /home/jf/src/power-fv/cores/microwatt/./run.py:29 ($1) in step 9. -SBY 13:58:23 [smoke_tb] engine_0: ## 0:00:29 Writing trace to VCD file: engine_0/trace0.vcd +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 ``` -In BMC mode, the pre-condition will indeed be unreachable at step 8: - -``` -python ./run.py --mode=bmc --pre=8 --post=8 -``` -``` -SBY 14:08:17 [smoke_tb] engine_0: ## 0:00:14 Checking assumptions in step 8.. -SBY 14:08:20 [smoke_tb] engine_0: ## 0:00:17 Assumptions are unsatisfiable! -SBY 14:08:20 [smoke_tb] engine_0: ## 0:00:17 Status: PREUNSAT -SBY 14:08:20 [smoke_tb] engine_0: finished (returncode=1) -SBY 14:08:20 [smoke_tb] engine_0: Status returned by engine: ERROR -``` +It takes at least 10 clock cycles to observe one retired instruction, and at least 11 for two instructions. -But it will be reachable at step 9: +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 --mode=bmc --pre=9 --post=9 -``` -``` -SBY 14:11:13 [smoke_tb] engine_0: ## 0:00:15 Checking assumptions in step 9.. -SBY 14:11:25 [smoke_tb] engine_0: ## 0:00:27 Checking assertions in step 9.. -SBY 14:11:26 [smoke_tb] engine_0: ## 0:00:27 Status: passed +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) ``` diff --git a/cores/microwatt/_wrapper.py b/cores/microwatt/_wrapper.py index b8915d2..0625925 100644 --- a/cores/microwatt/_wrapper.py +++ b/cores/microwatt/_wrapper.py @@ -50,9 +50,6 @@ class MicrowattWrapper(Elaboratable): terminated = Signal( attrs={"keep": True}) - complete_tag = Signal( 2, attrs={"keep": True}) - complete_valid = Signal( 1, attrs={"keep": True}) - # FIXME: ghdl-yosys-plugin doesn't yet support setting parameters (see issue 136). # As a workaround, use our own toplevel entity. m.submodules.toplevel = Instance("toplevel", @@ -97,15 +94,12 @@ class MicrowattWrapper(Elaboratable): ("o", "terminated_out", terminated), - ("o", "complete_out.tag", complete_tag), - ("o", "complete_out.valid", complete_valid), + ("o", "pfv_out.stb", self.pfv.stb), + ("o", "pfv_out.insn", self.pfv.insn), + ("o", "pfv_out.order", self.pfv.order), ) - m.d.comb += [ - self.pfv.stb.eq(complete_valid), - ] - with m.If(Initial()): - m.d.comb += Assume(~complete_valid) # FIXME + m.d.comb += Assume(~self.pfv.stb) return m diff --git a/cores/microwatt/microwatt_top.vhdl b/cores/microwatt/microwatt_top.vhdl index a406f50..488d471 100644 --- a/cores/microwatt/microwatt_top.vhdl +++ b/cores/microwatt/microwatt_top.vhdl @@ -5,6 +5,7 @@ use ieee.numeric_std.all; library work; use work.common.all; use work.wishbone_types.all; +use work.powerfv_types.all; entity toplevel is port ( @@ -34,7 +35,7 @@ entity toplevel is terminated_out : out std_logic; - complete_out : out instr_tag_t + pfv_out : out pfv_t ); end entity toplevel; @@ -74,6 +75,6 @@ begin dmi_ack => dmi_ack, ext_irq => ext_irq, terminated_out => terminated_out, - complete_out => complete_out + pfv_out => pfv_out ); end architecture behave; diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index 8bcc8f4..f9bf2a3 100644 --- a/cores/microwatt/run.py +++ b/cores/microwatt/run.py @@ -5,44 +5,29 @@ 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 -class SmokeCheck(Elaboratable): - def __init__(self, mode="bmc"): - self.mode = mode - self.pre = Signal() - self.post = Signal() - self.pfv = pfv.Interface() - - def elaborate(self, platform): - m = Module() - - if self.mode == "bmc": - with m.If(self.pre): - m.d.comb += Assume(self.pfv.stb) - - if self.mode == "cover": - m.d.comb += Cover(self.pfv.stb) - - return m - - if __name__ == "__main__": parser = argparse.ArgumentParser() + parser.add_argument("check", help="check", type=str, choices=("unique")) 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: 10)", type=int, default=10) - parser.add_argument("--post", help="post-condition step, in clock cycles (default: 10)", type=int, default=10) + 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() - microwatt = MicrowattWrapper() - smoke_check = SmokeCheck(mode=args.mode) - smoke_tb = Testbench(smoke_check, microwatt, t_pre=args.pre, t_post=args.post) - platform = SymbiYosysPlatform() + check = None + if args.check == "unique": + check = UniquenessCheck() if args.mode == "bmc" else UniquenessCover() + + cpu = MicrowattWrapper() + testbench = Testbench(check, cpu, t_pre=args.pre, t_post=args.post) + platform = SymbiYosysPlatform() microwatt_files = [ "cache_ram.vhdl", @@ -77,6 +62,9 @@ if __name__ == "__main__": "utils.vhdl", "wishbone_types.vhdl", "writeback.vhdl", + + "powerfv_types.vhdl", + "powerfv.vhdl", ] for filename in microwatt_files: @@ -85,8 +73,11 @@ if __name__ == "__main__": platform.add_file("microwatt_top.vhdl", open(os.path.join(os.curdir, "microwatt_top.vhdl"), "r")) - platform.build(smoke_tb, name="smoke_tb", build_dir="build/smoke", - ghdl_opts="--std=08 --no-formal", + platform.build(testbench, + name = f"{args.check}_{args.mode}_tb", + build_dir = f"build/{args.check}_{args.mode}", + mode = args.mode, + ghdl_opts = "--std=08 --no-formal", # TODO: investigate why combinatorial loops appear with `prep -flatten -nordff` - prep_opts="-nordff", + prep_opts = "-nordff", )