Alan Mishchenko
|
7b1c25086b
|
Improvements and tuning of CBA.
|
2015-02-01 20:50:59 -08:00 |
Alan Mishchenko
|
14425c111e
|
Organizing commands for barbuf-aware flow.
|
2015-01-20 21:20:31 -08:00 |
Alan Mishchenko
|
ac7633c5a4
|
Integrating barrier buffers.
|
2014-12-11 11:14:04 -08:00 |
Alan Mishchenko
|
4f940de518
|
Converting AIG with MUXes into a logic network.
|
2014-12-10 22:52:34 -08:00 |
Alan Mishchenko
|
1398de7c46
|
Integrating barrier buffers.
|
2014-12-08 14:10:41 -08:00 |
Alan Mishchenko
|
b4cf2f7448
|
Added switches '-c' and '-n' to 'init'.
|
2014-11-02 17:35:47 -08:00 |
Alan Mishchenko
|
7fb1954268
|
Small changes.
|
2014-07-29 22:49:10 -07:00 |
Alan Mishchenko
|
6a69a9139c
|
Adding support for standard-cell mapping.
|
2014-07-28 11:31:31 -07:00 |
Alan Mishchenko
|
44d9c7e543
|
Improvements to CNF generation.
|
2014-06-23 13:11:59 -07:00 |
Jiang Long
|
574af21208
|
merge unfold2
|
2014-06-04 21:59:03 -07:00 |
Alan Mishchenko
|
4bafc98aba
|
Pass file name correctly.
|
2014-04-10 15:44:26 -07:00 |
Alan Mishchenko
|
473c584563
|
Mismatch in bmc3 printout.
|
2014-03-30 14:21:23 -07:00 |
Alan Mishchenko
|
a1cdcb0b43
|
Updating code to support barrier buffers.
|
2014-03-18 17:50:53 -07:00 |
Alan Mishchenko
|
12c8a54cff
|
Adding barrier buffers.
|
2014-03-16 22:12:17 -07:00 |
Alan Mishchenko
|
3b30fb2a11
|
Multi-output property solver.
|
2013-10-26 23:05:13 -07:00 |
Alan Mishchenko
|
47afd0f4f4
|
Multi-output property solver.
|
2013-10-23 16:26:13 -07:00 |
Alan Mishchenko
|
e2f11e14d0
|
Adding switch &get -m to import mapped network into the &-space.
|
2013-09-01 19:34:32 -07:00 |
Alan Mishchenko
|
8c7ca72ea9
|
Adding timeout to command 'ind'.
|
2013-06-28 12:21:48 -07:00 |
Alan Mishchenko
|
a66dc0afb6
|
Unifying representation of mapping in GIA.
|
2013-06-25 23:05:51 -07:00 |
Alan Mishchenko
|
19c25fd6aa
|
Adding a wrapper around clock() for more accurate time counting in ABC.
|
2013-05-27 15:09:23 -07:00 |
Alan Mishchenko
|
50095be5ac
|
Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).
|
2013-05-03 19:58:25 -07:00 |
Alan Mishchenko
|
7808ee8e70
|
Adding parameter structure for rarity simulation.
|
2013-04-17 19:40:02 -07:00 |
Alan Mishchenko
|
48fce79453
|
Updating 'sim3' to move the design into the last rare state.
|
2013-04-01 18:39:42 -07:00 |
Alan Mishchenko
|
7a2132b237
|
Added dumping QDIMACS files in command 'qbf'.
|
2013-03-27 17:21:08 -07:00 |
Alan Mishchenko
|
91ca83e864
|
Adding new features to 'dualrail'.
|
2013-02-21 22:51:25 -08:00 |
Alan Mishchenko
|
dfe5f511b2
|
Adding new features to 'dualrail'.
|
2013-02-21 22:46:53 -08:00 |
Alan Mishchenko
|
fd0ff0171e
|
Added 'gap timeout' to bmc3 and sim3.
|
2013-02-15 16:47:18 -08:00 |
Alan Mishchenko
|
6863688789
|
Enabled detecting CEXes in multiple POs without stopping (sim3 -a).
|
2013-01-23 12:37:44 +07:00 |
Alan Mishchenko
|
ac1207abea
|
Enabled detecting CEXes in multiple POs without stopping (sim3 -a).
|
2013-01-23 02:07:50 +07:00 |
Alan Mishchenko
|
a8dad4ed61
|
Fixing C++ compilation issues.
|
2013-01-08 13:12:28 +08:00 |
Alan Mishchenko
|
8355eb1d41
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 17:52:34 -08:00 |
Alan Mishchenko
|
ce63869fe7
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 17:33:44 -08:00 |
Alan Mishchenko
|
9fc1cd0b3f
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 15:12:40 -08:00 |
Alan Mishchenko
|
58d4012a55
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 14:46:16 -08:00 |
Alan Mishchenko
|
9f396a0d7e
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 10:11:52 -08:00 |
Alan Mishchenko
|
b65ae7349a
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 09:47:48 -08:00 |
Alan Mishchenko
|
be7a4e4259
|
Isolating BMC code into a separate package.
|
2012-11-14 13:55:24 -08:00 |
Alan Mishchenko
|
fdcbb2cf37
|
Performance bug fix in choice generation.
|
2012-11-09 12:43:03 -08:00 |
Alan Mishchenko
|
6b96d9a84e
|
Integrating GIA with LUT mapping.
|
2012-10-24 17:39:38 -07:00 |
Alan Mishchenko
|
3af0f719af
|
Extending BLIF parser/write to hangle multi-output cells.
|
2012-09-19 16:28:06 -07:00 |
Alan Mishchenko
|
117bc0dbcd
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:20:37 -07:00 |
Alan Mishchenko
|
3b14c7b490
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:31:29 -07:00 |
Alan Mishchenko
|
d40af538e2
|
Unified print-out of property failures produced by all engines.
|
2012-09-09 20:46:34 -07:00 |
Alan Mishchenko
|
f6b67d7846
|
Added new command &gla_shrink.
|
2012-09-04 23:57:58 -07:00 |
Alan Mishchenko
|
942600414d
|
Added simulation of comb circuits with user-specified patterns in command 'sim'.
|
2012-08-24 11:12:51 -07:00 |
Alan Mishchenko
|
94193472c8
|
Fixing assertion mismatch in bmc2.
|
2012-07-14 09:25:18 -07:00 |
Alan Mishchenko
|
b9ee5d8564
|
Improvements in the proof-logging SAT solver.
|
2012-07-11 12:45:46 -07:00 |
Alan Mishchenko
|
637736827a
|
Adding several command-line arguments to 'dsat'.
|
2012-07-09 19:24:39 -07:00 |
Alan Mishchenko
|
ff0ec52d4d
|
Updating memory print-out of &vta and &gla.
|
2012-07-08 14:01:28 -07:00 |
Alan Mishchenko
|
6c3363f777
|
Adding restart to rarity simulation in sim3 and &sim3.
|
2012-07-08 13:23:05 -07:00 |