Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-04 | 1 | -6/+7 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-04 | 1 | -9/+42 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-04 | 1 | -52/+59 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-04 | 1 | -2/+1 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-04 | 1 | -1/+1 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-04 | 1 | -46/+108 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-02 | 1 | -8/+9 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-02 | 1 | -0/+1 | |
| | ||||||
* | Adding CEC command &splitprove. | Alan Mishchenko | 2014-06-02 | 1 | -20/+160 | |
| | ||||||
* | Code to explore cofactors of CEC problems. | Alan Mishchenko | 2014-06-02 | 1 | -0/+213 | |
| | ||||||
* | Adding switch to handle only single faults. | Alan Mishchenko | 2014-04-01 | 1 | -1/+1 | |
| | ||||||
* | Compiler warnings. | Alan Mishchenko | 2014-03-31 | 1 | -1/+1 | |
| | ||||||
* | Undoing previous change, which was made by mistake. | Alan Mishchenko | 2014-03-31 | 1 | -1/+1 | |
| | ||||||
* | Making per-output timeout in bmc3 -a and pdr -a work in CLOCKS_PER_SECs ↵ | Alan Mishchenko | 2014-03-31 | 1 | -1/+1 | |
| | | | | instead of miliseconds. | |||||
* | Adding new code to verify invariant derived by 'pdr'. | Alan Mishchenko | 2014-03-30 | 2 | -1/+83 | |
| | ||||||
* | Synchronizing with the recent version. | Alan Mishchenko | 2014-03-16 | 1 | -2/+2 | |
| | ||||||
* | Significant improvement to LUT mappers (if, &if). | Alan Mishchenko | 2014-02-16 | 1 | -1/+1 | |
| | ||||||
* | Handing trivially UNSAT outputs in 'pdr'. | Alan Mishchenko | 2014-02-13 | 1 | -0/+10 | |
| | ||||||
* | Initial new interpolation code. | Alan Mishchenko | 2014-01-28 | 7 | -0/+1254 | |
| | ||||||
* | Tuning for multi-ouptut solver. | Alan Mishchenko | 2013-11-05 | 1 | -1/+1 | |
| | ||||||
* | Sweeper internal verification. | Alan Mishchenko | 2013-11-01 | 1 | -1/+1 | |
| | ||||||
* | Sweeper internal verification and new switch for &cfraig. | Alan Mishchenko | 2013-11-01 | 2 | -2/+9 | |
| | ||||||
* | Sweeper internal verification. | Alan Mishchenko | 2013-11-01 | 1 | -0/+43 | |
| | ||||||
* | Sweeper condition complement bug-fix and code for internal verification. | Alan Mishchenko | 2013-11-01 | 1 | -1/+1 | |
| | ||||||
* | Sweeper assertion. | Alan Mishchenko | 2013-11-01 | 1 | -0/+2 | |
| | ||||||
* | Sweeper assertion. | Alan Mishchenko | 2013-11-01 | 1 | -0/+1 | |
| | ||||||
* | Sweeper return value normalization. | Alan Mishchenko | 2013-11-01 | 2 | -7/+17 | |
| | ||||||
* | Multi-output property solver. | Alan Mishchenko | 2013-10-26 | 1 | -0/+2 | |
| | ||||||
* | Multi-output property solver. | Alan Mishchenko | 2013-10-26 | 1 | -2/+2 | |
| | ||||||
* | Multi-output property solver. | Alan Mishchenko | 2013-10-23 | 2 | -0/+13 | |
| | ||||||
* | Compiler warnings. | Alan Mishchenko | 2013-10-17 | 3 | -4/+6 | |
| | ||||||
* | Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe. | Alan Mishchenko | 2013-10-15 | 2 | -4/+4 | |
| | ||||||
* | Extending truth table support in &jf for more than 6 inputs. | Alan Mishchenko | 2013-10-10 | 1 | -3/+3 | |
| | ||||||
* | Compiler warning. | Alan Mishchenko | 2013-10-05 | 1 | -69/+5 | |
| | ||||||
* | Compiler warning. | Alan Mishchenko | 2013-10-05 | 1 | -1/+1 | |
| | ||||||
* | Added 'abort' message in bridge mode for pdr -a timeout | Niklas Een | 2013-10-04 | 1 | -34/+95 | |
| | ||||||
* | Changing switch -R <num> in &gla to mean the max allowed size of ↵ | Alan Mishchenko | 2013-09-23 | 2 | -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 Mishchenko | 2013-09-21 | 1 | -0/+8 | |
| | | | | less than R/2 during refinement. | |||||
* | Adding switch to enable reuse of proof-obligations in the last timeframe. | Alan Mishchenko | 2013-09-16 | 2 | -1/+2 | |
| | ||||||
* | Added bridge integration for multi-output 'pdr -a'. | Alan Mishchenko | 2013-09-16 | 2 | -3/+18 | |
| | ||||||
* | Bug fix in PDR. | Alan Mishchenko | 2013-09-16 | 1 | -1/+1 | |
| | ||||||
* | Fixing return value of 'pdr -a'. | Alan Mishchenko | 2013-09-15 | 1 | -1/+5 | |
| | ||||||
* | Handling the case when all outputs are undecided in 'pdr -a' with per-output ↵ | Alan Mishchenko | 2013-09-14 | 2 | -6/+3 | |
| | | | | timeout. | |||||
* | Fixing several bugs, which led to unsound results produced by 'pdr -a' with ↵ | Alan Mishchenko | 2013-09-13 | 3 | -4/+15 | |
| | | | | per-output timeout. | |||||
* | Enabling additional printouts in 'pdr'. | Alan Mishchenko | 2013-09-13 | 1 | -2/+4 | |
| | ||||||
* | New API to return the set of all reachable states as an AIG. | Alan Mishchenko | 2013-09-10 | 1 | -1/+93 | |
| | ||||||
* | Unifying parameters for the &ps command. | Alan Mishchenko | 2013-09-05 | 4 | -11/+11 | |
| | ||||||
* | Adding procedures to specify permutations with unused flops. | Alan Mishchenko | 2013-08-28 | 1 | -3/+12 | |
| | ||||||
* | Added switch &sim -g to enable flop grouping. | Alan Mishchenko | 2013-08-20 | 2 | -1/+38 | |
| | ||||||
* | Experiment with 'pdr'. | Alan Mishchenko | 2013-07-19 | 3 | -34/+126 | |
| |