summaryrefslogtreecommitdiffstats
path: root/src/base/wlc/wlcCom.c
Commit message (Expand)AuthorAgeFilesLines
* Adding new type of MUX blasting.Alan Mishchenko2017-07-071-4/+8
* mergeYen-Sheng Ho2017-06-061-4/+8
|\
| * Adding switch %blast -d to dump dual-output miter after blasting.Alan Mishchenko2017-04-291-4/+8
* | %pdra: added an option for disabling incremental solvingYen-Sheng Ho2017-04-161-2/+6
|/
* %pdra: added an option -t for disabling trace reuseYen-Sheng Ho2017-03-311-2/+6
* %pdra: added an option -sYen-Sheng Ho2017-03-281-2/+6
* %pdra: working on bmc3Yen-Sheng Ho2017-03-181-2/+6
* New word-level transformation.Alan Mishchenko2017-03-171-1/+49
* %pdra: added an option -i for weaker proof-based refinementYen-Sheng Ho2017-03-091-2/+6
* %pdra, %abs: added option -d for apple-to-apple comparisonYen-Sheng Ho2017-03-091-4/+12
* %pdra: added an option -u for checking comb. unsatYen-Sheng Ho2017-03-011-2/+6
* small tweaksYen-Sheng Ho2017-02-281-1/+1
* added an option -r to %pdra: proof-based refinement onlyYen-Sheng Ho2017-02-281-1/+5
* added -L to %absYen-Sheng Ho2017-02-281-2/+14
* %pdra -L: now applies to all typesYen-Sheng Ho2017-02-271-3/+3
* added an option -L to %pdra for limiting the number of muxesYen-Sheng Ho2017-02-261-2/+14
* added an option -b to %pdraYen-Sheng Ho2017-02-251-3/+7
* added %pdra -a: run with pdr -nctYen-Sheng Ho2017-02-231-2/+6
* added an option -m for %pdraYen-Sheng Ho2017-02-221-3/+7
* clean upYen-Sheng Ho2017-02-211-2/+2
* added options of checking and pushing to %pdraYen-Sheng Ho2017-02-201-2/+10
* added datastructure for %pdra optionsYen-Sheng Ho2017-02-201-2/+2
* working on pdr with wlaYen-Sheng Ho2017-02-191-1/+1
* started %pdraYen-Sheng Ho2017-02-191-0/+117
* Word-level abstraction engine.Alan Mishchenko2017-02-151-4/+139
* Word-level abstraction.Alan Mishchenko2017-02-091-3/+5
* Making sure 'inv_out' can match flops by name.Alan Mishchenko2017-02-091-2/+2
* Word-level abstraction.Alan Mishchenko2017-02-091-1/+98
* Adding visualization of word-level networks Wlc_Ntk_t.Alan Mishchenko2017-01-261-6/+22
* Adding visualization of word-level networks Wlc_Ntk_t.Alan Mishchenko2017-01-261-45/+111
* Adding visualization of word-level networks Wlc_Ntk_t.Alan Mishchenko2017-01-261-0/+116
* Adding features for invariant minimization.Alan Mishchenko2017-01-251-1/+1
* Adding features for invariant minimization.Alan Mishchenko2017-01-241-8/+8
* Adding features for invariant minimization.Alan Mishchenko2017-01-241-8/+20
* Adding features for invariant minimization.Alan Mishchenko2017-01-241-63/+275
* New command to profile arithmetic logic cones.Alan Mishchenko2016-11-261-1/+47
* Change Verilog reader to take a string rather than file name.Alan Mishchenko2016-10-061-1/+1
* Updates to arithmetic verification.Alan Mishchenko2016-08-051-4/+8
* Adding output range support to %blast.Alan Mishchenko2016-07-181-4/+33
* Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift).Alan Mishchenko2016-07-121-2/+2
* New profiling features for word-level optimizations.Alan Mishchenko2016-06-041-4/+8
* Improving SMT-LIB parser.Alan Mishchenko2016-05-211-3/+13
* Enabling AIGs without structural hashing.Alan Mishchenko2016-05-201-4/+8
* Changes to PDR to compute f-inf clauses and import invariant (or clauses) as ...Alan Mishchenko2016-01-141-1/+66
* Corner-case bug in invariant profiling.Alan Mishchenko2015-12-181-0/+5
* New command %psinv.Alan Mishchenko2015-11-231-0/+54
* Bug fixing in %blast when blasting MUX coming from always-statement.Alan Mishchenko2015-07-071-4/+9
* Bug fixing in %blast when blasting mod operator (handling zero divisor).Alan Mishchenko2015-07-071-4/+22
* Adding new debugging feature to Wlc_Ntk_t.Alan Mishchenko2015-06-191-1/+3
* Sequential word-level simulator for Wlc_Ntk_t.Alan Mishchenko2015-06-041-0/+2