mirror of https://github.com/YosysHQ/yosys.git
0fda8308bc
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. |
||
|---|---|---|
| .. | ||
| .gitignore | ||
| Makefile | ||
| demo1.v | ||
| demo2.v | ||
| demo3.smtc | ||
| demo3.v | ||
| demo4.smtc | ||
| demo4.v | ||
| demo5.v | ||
| demo6.v | ||
| demo7.v | ||
| demo8.v | ||
| demo9.v | ||