Commit Graph

727 Commits

Author SHA1 Message Date
Alan Mishchenko 32e7b75829 APIs to represent simple gates in CNF. 2012-01-05 13:15:05 +07:00
Alan Mishchenko 660779b53c Configuration changes in the Boolean matching code. 2012-01-05 13:14:04 +07:00
Alan Mishchenko e3a412b2e7 Backward reachability using circuit cofactoring. 2012-01-01 15:58:49 +07:00
Alan Mishchenko aec5d33889 Backward reachability using circuit cofactoring. 2012-01-01 15:58:17 +07:00
Alan Mishchenko 1e20e2ccbc Delay optimization using precomputed library. 2011-12-30 13:11:52 +07:00
Alan Mishchenko 655d452cbb Delay optimization using precomputed library. 2011-12-30 11:36:25 +07:00
Alan Mishchenko 6ed8340226 Delay optimization using precomputed library. 2011-12-30 11:27:12 +07:00
Alan Mishchenko 64b8aa51e9 Delay optimization using precomputed library. 2011-12-30 09:54:30 +07:00
Alan Mishchenko 6c19c1dfed Delay optimization using precomputed library. 2011-12-29 21:14:01 +07:00
Alan Mishchenko fce98abf43 Experiments with flattening hierarchy. 2011-12-29 10:27:46 +07:00
Alan Mishchenko ed13bd16fd New variable-time frame abstraction. 2011-12-29 10:13:25 +07:00
Alan Mishchenko 21df8bf021 Experiments with flattening hierarchy. 2011-12-28 22:16:04 +07:00
Alan Mishchenko afc8553f89 Experiments with flattening hierarchy. 2011-12-28 21:15:19 +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 1c51d9577d Added switch -n to 'miter' to ignore PI/PO names. 2011-12-22 14:55:10 -08:00
Alan Mishchenko 810c0be127 Added alias blif2aig = undc; strash; zero 2011-12-22 14:29:36 -08:00
Alan Mishchenko d0da3a8258 Computing interpolants as truth tables. 2011-12-22 14:26:47 -08:00
Alan Mishchenko 82a2495ce9 Improvements to hierarchical BLIF parser. 2011-12-22 14:26:03 -08:00
Alan Mishchenko b3c9609e82 Improvements to hierarchical BLIF parser. 2011-12-21 12:56:28 -08:00
Alan Mishchenko 3418a8820a Fixed a bug in matching code. 2011-12-17 17:51:13 -08:00
Alan Mishchenko cd4752b565 Added utility to sort lines in a file alphabetically. 2011-12-17 13:57:56 -08:00
Alan Mishchenko 024f9a2b13 Performance improvement in 'dch' for designs having nodes with many fanouts. 2011-12-15 19:32:53 -08:00
Alan Mishchenko f67cb76dff Added optional printout of the hierarchy structure before collapsing. 2011-12-15 19:32:05 -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 4a7ef41db2 Adding switch '-W' to fx to control the quality of extracted divisors. 2011-12-15 15:46:32 -08:00
Alan Mishchenko 2bb95a97d0 Adding switch '-W' to fx to control the quality of extracted divisors. 2011-12-15 15:44:56 -08:00
Alan Mishchenko c80c0cc6c9 Trying to make sorting of nodes platform-indendent. 2011-12-15 13:39:16 -08:00
Alan Mishchenko 9608bcd1d8 Enabling balance again. 2011-12-15 13:39:03 -08:00
Alan Mishchenko 6531899709 Temporarily disabling balance. 2011-12-15 13:24:27 -08:00
Alan Mishchenko c8e4a05fd3 Additional print-outs in dc2. 2011-12-15 13:13:23 -08:00
Alan Mishchenko b63b332bac Trying to make sorting of nodes platform-indendent. 2011-12-15 12:42:42 -08:00
Alan Mishchenko 40ddda3edd Trying to make sorting of nodes platform-indendent. 2011-12-15 12:27:35 -08:00
Alan Mishchenko bc2f199bd3 Started SAT-based reparameterization. 2011-12-13 23:38:41 -08:00
Alan Mishchenko 8fdc5d220f g++ portability changes. 2011-12-13 12:17:03 -08:00
Alan Mishchenko 23af7f9036 Added command &read_blif to read hierarchical BLIF directly into the &-space. 2011-12-12 19:10:33 -08:00
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