Yen-Sheng Ho
|
70511b001c
|
%pdra: added an option -i for weaker proof-based refinement
|
2017-03-09 21:43:18 -08:00 |
Yen-Sheng Ho
|
3ae83d376a
|
%pdra, %abs: added option -d for apple-to-apple comparison
|
2017-03-09 13:07:30 -08:00 |
Yen-Sheng Ho
|
18b47dfbd5
|
%pdra: added an option -u for checking comb. unsat
|
2017-03-01 14:57:43 -08:00 |
Yen-Sheng Ho
|
007195ddd8
|
small tweaks
|
2017-02-28 19:25:11 -08:00 |
Yen-Sheng Ho
|
902a78eeb8
|
added an option -r to %pdra: proof-based refinement only
|
2017-02-28 18:05:58 -08:00 |
Yen-Sheng Ho
|
43f34ddc02
|
added -L to %abs
|
2017-02-28 08:05:33 -08:00 |
Yen-Sheng Ho
|
9195192f65
|
%pdra -L: now applies to all types
|
2017-02-27 14:31:59 -08:00 |
Yen-Sheng Ho
|
86b3cb3da9
|
added an option -L to %pdra for limiting the number of muxes
|
2017-02-26 15:39:48 -08:00 |
Yen-Sheng Ho
|
a8f6e5c60a
|
added an option -b to %pdra
|
2017-02-25 18:32:43 -08:00 |
Yen-Sheng Ho
|
d5bbf9188c
|
added %pdra -a: run with pdr -nct
|
2017-02-23 08:48:53 -08:00 |
Yen-Sheng Ho
|
2f90e5e15d
|
added an option -m for %pdra
|
2017-02-22 15:37:49 -08:00 |
Yen-Sheng Ho
|
01e6beea8e
|
clean up
|
2017-02-21 20:06:13 -08:00 |
Yen-Sheng Ho
|
9f43c84501
|
added options of checking and pushing to %pdra
|
2017-02-20 12:51:04 -08:00 |
Yen-Sheng Ho
|
19510bd38e
|
added datastructure for %pdra options
|
2017-02-20 11:07:12 -08:00 |
Yen-Sheng Ho
|
6cf289dadd
|
working on pdr with wla
|
2017-02-19 09:55:58 -08:00 |
Yen-Sheng Ho
|
24fdcecb2d
|
started %pdra
|
2017-02-19 09:20:44 -08:00 |
Alan Mishchenko
|
ab387953ab
|
Word-level abstraction engine.
|
2017-02-15 17:16:19 -08:00 |
Alan Mishchenko
|
7a2984bbe9
|
Word-level abstraction.
|
2017-02-09 16:38:08 -08:00 |
Alan Mishchenko
|
32712ec9ab
|
Making sure 'inv_out' can match flops by name.
|
2017-02-09 14:17:19 -08:00 |
Alan Mishchenko
|
e20ef654d9
|
Word-level abstraction.
|
2017-02-09 13:31:07 -08:00 |
Alan Mishchenko
|
c2b805dc85
|
Adding visualization of word-level networks Wlc_Ntk_t.
|
2017-01-26 22:22:22 -08:00 |
Alan Mishchenko
|
64d7119ddc
|
Adding visualization of word-level networks Wlc_Ntk_t.
|
2017-01-26 21:43:28 -08:00 |
Alan Mishchenko
|
7d82819d51
|
Adding visualization of word-level networks Wlc_Ntk_t.
|
2017-01-26 15:17:02 -08:00 |
Alan Mishchenko
|
3119e1e30f
|
Adding features for invariant minimization.
|
2017-01-25 13:56:16 -08:00 |
Alan Mishchenko
|
cf1106aba8
|
Adding features for invariant minimization.
|
2017-01-24 22:28:28 -08:00 |
Alan Mishchenko
|
849f180764
|
Adding features for invariant minimization.
|
2017-01-24 20:44:25 -08:00 |
Alan Mishchenko
|
51f4dab475
|
Adding features for invariant minimization.
|
2017-01-24 20:02:19 -08:00 |
Alan Mishchenko
|
de71ef44cd
|
New command to profile arithmetic logic cones.
|
2016-11-26 17:06:54 -08:00 |
Alan Mishchenko
|
eb65c01888
|
Change Verilog reader to take a string rather than file name.
|
2016-10-06 22:04:11 -07:00 |
Alan Mishchenko
|
640100954a
|
Updates to arithmetic verification.
|
2016-08-05 20:34:44 -07:00 |
Alan Mishchenko
|
2f86667326
|
Adding output range support to %blast.
|
2016-07-18 08:34:05 -07:00 |
Alan Mishchenko
|
3b76bc2792
|
Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift).
|
2016-07-12 13:34:06 -07:00 |
Alan Mishchenko
|
00242f2fb2
|
New profiling features for word-level optimizations.
|
2016-06-04 17:31:15 -07:00 |
Alan Mishchenko
|
0f29f0aec9
|
Improving SMT-LIB parser.
|
2016-05-21 20:08:05 -07:00 |
Alan Mishchenko
|
555ed0b158
|
Enabling AIGs without structural hashing.
|
2016-05-20 13:50:19 -07:00 |
Alan Mishchenko
|
c4446189a9
|
Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network.
|
2016-01-14 20:42:22 -08:00 |
Alan Mishchenko
|
ba5e69952d
|
Corner-case bug in invariant profiling.
|
2015-12-18 12:25:24 -10:00 |
Alan Mishchenko
|
56880eab52
|
New command %psinv.
|
2015-11-23 23:42:20 +07:00 |
Alan Mishchenko
|
6bd77858c5
|
Bug fixing in %blast when blasting MUX coming from always-statement.
|
2015-07-07 22:34:21 -07:00 |
Alan Mishchenko
|
8efc9cb7a9
|
Bug fixing in %blast when blasting mod operator (handling zero divisor).
|
2015-07-07 15:38:54 -07:00 |
Alan Mishchenko
|
4b7dd69260
|
Adding new debugging feature to Wlc_Ntk_t.
|
2015-06-19 22:58:07 -07:00 |
Alan Mishchenko
|
0489deb631
|
Sequential word-level simulator for Wlc_Ntk_t.
|
2015-06-04 22:32:51 -07:00 |
Alan Mishchenko
|
6b0accd22a
|
Modifications to read SMTLIB file from stdin.
|
2015-02-18 20:42:48 -08:00 |
Alan Mishchenko
|
ff1fd41a47
|
Modifications to read SMTLIB file from stdin.
|
2015-02-15 21:57:42 -08:00 |
Alan Mishchenko
|
ea2d82ab14
|
Modifications to read SMTLIB file from stdin.
|
2015-02-11 18:09:15 -08:00 |
Alan Mishchenko
|
55c5c1b58f
|
Added SMT parser for Wlc_Ntk_t.
|
2015-02-07 22:05:02 -08:00 |
Alan Mishchenko
|
345d4e24f3
|
Bug fix in abstracting boxes.
|
2014-11-17 12:55:12 -08:00 |
Alan Mishchenko
|
cc37fb9573
|
Improvements to word-level network package.
|
2014-11-14 20:12:20 -08:00 |
Alan Mishchenko
|
a34183790f
|
Enabling AIGs with boxes for word-level and sequential designs.
|
2014-11-13 18:28:25 -08:00 |
Alan Mishchenko
|
6aa1c94ea5
|
Enabling print-out, for each operator, of the percetage of AND nodes after bit-blasting.
|
2014-09-25 20:33:29 -07:00 |