luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
2,222 Commits 27 Branches 57 Tags 58 MiB
Commit Graph

332 Commits

Author SHA1 Message Date
Alan Mishchenko ed564664f1 Disabling learned clause removal when incremental proof-logging is running (tends to generate smaller abstarctions). 2012-07-30 11:31:26 -07:00
Alan Mishchenko cd39fd6b05 Fixing performance bug with old proof-logging (adding clauses multiple times). 2012-07-30 11:05:54 -07:00
Alan Mishchenko 216fc33a47 Fixed compiler warnings. 2012-07-29 22:36:21 -07:00
Alan Mishchenko 8982bf58cb Reducing memory usage in proof-based abstraction. 2012-07-29 22:31:00 -07:00
Alan Mishchenko 1b18583840 Fixed the problem with 'write_cnf' after recent changes to the SAT solver. 2012-07-28 14:55:55 -07:00
Alan Mishchenko 18737f7408 Fixed the problem with 'write_cnf' after recent changes to the SAT solver. 2012-07-28 11:03:56 -07:00
Alan Mishchenko a40c13a93c Recording and reusing learned util clauses in bmc2. 2012-07-22 22:28:24 -07:00
Alan Mishchenko 2379dea445 Recording and reusing learned util clauses in bmc3. 2012-07-22 16:52:24 -07:00
Alan Mishchenko 3c4351aee4 Debugging a proof error. 2012-07-13 19:06:32 -07:00
Alan Mishchenko 8c162f0577 Debugging a proof error. 2012-07-13 18:56:15 -07:00
Alan Mishchenko 08bb2e70b7 Debugging a proof error. 2012-07-13 18:51:24 -07:00
Alan Mishchenko bbf4b9a58d Debugging a proof error. 2012-07-13 18:47:04 -07:00
Alan Mishchenko 5ec4db2d44 Debugging a proof error. 2012-07-13 18:11:02 -07:00
Alan Mishchenko 7913c1d84f Debugging a proof error. 2012-07-13 17:58:56 -07:00
Alan Mishchenko 6578d9cd00 Debugging a proof error. 2012-07-13 17:46:30 -07:00
Alan Mishchenko 4051572726 Debugging a proof error. 2012-07-13 17:39:52 -07:00
Alan Mishchenko 0f82d82ba0 Debugging a proof error. 2012-07-13 17:36:31 -07:00
Alan Mishchenko f37d0544de Debugging a proof error. 2012-07-13 17:23:30 -07:00
Alan Mishchenko 47b5ad1dfb Debugging a proof error. 2012-07-13 17:17:12 -07:00
Alan Mishchenko 7b367f5ecb Debugging a proof error. 2012-07-13 17:06:22 -07:00
Alan Mishchenko be95437d1a Debugging a proof error. 2012-07-13 15:44:45 -07:00
Alan Mishchenko f54bf25d70 Debugging a proof error. 2012-07-13 15:12:21 -07:00
Alan Mishchenko d3ad7fbaf3 Several small changes and fixes. 2012-07-13 15:02:46 -07:00
Alan Mishchenko 86a0ae0bca Removed useless file. 2012-07-12 19:07:24 -07:00
Alan Mishchenko 97d2c9a264 Added procedure for checking satisfied clauses. 2012-07-12 18:55:24 -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 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 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 637736827a Adding several command-line arguments to 'dsat'. 2012-07-09 19:24:39 -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 ff0ec52d4d Updating memory print-out of &vta and &gla. 2012-07-08 14:01:28 -07:00
Alan Mishchenko 1c33107cbb Updating project settings to have simpler include paths. 2012-07-07 20:14:12 -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 9ebcd9eca9 Various changes to enable sensitization-based refinement in &gla. 2012-07-04 14:53:07 -07:00
Alan Mishchenko 7fd6534492 Performance improvement in &gla. 2012-07-04 00:11:47 -07:00
Alan Mishchenko 735a831e13 Added memory reporting to &vta. 2012-06-22 10:30:22 -07:00
Alan Mishchenko 675b0892a8 Reporing memory usage by the SAT solver in 'bmc3'. 2012-06-15 09:51:33 -07:00
Alan Mishchenko 265e3e5cd4 Moving Vec_Set_t to the vector directory. 2012-03-28 10:13:42 -07:00
Alan Mishchenko f50ce3dbd9 Switching to a variable-page-size memory manager for clauses and proofs. 2012-03-21 17:13:39 -07:00
Alan Mishchenko 0dc699f777 Preventing gcc compilation errors in handling memory pages. 2012-03-21 15:26:09 -07:00
Alan Mishchenko c46c957a07 Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)... 2012-03-09 19:50:18 -08:00
Alan Mishchenko 2c8f1a67ec Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ...Ci/Co. 2012-03-09 19:32:44 -08:00
Alan Mishchenko 5ad0fea606 Extending memory page size for proof logging. 2012-03-05 09:01:50 +01:00
Niklas Een 12d9aaa7b4 Some fixes for VTA under Bridge. 2012-03-03 11:03:59 -08:00
Alan Mishchenko 596bbbe6dc Added QuickSort based on 3-way partitioning. 2012-02-19 13:16:51 -08:00
Alan Mishchenko fe2d7d9612 Silencing some of the gcc warnings. 2012-02-17 00:24:38 -08:00
Alan Mishchenko 2d316b86e2 Silencing some of the gcc warnings. 2012-02-17 00:06:39 -08:00
Alan Mishchenko 97856d021a Silencing some of the gcc warnings. 2012-02-16 23:40:23 -08:00
Alan Mishchenko 791b107e7a Silencing some of the gcc warnings. 2012-02-16 21:53:16 -08:00
Alan Mishchenko 16dc02e7f6 Improved memory management of proof-logging and propagated changes. 2012-02-16 20:54:41 -08:00
Alan Mishchenko f1dba69c57 Improved memory management of proof-logging and propagated changes. 2012-02-16 14:23:52 -08:00
Alan Mishchenko 59ea100dbf Variable timeframe abstraction. 2012-02-13 20:40:38 -08:00
Alan Mishchenko d931de7feb Variable timeframe abstraction. 2012-02-13 20:03:55 -08:00
Alan Mishchenko 6f4bb33ce1 Variable timeframe abstraction. 2012-02-13 14:35:00 -08:00
Alan Mishchenko f80841a5fd Variable timeframe abstraction. 2012-02-13 14:17:01 -08:00
Alan Mishchenko d9edb7e549 Variable timeframe abstraction. 2012-02-12 02:16:36 -08:00
Alan Mishchenko 309ab1c12b Variable timeframe abstraction. 2012-02-11 20:48:23 -08:00
Alan Mishchenko a2df331852 Variable timeframe abstraction. 2012-01-28 13:48:48 -08:00
Alan Mishchenko ce0e8caf79 Variable timeframe abstraction. 2012-01-27 00:48:06 -08:00
Alan Mishchenko c7e855619a Variable timeframe abstraction. 2012-01-24 14:39:49 -08:00
Alan Mishchenko 94d35a2592 Variable timeframe abstraction. 2012-01-24 01:04:56 -08:00
Alan Mishchenko fb918249ca Variable timeframe abstraction. 2012-01-21 22:57:18 -08:00
Alan Mishchenko 8014f25f6d Major restructuring of the code. 2012-01-21 04:30:10 -08:00
Alan Mishchenko 719b06f912 Variable timeframe abstraction. 2012-01-20 17:55:34 -08:00
Alan Mishchenko 37b8a190ba Improving printout in the SAT solver. 2012-01-13 20:57:26 -08:00
Alan Mishchenko 56cc5734a4 Bug fix related to not properly resizing SAT solver's model array. 2012-01-12 07:28:01 -08:00
Alan Mishchenko 10ad89490a Bug fix related to not properly resizing SAT solver's model array. 2012-01-06 11:34:06 +07:00
Alan Mishchenko 5a45a75dca APIs to represent simple gates in CNF. 2012-01-05 19:19:13 +07:00
Alan Mishchenko 32e7b75829 APIs to represent simple gates in CNF. 2012-01-05 13:15:05 +07:00
Alan Mishchenko c59e2e9c96 Transforming the solver to use different clause representation. 2011-12-23 21:45:23 -08:00
Alan Mishchenko 7facbc3cc9 Transforming the solver to use different clause representation. 2011-12-23 10:23:45 -08:00
Alan Mishchenko 94174d0f04 Transforming the solver to use different clause representation. 2011-12-23 00:43:31 -08:00
Alan Mishchenko 9d2893040e Transforming the solver to use different clause representation. 2011-12-23 00:29:26 -08:00
Alan Mishchenko 844c385e2b Transforming the solver to use different clause representation. 2011-12-22 15:38:06 -08:00
Alan Mishchenko d0da3a8258 Computing interpolants as truth tables. 2011-12-22 14:26:47 -08:00
Alan Mishchenko 8404ecda54 Undoing temporary change to the solver. 2011-12-15 17:05:38 -08:00
Alan Mishchenko 4d000265f6 Temporary change to the solver. 2011-12-15 16:47:28 -08:00
Alan Mishchenko bc2f199bd3 Started SAT-based reparameterization. 2011-12-13 23:38:41 -08:00
Alan Mishchenko c2a1a9ef37 Implementing rollback in the updated solver. 2011-12-10 14:55:33 -08:00
Alan Mishchenko a2228ee09b Implementing rollback in the updated solver. 2011-12-10 14:45:35 -08:00
Alan Mishchenko 871171ffa4 Implemented rollback in the main SAT solver and updated PDR to use it (saves about 5% of runtime). 2011-12-10 14:06:01 -08:00
Alan Mishchenko 6c766b4f1a Implementing rollback in the updated solver. 2011-12-10 13:11:28 -08:00
Alan Mishchenko dea5708d4e Removing unused files. 2011-12-10 11:30:29 -08:00
Alan Mishchenko f67c0c173d Changes to the main SAT solver: fixing performance bug (resetting decay params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity). 2011-12-09 23:49:30 -08:00
Alan Mishchenko 07405ca1c5 Integrated new proof-logging into proof-based gate-level abstraction. 2011-12-08 22:42:50 -08:00
Alan Mishchenko b5c3992b6b Proof-logging in the updated solver. 2011-12-08 19:43:08 -08:00
Alan Mishchenko c985e17d1f Proof-logging in the updated solver. 2011-12-08 15:06:26 -08:00
Alan Mishchenko d1fa7f7a61 Proof-logging in the updated solver. 2011-12-07 22:26:50 -08:00
Alan Mishchenko 565fefec7a Proof-logging in the updated solver. 2011-12-06 21:11:18 -08:00
Alan Mishchenko e84dcb7862 g++ portability changes. 2011-12-06 16:06:59 -08:00
Alan Mishchenko b743298cd5 Proof-logging in the updated solver. 2011-12-05 20:02:46 -08:00
Alan Mishchenko 72404d1fdf Proof-logging in the updated solver. 2011-12-05 18:00:49 -08:00
Alan Mishchenko bb96fa361c Proof-logging in the updated solver. 2011-12-05 11:53:57 -08:00
Alan Mishchenko 7a19593d3f Proof-logging in the updated solver. 2011-12-04 23:30:09 -08:00
Alan Mishchenko f0d44a4a93 Proof-logging in the updated solver. 2011-12-04 22:58:24 -08:00
Alan Mishchenko 09d3e1ff77 Proof-logging in the updated solver. 2011-12-04 16:10:11 -08:00
Alan Mishchenko a7031bb3f7 Removing redundant function declarations. 2011-12-02 10:11:39 -05:00
Alan Mishchenko 5161978d05 Started proof transformations. 2011-12-01 01:14:32 -05:00
Alan Mishchenko 1c16c45679 Started experiments with a new solver. 2011-11-27 16:28:57 -08:00
Alan Mishchenko fc4ab6bd39 Started experiments with a new solver. 2011-11-26 18:17:39 -08:00
Alan Mishchenko 0cfc97b940 Started experiments with a new solver. 2011-11-26 11:54:01 -08:00
Alan Mishchenko 8ac9515d36 Started experiments with a new solver. 2011-11-26 11:37:27 -08:00
Alan Mishchenko 06416a981f Started experiments with a new solver. 2011-11-26 11:33:37 -08:00
Alan Mishchenko d2db956a61 Started experiments with a new solver. 2011-11-25 18:08:48 -08:00
Alan Mishchenko 0f594b78fa Commented out the default call to UNSAT core verification. 2011-11-25 18:07:41 -08:00
Alan Mishchenko 9726d5a85e Improvement to the SAT solver (skipping binary clauses). 2011-11-25 18:06:36 -08:00
Alan Mishchenko df3e23ae3a Enabled skipping random decisions in PBA, which are performed by default. 2011-11-12 17:50:41 -08:00
Alan Mishchenko 814ee4841b Dump last frame clauses with 'pdr -d' even if the problem is SAT or undecided. 2011-11-12 14:03:00 -08:00
Alan Mishchenko 9fe4c74952 Corner-case bug in PDR. 2011-11-11 19:29:15 -08:00
Alan Mishchenko 868a1b9aeb Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc. 2011-10-31 14:59:47 -05:00
Alan Mishchenko 6f0b87dd5c New abstraction code. 2011-10-15 22:04:05 +03:00
Alan Mishchenko dbe2b466d7 Added handling of exceeding conflict limit in PushClasses. 2011-10-01 08:00:04 +07:00
Alan Mishchenko 961f7532d7 Changing the ordering of arguments in two iterators. 2011-08-01 13:47:51 +07:00
Alan Mishchenko 820a147ef1 Removed useless typecasts related to changes in Vec_VecEntry(). 2011-08-01 12:35:34 +07:00
Alan Mishchenko 2dd6b9789d Reduced default growth rate of vectors in the SAT solver. 2011-07-13 16:35:53 +07:00
Alan Mishchenko 6a020d6f69 Added switch to PDR to disable expensive generalization step. 2011-07-13 15:13:08 +07:00
Alan Mishchenko c4e8593075 Modified the PDR print-out to be compatible with Niklas. 2011-07-12 22:41:44 +07:00
Alan Mishchenko af84c0d205 Added printout of flop names in the PLA file representing the invariant. 2011-07-11 10:49:36 +07:00
Alan Mishchenko 86ba294dc8 The cube in PDR can have more than 2^15 literals. 2011-06-27 10:35:36 -07:00
Alan Mishchenko 3c7842be32 Improvements to timeout. 2011-05-11 22:14:12 +08:00
Alan Mishchenko 5222f382af Adding SAT-solver-level timeouts to the BMC engines. 2011-04-08 15:35:59 -07:00
Alan Mishchenko a28fe0d324 Unsuccessful attempt to improve PDR and a few minor changes. 2011-04-07 13:49:03 -07:00
Alan Mishchenko 02f7ede7c6 Added test package (new files). 2011-03-29 19:11:34 -07:00
Alan Mishchenko 4dcf8cee2d Improvements in Vec_Vec_t. 2011-03-27 11:35:31 -07:00
Alan Mishchenko 148a786b69 Made abc.h independent of CUDD and Extra. 2011-03-03 12:28:52 -08:00
Alan Mishchenko 71cbf17e7f Unified the use of counter-examples in three packages. 2011-02-13 17:46:48 -08:00
Alan Mishchenko 686d38d667 Changes to enable C++ compilation after recent modifications. 2011-02-13 15:16:10 -08:00
Alan Mishchenko e6f8744777 Make PDR return the number of completed frames. 2011-02-03 21:34:46 -08:00
Alan Mishchenko 624af674a0 New code since Dec 2010. 2011-01-13 13:32:18 -08:00
Alan Mishchenko ae4b51351c Cumulative changes in the last few weeks. 2011-01-13 12:38:59 -08:00
Alan Mishchenko f4066b5be3 Initial implementation of AnalyseFinal 2010-12-03 09:26:08 -08:00
Alan Mishchenko cdcbd60b39 Adding missing license agreements 2010-11-29 01:23:21 -08:00
Alan Mishchenko 6130e39b18 initial commit of public abc 2010-11-01 01:35:04 -07:00
Alan Mishchenko df6fdd1dff Version abc90408 2009-04-08 08:01:00 -07:00
Alan Mishchenko 32314347ba Version abc90310 2009-03-10 08:01:00 -07:00
Alan Mishchenko 0871bffae3 Version abc90215 2009-02-15 08:01:00 -08:00
Alan Mishchenko f936cc0680 Version abc90118 2009-01-18 08:01:00 -08:00
Alan Mishchenko c9ad5880cc Version abc81029 2008-10-29 08:01:00 -07:00
Alan Mishchenko e917dda1d3 Version abc81013 2008-10-13 08:01:00 -07:00
Alan Mishchenko eb75697fe0 Version abc81004 2008-10-04 08:01:00 -07:00