Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | added %pdra -a: run with pdr -nct | Yen-Sheng Ho | 2017-02-23 | 1 | -0/+26 | |
| | ||||||
* | Remapping flops in '%pdra. | Alan Mishchenko | 2017-02-21 | 1 | -2/+11 | |
| | ||||||
* | Changes to Visual Studio project file to support 'pdra'. | Alan Mishchenko | 2017-02-21 | 1 | -2/+2 | |
| | ||||||
* | Merged in ysho/abc (pull request #59) | Alan Mishchenko | 2017-02-22 | 2 | -1/+753 | |
|\ | | | | | | | added a new abstraction | |||||
| * | small tweaks in %pdra -p | Yen-Sheng Ho | 2017-02-20 | 1 | -0/+7 | |
| | | ||||||
| * | added options of checking and pushing to %pdra | Yen-Sheng Ho | 2017-02-20 | 1 | -4/+33 | |
| | | ||||||
| * | fixed a tricky bug: property should not be assumed true in the last frame | Yen-Sheng Ho | 2017-02-19 | 1 | -4/+8 | |
| | | ||||||
| * | working on pdr with wla | Yen-Sheng Ho | 2017-02-19 | 1 | -2/+5 | |
| | | ||||||
| * | working on pdr with wla | Yen-Sheng Ho | 2017-02-19 | 1 | -5/+42 | |
| | | ||||||
| * | working on pdr with wla | Yen-Sheng Ho | 2017-02-19 | 1 | -0/+3 | |
| | | ||||||
| * | working on pdr with wla | Yen-Sheng Ho | 2017-02-19 | 1 | -4/+7 | |
| | | ||||||
| * | working on incremental pdr | Yen-Sheng Ho | 2017-02-18 | 1 | -34/+36 | |
| | | ||||||
| * | working on incremental pdr | Yen-Sheng Ho | 2017-02-18 | 1 | -3/+146 | |
| | | ||||||
| * | copied some functions from pdr | Yen-Sheng Ho | 2017-02-18 | 1 | -2/+427 | |
| | | ||||||
| * | copied pdr_mansolve | Yen-Sheng Ho | 2017-02-18 | 1 | -1/+40 | |
| | | ||||||
| * | started pdrIncr.c | Yen-Sheng Ho | 2017-02-18 | 2 | -1/+58 | |
| | | ||||||
* | | Experiments with SAT sweeping. | Alan Mishchenko | 2017-02-20 | 1 | -2/+17 | |
| | | ||||||
* | | Experiments with SAT sweeping. | Alan Mishchenko | 2017-02-19 | 1 | -18/+71 | |
| | | ||||||
* | | Experiments with SAT sweeping. | Alan Mishchenko | 2017-02-18 | 1 | -23/+96 | |
| | | ||||||
* | | Experiments with SAT sweeping. | Alan Mishchenko | 2017-02-18 | 2 | -0/+863 | |
|/ | ||||||
* | Promising modification of the generalization procedure in 'pdr'. | Alan Mishchenko | 2017-02-17 | 1 | -0/+10 | |
| | ||||||
* | Promising alternative of CEX minimization in 'pdr'. | Alan Mishchenko | 2017-02-16 | 3 | -35/+51 | |
| | ||||||
* | Fixing memory leak in 'pdr'. | Alan Mishchenko | 2017-02-16 | 1 | -6/+7 | |
| | ||||||
* | Promising modification of the generalization procedure in 'pdr'. | Alan Mishchenko | 2017-02-16 | 4 | -16/+28 | |
| | ||||||
* | Word-level abstraction engine. | Alan Mishchenko | 2017-02-15 | 2 | -3/+12 | |
| | ||||||
* | Experiments with simulation. | Alan Mishchenko | 2017-02-14 | 1 | -0/+194 | |
| | ||||||
* | Adding PDR with abstraction. | Alan Mishchenko | 2017-02-13 | 1 | -5/+5 | |
| | ||||||
* | Adding PDR with abstraction. | Alan Mishchenko | 2017-02-11 | 1 | -1/+10 | |
| | ||||||
* | Adding PDR with abstraction. | Alan Mishchenko | 2017-02-11 | 3 | -41/+11 | |
| | ||||||
* | Adding PDR with abstraction. | Alan Mishchenko | 2017-02-10 | 5 | -13/+39 | |
| | ||||||
* | Compiler warnings. | Alan Mishchenko | 2017-02-10 | 1 | -1/+1 | |
| | ||||||
* | Adding PDR with abstraction. | Alan Mishchenko | 2017-02-10 | 5 | -71/+221 | |
| | ||||||
* | Re-introducing floating-point activity in the SAT solver. | Alan Mishchenko | 2017-02-10 | 3 | -0/+5 | |
| | ||||||
* | Standardizing the use of new CNF generator. Adding CNF variable connectivity ↵ | Alan Mishchenko | 2017-02-10 | 2 | -7/+4 | |
| | | | | information. | |||||
* | Making sure 'inv_out' can match flops by name. | Alan Mishchenko | 2017-02-09 | 1 | -0/+2 | |
| | ||||||
* | Adding specialized flop ordering before generalization in 'pdr'. | Alan Mishchenko | 2017-02-06 | 2 | -1/+32 | |
| | ||||||
* | Improving new X-valued simulation in 'pdr'. | Alan Mishchenko | 2017-02-06 | 3 | -13/+176 | |
| | ||||||
* | Compiler warnings. | Alan Mishchenko | 2017-02-05 | 1 | -18/+22 | |
| | ||||||
* | Adding structural flop priority heuristics in 'pdr' (bug fix). | Alan Mishchenko | 2017-02-03 | 1 | -9/+126 | |
| | ||||||
* | Adding structural flop priority heuristics in 'pdr'. | Alan Mishchenko | 2017-02-03 | 7 | -120/+208 | |
| | ||||||
* | Removing dead code in 'pdr'. | Alan Mishchenko | 2017-02-03 | 4 | -81/+0 | |
| | ||||||
* | Enabling new X-valued simulation in 'pdr'. | Alan Mishchenko | 2017-02-03 | 8 | -3/+414 | |
| | ||||||
* | Improvements to inductive generalization in IC3/PDR by Zyad Hassan. | Alan Mishchenko | 2017-02-02 | 6 | -9/+342 | |
| | ||||||
* | Updates to arithmetic verification. | Alan Mishchenko | 2017-01-30 | 4 | -5/+400 | |
| | ||||||
* | Updates to arithmetic verification. | Alan Mishchenko | 2017-01-29 | 4 | -143/+152 | |
| | ||||||
* | Updates to arithmetic verification. | Alan Mishchenko | 2017-01-28 | 5 | -10/+422 | |
| | ||||||
* | Adding features for invariant minimization. | Alan Mishchenko | 2017-01-25 | 1 | -2/+2 | |
| | ||||||
* | Adding features for invariant minimization. | Alan Mishchenko | 2017-01-25 | 1 | -3/+13 | |
| | ||||||
* | Adding features for invariant minimization. | Alan Mishchenko | 2017-01-25 | 1 | -0/+2 | |
| | ||||||
* | Adding features for invariant minimization. | Alan Mishchenko | 2017-01-25 | 1 | -29/+73 | |
| |