Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding dump of trivial abstraction map at the beginning in &gla -m. | Alan Mishchenko | 2017-02-25 | 1 | -15/+25 |
| | |||||
* | Adding dump of trivial abstraction map at the beginning in &gla -m. | Alan Mishchenko | 2017-02-25 | 1 | -1/+19 |
| | |||||
* | changed how pdr -t cleans up abs flops | Yen-Sheng Ho | 2017-02-23 | 1 | -0/+15 |
| | |||||
* | 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 |
| |