summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcDar.c
Commit message (Collapse)AuthorAgeFilesLines
...
* Enabled detecting CEXes in multiple POs without stopping (sim3 -a).Alan Mishchenko2013-01-231-2/+5
|
* Enabled detecting CEXes in multiple POs without stopping (sim3 -a).Alan Mishchenko2013-01-231-2/+2
|
* Fixing C++ compilation issues.Alan Mishchenko2013-01-081-1/+1
|
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-2/+2
|
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-4/+4
|
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-15/+29
|
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-29/+18
|
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-1/+9
|
* Enabling multi-output solving in 'pdr'.Alan Mishchenko2012-12-091-1/+5
|
* Isolating BMC code into a separate package.Alan Mishchenko2012-11-141-0/+1
|
* Performance bug fix in choice generation.Alan Mishchenko2012-11-091-11/+18
|
* Integrating GIA with LUT mapping.Alan Mishchenko2012-10-241-0/+144
|
* Extending BLIF parser/write to hangle multi-output cells.Alan Mishchenko2012-09-191-2/+2
|
* Prepared &gla to try abstracting and proving concurrently.Alan Mishchenko2012-09-141-1/+1
|
* Prepared &gla to try abstracting and proving concurrently.Alan Mishchenko2012-09-141-9/+12
|
* Unified print-out of property failures produced by all engines.Alan Mishchenko2012-09-091-5/+5
|
* Added new command &gla_shrink.Alan Mishchenko2012-09-041-2/+2
|
* Added simulation of comb circuits with user-specified patterns in command 'sim'.Alan Mishchenko2012-08-241-112/+16
|
* Fixing assertion mismatch in bmc2.Alan Mishchenko2012-07-141-1/+1
|
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-111-2/+2
|
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-091-3/+3
|
* Updating memory print-out of &vta and &gla.Alan Mishchenko2012-07-081-1/+1
|
* Adding restart to rarity simulation in sim3 and &sim3.Alan Mishchenko2012-07-081-5/+5
|
* Updating project settings to have simpler include paths.Alan Mishchenko2012-07-071-19/+19
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-25/+34
|
* Changing the rules of assigning the names when AIG is converted into a logic ↵Alan Mishchenko2012-05-111-4/+9
| | | | network.
* Making demiter dump files in the current directory.Alan Mishchenko2012-03-261-5/+13
|
* Logic sharing for multi-input gates.Alan Mishchenko2012-03-251-0/+1
|
* Enabled demitering dual-output miters.Alan Mishchenko2012-03-231-1/+1
|
* Additional features for delay optimizationAlan Mishchenko2012-03-211-0/+9
|
* Renamed Aig_ObjPioNum to be Aig_ObjCioId.Alan Mishchenko2012-03-091-2/+2
|
* Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)...Alan Mishchenko2012-03-091-14/+14
|
* Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ↵Alan Mishchenko2012-03-091-16/+16
| | | | ...Ci/Co.
* Redirecting printf messages.Alan Mishchenko2012-03-021-181/+181
|
* Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default (bug ↵Alan Mishchenko2012-02-251-1/+1
| | | | fix).
* Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default.Alan Mishchenko2012-02-241-8/+11
|
* Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default.Alan Mishchenko2012-02-241-1/+8
|
* Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default.Alan Mishchenko2012-02-241-51/+165
|
* Silencing some of the gcc warnings.Alan Mishchenko2012-02-161-3/+3
|
* Added returning counter-example after BMC, which was recently added to 'dprove'.Alan Mishchenko2012-01-231-0/+4
|
* Major restructuring of the code.Alan Mishchenko2012-01-211-23/+23
|
* Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to control ↵Alan Mishchenko2012-01-191-13/+15
| | | | BMC frames and conflicts.
* Started experiments with a new solver.Alan Mishchenko2011-11-251-3/+3
|
* Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.Alan Mishchenko2011-10-311-5/+5
|
* Changes to CNF generation code.Alan Mishchenko2011-10-171-5/+18
|
* Sequential cleanup with symbolic/ternary simulation.Alan Mishchenko2011-08-251-1/+1
|
* Sequential cleanup with symbolic/ternary simulation.Alan Mishchenko2011-08-241-8/+8
|
* Several bug fixes.Alan Mishchenko2011-08-021-4/+14
|
* Enabled saving vector of counter-examples in the ABC framework.Alan Mishchenko2011-08-021-3/+3
|
* Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when ↵Alan Mishchenko2011-07-311-6/+4
| | | | 2^nRegs frames are completed).
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 06:46:19 +0000