aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/satgen.h
Commit message (Expand)AuthorAgeFilesLines
* SigSpec refactoring: using the accessor functions everywhereClifford Wolf2014-07-221-7/+7
* SigSpec refactoring: renamed chunks and width to __chunks and __widthClifford Wolf2014-07-221-7/+7
* Bugfix in satgen for cells with wider in- than outputs.Clifford Wolf2014-07-211-1/+9
* Added libs/minisat (copy of minisat git master)Clifford Wolf2014-03-121-6/+1
* Fixed use of frozen literals in SatGenClifford Wolf2014-03-061-3/+2
* Strictly zero-extend unsigned A-inputs of shift operationsClifford Wolf2014-03-061-1/+1
* Added support for $bu0 to SatGenClifford Wolf2014-02-261-4/+4
* Added support for Minisat::SimpSolver + ezSAT frezze() APIClifford Wolf2014-02-231-0/+1
* Added $slice and $concat cell typesClifford Wolf2014-02-071-0/+21
* Fixed bug in sequential sat proofs and improved handling of assertsClifford Wolf2014-02-041-7/+16
* Added $assert support to satgenClifford Wolf2014-01-191-0/+21
* Fixed SAT and ConstEval undef handling for $pmux and $safe_pmuxClifford Wolf2014-01-031-6/+37
* Added SAT undef model for $pmux and $safe_pmuxClifford Wolf2014-01-021-4/+19
* Major rewrite of "freduce" commandClifford Wolf2014-01-021-5/+3
* Fixed undef extend for bitwise binary ops (bugs in simplemap and satgen)Clifford Wolf2013-12-291-11/+8
* Fixed sat handling of $eqx and $nex with unequal port widthsClifford Wolf2013-12-271-0/+2
* Small cleanup in SatGenClifford Wolf2013-12-271-2/+0
* Fixed sat handling of $eqx and $nex cellsClifford Wolf2013-12-271-1/+12
* Added support for non-const === and !== (for miter circuits)Clifford Wolf2013-12-271-4/+16
* Added "sat" undef support and "sat -set-init" optionsClifford Wolf2013-12-071-13/+24
* Improvements in satgen undef handlingClifford Wolf2013-11-251-73/+170
* Improvements in satgen undef handlingClifford Wolf2013-11-251-27/+122
* Started implementing undef handling in satgenClifford Wolf2013-11-251-25/+172
* Added verification of SAT model to "eval -vloghammer_report" commandClifford Wolf2013-11-091-6/+5
* Improved width extension with regard to undef propagationClifford Wolf2013-11-061-3/+3
* Implemented same div-by-zero behavior as found in other synthesis toolsClifford Wolf2013-08-151-5/+28
* Added sat -ignore_div_by_zero switchClifford Wolf2013-08-151-1/+6
* Added SAT support for $div and $mod cellsClifford Wolf2013-08-111-0/+46
* Fixed shift ops with large right hand sideClifford Wolf2013-07-091-1/+1
* More fixes for bugs found using xsthammerClifford Wolf2013-06-131-0/+1
* Another fix for a bug found using xsthammerClifford Wolf2013-06-121-0/+10
* Sign-extension related fixes in SatGen and AST frontendClifford Wolf2013-06-101-8/+8
* Improvements and fixes in SAT codeClifford Wolf2013-06-101-5/+22
* Implemented temporal induction proofs in sat_solveClifford Wolf2013-06-091-2/+2
* Fixed handling of $_XOR_ in SAT generatorClifford Wolf2013-06-091-1/+1
* Added sequential solving support to sat_solveClifford Wolf2013-06-091-32/+49
* Added support for shifter cells to SAT generatorClifford Wolf2013-06-081-7/+26
* Various improvements in sat_solve pass and SAT generatorClifford Wolf2013-06-081-31/+81
* Improved sat generator and sat_solve passClifford Wolf2013-06-071-9/+46
* Added SAT generator and simple sat_solve commandClifford Wolf2013-06-071-0/+137