mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-07-24 13:18:56 +00:00
Code Activity

Add support for optimizing exists-forall problems.

Browse source 
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
This commit is contained in:
Alberto Gonzalez 2020-03-08 06:34:47 +00:00
parent bfeba9ad11
commit 0fda8308bc
5 changed files with 55 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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)