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

Write native yosys witness traces

Browse source
This commit is contained in:
Jannis Harder 2022-08-02 18:19:01 +02:00
parent acaf6ef0c2
commit d3520037b9
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_core.py
View file

@ -739,7 +739,7 @@ class SbyTask(SbyConfig):
print("abc -g AND -fast", file=f) print("abc -g AND -fast", file=f)
print("opt_clean", file=f) print("opt_clean", file=f)
print("stat", file=f) print("stat", file=f)
print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim design_aiger.aig", file=f) print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim -ywmap design_aiger.ywa design_aiger.aig", file=f)
proc = SbyProc( proc = SbyProc(
self, self,

4
sbysrc/sby_engine_aiger.py
View file

@ -111,7 +111,7 @@ def run(mode, task, engine_idx, engine):
f"engine_{engine_idx}", f"engine_{engine_idx}",
task.model("smt2"), task.model("smt2"),
("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
"--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format "--dump-smtc engine_{i}/trace.smtc --dump-yw engine_{i}/trace.yw --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
(task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt, (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
"" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}", "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
i=engine_idx), i=engine_idx),
@ -123,7 +123,7 @@ def run(mode, task, engine_idx, engine):
f"engine_{engine_idx}", f"engine_{engine_idx}",
task.model("smt2"), task.model("smt2"),
("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
"--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format "--dump-smtc engine_{i}/trace.smtc --dump-yw engine_{i}/trace.yw --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
(task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt, (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
"" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}", "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
task.opt_append, i=engine_idx), task.opt_append, i=engine_idx),

2
sbysrc/sby_engine_smtbmc.py
View file

@ -152,7 +152,7 @@ def run(mode, task, engine_idx, engine):
task, task,
procname, procname,
task.model(model_name), task.model(model_name),
f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""", f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
logfile=open(logfile_prefix + ".txt", "w"), logfile=open(logfile_prefix + ".txt", "w"),
logstderr=(not progress) logstderr=(not progress)
) )