summaryrefslogtreecommitdiffstats
path: root/src/proof
Commit message (Collapse)AuthorAgeFilesLines
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-051-1/+1
|
* Sweeper internal verification.Alan Mishchenko2013-11-011-1/+1
|
* Sweeper internal verification and new switch for &cfraig.Alan Mishchenko2013-11-012-2/+9
|
* Sweeper internal verification.Alan Mishchenko2013-11-011-0/+43
|
* Sweeper condition complement bug-fix and code for internal verification.Alan Mishchenko2013-11-011-1/+1
|
* Sweeper assertion.Alan Mishchenko2013-11-011-0/+2
|
* Sweeper assertion.Alan Mishchenko2013-11-011-0/+1
|
* Sweeper return value normalization.Alan Mishchenko2013-11-012-7/+17
|
* Multi-output property solver.Alan Mishchenko2013-10-261-0/+2
|
* Multi-output property solver.Alan Mishchenko2013-10-261-2/+2
|
* Multi-output property solver.Alan Mishchenko2013-10-232-0/+13
|
* Compiler warnings.Alan Mishchenko2013-10-173-4/+6
|
* Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe.Alan Mishchenko2013-10-152-4/+4
|
* Extending truth table support in &jf for more than 6 inputs.Alan Mishchenko2013-10-101-3/+3
|
* Compiler warning.Alan Mishchenko2013-10-051-69/+5
|
* Compiler warning.Alan Mishchenko2013-10-051-1/+1
|
* Added 'abort' message in bridge mode for pdr -a timeoutNiklas Een2013-10-041-34/+95
|
* Changing switch -R <num> in &gla to mean the max allowed size of ↵Alan Mishchenko2013-09-232-9/+10
| | | | abstraction. Adding switch -Q <num> to stop when the number of objects exceeds num % _during_refinement_.
* Adding resource limit to stop &gla when the number of remaining objects is ↵Alan Mishchenko2013-09-211-0/+8
| | | | less than R/2 during refinement.
* Adding switch to enable reuse of proof-obligations in the last timeframe.Alan Mishchenko2013-09-162-1/+2
|
* Added bridge integration for multi-output 'pdr -a'.Alan Mishchenko2013-09-162-3/+18
|
* Bug fix in PDR.Alan Mishchenko2013-09-161-1/+1
|
* Fixing return value of 'pdr -a'.Alan Mishchenko2013-09-151-1/+5
|
* Handling the case when all outputs are undecided in 'pdr -a' with per-output ↵Alan Mishchenko2013-09-142-6/+3
| | | | timeout.
* Fixing several bugs, which led to unsound results produced by 'pdr -a' with ↵Alan Mishchenko2013-09-133-4/+15
| | | | per-output timeout.
* Enabling additional printouts in 'pdr'.Alan Mishchenko2013-09-131-2/+4
|
* New API to return the set of all reachable states as an AIG.Alan Mishchenko2013-09-101-1/+93
|
* Unifying parameters for the &ps command.Alan Mishchenko2013-09-054-11/+11
|
* Adding procedures to specify permutations with unused flops.Alan Mishchenko2013-08-281-3/+12
|
* Added switch &sim -g to enable flop grouping.Alan Mishchenko2013-08-202-1/+38
|
* Experiment with 'pdr'.Alan Mishchenko2013-07-193-34/+126
|
* Small data-structure improvements in 'pdr'.Alan Mishchenko2013-07-193-25/+33
|
* Adding timeout to AIG rewriting inside 'int'.Alan Mishchenko2013-07-081-2/+0
|
* Adding timeout to AIG rewriting inside 'int'.Alan Mishchenko2013-07-071-0/+12
|
* Adding timeout to the interpolant computation procedure.Alan Mishchenko2013-06-281-1/+3
|
* Unifying representation of mapping in GIA.Alan Mishchenko2013-06-252-2/+2
|
* Improving CEC (command 'dcec') by integrating XOR balancing.Alan Mishchenko2013-06-251-1/+1
|
* Improving CEC (command 'dcec') by integrating XOR balancing.Alan Mishchenko2013-06-251-0/+35
|
* Performance improvements in 'pdr'.Alan Mishchenko2013-06-182-4/+10
|
* Bug fixes in the implementation of varius resource limits in 'pdr'.Alan Mishchenko2013-06-181-7/+18
|
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-27102-1090/+1090
|
* Changing how often timeout is checked in the SAT solver and several ↵Alan Mishchenko2013-05-272-1/+19
| | | | application packages.
* g++ warnings.Alan Mishchenko2013-05-192-2/+2
|
* Potential improvement to &scorr.Alan Mishchenko2013-05-181-0/+72
|
* Fixed gap timeout in 'pdr'.Alan Mishchenko2013-05-181-0/+4
|
* Adding new command &mprove for proving groups of properties.Alan Mishchenko2013-05-173-12/+15
|
* Bug fix in the timeout mechanism of 'pdr'.Alan Mishchenko2013-05-171-2/+2
|
* SAT sweeping under constraints (bug fix).Alan Mishchenko2013-05-121-0/+3
|
* Changing per-output runtime limit to be in miliseconds.Alan Mishchenko2013-05-092-2/+2
|
* Bug fix in the sweeper.Alan Mishchenko2013-05-081-1/+3
|