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

Rename "abc_bmc3" engine to "abc bmc3"

Browse source
This commit is contained in:
Clifford Wolf 2017-01-28 15:25:49 +01:00
parent fb9dafd920
commit 4f97a20acd
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/demo.sby
View file

@ -7,7 +7,7 @@ depth 10
smtbmc -s yices smtbmc -s yices
smtbmc -s boolector smtbmc -s boolector
smtbmc -s z3 --nomem smtbmc -s z3 --nomem
abc_bmc3 abc bmc3
[script] [script]
read_verilog -formal -norestrict -assume-asserts picorv32.v read_verilog -formal -norestrict -assume-asserts picorv32.v

8
sbysrc/sby_bmc.py
View file

@ -78,7 +78,9 @@ def run_smtbmc(job, engine_idx, engine):
job.engine_tasks.append(task) job.engine_tasks.append(task)
def run_abc_bmc3(job, engine_idx, engine): def run_abc(job, engine_idx, engine):
assert engine == ["abc", "bmc3"]
task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; bmc3 -F %d -v; " + ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; bmc3 -F %d -v; " +
"undc -c; write_cex -a engine_%d/trace.aiw'") % (job.workdir, job.opt_depth, engine_idx), "undc -c; write_cex -a engine_%d/trace.aiw'") % (job.workdir, job.opt_depth, engine_idx),
@ -159,8 +161,8 @@ def run(job):
if engine[0] == "smtbmc": if engine[0] == "smtbmc":
run_smtbmc(job, engine_idx, engine) run_smtbmc(job, engine_idx, engine)
elif engine[0] == "abc_bmc3": elif engine[0] == "abc":
run_abc_bmc3(job, engine_idx, engine) run_abc(job, engine_idx, engine)
else: else:
assert False assert False