From 0cf05e305e2b0425b7b4b074e1d8c7760e12f94e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Wed, 6 Apr 2022 14:49:06 +0200 Subject: [PATCH] cores/microwatt: update proof-of-concept. --- cores/microwatt/0001-WIP.patch | 35 +++++++++++++ cores/microwatt/README.md | 57 +++++++++++++++++++-- cores/microwatt/_wrapper.py | 44 +++++++---------- cores/microwatt/microwatt_top.vhdl | 79 ++++++++++++++++++++++++++++++ cores/microwatt/run.py | 48 ++++++++++++------ 5 files changed, 219 insertions(+), 44 deletions(-) create mode 100644 cores/microwatt/0001-WIP.patch create mode 100644 cores/microwatt/microwatt_top.vhdl diff --git a/cores/microwatt/0001-WIP.patch b/cores/microwatt/0001-WIP.patch new file mode 100644 index 0000000..7f55d61 --- /dev/null +++ b/cores/microwatt/0001-WIP.patch @@ -0,0 +1,35 @@ +From 43c771bbffb891c6c8b1f9a4b4dea173a1830ef3 Mon Sep 17 00:00:00 2001 +From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= +Date: Wed, 6 Apr 2022 14:14:57 +0200 +Subject: [PATCH] WIP + +--- + core.vhdl | 5 ++++- + 1 file changed, 4 insertions(+), 1 deletion(-) + +diff --git a/core.vhdl b/core.vhdl +index cf730c5..3fb54b8 100644 +--- a/core.vhdl ++++ b/core.vhdl +@@ -49,7 +49,9 @@ entity core is + + ext_irq : in std_ulogic; + +- terminated_out : out std_logic ++ terminated_out : out std_logic; ++ ++ complete_out : out instr_tag_t + ); + end core; + +@@ -187,6 +189,7 @@ architecture behave of core is + begin + + core_rst <= dbg_core_rst or rst; ++ complete_out <= complete; + + resets: process(clk) + begin +-- +2.35.1 + diff --git a/cores/microwatt/README.md b/cores/microwatt/README.md index 462ddb9..3852f27 100644 --- a/cores/microwatt/README.md +++ b/cores/microwatt/README.md @@ -3,9 +3,60 @@ - [ghdl](https://github.com/ghdl/ghdl) with the LLVM or GCC backend - [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin) -## Usage -```shell +``` git clone https://github.com/antonblanchard/microwatt -poetry run python ./run.py +cd microwatt; +git apply ../0001-WIP.patch +cd - +``` + +## Usage + +``` +# Enter virtual environment +poetry shell # Activate virtual environment + +python ./run.py --help + +# Exit virtual environment +exit +``` + +## Example + +In `run.py`, we check that Microwatt is able to retire one instruction. + +Let's find the minimal number of clock cycles to reach this state: + +``` +python run.py --mode=cover --pre=20 --post=20 +``` +``` +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 +``` + +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 +``` + +But it will be reachable at step 9: + +``` +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 ``` diff --git a/cores/microwatt/_wrapper.py b/cores/microwatt/_wrapper.py index 03c6e50..b8915d2 100644 --- a/cores/microwatt/_wrapper.py +++ b/cores/microwatt/_wrapper.py @@ -1,7 +1,7 @@ from amaranth import * from amaranth.asserts import * -import power_fv as pfv +from power_fv import pfv __all__ = ["MicrowattWrapper"] @@ -50,27 +50,14 @@ class MicrowattWrapper(Elaboratable): terminated = Signal( attrs={"keep": True}) - m.submodules.core = Instance("core", - # FIXME: ghdl-yosys-plugin doesn't yet support setting parameters - # (see issue 136). - - # ("p", "SIM", False), - # ("p", "DISABLE_FLATTEN", False), - # ("p", "EX1_BYPASS", False), - # ("p", "HAS_FPU", False), - # ("p", "HAS_BTC", False), - # ("p", "ALT_RESET_ADDRESS", 0x00000000), - # ("p", "LOG_LENGTH", 0), - # ("p", "ICACHE_NUM_LINES", 0), - # ("p", "ICACHE_NUM_WAYS", 0), - # ("p", "ICACHE_TLB_SIZE", 0), - # ("p", "DCACHE_NUM_LINES", 0), - # ("p", "DCACHE_NUM_WAYS", 0), - # ("p", "DCACHE_TLB_SET_SIZE", 0), - # ("p", "DCACHE_TLB_NUM_WAYS", 0), - - ("i", "clk", ClockSignal()), - ("i", "rst", ResetSignal()), + 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", + ("i", "clk", ClockSignal("sync")), + ("i", "rst", ResetSignal("sync")), ("i", "alt_reset", Const(0)), ("i", "ext_irq", Const(0)), @@ -110,12 +97,15 @@ class MicrowattWrapper(Elaboratable): ("o", "terminated_out", terminated), - # TODO: - # ("o", "pfv_stb", self.pfv.stb), - # ... + ("o", "complete_out.tag", complete_tag), + ("o", "complete_out.valid", complete_valid), ) - # for now, to try run.py - m.d.comb += self.pfv.stb.eq(1) + m.d.comb += [ + self.pfv.stb.eq(complete_valid), + ] + + with m.If(Initial()): + m.d.comb += Assume(~complete_valid) # FIXME return m diff --git a/cores/microwatt/microwatt_top.vhdl b/cores/microwatt/microwatt_top.vhdl new file mode 100644 index 0000000..a406f50 --- /dev/null +++ b/cores/microwatt/microwatt_top.vhdl @@ -0,0 +1,79 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +library work; +use work.common.all; +use work.wishbone_types.all; + +entity toplevel is + port ( + clk : in std_ulogic; + rst : in std_ulogic; + + -- Alternate reset (0xffff0000) for use by DRAM init fw + alt_reset : in std_ulogic; + + -- Wishbone interface + wishbone_insn_in : in wishbone_slave_out; + wishbone_insn_out : out wishbone_master_out; + + wishbone_data_in : in wishbone_slave_out; + wishbone_data_out : out wishbone_master_out; + + wb_snoop_in : in wishbone_master_out; + + dmi_addr : in std_ulogic_vector(3 downto 0); + dmi_din : in std_ulogic_vector(63 downto 0); + dmi_dout : out std_ulogic_vector(63 downto 0); + dmi_req : in std_ulogic; + dmi_wr : in std_ulogic; + dmi_ack : out std_ulogic; + + ext_irq : in std_ulogic; + + terminated_out : out std_logic; + + complete_out : out instr_tag_t + ); +end entity toplevel; + +architecture behave of toplevel is +begin + core: entity work.core + generic map ( + SIM => false, + DISABLE_FLATTEN => true, + EX1_BYPASS => false, + HAS_FPU => false, + HAS_BTC => false, + HAS_SHORT_MULT => false + --LOG_LENGTH => 0, + --ICACHE_NUM_LINES => 0, + --ICACHE_NUM_WAYS => 0, + --ICACHE_TLB_SIZE => 0, + --DCACHE_NUM_LINES => 0, + --DCACHE_NUM_WAYS => 0, + --DCACHE_TLB_SET_SIZE => 0, + --DCACHE_TLB_NUM_WAYS => 0 + ) + port map ( + clk => clk, + rst => rst, + alt_reset => alt_reset, + wishbone_insn_in => wishbone_insn_in, + wishbone_insn_out => wishbone_insn_out, + wishbone_data_in => wishbone_data_in, + wishbone_data_out => wishbone_data_out, + wb_snoop_in => wb_snoop_in, + dmi_addr => dmi_addr, + dmi_din => dmi_din, + dmi_dout => dmi_dout, + dmi_req => dmi_req, + dmi_wr => dmi_wr, + dmi_ack => dmi_ack, + ext_irq => ext_irq, + terminated_out => terminated_out, + complete_out => complete_out + ); +end architecture behave; diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index 387b495..8bcc8f4 100644 --- a/cores/microwatt/run.py +++ b/cores/microwatt/run.py @@ -1,29 +1,48 @@ -import power_fv as pfv +import argparse +import os from amaranth import * from amaranth.asserts import * +from power_fv import pfv +from power_fv.tb import Testbench +from power_fv.build import SymbiYosysPlatform + from _wrapper import MicrowattWrapper class SmokeCheck(Elaboratable): - def __init__(self): - self.dut = pfv.Interface() + def __init__(self, mode="bmc"): + self.mode = mode self.pre = Signal() self.post = Signal() + self.pfv = pfv.Interface() def elaborate(self, platform): m = Module() - with m.If(self.post): - m.d.comb += Assume(self.dut.stb) + + 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__": - dut = MicrowattWrapper() - check = SmokeCheck() - tb = pfv.Testbench(check, dut, t_post=0) - plat = pfv.SymbiYosysPlatform() + parser = argparse.ArgumentParser() + 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) + + 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() microwatt_files = [ "cache_ram.vhdl", @@ -59,14 +78,15 @@ if __name__ == "__main__": "wishbone_types.vhdl", "writeback.vhdl", ] - import os + for filename in microwatt_files: file = open(os.path.join(os.curdir, "microwatt", filename), "r") - plat.add_file(filename, file.read()) + platform.add_file(filename, file.read()) + + platform.add_file("microwatt_top.vhdl", open(os.path.join(os.curdir, "microwatt_top.vhdl"), "r")) - plat.build(tb, name="smoke_tb", - sby_depth=2, sby_skip=1, - ghdl_top="core", ghdl_opts="--std=08 --no-formal", + platform.build(smoke_tb, name="smoke_tb", build_dir="build/smoke", + ghdl_opts="--std=08 --no-formal", # TODO: investigate why combinatorial loops appear with `prep -flatten -nordff` prep_opts="-nordff", )