aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
* Improved performance of freduce input cone reductionClifford Wolf2014-01-041-23/+78
|
* Improved freduce performance on const signalsClifford Wolf2014-01-041-13/+63
|
* Performance improvements in freduce passClifford Wolf2014-01-031-27/+69
|
* More freduce cleanupsClifford Wolf2014-01-031-0/+24
|
* Cleanups in freduce commandClifford Wolf2014-01-031-2/+5
|
* Use selection in freduce commandClifford Wolf2014-01-031-5/+20
|
* Another small freduce cleanup/bugfixClifford Wolf2014-01-031-1/+2
|
* More freduce cleanups and bugfixesClifford Wolf2014-01-031-11/+32
|
* Fixed more complex undef cases in freduceClifford Wolf2014-01-021-4/+36
|
* More "freduce" related fixes and improvementsClifford Wolf2014-01-021-19/+67
|
* Some cleanups in freduce -inv mode (and switched from -noinv to -inv)Clifford Wolf2014-01-021-26/+29
|
* Major rewrite of "freduce" commandClifford Wolf2014-01-023-281/+335
|
* Added sat -prove-x and -set-def-inputsClifford Wolf2013-12-281-32/+96
|
* Added sat -set-def/-set-*-undef supportClifford Wolf2013-12-271-5/+66
|
* Renamed sat -set-undef to -set-any-undefClifford Wolf2013-12-271-20/+20
|
* Added sat -max_undef featureClifford Wolf2013-12-071-11/+50
|
* Added "sat" undef support and "sat -set-init" optionsClifford Wolf2013-12-071-40/+146
|
* Fixed compiler warining in passes/sat/eval.ccClifford Wolf2013-12-071-2/+2
|
* Added eval -set-undef and eval -tableClifford Wolf2013-12-071-11/+140
|
* Started implementing undef support in "sat" commandClifford Wolf2013-11-251-12/+103
|
* Improvements in satgen undef handlingClifford Wolf2013-11-251-14/+39
|
* Improvements in satgen undef handlingClifford Wolf2013-11-251-4/+20
|
* Started implementing undef handling in satgenClifford Wolf2013-11-251-9/+30
|
* Improved user-friendliness of "sat" and "eval" expression parsingClifford Wolf2013-11-092-20/+16
|
* Added verification of SAT model to "eval -vloghammer_report" commandClifford Wolf2013-11-091-0/+43
|
* Added handling of unconnected/unspecified signals to eval -vloghammer_reportClifford Wolf2013-11-061-2/+6
|
* Added correct RTL undef handling to eval vloghammer modeClifford Wolf2013-11-061-3/+17
|
* Added eval -vloghammer_report modeClifford Wolf2013-11-061-4/+142
|
* Added sat -ignore_div_by_zero switchClifford Wolf2013-08-151-1/+11
|
* Added eval -brute_force_equiv_checker_x modeClifford Wolf2013-08-151-5/+15
|
* freduce performance fixClifford Wolf2013-08-101-4/+8
|
* Added -try option to freduce passClifford Wolf2013-08-081-16/+44
|
* Fixed topological ordering in freduce passClifford Wolf2013-08-071-54/+67
|
* Small bugfixes in freduce passClifford Wolf2013-08-061-4/+14
|
* Added freduce commandClifford Wolf2013-08-062-0/+362
|
* Added SAT support for -all/-max with -verifyClifford Wolf2013-06-231-6/+11
|
* Added timout functionality to SAT solverClifford Wolf2013-06-201-5/+62
|
* Added "eval" passClifford Wolf2013-06-193-187/+228
|
* Fixed even more ConstEval bugs found using xsthammerClifford Wolf2013-06-141-2/+1
|
* Added consteval testing to xsthammer and fixed bugsClifford Wolf2013-06-131-0/+97
|
* More xsthammer improvements (using xst 14.5 now)Clifford Wolf2013-06-131-1/+1
|
* Improvements and fixes in SAT codeClifford Wolf2013-06-101-4/+14
|
* Renamed "sat_solve" pass to "sat"Clifford Wolf2013-06-093-13/+13
|
* Implemented temporal induction proofs in sat_solveClifford Wolf2013-06-092-37/+178
|
* Added support for non-temporal proofs to sat_solveClifford Wolf2013-06-092-26/+127
|
* Re-organization in sat_solver pass for temporal inductionClifford Wolf2013-06-091-251/+296
|
* Added ezSAT api support for don't care values in modelsClifford Wolf2013-06-091-1/+4
|
* Fixed handling of $_XOR_ in SAT generatorClifford Wolf2013-06-091-1/+3
|
* Added sequential solving support to sat_solveClifford Wolf2013-06-092-57/+208
|
* Fixed typo is sat_solve help msgClifford Wolf2013-06-081-1/+1
|