Rename "abc_bmc3" engine to "abc bmc3"
authorClifford Wolf <clifford@clifford.at>
Sat, 28 Jan 2017 14:25:49 +0000 (15:25 +0100)
committerClifford Wolf <clifford@clifford.at>
Sat, 28 Jan 2017 14:25:49 +0000 (15:25 +0100)
sbysrc/demo.sby
sbysrc/sby_bmc.py

index 5ec08035d36dc1bc8124076acc99b3cc9e344869..c0fefc89084598901f04b270eaab83d26ccff2d5 100644 (file)
@@ -7,7 +7,7 @@ depth 10
 smtbmc -s yices
 smtbmc -s boolector
 smtbmc -s z3 --nomem
-abc_bmc3
+abc bmc3
 
 [script]
 read_verilog -formal -norestrict -assume-asserts picorv32.v
index 1b8eb4b2f2c85ccb37aa0d50295e201501db34ab..feaccf8c383b80a8f50cd8cb7381831084c5e2bb 100644 (file)
@@ -78,7 +78,9 @@ def run_smtbmc(job, engine_idx, engine):
     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"),
             ("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),
@@ -159,8 +161,8 @@ def run(job):
         if engine[0] == "smtbmc":
             run_smtbmc(job, engine_idx, engine)
 
-        elif engine[0] == "abc_bmc3":
-            run_abc_bmc3(job, engine_idx, engine)
+        elif engine[0] == "abc":
+            run_abc(job, engine_idx, engine)
 
         else:
             assert False