Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Integration of new SAT sweeper. | Alan Mishchenko | 2017-03-11 | 1 | -10/+32 | |
| | ||||||
* | Improvements to ternary simulation. | Alan Mishchenko | 2017-03-09 | 1 | -3/+3 | |
| | ||||||
* | Improvements to ternary simulation. | Alan Mishchenko | 2017-03-09 | 5 | -8/+375 | |
| | ||||||
* | merge | Yen-Sheng Ho | 2017-03-03 | 1 | -10/+185 | |
|\ | ||||||
| * | Adding alternative generalization procedure. | Alan Mishchenko | 2017-03-02 | 1 | -18/+40 | |
| | | ||||||
| * | Adding alternative generalization procedure. | Alan Mishchenko | 2017-03-01 | 1 | -0/+1 | |
| | | ||||||
| * | Adding alternative generalization procedure. | Alan Mishchenko | 2017-03-01 | 1 | -6/+158 | |
| | | ||||||
* | | added experimental codes | Yen-Sheng Ho | 2017-03-02 | 1 | -2/+105 | |
| | | ||||||
* | | %pdra: added an option -u for checking comb. unsat | Yen-Sheng Ho | 2017-03-01 | 1 | -0/+13 | |
|/ | ||||||
* | 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 | |
| |