mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 14:24:08 +00:00
Code Activity

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

Browse source
This commit is contained in:
Jannis Harder 2023-10-02 16:58:52 +02:00 committed by GitHub
parent 7415abfcfa 36f84b8b9f
commit 5b1f26c1e1
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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 nonlocal procs_running
if pending_sim: 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) sim_proc.register_exit_callback(simple_exit_callback)
procs_running += 1 procs_running += 1
pending_sim = None 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_core import SbyProc
from sby_design import pretty_path 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] trace_name = os.path.basename(witness_file)[:-3]
formats = [] formats = []
tracefile = None 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: 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"# running in {task.workdir}/engine_{engine_idx}/", file=f)
print(f"read_rtlil ../model/design_prep.il", file=f) print("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) 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): def exit_callback(retval):