cores/microwatt: update proof-of-concept.

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?= <jf@jfng.fr>
+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
+

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
 ```

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

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;

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",
     )