From 6922b4bd538dea4a1b324015383ba80b2dbc7e21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Thu, 5 May 2022 20:43:26 +0200 Subject: [PATCH] cores/microwatt: add support for IAForwardCheck. Also, use non-default cache sizes for faster verification. --- cores/microwatt/_wrapper.py | 8 ++++++++ cores/microwatt/microwatt_top.vhdl | 27 ++++++++++++++------------- cores/microwatt/run.py | 6 ++++-- 3 files changed, 26 insertions(+), 15 deletions(-) diff --git a/cores/microwatt/_wrapper.py b/cores/microwatt/_wrapper.py index 0625925..7df5b5e 100644 --- a/cores/microwatt/_wrapper.py +++ b/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 diff --git a/cores/microwatt/microwatt_top.vhdl b/cores/microwatt/microwatt_top.vhdl index 488d471..010a94b 100644 --- a/cores/microwatt/microwatt_top.vhdl +++ b/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, diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index f9bf2a3..80b6371 100644 --- a/cores/microwatt/run.py +++ b/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", )