diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-08 06:34:47 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-13 17:10:29 +0000 |
| commit | 0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7 (patch) | |
| tree | 7ebed8b82028a5ddc35771917e16aba5774cf354 /backends/smt2/smt2.cc | |
| parent | bfeba9ad11847e6a0cbe47f880f3642d5e3a8061 (diff) | |
| download | yosys-0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7.tar.gz yosys-0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7.tar.bz2 yosys-0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7.zip | |
Add support for optimizing exists-forall problems.
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.
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 081dcda99..3e08ce37b 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -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)); |