Alan Mishchenko
|
3b14c7b490
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:31:29 -07:00 |
Alan Mishchenko
|
19c28cae94
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 10:27:48 -07:00 |
Alan Mishchenko
|
9b15f71f2f
|
Added new command 'upsize'.
|
2012-09-12 14:39:50 -07:00 |
Alan Mishchenko
|
e3d75484ce
|
Reversed to a buggy version of reduceDB in complete proof-logging, because it works with rollback and it is not used in &gla -pn -L 0.
|
2012-09-12 12:46:56 -07:00 |
Alan Mishchenko
|
606341dca6
|
Added code to collect experimental results.
|
2012-09-11 22:36:38 -07:00 |
Alan Mishchenko
|
e95844c0af
|
Added code to collect experimental results.
|
2012-09-11 22:35:27 -07:00 |
Alan Mishchenko
|
087ec9eb1f
|
Added code to collect experimental results.
|
2012-09-11 22:34:49 -07:00 |
Alan Mishchenko
|
825bcd823c
|
Added code to collect experimental results.
|
2012-09-11 22:33:47 -07:00 |
Alan Mishchenko
|
4c06c8afc0
|
Improved topo print-out.
|
2012-09-11 19:40:12 -07:00 |
Alan Mishchenko
|
a246882a5b
|
Scalable gate-level abstraction.
|
2012-09-11 19:11:51 -07:00 |
Niklas Een
|
1c865bf229
|
Added -C to command line for running commands, then staying in interactive mode
|
2012-09-11 18:48:43 -07:00 |
Alan Mishchenko
|
784a3579e5
|
Fixing Verilog writer's way of writing module names.
|
2012-09-11 18:44:07 -07:00 |
Alan Mishchenko
|
759b7c0855
|
Added code to collect experimental results.
|
2012-09-11 16:26:01 -07:00 |
Alan Mishchenko
|
d257fce824
|
Added code to collect experimental results.
|
2012-09-11 16:25:00 -07:00 |
Alan Mishchenko
|
20bd241e20
|
Commenting out some assertions in the 'map' mapper.
|
2012-09-10 00:23:41 -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
|
71d7c9e66d
|
Disable printing refinement statistics by default.
|
2012-09-09 20:25:55 -07:00 |
Alan Mishchenko
|
56117d56e8
|
Added switch '-p' to '&gla -n' to use full proof for UNSAT core computation (for experiments).
|
2012-09-09 15:28:31 -07:00 |
Alan Mishchenko
|
4333fd24d2
|
Started CEX minimization procedure.
|
2012-09-08 18:28:13 -07:00 |
Alan Mishchenko
|
9efe9579f9
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 15:04:44 -07:00 |
Alan Mishchenko
|
519b9fdf7c
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 15:04:00 -07:00 |
Alan Mishchenko
|
002117c0e9
|
Started CEX minimization procedure.
|
2012-09-08 14:56:25 -07:00 |
Alan Mishchenko
|
cc6da1f905
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 00:19:46 -07:00 |
Alan Mishchenko
|
e1b76633dc
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 00:14:49 -07:00 |
Alan Mishchenko
|
5ca4f3cf9f
|
Updating &gla_refine to perform suffic refinement.
|
2012-09-07 23:26:23 -07:00 |
Alan Mishchenko
|
548e04192b
|
Updating &gla_refine to perform suffic refinement.
|
2012-09-07 20:44:12 -07:00 |
Alan Mishchenko
|
0b8e07bdde
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-07 13:36:39 -07:00 |
Alan Mishchenko
|
6c1d4ee8dd
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-07 13:33:52 -07:00 |
Alan Mishchenko
|
509194a898
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-07 13:02:46 -07:00 |
Alan Mishchenko
|
75a5c46b99
|
Added switch 'dch -r' to skip choices with structural support redundancy.
|
2012-09-07 00:18:54 -07:00 |
Alan Mishchenko
|
ce0e96bcaa
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 23:15:08 -07:00 |
Alan Mishchenko
|
5b3e31bd4d
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 23:11:34 -07:00 |
Alan Mishchenko
|
894fc81041
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:44:56 -07:00 |
Alan Mishchenko
|
4efd8bf7b3
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:33:43 -07:00 |
Alan Mishchenko
|
bf69a345c9
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:10:03 -07:00 |
Alan Mishchenko
|
794bd2fd33
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 21:01:48 -07:00 |
Alan Mishchenko
|
aff7f38495
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 20:58:14 -07:00 |
Alan Mishchenko
|
1cefca7dea
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 20:54:00 -07:00 |
Alan Mishchenko
|
58d50bf94a
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 20:51:16 -07:00 |
Alan Mishchenko
|
460f1905e2
|
Debugging 64-bit bug in new semi-canonical form..
|
2012-09-06 16:30:00 -07:00 |
Alan Mishchenko
|
5a5577f907
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:55:54 -07:00 |
Alan Mishchenko
|
39fe23f079
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:52:54 -07:00 |
Alan Mishchenko
|
7a6cf9f48c
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:40:47 -07:00 |
Alan Mishchenko
|
9c8be56ccd
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:32:07 -07:00 |
Alan Mishchenko
|
4393a5fade
|
Added platform-independent random-number generator to 'fraig'.
|
2012-09-05 19:50:32 -07:00 |
Alan Mishchenko
|
cd2bd70865
|
Added switch 'dch -r' to skip choices with structural support redundancy.
|
2012-09-05 19:39:25 -07:00 |
Alan Mishchenko
|
c1f4545e07
|
Added error message when the user is trying 'dsat' for multi-output comb miters.
|
2012-09-05 18:53:21 -07:00 |
Alan Mishchenko
|
9cb16d654a
|
Added new command &gla_shrink.
|
2012-09-05 00:55:33 -07:00 |
Alan Mishchenko
|
f6b67d7846
|
Added new command &gla_shrink.
|
2012-09-04 23:57:58 -07:00 |
Alan Mishchenko
|
2071d9a732
|
Enabling additinal printouts.
|
2012-09-04 21:14:47 -07:00 |