mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00
Code Activity

Merge pull request #1746 from boqwxp/optimization

Browse source 
Add support for optimizing exists-forall problems.
This commit is contained in:
N. Engelhardt 2020-03-16 12:23:14 +01:00 • committed by GitHub
commit a2e340de43
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 55 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
backends/smt2/smt2.cc
View file

@ -536,6 +536,14 @@ struct Smt2Worker
if (cell->attributes.count("\\reg"))
infostr += " " + cell->attributes.at("\\reg").decode_string();
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){
decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
}
else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){
decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
}
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
if (cell->type == "$anyseq")
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));

14
backends/smt2/smtbmc.py
View file

@ -1158,6 +1158,8 @@ def smt_forall_assert():
global asserts_cache_dirty
asserts_cache_dirty = False
assert (len(smt.modinfo[topmod].maximize) + len(smt.modinfo[topmod].minimize) <= 1)
def make_assert_expr(asserts_cache):
expr = list()
for lst in asserts_cache:
@ -1236,6 +1238,18 @@ def smt_forall_assert():
smt.write("".join(assert_expr))
if len(smt.modinfo[topmod].maximize) > 0:
for s in states:
if s in used_states_db:
smt.write("(maximize (|%s| %s))\n" % (smt.modinfo[topmod].maximize.copy().pop(), s))
break
if len(smt.modinfo[topmod].minimize) > 0:
for s in states:
if s in used_states_db:
smt.write("(minimize (|%s| %s))\n" % (smt.modinfo[topmod].minimize.copy().pop(), s))
break
def smt_push():
global asserts_cache_dirty
asserts_cache_dirty = True

12
backends/smt2/smtio.py
View file

@ -101,6 +101,8 @@ class SmtModInfo:
self.cells = dict()
self.asserts = dict()
self.covers = dict()
self.maximize = set()
self.minimize = set()
self.anyconsts = dict()
self.anyseqs = dict()
self.allconsts = dict()
@ -502,6 +504,12 @@ class SmtIo:
if fields[1] == "yosys-smt2-cover":
self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-maximize":
self.modinfo[self.curmod].maximize.add(fields[2])
if fields[1] == "yosys-smt2-minimize":
self.modinfo[self.curmod].minimize.add(fields[2])
if fields[1] == "yosys-smt2-anyconst":
self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
@ -696,7 +704,9 @@ class SmtIo:
if msg is not None:
print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
result = self.read()
result = ""
while result not in ["sat", "unsat"]:
result = self.read()
if self.debug_file:
print("(set-info :status %s)" % result, file=self.debug_file)