Alan Mishchenko
|
d1fed2dd89
|
Fixing return value of 'pdr -a'.
|
2013-09-15 11:02:53 -07:00 |
Alan Mishchenko
|
ab5c1692db
|
Handling the case when all outputs are undecided in 'pdr -a' with per-output timeout.
|
2013-09-14 12:23:46 -07:00 |
Alan Mishchenko
|
60fae35d36
|
Fixing several bugs, which led to unsound results produced by 'pdr -a' with per-output timeout.
|
2013-09-13 19:44:54 -07:00 |
Alan Mishchenko
|
a4087e45f0
|
Enabling additional printouts in 'pdr'.
|
2013-09-13 17:36:29 -07:00 |
Alan Mishchenko
|
bc39220df4
|
Performance improvements in 'pdr'.
|
2013-06-18 17:46:37 -07:00 |
Alan Mishchenko
|
91f06107bf
|
Bug fixes in the implementation of varius resource limits in 'pdr'.
|
2013-06-18 12:12:01 -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
|
dfcdffe4be
|
Fixed gap timeout in 'pdr'.
|
2013-05-18 13:22:05 -07:00 |
Alan Mishchenko
|
760c1f60d2
|
Adding new command &mprove for proving groups of properties.
|
2013-05-17 11:50:16 -07:00 |
Alan Mishchenko
|
7c7d527755
|
Changing per-output runtime limit to be in miliseconds.
|
2013-05-09 11:35:04 -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
|
bdae7c625a
|
Adding callback to bmc3, sim3, pdr in the multi-output mode.
|
2013-04-17 20:46:14 -07:00 |
Alan Mishchenko
|
4876f1e21c
|
Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output mode.
|
2013-04-09 16:26:28 -07:00 |
Alan Mishchenko
|
be8125f364
|
Updating 'pdr' to report the number of failed POs.
|
2013-03-30 14:31:09 -07:00 |
Alan Mishchenko
|
e5054fa757
|
Making sure 'pdr -a' return UNDEC if it did not finish proving the remaining outputs to be UNSAT.
|
2013-03-26 16:57:42 -07:00 |
Alan Mishchenko
|
7adc34ad9e
|
Fixing gap timeout in 'pdr'.
|
2013-03-07 21:51:26 -08:00 |
Alan Mishchenko
|
baa944e6a2
|
Added 'gap timeout' to pdr.
|
2013-02-16 14:54:11 -08:00 |
Alan Mishchenko
|
61f8112da0
|
Corner-case bug fix in PDR.
|
2013-02-01 23:56:02 +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
|
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
|
b65ae7349a
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 09:47:48 -08:00 |
Alan Mishchenko
|
daeffe791c
|
Making report about the number of correcty covered frames consistent across the engines.
|
2012-10-09 15:42:25 -07:00 |
Alan Mishchenko
|
3b14c7b490
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:31:29 -07:00 |
Alan Mishchenko
|
3aab724573
|
Fixing time primtouts throughout the code.
|
2012-07-07 17:46:54 -07:00 |
Alan Mishchenko
|
e484231598
|
Fixing time printouts in 'pdr'.
|
2012-07-07 09:16:41 -07:00 |
Alan Mishchenko
|
23467b83b6
|
Setting infinite default conflict limits in 'bmc', 'int', 'pdr'.
|
2012-07-06 18:48:35 -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
|
c47dc99a94
|
Redirecting printf messages.
|
2012-03-02 01:15:40 -08:00 |
Alan Mishchenko
|
97856d021a
|
Silencing some of the gcc warnings.
|
2012-02-16 23:40:23 -08:00 |
Alan Mishchenko
|
faa934e2e6
|
Added restarts to PDR.
|
2012-02-14 00:17:01 -08:00 |
Alan Mishchenko
|
77b5dc261e
|
Added restarts to PDR.
|
2012-02-13 23:31:01 -08:00 |
Alan Mishchenko
|
8014f25f6d
|
Major restructuring of the code.
|
2012-01-21 04:30:10 -08:00 |