aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Expand)AuthorAgeFilesLines
...
* Progress in "share" passClifford Wolf2014-07-201-19/+56
* Started to implement real resource sharingClifford Wolf2014-07-192-0/+444
* now ignore init attributes on non-register wires in sat commandClifford Wolf2014-07-051-4/+24
* added log_header to miter and expose pass, show cell type for exposed portsJohann Glaser2014-05-282-3/+9
* Small improvement in SAT log messagesClifford Wolf2014-03-131-3/+3
* Fixed bug in freduce commandClifford Wolf2014-03-071-0/+30
* Some minor code cleanups in freduce commandClifford Wolf2014-03-071-5/+5
* Added freduce -dumpClifford Wolf2014-03-061-1/+24
* Added freduce -stopClifford Wolf2014-03-061-3/+18
* fixed freduce for Minisat::SimpSolver: use frozen_literal()Clifford Wolf2014-03-031-2/+2
* Added "sat -dump_cnf"Clifford Wolf2014-02-181-5/+34
* Coding style corrections in SatHelper::dump_model_to_vcd()Clifford Wolf2014-02-181-31/+31
* Added "sat -initsteps"Clifford Wolf2014-02-181-14/+29
* Renamed "sat -dump_fail_to_vcd" to "sat -dump_vcd" and some minor cleanupsClifford Wolf2014-02-171-5/+9
* Added "-dump_fail_to_vcd" argument to SAT solverAndrew Zonenberg2014-02-171-0/+114
* Various improvements in expose command (added -sep and -cut)Clifford Wolf2014-02-091-36/+119
* Fixed handling of async reset in expose -evert-dffClifford Wolf2014-02-081-0/+1
* Implemented expose -evert-dffClifford Wolf2014-02-081-11/+301
* Added generic RTLIL::SigSpec::parse_sel() with support for selection variablesClifford Wolf2014-02-062-34/+17
* Added support for sat -show @<sel_name>Clifford Wolf2014-02-061-0/+17
* Added sat -set-init-def and sat -tempinduct-defClifford Wolf2014-02-061-4/+34
* Added expose -dffClifford Wolf2014-02-061-1/+44
* Added miter -make_outcmpClifford Wolf2014-02-061-2/+23
* Added sat -set-init-zero supportClifford Wolf2014-02-061-2/+22
* Added sat -verify and -falsify support for non-prove casesClifford Wolf2014-02-061-14/+26
* Added expose commandClifford Wolf2014-02-052-0/+264
* added sat -falsifyClifford Wolf2014-02-041-4/+28
* Fixed bug in sequential sat proofs and improved handling of assertsClifford Wolf2014-02-041-2/+27
* Addred sat option -ignore_unknown_cellsClifford Wolf2014-02-031-3/+17
* Fixed a bug in miter commandClifford Wolf2014-02-011-2/+2
* Added sat -show-inputs and -show-outputsClifford Wolf2014-02-011-1/+24
* Added miter commandClifford Wolf2014-02-012-0/+307
* Added sat -tempinduc and sat -prove-assertsClifford Wolf2014-01-191-10/+41
* 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