iCE40/yosys - [no description]

	Commit message (Collapse)	Author	Age	Files	Lines
*	glift: Add examples, including a number of benchmarks used in some academic ↵	Alberto Gonzalez	2020-07-01	1	-1/+5
\| \| \| \|	works.
*	Add support for optimizing exists-forall problems.	Alberto Gonzalez	2020-03-13	1	-2/+9
\| \| \| \| \| \|	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.
*	Add smtbmc support for exist-forall problems	Clifford Wolf	2018-02-23	1	-2/+9
\| \| \| \|	Signed-off-by: Clifford Wolf <clifford@clifford.at>
*	yosys-smtbmc meminit support	Clifford Wolf	2016-09-08	1	-2/+9
\|
*	Improvements in assertpmux	Clifford Wolf	2016-09-07	1	-2/+9
\|
*	Added $anyconst support to yosys-smtbmc	Clifford Wolf	2016-08-30	1	-1/+8
\|
*	Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"	Clifford Wolf	2016-08-30	1	-4/+4
\|
*	Added smtc "final" statement	Clifford Wolf	2016-08-27	1	-2/+9
\|
*	More yosys-smtbmc smtc features	Clifford Wolf	2016-08-24	1	-4/+11
\|
*	yosys-smtbmc --smtc -g	Clifford Wolf	2016-08-24	1	-5/+5
\|
*	Added "yosys-smtbmc --dump-constr"	Clifford Wolf	2016-08-22	1	-1/+1
\|
*	Added examples/smtbmc/demo2.v	Clifford Wolf	2016-08-20	1	-2/+13
\|
*	Added smtbmc longopt support	Clifford Wolf	2016-08-20	1	-2/+2
\|
*	Added examples/smtbmc	Clifford Wolf	2016-07-13	1	-0/+13