Commit Graph

91 Commits

Author SHA1 Message Date
Alan Mishchenko 265e3e5cd4 Moving Vec_Set_t to the vector directory. 2012-03-28 10:13:42 -07:00
Alan Mishchenko b4df114e4a Logic sharing for multi-input gates. 2012-03-25 16:49:29 -07:00
Alan Mishchenko 309bcf2dec Logic sharing for multi-input gates. 2012-03-25 01:24:26 -07:00
Alan Mishchenko aeedc6ace5 Exploration of ISO and minor changes. 2012-03-13 16:12:16 -07:00
Alan Mishchenko 325ac583e6 Created a communication bridge. 2012-03-01 21:20:18 -08:00
Alan Mishchenko e60d6c94a3 Experiment with technology mapping. 2012-02-20 21:33:51 -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 ecd14d4daf Isomorphism checking code. 2012-02-15 18:40:05 -08:00
Alan Mishchenko c5067f7d04 Graph isomorphism checking code. 2012-02-11 00:22:05 -08:00
Alan Mishchenko 7ea40494eb Graph isomorphism checking code. 2012-01-29 21:22:54 -08:00
Alan Mishchenko 94d35a2592 Variable timeframe abstraction. 2012-01-24 01:04:56 -08:00
Alan Mishchenko 8014f25f6d Major restructuring of the code. 2012-01-21 04:30:10 -08:00
Alan Mishchenko 095345fc4a Added new name manager and modified hierarchy manager to use it. 2012-01-13 15:43:09 -08:00
Alan Mishchenko cb2d12bb04 New hierarchy manager. 2012-01-13 00:34:13 -08:00
Alan Mishchenko aec5d33889 Backward reachability using circuit cofactoring. 2012-01-01 15:58:17 +07:00
Alan Mishchenko ed13bd16fd New variable-time frame abstraction. 2011-12-29 10:13:25 +07:00
Alan Mishchenko d0da3a8258 Computing interpolants as truth tables. 2011-12-22 14:26:47 -08:00
Alan Mishchenko bc2f199bd3 Started SAT-based reparameterization. 2011-12-13 23:38:41 -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 36a80c7579 Added support for generating a library of real-life truth-tables. 2011-12-09 00:38:49 -08:00
Alan Mishchenko e84dcb7862 g++ portability changes. 2011-12-06 16:06:59 -08:00
Alan Mishchenko 5161978d05 Started proof transformations. 2011-12-01 01:14:32 -05:00
Alan Mishchenko d2db956a61 Started experiments with a new solver. 2011-11-25 18:08:48 -08:00
Alan Mishchenko 0736f39609 New truth table permutation procedure. 2011-10-26 23:15:42 +08:00
Alan Mishchenko 0f77840520 New proof-based abstraction code. 2011-10-25 18:32:06 +08:00
Alan Mishchenko 12b70d4946 Changes to CNF generation code. 2011-10-17 10:39:05 +03:00
Alan Mishchenko c6982485e4 New abstraction code. 2011-10-14 16:48:45 +03:00
Alan Mishchenko 519b03e8e8 Changes to the matching procedure and new abstraction code. 2011-09-27 15:10:53 +07:00
Alan Mishchenko 23671d65a9 Experiments with SPFD-based decomposition. 2011-08-17 20:48:56 +07:00
Alan Mishchenko 81620f2e92 Changes to enable CEX minimization. 2011-08-01 12:13:49 +07:00
Alan Mishchenko b8de7a28e0 Changes to enable smarter simulation. 2011-07-30 19:56:52 +07:00
Alan Mishchenko ce38474c74 Improving and updating the abstraction code. 2011-07-29 15:38:44 +07:00
Alan Mishchenko e7a5a74b4c Adding procedures to find the care bits of a counter-example. 2011-07-25 20:35:06 +07:00
Alan Mishchenko 267f61164a Changes to enable smarter simulation. 2011-07-20 18:40:09 +07:00
Alan Mishchenko 204fac4dca Other changes to enable new features in the mapper. 2011-07-10 13:56:05 +07:00
Alan Mishchenko ebfd70cdf4 Initial changes to enable new features in the mapper 2011-07-08 19:40:07 -07:00
Alan Mishchenko 4669839b24 Added new mapping feature. 2011-06-20 22:23:32 -07:00
Alan Mishchenko 31360734b7 Added new command 'outdec'. 2011-05-19 11:43:11 +07:00
Alan Mishchenko 3c7842be32 Improvements to timeout. 2011-05-11 22:14:12 +08:00
Alan Mishchenko e4d0f4715a Added new options to testcex. 2011-04-28 09:56:14 -04:00
Alan Mishchenko affb43e2a3 Added switch to control duplication of logic after mapping. 2011-04-24 10:43:24 -07:00
Alan Mishchenko 05b61206e4 Adding constant correspondence. 2011-04-18 23:27:51 -07:00
Alan Mishchenko dd71ca94f1 Added cex generation for clustered reachability. 2011-04-16 00:08:43 -07:00
Alan Mishchenko 75e60ab2ee Experiments with reachability. 2011-04-14 09:57:35 -07:00
Alan Mishchenko 6e74c46bcf Enabled new BDD-based reachability engine 'reachy'. 2011-04-13 22:41:54 -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 1794bd37cd Made gate library package Mio independent of CUDD. 2011-03-30 21:02:29 -07:00
Alan Mishchenko 02f7ede7c6 Added test package (new files). 2011-03-29 19:11:34 -07:00
Alan Mishchenko 2b336851a2 Added test package. 2011-03-29 13:04:21 -07:00