mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-23 13:18:00 +00:00
Code Activity

Add btor engine

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-12-08 05:23:04 +01:00
parent 4eb91d5b88
commit 4c485766e2
4 changed files with 164 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

19
sbysrc/sby_core.py
View file

@ -153,6 +153,7 @@ class SbyJob:
"suprove": "suprove",
"aigbmc": "aigbmc",
"avy": "avy",
"btormc": "btormc",
}
self.tasks_running = []
@ -333,6 +334,24 @@ class SbyJob:
return [task]
if re.match(r"^btor(_syn)?(_nomem)?$", model_name):
with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f:
print("# running in %s/model/" % (self.workdir), file=f)
print("read_ilang design%s.il" % ("_nomem" if "_nomem" in model_name else ""), file=f)
if "_syn" in model_name:
print("techmap", file=f)
print("opt -fast", file=f)
print("abc", file=f)
print("opt_clean", file=f)
print("stat", file=f)
print("write_btor design_%s.btor" % model_name, file=f)
task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"),
"cd %s/model; %s -ql design_%s.log design_%s.ys" % (self.workdir, self.exe_paths["yosys"], model_name, model_name))
task.checkretcode = True
return [task]
if model_name == "aig":
with open("%s/model/design_aiger.ys" % (self.workdir), "w") as f:
print("# running in %s/model/" % (self.workdir), file=f)