cores/microwatt: update demo.

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

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

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;

cores/microwatt/run.py

@@ -5,43 +5,28 @@ 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)
+    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 = [
@@ -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",
     )