Alan Mishchenko
|
9cbd97b5ef
|
Improving printouts in &gla.
|
2012-09-16 16:50:18 -07:00 |
Alan Mishchenko
|
c15137bd3f
|
Improving printouts in &gla.
|
2012-09-16 16:48:50 -07:00 |
Alan Mishchenko
|
ee436f9377
|
Changed a few things in the refinement package of &gla.
|
2012-09-16 13:56:10 -07:00 |
Alan Mishchenko
|
33cd4dea67
|
Forgot to add one file into Windows project.
|
2012-09-16 11:21:45 -07:00 |
Alan Mishchenko
|
5953beb2da
|
Restructured the code to post-process object used during refinement in &gla.
|
2012-09-16 09:54:19 -07:00 |
Alan Mishchenko
|
5a4f1fe44c
|
Made abstraction and PDR communicate in-memory rather than through a file.
|
2012-09-16 00:26:18 -07:00 |
Alan Mishchenko
|
fdf5ad3433
|
Cleaned 'abc.c' by removing useless procedures.
|
2012-09-15 23:52:36 -07:00 |
Alan Mishchenko
|
69bbfa9856
|
Created new abstraction package from the code that was all over the place.
|
2012-09-15 23:27:46 -07:00 |
Alan Mishchenko
|
ec95f569dd
|
Corrected &gla -a to work as expected.
|
2012-09-15 21:18:32 -07:00 |
Alan Mishchenko
|
152aaedcb2
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 22:45:51 -07:00 |
Alan Mishchenko
|
080c325500
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:22:31 -07:00 |
Alan Mishchenko
|
117bc0dbcd
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:20:37 -07:00 |
Alan Mishchenko
|
f64bb36fd5
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:33:23 -07:00 |
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 |