summaryrefslogtreecommitdiff
path: root/kernel/satgen.h
Commit message (Collapse)AuthorAge
* Renamed port access function on RTLIL::Cell, added param access functionsClifford Wolf2014-07-31
|
* Using native ezSAT shift ops in satgen, fixed $shift and $shiftx SAT modelsClifford Wolf2014-07-30
|
* Added $shift and $shiftx cell types (needed for correct part select behavior)Clifford Wolf2014-07-29
|
* Using log_assert() instead of assert()Clifford Wolf2014-07-28
|
* Changed users of cell->connections_ to the new API (sed command)Clifford Wolf2014-07-26
| | | | | | | | | git grep -l 'connections_' | xargs sed -i -r -e ' s/(->|\.)connections_\["([^"]*)"\] = (.*);/\1set("\2", \3);/g; s/(->|\.)connections_\["([^"]*)"\]/\1get("\2")/g; s/(->|\.)connections_.at\("([^"]*)"\)/\1get("\2")/g; s/(->|\.)connections_.push_back/\1connect/g; s/(->|\.)connections_/\1connections()/g;'
* Renamed RTLIL::{Module,Cell}::connections to connections_Clifford Wolf2014-07-26
|
* Removed RTLIL::SigSpec::expand() methodClifford Wolf2014-07-23
|
* SigSpec refactoring: using the accessor functions everywhereClifford Wolf2014-07-22
|
* SigSpec refactoring: renamed chunks and width to __chunks and __widthClifford Wolf2014-07-22
|
* Bugfix in satgen for cells with wider in- than outputs.Clifford Wolf2014-07-21
|
* Added libs/minisat (copy of minisat git master)Clifford Wolf2014-03-12
|
* Fixed use of frozen literals in SatGenClifford Wolf2014-03-06
|
* Strictly zero-extend unsigned A-inputs of shift operationsClifford Wolf2014-03-06
|
* Added support for $bu0 to SatGenClifford Wolf2014-02-26
|
* Added support for Minisat::SimpSolver + ezSAT frezze() APIClifford Wolf2014-02-23
|
* Added $slice and $concat cell typesClifford Wolf2014-02-07
|
* Fixed bug in sequential sat proofs and improved handling of assertsClifford Wolf2014-02-04
|
* Added $assert support to satgenClifford Wolf2014-01-19
|
* Fixed SAT and ConstEval undef handling for $pmux and $safe_pmuxClifford Wolf2014-01-03
|
* Added SAT undef model for $pmux and $safe_pmuxClifford Wolf2014-01-02
|
* Major rewrite of "freduce" commandClifford Wolf2014-01-02
|
* Fixed undef extend for bitwise binary ops (bugs in simplemap and satgen)Clifford Wolf2013-12-29
|
* Fixed sat handling of $eqx and $nex with unequal port widthsClifford Wolf2013-12-27
|
* Small cleanup in SatGenClifford Wolf2013-12-27
|
* Fixed sat handling of $eqx and $nex cellsClifford Wolf2013-12-27
|
* Added support for non-const === and !== (for miter circuits)Clifford Wolf2013-12-27
|
* Added "sat" undef support and "sat -set-init" optionsClifford Wolf2013-12-07
|
* Improvements in satgen undef handlingClifford Wolf2013-11-25
|
* Improvements in satgen undef handlingClifford Wolf2013-11-25
|
* Started implementing undef handling in satgenClifford Wolf2013-11-25
|
* Added verification of SAT model to "eval -vloghammer_report" commandClifford Wolf2013-11-09
|
* Improved width extension with regard to undef propagationClifford Wolf2013-11-06
|
* Implemented same div-by-zero behavior as found in other synthesis toolsClifford Wolf2013-08-15
|
* Added sat -ignore_div_by_zero switchClifford Wolf2013-08-15
|
* Added SAT support for $div and $mod cellsClifford Wolf2013-08-11
|
* Fixed shift ops with large right hand sideClifford Wolf2013-07-09
|
* More fixes for bugs found using xsthammerClifford Wolf2013-06-13
|
* Another fix for a bug found using xsthammerClifford Wolf2013-06-12
|
* Sign-extension related fixes in SatGen and AST frontendClifford Wolf2013-06-10
|
* Improvements and fixes in SAT codeClifford Wolf2013-06-10
|
* Implemented temporal induction proofs in sat_solveClifford Wolf2013-06-09
|
* Fixed handling of $_XOR_ in SAT generatorClifford Wolf2013-06-09
|
* Added sequential solving support to sat_solveClifford Wolf2013-06-09
|
* Added support for shifter cells to SAT generatorClifford Wolf2013-06-08
|
* Various improvements in sat_solve pass and SAT generatorClifford Wolf2013-06-08
|
* Improved sat generator and sat_solve passClifford Wolf2013-06-07
|
* Added SAT generator and simple sat_solve commandClifford Wolf2013-06-07