aboutsummaryrefslogtreecommitdiffstats
path: root/examples/smtbmc
Commit message (Collapse)AuthorAgeFilesLines
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-233-2/+23
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add $allconst and $allseq cell typesClifford Wolf2018-02-231-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Added $anyseq cell typeClifford Wolf2016-10-141-1/+2
|
* yosys-smtbmc meminit supportClifford Wolf2016-09-083-2/+29
|
* Improvements in assertpmuxClifford Wolf2016-09-073-2/+25
|
* Made examples/smtbmc/demo1.v more interestingClifford Wolf2016-09-021-1/+1
|
* Added $anyconst support to yosys-smtbmcClifford Wolf2016-08-303-1/+29
|
* Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"Clifford Wolf2016-08-301-4/+4
|
* Removed $predict againClifford Wolf2016-08-281-1/+0
|
* Added smtc "final" statementClifford Wolf2016-08-274-2/+36
|
* More yosys-smtbmc smtc featuresClifford Wolf2016-08-244-5/+38
|
* yosys-smtbmc --smtc -gClifford Wolf2016-08-242-5/+14
|
* Added "yosys-smtbmc --dump-constr"Clifford Wolf2016-08-221-1/+1
|
* Added examples/smtbmc/demo2.vClifford Wolf2016-08-203-3/+45
|
* Added smtbmc longopt supportClifford Wolf2016-08-201-2/+2
|
* Added $initstate support to smtbmc flowClifford Wolf2016-07-271-1/+2
|
* After reading the SV spec, using non-standard predict() instead of expect()Clifford Wolf2016-07-211-1/+1
|
* Added examples/smtbmcClifford Wolf2016-07-132-0/+30