riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
yosys/examples/smtbmc/Makefile

74 lines
2.4 KiB
Makefile
Raw Normal View History

Added examples/smtbmc
2016-07-13 02:49:05 -05:00
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.
2020-03-08 00:34:47 -06:00
all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9
Added examples/smtbmc/demo2.v
2016-08-20 11:44:27 -05:00
Added examples/smtbmc
2016-07-13 02:49:05 -05:00
demo1: demo1.smt2
Added smtbmc longopt support
2016-08-20 09:07:59 -05:00
yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
Added examples/smtbmc
2016-07-13 02:49:05 -05:00
Added examples/smtbmc/demo2.v
2016-08-20 11:44:27 -05:00
demo2: demo2.smt2
More yosys-smtbmc smtc features
2016-08-24 16:18:29 -05:00
yosys-smtbmc -g --dump-vcd demo2.vcd --dump-smtc demo2.smtc --dump-vlogtb demo2_tb.v demo2.smt2
Added examples/smtbmc/demo2.v
2016-08-20 11:44:27 -05:00
iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
vvp demo2_tb +vcd=demo2_tb.vcd
More yosys-smtbmc smtc features
2016-08-24 16:18:29 -05:00
demo3: demo3.smt2
yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2
Added smtc "final" statement
2016-08-27 07:30:36 -05:00
demo4: demo4.smt2
yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2
Added $anyconst support to yosys-smtbmc
2016-08-30 12:27:42 -05:00
demo5: demo5.smt2
yosys-smtbmc -g -t 50 --dump-vcd demo5.vcd demo5.smt2
Improvements in assertpmux
2016-09-07 05:42:16 -05:00
demo6: demo6.smt2
yosys-smtbmc -t 1 demo6.smt2
yosys-smtbmc meminit support
2016-09-08 04:16:12 -05:00
demo7: demo7.smt2
yosys-smtbmc -t 10 demo7.smt2
Add smtbmc support for exist-forall problems Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 12:33:30 -06:00
demo8: demo8.smt2
yosys-smtbmc -s z3 -t 1 -g demo8.smt2
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.
2020-03-08 00:34:47 -06:00
demo9: demo9.smt2
yosys-smtbmc -s z3 -t 1 -g demo9.smt2
Added examples/smtbmc
2016-07-13 02:49:05 -05:00
demo1.smt2: demo1.v
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
2016-08-30 05:40:09 -05:00
yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
Added examples/smtbmc/demo2.v
2016-08-20 11:44:27 -05:00
demo2.smt2: demo2.v
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
2016-08-30 05:40:09 -05:00
yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires demo2.smt2'
Added examples/smtbmc
2016-07-13 02:49:05 -05:00
More yosys-smtbmc smtc features
2016-08-24 16:18:29 -05:00
demo3.smt2: demo3.v
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
2016-08-30 05:40:09 -05:00
yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires demo3.smt2'
More yosys-smtbmc smtc features
2016-08-24 16:18:29 -05:00
Added smtc "final" statement
2016-08-27 07:30:36 -05:00
demo4.smt2: demo4.v
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
2016-08-30 05:40:09 -05:00
yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires demo4.smt2'
Added smtc "final" statement
2016-08-27 07:30:36 -05:00
Added $anyconst support to yosys-smtbmc
2016-08-30 12:27:42 -05:00
demo5.smt2: demo5.v
yosys -ql demo5.yslog -p 'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'
Improvements in assertpmux
2016-09-07 05:42:16 -05:00
demo6.smt2: demo6.v
yosys -ql demo6.yslog -p 'read_verilog demo6.v; prep -top demo6 -nordff; assertpmux; opt -keepdc -fast; write_smt2 -wires demo6.smt2'
yosys-smtbmc meminit support
2016-09-08 04:16:12 -05:00
demo7.smt2: demo7.v
yosys -ql demo7.yslog -p 'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.smt2'
Add smtbmc support for exist-forall problems Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 12:33:30 -06:00
demo8.smt2: demo8.v
yosys -ql demo8.yslog -p 'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2'
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.
2020-03-08 00:34:47 -06:00
demo9.smt2: demo9.v
yosys -ql demo9.yslog -p 'read_verilog -formal demo9.v; prep -top demo9 -nordff; write_smt2 -stbv -wires demo9.smt2'
Added examples/smtbmc
2016-07-13 02:49:05 -05:00
clean:
yosys-smtbmc --smtc -g
2016-08-24 15:09:50 -05:00
rm -f demo1.yslog demo1.smt2 demo1.vcd
More yosys-smtbmc smtc features
2016-08-24 16:18:29 -05:00
rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
rm -f demo3.yslog demo3.smt2 demo3.vcd
Added smtc "final" statement
2016-08-27 07:30:36 -05:00
rm -f demo4.yslog demo4.smt2 demo4.vcd
Added $anyconst support to yosys-smtbmc
2016-08-30 12:27:42 -05:00
rm -f demo5.yslog demo5.smt2 demo5.vcd
Improvements in assertpmux
2016-09-07 05:42:16 -05:00
rm -f demo6.yslog demo6.smt2
yosys-smtbmc meminit support
2016-09-08 04:16:12 -05:00
rm -f demo7.yslog demo7.smt2
Add smtbmc support for exist-forall problems Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 12:33:30 -06:00
rm -f demo8.yslog demo8.smt2
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.
2020-03-08 00:34:47 -06:00
rm -f demo9.yslog demo9.smt2
Added examples/smtbmc
2016-07-13 02:49:05 -05:00
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.
2020-03-08 00:34:47 -06:00
.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 clean
Added examples/smtbmc
2016-07-13 02:49:05 -05:00