cores/microwatt: add support for GPRCheck.

cores/microwatt/_wrapper.py

@@ -94,12 +94,32 @@ class MicrowattWrapper(Elaboratable):
 
             ("o", "terminated_out", terminated),
 
-            ("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),
+            ("o", "pfv_stb",        self.pfv.stb),
+            ("o", "pfv_insn",       self.pfv.insn),
+            ("o", "pfv_order",      self.pfv.order),
+            ("o", "pfv_intr",       self.pfv.intr),
+            ("o", "pfv_cia",        self.pfv.cia),
+            ("o", "pfv_nia",        self.pfv.nia),
+
+            ("o", "pfv_ra_index",   self.pfv.ra.index),
+            ("o", "pfv_ra_r_stb",   self.pfv.ra.r_stb),
+            ("o", "pfv_ra_r_data",  self.pfv.ra.r_data),
+            ("o", "pfv_ra_w_stb",   self.pfv.ra.w_stb),
+            ("o", "pfv_ra_w_data",  self.pfv.ra.w_data),
+
+            ("o", "pfv_rb_index",   self.pfv.rb.index),
+            ("o", "pfv_rb_r_stb",   self.pfv.rb.r_stb),
+            ("o", "pfv_rb_r_data",  self.pfv.rb.r_data),
+
+            ("o", "pfv_rs_index",   self.pfv.rs.index),
+            ("o", "pfv_rs_r_stb",   self.pfv.rs.r_stb),
+            ("o", "pfv_rs_r_data",  self.pfv.rs.r_data),
+
+            ("o", "pfv_rt_index",   self.pfv.rt.index),
+            ("o", "pfv_rt_r_stb",   self.pfv.rt.r_stb),
+            ("o", "pfv_rt_r_data",  self.pfv.rt.r_data),
+            ("o", "pfv_rt_w_stb",   self.pfv.rt.w_stb),
+            ("o", "pfv_rt_w_data",  self.pfv.rt.w_data),
         )
 
         with m.If(Initial()):

cores/microwatt/microwatt_top.vhdl

@@ -35,11 +35,34 @@ entity toplevel is
 
 	terminated_out  : out std_logic;
 
-        pfv_out : out pfv_t
+        pfv_stb        : out std_ulogic;
+        pfv_insn       : out std_ulogic_vector(63 downto 0);
+        pfv_order      : out std_ulogic_vector(63 downto 0);
+        pfv_intr       : out std_ulogic;
+        pfv_cia        : out std_ulogic_vector(63 downto 0);
+        pfv_nia        : out std_ulogic_vector(63 downto 0);
+
+        pfv_ra_index   : out std_ulogic_vector( 4 downto 0);
+        pfv_ra_r_stb   : out std_ulogic;
+        pfv_ra_r_data  : out std_ulogic_vector(63 downto 0);
+        pfv_ra_w_stb   : out std_ulogic;
+        pfv_ra_w_data  : out std_ulogic_vector(63 downto 0);
+        pfv_rb_index   : out std_ulogic_vector( 4 downto 0);
+        pfv_rb_r_stb   : out std_ulogic;
+        pfv_rb_r_data  : out std_ulogic_vector(63 downto 0);
+        pfv_rs_index   : out std_ulogic_vector( 4 downto 0);
+        pfv_rs_r_stb   : out std_ulogic;
+        pfv_rs_r_data  : out std_ulogic_vector(63 downto 0);
+        pfv_rt_index   : out std_ulogic_vector( 4 downto 0);
+        pfv_rt_r_stb   : out std_ulogic;
+        pfv_rt_r_data  : out std_ulogic_vector(63 downto 0);
+        pfv_rt_w_stb   : out std_ulogic;
+        pfv_rt_w_data  : out std_ulogic_vector(63 downto 0);
         );
 end entity toplevel;
 
 architecture behave of toplevel is
+    signal pfv : pfv_t;
 begin
     core: entity work.core
         generic map (
@@ -76,6 +99,31 @@ begin
             dmi_ack           => dmi_ack,
             ext_irq           => ext_irq,
             terminated_out    => terminated_out,
-            pfv_out           => pfv_out
+            pfv_out           => pfv
         );
+
+        pfv_stb        <= pfv.stb;
+        pfv_insn       <= pfv.insn;
+        pfv_order      <= pfv.order;
+        pfv_intr       <= pfv.intr;
+        pfv_cia        <= pfv.cia;
+        pfv_nia        <= pfv.nia;
+
+        pfv_ra_index   <= pfv.ra.index;
+        pfv_ra_r_stb   <= pfv.ra.r_stb;
+        pfv_ra_r_data  <= pfv.ra.r_data;
+        pfv_ra_w_stb   <= pfv.ra.w_stb;
+        pfv_ra_w_data  <= pfv.ra.w_data;
+        pfv_rb_index   <= pfv.rb.index;
+        pfv_rb_r_stb   <= pfv.rb.r_stb;
+        pfv_rb_r_data  <= pfv.rb.r_data;
+        pfv_rs_index   <= pfv.rs.index;
+        pfv_rs_r_stb   <= pfv.rs.r_stb;
+        pfv_rs_r_data  <= pfv.rs.r_data;
+        pfv_rt_index   <= pfv.rt.index;
+        pfv_rt_r_stb   <= pfv.rt.r_stb;
+        pfv_rt_r_data  <= pfv.rt.r_data;
+        pfv_rt_w_stb   <= pfv.rt.w_stb;
+        pfv_rt_w_data  <= pfv.rt.w_data;
+
 end architecture behave;

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", "ia_fwd"))
+    parser.add_argument("check", help="check", type=str, choices=("unique", "ia_fwd", "gpr"))
     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)
@@ -26,6 +26,8 @@ if __name__ == "__main__":
         check = UniquenessCheck() if args.mode == "bmc" else UniquenessCover()
     if args.check == "ia_fwd":
         check = IAForwardCheck() if args.mode == "bmc" else IAForwardCover()
+    if args.check == "gpr":
+        check = GPRCheck()
 
     cpu       = MicrowattWrapper()
     testbench = Testbench(check, cpu, t_pre=args.pre, t_post=args.post)