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

687 Commits

Author SHA1 Message Date
Alan Mishchenko be874a7abe Added command &read_blif to read hierarchical BLIF directly into the &-space. 2011-12-12 18:43:49 -08:00
Alan Mishchenko ed4f4adeee Added the hierarchy printout. 2011-12-11 17:29:25 -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 eb35f0ef65 Added support for generating a library of real-life truth-tables. 2011-12-09 01:05:18 -08:00
Alan Mishchenko 36a80c7579 Added support for generating a library of real-life truth-tables. 2011-12-09 00:38:49 -08:00
Alan Mishchenko beb29257bf Added support for generating a library of real-life truth-tables. 2011-12-09 00:38:16 -08:00
Alan Mishchenko 200c5cc659 Added support for generating a library of real-life truth-tables. 2011-12-09 00:37:05 -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 35733eb1a1 Added/renamed useful APIs. 2011-12-06 21:10:58 -08:00
Alan Mishchenko 68baf03809 Another attempt to make CUDD platform- and runtime-independent. 2011-12-06 18:58:41 -08:00
Alan Mishchenko 780321cf54 Another attempt to make CUDD platform- and runtime-independent. 2011-12-06 17:48:31 -08:00
Alan Mishchenko 7cce97b4b3 Added new switch to the LUT matching code. 2011-12-06 16:50:04 -08:00
Alan Mishchenko e84dcb7862 g++ portability changes. 2011-12-06 16:06:59 -08:00
Alan Mishchenko ef37d14bc6 Added recording of AIG subgraphs. 2011-12-06 15:37:09 -08:00
Alan Mishchenko f95e73c40b Added recording of AIG subgraphs. 2011-12-06 14:29:32 -08:00
Alan Mishchenko 0f8b68aef8 Performance bug fix in SOP balancing. 2011-12-06 13:15:53 -08:00
Alan Mishchenko 360c705fc4 Added recording of AIG subgraphs. 2011-12-06 12:42:00 -08:00
Alan Mishchenko b4a46eb688 Bug fixes in CUDD 2.4.2. 2011-12-06 07:39:55 -08:00
Alan Mishchenko a24e678a79 Bug fixes in CUDD 2.4.2. 2011-12-06 07:32:17 -08:00
Alan Mishchenko b743298cd5 Proof-logging in the updated solver. 2011-12-05 20:02:46 -08:00
Alan Mishchenko df8b636169 Fixed performance bug in matching code. 2011-12-05 18:27:03 -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 12869de14b Previusly forgotten debug printout. 2011-12-02 01:08:48 -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 7a0a4d4d79 Added a warning to Makefile about setting compilation flags when compiling on 32-bit Linux. 2011-11-24 14:25:47 -08:00
Alan Mishchenko 0a5d856cec Making GLA PBA and GLA CBA communicate information. 2011-11-22 19:07:00 -08:00
Alan Mishchenko ff938c7141 Modifications to the matching procedure 2011-11-22 18:48:03 -08:00
Alan Mishchenko 24408a483c Bug fix in GLA PBA. 2011-11-13 00:17:00 -08:00