Alan Mishchenko
|
6863688789
|
Enabled detecting CEXes in multiple POs without stopping (sim3 -a).
|
2013-01-23 12:37:44 +07:00 |
|
Alan Mishchenko
|
70655d5d31
|
Integration of timing manager.
|
2013-01-23 01:34:34 +07:00 |
|
Alan Mishchenko
|
ab2dfec272
|
Improvements to LMS code.
|
2012-10-27 17:38:45 -07:00 |
|
Alan Mishchenko
|
94d722c58e
|
Improvements to LMS code.
|
2012-10-27 17:33:13 -07:00 |
|
Alan Mishchenko
|
dd25b90f8e
|
Improvements to gate sizing.
|
2012-10-09 01:20:51 -07:00 |
|
Alan Mishchenko
|
9206e6ff80
|
Improvements to gate sizing.
|
2012-10-08 21:20:13 -07:00 |
|
Alan Mishchenko
|
8b4e762e5a
|
Minor bug fix.
|
2012-10-04 12:05:57 -07:00 |
|
Alan Mishchenko
|
63c9540543
|
Minor bug fixes.
|
2012-10-03 20:38:03 -07:00 |
|
Alan Mishchenko
|
f7caf84f21
|
Modified structural constraint extraction (unfold -s) to work for multi-output testcases.
|
2012-09-23 14:30:17 -07:00 |
|
Alan Mishchenko
|
fdd043ca34
|
Upgrading hierarchy timing manager.
|
2012-09-21 22:00:39 -07:00 |
|
Alan Mishchenko
|
e0eb270324
|
Changes to command 'upsize'.
|
2012-09-18 13:23:58 -07:00 |
|
Alan Mishchenko
|
790ea6545f
|
Moving binary IO streams to the vector package.
|
2012-09-17 01:01:47 -07:00 |
|
Alan Mishchenko
|
7772a4af05
|
Added printout of library cells.
|
2012-08-27 19:58:15 -07:00 |
|
Alan Mishchenko
|
13bd7b334c
|
New package to read/write a subset of Liberty for STA.
|
2012-08-24 21:31:46 -07:00 |
|
Alan Mishchenko
|
5b80d704a1
|
Improved abstraction refinement.
|
2012-08-09 17:53:38 -07:00 |
|
Alan Mishchenko
|
cd39fd6b05
|
Fixing performance bug with old proof-logging (adding clauses multiple times).
|
2012-07-30 11:05:54 -07:00 |
|
Alan Mishchenko
|
8982bf58cb
|
Reducing memory usage in proof-based abstraction.
|
2012-07-29 22:31:00 -07:00 |
|
Alan Mishchenko
|
8a2d237f78
|
Adding memory reporting to vectors.
|
2012-07-29 12:34:32 -07:00 |
|
Alan Mishchenko
|
6df122bda6
|
Updated code for lazy man's synthesis (memory optimization).
|
2012-07-20 18:56:26 -07:00 |
|
Alan Mishchenko
|
6c9b59bfc0
|
Updated code for lazy man's synthesis.
|
2012-07-20 15:54:08 -07:00 |
|
Alan Mishchenko
|
bbf4b9a58d
|
Debugging a proof error.
|
2012-07-13 18:47:04 -07:00 |
|
Alan Mishchenko
|
4ebda996d7
|
Debugging a proof error.
|
2012-07-13 18:22:10 -07:00 |
|
Alan Mishchenko
|
c50d108f98
|
Debugging a proof error.
|
2012-07-13 18:15:32 -07:00 |
|
Alan Mishchenko
|
c25f488a83
|
Debugging a proof error.
|
2012-07-13 17:53:08 -07:00 |
|
Alan Mishchenko
|
3fb103dadc
|
Debugging a proof error.
|
2012-07-13 16:31:12 -07:00 |
|
Alan Mishchenko
|
da525b2a23
|
Debugging a proof error.
|
2012-07-13 16:25:07 -07:00 |
|
Alan Mishchenko
|
b7b60ebdcb
|
Fixing a mismatch in regular/shadow page memory appending procedure.
|
2012-07-13 16:10:20 -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
|
735a831e13
|
Added memory reporting to &vta.
|
2012-06-22 10:30:22 -07:00 |
|
Alan Mishchenko
|
675b0892a8
|
Reporing memory usage by the SAT solver in 'bmc3'.
|
2012-06-15 09:51:33 -07:00 |
|
Alan Mishchenko
|
d4399dbf92
|
Misc changes.
|
2012-05-03 19:54:40 +08:00 |
|
Alan Mishchenko
|
73789120c1
|
Misc changes.
|
2012-04-20 10:12:29 -07:00 |
|
Alan Mishchenko
|
993c2027d8
|
Added several new APIs.
|
2012-03-31 16:33:22 -07:00 |
|
Alan Mishchenko
|
38494b41a6
|
Moving Vec_Set_t to the vector directory.
|
2012-03-28 10:19:12 -07:00 |
|
Alan Mishchenko
|
265e3e5cd4
|
Moving Vec_Set_t to the vector directory.
|
2012-03-28 10:13:42 -07:00 |
|
Alan Mishchenko
|
309bcf2dec
|
Logic sharing for multi-input gates.
|
2012-03-25 01:24:26 -07:00 |
|
Alan Mishchenko
|
92539a91a0
|
Added one currently unused iterator.
|
2012-03-21 15:27:47 -07:00 |
|
Alan Mishchenko
|
3f525b0d42
|
Silenced a gcc warning.
|
2012-02-24 16:18:38 -08:00 |
|
Alan Mishchenko
|
97a2e6f29e
|
Isomorphism checking code.
|
2012-02-17 19:04:28 -08:00 |
|
Alan Mishchenko
|
ee9f66e2c4
|
Isomorphism checking code.
|
2012-02-17 13:19:09 -08:00 |
|
Alan Mishchenko
|
a9980135a0
|
Isomorphism checking code.
|
2012-02-14 22:15:49 -08:00 |
|
Alan Mishchenko
|
c5067f7d04
|
Graph isomorphism checking code.
|
2012-02-11 00:22:05 -08:00 |
|
Alan Mishchenko
|
044149593d
|
Graph isomorphism checking code.
|
2012-01-30 23:11:38 -08:00 |
|
Alan Mishchenko
|
e511b87237
|
Moving Vec_IntPrint to where it belongs.
|
2012-01-29 21:22:26 -08:00 |
|
Alan Mishchenko
|
8014f25f6d
|
Major restructuring of the code.
|
2012-01-21 04:30:10 -08:00 |
|
Alan Mishchenko
|
10478a9cbf
|
Variable timeframe abstraction.
|
2012-01-15 20:47:58 -08:00 |
|
Alan Mishchenko
|
1aeaacc03d
|
Added bit vector.
|
2012-01-13 19:31:58 -08:00 |
|
Alan Mishchenko
|
5161978d05
|
Started proof transformations.
|
2011-12-01 01:14:32 -05:00 |
|
Alan Mishchenko
|
1dcdba1bee
|
New proof-based abstraction code (bug fix).
|
2011-10-27 10:10:10 -07:00 |
|