Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Bug fix in &sat -x. | Alan Mishchenko | 2018-05-07 | 1 | -0/+2 |
| | |||||
* | Adding &sat -x to save CEXes for multi-output combinational miters. | Alan Mishchenko | 2018-05-06 | 3 | -0/+23 |
| | |||||
* | Adding switch 'scorr -f' to dump inductive invariant as an AIG. | Alan Mishchenko | 2018-03-22 | 3 | -9/+18 |
| | |||||
* | Compilation problem with pow(). | Alan Mishchenko | 2018-02-19 | 1 | -3/+3 |
| | |||||
* | Experiments with circuit-based SAT. | Alan Mishchenko | 2018-01-27 | 1 | -1/+1 |
| | |||||
* | Experiments with SAT-based simulation. | Alan Mishchenko | 2018-01-25 | 1 | -8/+11 |
| | |||||
* | Experiments with SAT-based simulation. | Alan Mishchenko | 2018-01-23 | 1 | -2/+17 |
| | |||||
* | Changes to make GIA structural hashing use a dedicated array instead of ↵ | Alan Mishchenko | 2017-11-13 | 1 | -1/+1 |
| | | | | pObj->Value. | ||||
* | Profiling quantification and other changes. | Alan Mishchenko | 2017-11-06 | 2 | -38/+43 |
| | |||||
* | Bug fix in old lcorr with constraints. | Alan Mishchenko | 2017-11-04 | 1 | -1/+1 |
| | |||||
* | Enabling Glucose in SAT sweeping: &fraig -g. | Alan Mishchenko | 2017-09-18 | 1 | -0/+1 |
| | |||||
* | Enabling Glucose in SAT sweeping: &fraig -g. | Alan Mishchenko | 2017-09-18 | 1 | -0/+1048 |
| | |||||
* | bridge relates: (1) fix netlist reader to read the latest version written by ↵ | Baruch Sterin | 2017-09-15 | 1 | -24/+24 |
| | | | | ZZ, (2) replace printf() with Abc_Print() in pdr so that it will not interfer with bridge messages | ||||
* | Changes to 'pdr' to run with updated Satoko. | Alan Mishchenko | 2017-09-06 | 1 | -1/+1 |
| | |||||
* | Changes to 'pdr' to run with updated Satoko. | Alan Mishchenko | 2017-09-06 | 3 | -6/+8 |
| | |||||
* | Fixing bronken C++ build; Satoko internal header, solver.h, should not be ↵ | Bruno Schmitt | 2017-08-29 | 2 | -12/+13 |
| | | | | used in other packages | ||||
* | Integrating Satoko into 'bmc' and 'bmc2'. | Alan Mishchenko | 2017-08-16 | 3 | -3/+3 |
| | |||||
* | Integrating Satoko into pdr. | Alan Mishchenko | 2017-08-16 | 9 | -42/+68 |
| | |||||
* | Compiler warnings. | Alan Mishchenko | 2017-07-22 | 2 | -3/+3 |
| | |||||
* | Experiments with SAT sweeping. | Alan Mishchenko | 2017-04-11 | 3 | -1/+8 |
| | |||||
* | Experiments with SAT sweeping. | Alan Mishchenko | 2017-04-11 | 2 | -23/+78 |
| | |||||
* | %pdra: added an option -t for disabling trace reuse | Yen-Sheng Ho | 2017-03-31 | 1 | -0/+3 |
| | |||||
* | merge | Yen-Sheng Ho | 2017-03-31 | 1 | -1/+3 |
|\ | |||||
| * | Experiments with multipliers. | Alan Mishchenko | 2017-03-28 | 1 | -1/+3 |
| | | |||||
* | | %pdra: fixed bugs | Yen-Sheng Ho | 2017-03-30 | 1 | -1/+2 |
| | | |||||
* | | added callbacks to sat solvers in pdr | Yen-Sheng Ho | 2017-03-29 | 1 | -0/+4 |
| | | |||||
* | | %pdra: fixed bugs | Yen-Sheng Ho | 2017-03-29 | 1 | -1/+5 |
| | | |||||
* | | %pdra: refactor | Yen-Sheng Ho | 2017-03-27 | 1 | -14/+0 |
| | | |||||
* | | %pdra: added a procedure to rebuild traces | Yen-Sheng Ho | 2017-03-27 | 1 | -5/+140 |
|/ | |||||
* | Experiments with don't-cares. | Alan Mishchenko | 2017-03-26 | 1 | -1/+1 |
| | |||||
* | Experiments with multipliers. | Alan Mishchenko | 2017-03-26 | 2 | -175/+463 |
| | |||||
* | Experiments with don't-cares. | Alan Mishchenko | 2017-03-22 | 2 | -0/+928 |
| | |||||
* | 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 |
| | |