Commit Graph

1128 Commits

Author SHA1 Message Date
Alan Mishchenko 743ab55fad Upgraded &equiv3 to periodically restart simulation from the init state. 2012-07-12 18:56:26 -07:00
Alan Mishchenko 97d2c9a264 Added procedure for checking satisfied clauses. 2012-07-12 18:55:24 -07:00
Alan Mishchenko 17305bd563 Fixing temporary linker problem. 2012-07-12 18:54:44 -07:00
Alan Mishchenko 83f1f27307 Silencing warnings. 2012-07-11 15:53:59 -07:00
Alan Mishchenko 719396a2ff Silencing warnings. 2012-07-11 15:52:33 -07:00
Alan Mishchenko da02d5aa9d Handling the trivial case when PO is driven by a constant. 2012-07-11 15:45:55 -07:00
Alan Mishchenko 2427563269 Changes to clause mapping. 2012-07-11 15:33:31 -07:00
Alan Mishchenko 05c8b78531 Changes to clause mapping. 2012-07-11 14:05:07 -07:00
Alan Mishchenko b9ee5d8564 Improvements in the proof-logging SAT solver. 2012-07-11 12:45:46 -07:00
Alan Mishchenko 5f3ba152e5 Fixed several problems when CEX is detected by &vta/&gla. 2012-07-11 09:31:00 -07:00
Alan Mishchenko 8dc61f1f20 Enabling refinement in &gla_refine even if CEX is invalid. 2012-07-11 09:05:20 -07:00
Alan Mishchenko 63dab64574 Replacing printf() by Abc_Print(). 2012-07-10 18:04:08 -07:00
Alan Mishchenko 448eec77b7 Improving print-outs of &vta and &gla. 2012-07-10 13:56:39 -07:00
Alan Mishchenko db6e7f97c1 Improving print-outs of &vta and &gla. 2012-07-10 12:47:47 -07:00
Alan Mishchenko 1d441b6489 Performance bug fix in the SAT solver (clearing variable activity after rollback). 2012-07-10 01:26:23 -07:00
Alan Mishchenko 997e4c77ac Performance bug fix in the SAT solver (clearing variable activity after rollback). 2012-07-09 23:15:12 -07:00
Alan Mishchenko 6ba6c3279a Performance bug fix in the SAT solver (clearing variable activity after rollback). 2012-07-09 23:09:59 -07:00
Alan Mishchenko 908d5e696c Replacing Mb/Gb to be MB/GB. 2012-07-09 22:57:03 -07:00
Alan Mishchenko d46c49088d Bug fix in the recent changes to the SAT solver. 2012-07-09 22:44:38 -07:00
Alan Mishchenko b2f1d21d37 Removing print-out message. 2012-07-09 22:29:24 -07:00
Alan Mishchenko a92c41f767 Removing print-out message in bridge mode. 2012-07-09 22:16:52 -07:00
Alan Mishchenko 291f1ee054 Performance bug fix in &gla. 2012-07-09 22:16:23 -07:00
Alan Mishchenko 637736827a Adding several command-line arguments to 'dsat'. 2012-07-09 19:24:39 -07:00
Alan Mishchenko 22dc498374 Updated Python code to reflect change in include files. 2012-07-09 17:04:10 -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 685faae8e2 Added command &gla_purify. 2012-07-08 17:56:49 -07:00
Alan Mishchenko 21b847a8db Updating truth table computation for GIA to work for internal nodes as well. 2012-07-08 14:04:52 -07:00
Alan Mishchenko ff0ec52d4d Updating memory print-out of &vta and &gla. 2012-07-08 14:01:28 -07:00
Alan Mishchenko d533f18219 Adding printout to report command line executed in batch mode. 2012-07-08 13:23:29 -07:00
Alan Mishchenko 6c3363f777 Adding restart to rarity simulation in sim3 and &sim3. 2012-07-08 13:23:05 -07:00
Alan Mishchenko e80bd69ed6 Adding flushing stdout after printing verbose stats. 2012-07-07 20:41:16 -07:00
Alan Mishchenko fc574a7c61 Adding simple program for executing several instances of ABC in parallel. 2012-07-07 20:37:16 -07:00
Alan Mishchenko 1c33107cbb Updating project settings to have simpler include paths. 2012-07-07 20:14:12 -07:00
Alan Mishchenko b0ef0aaf00 Fixing time primtouts throughout the code. 2012-07-07 18:43:04 -07:00
Alan Mishchenko ea98a2497e Fixing time primtouts throughout the code. 2012-07-07 18:41:02 -07:00
Alan Mishchenko 4760983a46 Fixing time primtouts throughout the code. 2012-07-07 18:15:08 -07:00
Alan Mishchenko 3aab724573 Fixing time primtouts throughout the code. 2012-07-07 17:46:54 -07:00
Alan Mishchenko 16d96fcf53 Changing the default value of &vta -t to reduce proof memory usage. 2012-07-07 14:43:14 -07:00
Alan Mishchenko 504cdad865 Fixing time primtouts in &vta and &gla. 2012-07-07 14:40:02 -07:00
Alan Mishchenko 44f04004fd Adding memory report to print-outs produced by &vta and &gla. 2012-07-07 14:33:54 -07:00
Alan Mishchenko e22f5d1246 Bug fix in &gla_refine. 2012-07-07 13:21:54 -07:00
Alan Mishchenko 5fb7c676c2 Procedure to compute truth tables for POs of GIA. 2012-07-07 13:13:32 -07:00
Alan Mishchenko bea33c0584 Diabling compact AIGER writing by default. 2012-07-07 12:23:03 -07:00
Alan Mishchenko d82142cbe5 Fixed &gla to work in the bridge mode. 2012-07-07 11:16:42 -07:00
Alan Mishchenko 8b881d235a Making 'pdr', &gla, &vta print correctly in batch mode. 2012-07-07 10:44:34 -07:00
Alan Mishchenko 31d85e732b Added warning for GIA reader when input AIG has dangling nodes. 2012-07-07 09:49:08 -07:00
Alan Mishchenko 00eafb2325 Fixing time printouts in 'pdr'. 2012-07-07 09:27:28 -07:00
Alan Mishchenko 968b59aa3b Fixing time printouts in 'pdr'. 2012-07-07 09:22:44 -07:00
Alan Mishchenko e484231598 Fixing time printouts in 'pdr'. 2012-07-07 09:16:41 -07:00
Alan Mishchenko 70331b585b Fixing time printouts in 'pdr'. 2012-07-07 08:43:03 -07:00
Alan Mishchenko f4867f3377 Fixing time printouts in 'pdr'. 2012-07-07 00:20:31 -07:00
Alan Mishchenko 5008b1a4f3 Commands &fla_gla/&gla_fla to convert between flop-level and gate-level abstraction. 2012-07-06 20:41:11 -07:00
Alan Mishchenko e879f0f6d1 Tentatively retiring command &abs_start, &abs_cba, &abs_pba, &gla_cba, &gla_pba. 2012-07-06 18:50:50 -07:00
Alan Mishchenko 23467b83b6 Setting infinite default conflict limits in 'bmc', 'int', 'pdr'. 2012-07-06 18:48:35 -07:00
Alan Mishchenko b2da2c3dc7 Other improvements to &vta and &gla. 2012-07-05 14:44:14 -07:00
Alan Mishchenko 8b0302cdab Changing default conflict limits in bmc2 and bmc3 to be 0 (no limit). 2012-07-05 13:32:52 -07:00
Alan Mishchenko 3c43fbba1a Other improvements to &vta and &gla. 2012-07-05 13:09:41 -07:00
Alan Mishchenko ce6e6551c3 Other improvements to &vta and &gla. 2012-07-04 18:23:33 -07:00
Alan Mishchenko 9ebcd9eca9 Various changes to enable sensitization-based refinement in &gla. 2012-07-04 14:53:07 -07:00
Alan Mishchenko c921058019 Added static fanout to GIA package. 2012-07-04 14:52:16 -07:00
Alan Mishchenko 7fd6534492 Performance improvement in &gla. 2012-07-04 00:11:47 -07:00
Alan Mishchenko 500c76d213 Performance improvement in &gla_refine. 2012-07-03 11:21:58 -07:00
Alan Mishchenko 32217230b0 Performance improvement in &gla_refine. 2012-07-03 11:17:04 -07:00
Alan Mishchenko 3bd0420bd9 Bug fix in Gia_ObjPrint() 2012-07-03 00:05:18 -07:00
Alan Mishchenko 9cb52998f5 Other improvements to &vta and &gla. 2012-07-01 23:16:23 -07:00
Alan Mishchenko bd4b2521e7 Other improvements to bmc2 and bmc3. 2012-07-01 15:27:28 -07:00
Alan Mishchenko 2cc51b4f75 Other improvements to bmc2 and bmc3. 2012-07-01 15:06:28 -07:00
Alan Mishchenko 71f67ef91e Other improvements to bmc2 and bmc3. 2012-07-01 15:04:46 -07:00
Alan Mishchenko 8765502ef8 Other improvements to bmc2 and bmc3. 2012-07-01 14:57:05 -07:00
Alan Mishchenko 5bb7dd6073 Other improvements to bmc2 and bmc3. 2012-07-01 12:43:22 -07:00
Alan Mishchenko d3c8c3da50 Reducing memory usage in bmc2 and bmc3. 2012-07-01 03:02:42 -07:00
Alan Mishchenko 0799766aea Reducing memory usage in bmc2 and bmc3. 2012-07-01 02:53:54 -07:00
Alan Mishchenko 40d4451e2c Reducing memory usage in bmc2 and bmc3. 2012-07-01 02:52:06 -07:00
Alan Mishchenko 34b8604a4d Reducing memory usage in bmc2 and bmc3. 2012-07-01 02:46:21 -07:00
Alan Mishchenko d3c018cd23 Reducing memory usage in bmc2 and bmc3. 2012-07-01 02:19:19 -07:00
Alan Mishchenko a4908534f1 Bug fix in &vta. 2012-06-29 15:17:03 -07:00
Alan Mishchenko 2c9827cb15 Bug fix in &gla. 2012-06-29 13:50:01 -07:00
Alan Mishchenko 7e9ccf7a23 Bug fix in &gla. 2012-06-29 13:15:40 -07:00
Alan Mishchenko 99c4a1be5f Bug fix in &gla_refine. 2012-06-29 13:06:22 -07:00
Alan Mishchenko 2f3a9f91e5 Bug fix when &vta returns empty absraction. 2012-06-29 12:38:36 -07:00
Alan Mishchenko 5d5ff3b99e Bug fix in &gla -d. 2012-06-29 12:19:48 -07:00
Alan Mishchenko a3a1810ab0 Improving printouts in &vta and &gla. 2012-06-28 23:56:45 -07:00
Alan Mishchenko 051cc64ee2 Gate level abstraction (command &gla). 2012-06-28 23:06:07 -07:00
Alan Mishchenko 311486d910 Gate level abstraction (command &gla). 2012-06-28 17:06:02 -07:00
Alan Mishchenko 520c436d28 Gate level abstraction (command &gla). 2012-06-28 16:44:03 -07:00
Alan Mishchenko 27c3ff1f9b New computation of tents for GIA package. 2012-06-28 10:41:15 -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 735a831e13 Added memory reporting to &vta. 2012-06-22 10:30:22 -07:00
Alan Mishchenko 3c0a9e0862 Switch -A <file_name> to specify file name for dumping abstrated model with &vta -d. 2012-06-21 20:20:26 -07:00
Alan Mishchenko 675b0892a8 Reporing memory usage by the SAT solver in 'bmc3'. 2012-06-15 09:51:33 -07:00
Alan Mishchenko 2f1f0ac93d Minor change to prevent assertion failure when verifying required times. 2012-06-15 08:45:12 -07:00
Alan Mishchenko 082d27ede8 Added option to compile on windows without DLL support. 2012-06-15 08:39:46 -07:00
Alan Mishchenko 98d9d5a61f Added warning when a command is missing 2012-06-15 08:37:56 -07:00
Alan Mishchenko 034fc5a14d Misc changes. 2012-05-21 23:52:05 +07:00
Alan Mishchenko 77b83074e0 Changing 'if' to allow for delay optimization on sequential paths only. 2012-05-20 22:18:23 +07:00
Alan Mishchenko c6af9094c0 Changing 'if' to allow for delay optimization on sequential paths only. 2012-05-20 17:27:53 +07:00
Alan Mishchenko 38214f01c2 Do not allow quitting bmc3 after exploring 2^<num_ff> frames if jump-forward is enabled. 2012-05-20 16:41:01 +07:00
Alan Mishchenko 6ecc71f8f9 Misc changes. 2012-05-19 16:37:32 +07:00
Alan Mishchenko 37a3e07d91 Prevent network from being unmapped after equivalence checking. 2012-05-15 15:36:51 +07:00
Alan Mishchenko 54670783e0 Better resolution of CO drivers. Should impact the QoR after 'if'. 2012-05-15 15:28:42 +07:00