Alan Mishchenko
|
cfc7fe7d31
|
Added new refinement manager for &gla and &abs_refine.
|
2012-07-14 16:39:11 -07:00 |
Alan Mishchenko
|
86a0ae0bca
|
Removed useless file.
|
2012-07-12 19:07:24 -07:00 |
Alan Mishchenko
|
c265d2449a
|
Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).
|
2012-07-09 15:57:18 -07:00 |
Alan Mishchenko
|
1c33107cbb
|
Updating project settings to have simpler include paths.
|
2012-07-07 20:14:12 -07:00 |
Alan Mishchenko
|
7629fd6aea
|
Added min-cut-based refinement of gate-level abstraction (command &gla_refine).
|
2012-06-24 18:45:42 -07:00 |
Alan Mishchenko
|
b8088b901d
|
Misc changes.
|
2012-04-22 23:33:50 -07:00 |
Alan Mishchenko
|
265e3e5cd4
|
Moving Vec_Set_t to the vector directory.
|
2012-03-28 10:13:42 -07:00 |
Alan Mishchenko
|
b4df114e4a
|
Logic sharing for multi-input gates.
|
2012-03-25 16:49:29 -07:00 |
Alan Mishchenko
|
309bcf2dec
|
Logic sharing for multi-input gates.
|
2012-03-25 01:24:26 -07:00 |
Alan Mishchenko
|
aeedc6ace5
|
Exploration of ISO and minor changes.
|
2012-03-13 16:12:16 -07:00 |
Alan Mishchenko
|
325ac583e6
|
Created a communication bridge.
|
2012-03-01 21:20:18 -08:00 |
Alan Mishchenko
|
e60d6c94a3
|
Experiment with technology mapping.
|
2012-02-20 21:33:51 -08:00 |
Alan Mishchenko
|
16dc02e7f6
|
Improved memory management of proof-logging and propagated changes.
|
2012-02-16 20:54:41 -08:00 |
Alan Mishchenko
|
f1dba69c57
|
Improved memory management of proof-logging and propagated changes.
|
2012-02-16 14:23:52 -08:00 |
Alan Mishchenko
|
ecd14d4daf
|
Isomorphism checking code.
|
2012-02-15 18:40:05 -08:00 |
Alan Mishchenko
|
c5067f7d04
|
Graph isomorphism checking code.
|
2012-02-11 00:22:05 -08:00 |
Alan Mishchenko
|
7ea40494eb
|
Graph isomorphism checking code.
|
2012-01-29 21:22:54 -08:00 |
Alan Mishchenko
|
94d35a2592
|
Variable timeframe abstraction.
|
2012-01-24 01:04:56 -08:00 |
Alan Mishchenko
|
8014f25f6d
|
Major restructuring of the code.
|
2012-01-21 04:30:10 -08:00 |
Alan Mishchenko
|
095345fc4a
|
Added new name manager and modified hierarchy manager to use it.
|
2012-01-13 15:43:09 -08:00 |
Alan Mishchenko
|
cb2d12bb04
|
New hierarchy manager.
|
2012-01-13 00:34:13 -08:00 |
Alan Mishchenko
|
aec5d33889
|
Backward reachability using circuit cofactoring.
|
2012-01-01 15:58:17 +07:00 |
Alan Mishchenko
|
ed13bd16fd
|
New variable-time frame abstraction.
|
2011-12-29 10:13:25 +07:00 |
Alan Mishchenko
|
d0da3a8258
|
Computing interpolants as truth tables.
|
2011-12-22 14:26:47 -08:00 |
Alan Mishchenko
|
bc2f199bd3
|
Started SAT-based reparameterization.
|
2011-12-13 23:38:41 -08:00 |
Alan Mishchenko
|
be874a7abe
|
Added command &read_blif to read hierarchical BLIF directly into the &-space.
|
2011-12-12 18:43:49 -08:00 |
Alan Mishchenko
|
36a80c7579
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 00:38:49 -08:00 |
Alan Mishchenko
|
e84dcb7862
|
g++ portability changes.
|
2011-12-06 16:06:59 -08:00 |
Alan Mishchenko
|
5161978d05
|
Started proof transformations.
|
2011-12-01 01:14:32 -05:00 |
Alan Mishchenko
|
d2db956a61
|
Started experiments with a new solver.
|
2011-11-25 18:08:48 -08:00 |
Alan Mishchenko
|
0736f39609
|
New truth table permutation procedure.
|
2011-10-26 23:15:42 +08:00 |
Alan Mishchenko
|
0f77840520
|
New proof-based abstraction code.
|
2011-10-25 18:32:06 +08:00 |
Alan Mishchenko
|
12b70d4946
|
Changes to CNF generation code.
|
2011-10-17 10:39:05 +03:00 |
Alan Mishchenko
|
c6982485e4
|
New abstraction code.
|
2011-10-14 16:48:45 +03:00 |
Alan Mishchenko
|
519b03e8e8
|
Changes to the matching procedure and new abstraction code.
|
2011-09-27 15:10:53 +07:00 |
Alan Mishchenko
|
23671d65a9
|
Experiments with SPFD-based decomposition.
|
2011-08-17 20:48:56 +07:00 |
Alan Mishchenko
|
81620f2e92
|
Changes to enable CEX minimization.
|
2011-08-01 12:13:49 +07:00 |
Alan Mishchenko
|
b8de7a28e0
|
Changes to enable smarter simulation.
|
2011-07-30 19:56:52 +07:00 |
Alan Mishchenko
|
ce38474c74
|
Improving and updating the abstraction code.
|
2011-07-29 15:38:44 +07:00 |
Alan Mishchenko
|
e7a5a74b4c
|
Adding procedures to find the care bits of a counter-example.
|
2011-07-25 20:35:06 +07:00 |
Alan Mishchenko
|
267f61164a
|
Changes to enable smarter simulation.
|
2011-07-20 18:40:09 +07:00 |
Alan Mishchenko
|
204fac4dca
|
Other changes to enable new features in the mapper.
|
2011-07-10 13:56:05 +07:00 |
Alan Mishchenko
|
ebfd70cdf4
|
Initial changes to enable new features in the mapper
|
2011-07-08 19:40:07 -07:00 |
Alan Mishchenko
|
4669839b24
|
Added new mapping feature.
|
2011-06-20 22:23:32 -07:00 |
Alan Mishchenko
|
31360734b7
|
Added new command 'outdec'.
|
2011-05-19 11:43:11 +07:00 |
Alan Mishchenko
|
3c7842be32
|
Improvements to timeout.
|
2011-05-11 22:14:12 +08:00 |
Alan Mishchenko
|
e4d0f4715a
|
Added new options to testcex.
|
2011-04-28 09:56:14 -04:00 |
Alan Mishchenko
|
affb43e2a3
|
Added switch to control duplication of logic after mapping.
|
2011-04-24 10:43:24 -07:00 |
Alan Mishchenko
|
05b61206e4
|
Adding constant correspondence.
|
2011-04-18 23:27:51 -07:00 |
Alan Mishchenko
|
dd71ca94f1
|
Added cex generation for clustered reachability.
|
2011-04-16 00:08:43 -07:00 |