mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-04 05:49:57 +00:00
Code Activity

smtbmc: Use new -noinitstate option when simulating inductive cex

Browse source 
This requires YosysHQ/yosys#3962
This commit is contained in:
Jannis Harder 2023-09-28 17:38:15 +02:00
parent 7415abfcfa
commit 36f84b8b9f
2 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_engine_smtbmc.py
View file

@ -196,7 +196,7 @@ def run(mode, task, engine_idx, engine):
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

9
sbysrc/sby_sim.py
View file

@ -20,7 +20,7 @@ import os, re, glob, json
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):