cores/microwatt: add support for IAForwardCheck.

Also, use non-default cache sizes for faster verification.

cores/microwatt/_wrapper.py

@@ -97,9 +97,17 @@ class MicrowattWrapper(Elaboratable):
             ("o", "pfv_out.stb",   self.pfv.stb),
             ("o", "pfv_out.insn",  self.pfv.insn),
             ("o", "pfv_out.order", self.pfv.order),
+            ("o", "pfv_out.intr",  self.pfv.intr),
+            ("o", "pfv_out.cia",   self.pfv.cia),
+            ("o", "pfv_out.nia",   self.pfv.nia),
         )
 
         with m.If(Initial()):
             m.d.comb += Assume(~self.pfv.stb)
 
+        m.d.comb += [
+            Assume(~dmi_req),
+            Assume(~terminated),
+        ]
+
         return m

cores/microwatt/microwatt_top.vhdl

@@ -33,7 +33,7 @@ entity toplevel is
 
 	ext_irq		: in std_ulogic;
 
-	terminated_out   : out std_logic;
+	terminated_out  : out std_logic;
 
         pfv_out : out pfv_t
         );
@@ -44,19 +44,20 @@ begin
     core: entity work.core
         generic map (
             SIM                 => false,
-            DISABLE_FLATTEN     => true,
-            EX1_BYPASS          => false,
+            DISABLE_FLATTEN     => false,
+            EX1_BYPASS          => true,
             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
+            HAS_BTC             => true,
+            HAS_SHORT_MULT      => false,
+            HAS_POWERFV         => true,
+            LOG_LENGTH          => 0,
+            ICACHE_NUM_LINES    => 2,
+            ICACHE_NUM_WAYS     => 1,
+            ICACHE_TLB_SIZE     => 1,
+            DCACHE_NUM_LINES    => 2,
+            DCACHE_NUM_WAYS     => 1,
+            DCACHE_TLB_SET_SIZE => 1,
+            DCACHE_TLB_NUM_WAYS => 1
             )
         port map (
             clk               => clk,

cores/microwatt/run.py

@@ -14,7 +14,7 @@ from _wrapper import MicrowattWrapper
 
 if __name__ == "__main__":
     parser = argparse.ArgumentParser()
-    parser.add_argument("check", help="check", type=str, choices=("unique"))
+    parser.add_argument("check", help="check", type=str, choices=("unique", "ia_fwd"))
     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)
@@ -24,6 +24,8 @@ if __name__ == "__main__":
     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()
 
     cpu       = MicrowattWrapper()
     testbench = Testbench(check, cpu, t_pre=args.pre, t_post=args.post)
@@ -77,7 +79,7 @@ if __name__ == "__main__":
         name      = f"{args.check}_{args.mode}_tb",
         build_dir = f"build/{args.check}_{args.mode}",
         mode      = args.mode,
-        ghdl_opts = "--std=08 --no-formal",
+        ghdl_opts = "--std=08",
         # TODO: investigate why combinatorial loops appear with `prep -flatten -nordff`
         prep_opts = "-nordff",
     )