Merge pull request #249 from jix/inductive-cex-sim

YosysHQ · Oct 2, 2023 · 5b1f26c · 5b1f26c
2 parents 7415abf + 36f84b8
commit 5b1f26c
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
@@ -196,7 +196,7 @@ def output_callback(line):
  nonlocal procs_running
 
  if pending_sim:
- sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append)
+ sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append, inductive=mode == "prove_induction")
  sim_proc.register_exit_callback(simple_exit_callback)
  procs_running += 1
  pending_sim = None

diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py
@@ -20,7 +20,7 @@
 from sby_core import SbyProc
 from sby_design import pretty_path
 
-def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()):
+def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, inductive=False, deps=()):
  trace_name = os.path.basename(witness_file)[:-3]
  formats = []
  tracefile = None
@@ -40,8 +40,11 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()
 
  with open(f"{task.workdir}/engine_{engine_idx}/{trace_name}.ys", "w") as f:
  print(f"# running in {task.workdir}/engine_{engine_idx}/", file=f)
- print(f"read_rtlil ../model/design_prep.il", file=f)
- print(f"sim -hdlname -summary {trace_name}.json -append {append} -r {trace_name}.yw {' '.join(formats)}", file=f)
+ print("read_rtlil ../model/design_prep.il", file=f)
+ sim_args = ""
+ if inductive:
+ sim_args += " -noinitstate"
+ print(f"sim -hdlname -summary {trace_name}.json -append {append}{sim_args} -r {trace_name}.yw {' '.join(formats)}", file=f)
 
  def exit_callback(retval):