Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Allow for skipping structural hashing when reading GIA from file. | Alan Mishchenko | 2012-07-25 | 5 | -20/+25 |
| | |||||
* | Recording and reusing learned util clauses in bmc2. | Alan Mishchenko | 2012-07-22 | 5 | -3/+22 |
| | |||||
* | Recording and reusing learned util clauses in bmc3. | Alan Mishchenko | 2012-07-22 | 5 | -16/+78 |
| | |||||
* | Scalable gate-level abstraction. | Alan Mishchenko | 2012-07-21 | 3 | -124/+263 |
| | |||||
* | Correcting &gla to update status as 'sat' after CEX is found. | Alan Mishchenko | 2012-07-20 | 2 | -8/+2 |
| | |||||
* | Updated code for lazy man's synthesis (memory optimization). | Alan Mishchenko | 2012-07-20 | 5 | -59/+372 |
| | |||||
* | Updated code for lazy man's synthesis. | Alan Mishchenko | 2012-07-20 | 5 | -90/+155 |
| | |||||
* | Added switch &trim -c to additionally remove direct connections (POs fed by ↵ | Alan Mishchenko | 2012-07-20 | 2 | -3/+66 |
| | | | | PIs). | ||||
* | Updated code for lazy man's synthesis. | Alan Mishchenko | 2012-07-20 | 3 | -309/+76 |
| | |||||
* | New procedures to generate NPN-classes for a library of 6-input functions. | Alan Mishchenko | 2012-07-20 | 1 | -8/+16 |
| | |||||
* | Merging recent changes. | Alan Mishchenko | 2012-07-20 | 3 | -0/+295 |
|\ | |||||
| * | New procedures to generate NPN-classes for a library of 6-input functions. | Alan Mishchenko | 2012-07-19 | 3 | -0/+295 |
| | | |||||
* | | Making GIA use independent truth table number storage when computing truth ↵ | Alan Mishchenko | 2012-07-19 | 3 | -6/+10 |
|/ | | | | tables. | ||||
* | Scalable gate-level abstraction. | Alan Mishchenko | 2012-07-18 | 1 | -0/+1021 |
| | |||||
* | Enabling &gla for combinational miters. | Alan Mishchenko | 2012-07-18 | 3 | -22/+13 |
| | |||||
* | Adding new file to the build file. | Alan Mishchenko | 2012-07-17 | 1 | -0/+1 |
| | |||||
* | Small bug in bmc2 timeout. | Alan Mishchenko | 2012-07-16 | 1 | -1/+1 |
| | |||||
* | Updated code for lazy man's synthesis. | Alan Mishchenko | 2012-07-15 | 2 | -0/+5 |
| | |||||
* | Updated code for lazy man's synthesis. | Alan Mishchenko | 2012-07-15 | 8 | -30/+3020 |
| | |||||
* | Added new refinement manager for &gla and &abs_refine. | Alan Mishchenko | 2012-07-14 | 1 | -0/+2 |
| | |||||
* | Added new refinement manager for &gla and &abs_refine. | Alan Mishchenko | 2012-07-14 | 5 | -8/+735 |
| | |||||
* | Fixing assertion mismatch in bmc2. | Alan Mishchenko | 2012-07-14 | 1 | -1/+1 |
| | |||||
* | Fixing the integer print-out problem. | Alan Mishchenko | 2012-07-13 | 1 | -13/+13 |
| | |||||
* | Fixing the integer print-out problem. | Alan Mishchenko | 2012-07-13 | 1 | -12/+18 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 2 | -12/+7 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 2 | -50/+26 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+7 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+1 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -3/+3 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+1 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -1/+1 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -1/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+5 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -1/+3 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -3/+21 |
| | |||||
* | Fixing compiler warning. | Alan Mishchenko | 2012-07-13 | 1 | -0/+1 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+19 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -31/+9 |
| | |||||
* | Fixing a mismatch in regular/shadow page memory appending procedure. | Alan Mishchenko | 2012-07-13 | 1 | -2/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+6 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+3 |
| | |||||
* | Several small changes and fixes. | Alan Mishchenko | 2012-07-13 | 7 | -31/+46 |
| | |||||
* | Removed useless file. | Alan Mishchenko | 2012-07-12 | 3 | -10/+6 |
| | |||||
* | Upgraded &equiv3 to periodically restart simulation from the init state. | Alan Mishchenko | 2012-07-12 | 1 | -7/+24 |
| | |||||
* | Added procedure for checking satisfied clauses. | Alan Mishchenko | 2012-07-12 | 1 | -0/+37 |
| | |||||
* | Fixing temporary linker problem. | Alan Mishchenko | 2012-07-12 | 1 | -1/+2 |
| |