summaryrefslogtreecommitdiffstats
path: root/src/proof
Commit message (Expand)AuthorAgeFilesLines
* Updating 'sim3' to move the design into the last rare state.Alan Mishchenko2013-04-012-5/+13
* Improving verbose printout of 'sim3' when solving multiple outputs.Alan Mishchenko2013-03-301-6/+14
* Updating 'pdr' to report the number of failed POs.Alan Mishchenko2013-03-302-1/+3
* Making sure 'pdr -a' return UNDEC if it did not finish proving the remaining ...Alan Mishchenko2013-03-261-9/+10
* Commenting out assertion that fails in 'dch', not sure why.Alan Mishchenko2013-03-141-1/+1
* Fixing gap timeout in 'pdr'.Alan Mishchenko2013-03-071-5/+16
* Modified command 'init' to allow for specific init values.Alan Mishchenko2013-03-071-1/+1
* Improvements to the hierarchy/timing manager.Alan Mishchenko2013-03-051-1/+1
* User-controlable SAT sweeper and other small changes.Alan Mishchenko2013-02-272-4/+2
* Compiler warnings.Alan Mishchenko2013-02-231-0/+2
* Compiler warnings.Alan Mishchenko2013-02-211-1/+1
* Enabling two-timeframe property check in the interpolation procedure.Alan Mishchenko2013-02-214-20/+31
* Added 'gap timeout' to pdr.Alan Mishchenko2013-02-162-14/+34
* Added 'gap timeout' to bmc3 and sim3.Alan Mishchenko2013-02-161-0/+1
* Added 'gap timeout' to bmc3 and sim3.Alan Mishchenko2013-02-152-4/+13
* Corner-case bug fix in PDR.Alan Mishchenko2013-02-011-1/+1
* Fixed a corner-case when 'sim3 -a' does not work for costant POs.Alan Mishchenko2013-01-251-5/+27
* Added switch &trim -V <num> to remove const POs with specific value <num>.Alan Mishchenko2013-01-251-1/+1
* Enabled detecting CEXes in multiple POs without stopping (sim3 -a).Alan Mishchenko2013-01-231-28/+24
* Enabled detecting CEXes in multiple POs without stopping (sim3 -a).Alan Mishchenko2013-01-234-29/+47
* Enabled detecting CEXes in multiple POs without stopping (sim3 -a).Alan Mishchenko2013-01-232-18/+50
* Reintroduced the old abstraction procedure Saig_ManCexAbstractionFlops() form...Alan Mishchenko2013-01-082-31/+162
* Fixing C++ compilation issues.Alan Mishchenko2013-01-083-3/+3
* Fixing C++ compilation issues.Alan Mishchenko2013-01-083-3/+0
* Unifification of custom extensions.Alan Mishchenko2012-12-109-12/+12
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-094-5/+14
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-9/+14
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-098-26/+45
* Corner-case bug fix in &rpm.Alan Mishchenko2012-12-091-0/+5
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-096-129/+165
* Making 'scorr -c' applicable to seq benchmarks without constraints.Alan Mishchenko2012-12-041-4/+4
* Isolating BMC code into a separate package.Alan Mishchenko2012-11-145-0/+5
* Made print-out of frontier cut an option ('-c') in '&ps'.Alan Mishchenko2012-11-122-6/+6
* Enabling verbose report of dumping abstraction in GLA.Alan Mishchenko2012-11-071-4/+4
* Improvements to LMS code.Alan Mishchenko2012-11-061-1/+1
* MergeNiklas Een2012-10-307-3/+38
|\
| * Added switch '-q' to 'scorr' and '&scorr' to quit when PO is not a candidate ...Alan Mishchenko2012-10-254-0/+33
| * Integrating GIA with LUT mapping.Alan Mishchenko2012-10-241-1/+1
| * Creating dedicated choice representation for GIA.Alan Mishchenko2012-10-242-2/+4
* | Replaced printfs with Abc_PrintNiklas Een2012-10-2919-450/+464
* | Replaced printfs with Abc_PrintNiklas Een2012-10-291-36/+35
* | Replaced printfs with Abc_PrintNiklas Een2012-10-291-46/+45
|/
* Making report about the number of correcty covered frames consistent across t...Alan Mishchenko2012-10-092-2/+3
* Bug fix in &gla (incorrect reporting of proved timeframes).Alan Mishchenko2012-10-091-2/+2
* Bug fix in &gla (incorrect reporting of proved timeframes).Alan Mishchenko2012-10-091-1/+2
* Making explicit cast to 64-bit unsigned in a few places.Alan Mishchenko2012-10-091-6/+6
* Updating readme.Alan Mishchenko2012-10-061-1/+2
* C++ portability changes.Alan Mishchenko2012-10-033-3/+3
* C++ portability changes.Alan Mishchenko2012-10-031-1/+1
* C++ portability changes.Alan Mishchenko2012-10-031-4/+4