Commit Graph

374 Commits

Author SHA1 Message Date
Alan Mishchenko b7ba9aa8dc New hierarchy manager. 2012-01-13 20:58:28 -08:00
Alan Mishchenko fadde52dc6 Changes to the lazy man's synthesis code. 2012-01-11 22:08:35 -08:00
Alan Mishchenko 564a3553f0 Gate level abstraction. 2012-01-08 13:15:03 +07:00
Alan Mishchenko 376bf3a703 Bug fix: changing output number to 0 in the CEX after ORing POs. 2012-01-07 11:19:03 +07:00
Alan Mishchenko aec5d33889 Backward reachability using circuit cofactoring. 2012-01-01 15:58:17 +07:00
Alan Mishchenko 6c19c1dfed Delay optimization using precomputed library. 2011-12-29 21:14:01 +07:00
Alan Mishchenko ed13bd16fd New variable-time frame abstraction. 2011-12-29 10:13:25 +07:00
Alan Mishchenko 1c51d9577d Added switch -n to 'miter' to ignore PI/PO names. 2011-12-22 14:55:10 -08:00
Alan Mishchenko d0da3a8258 Computing interpolants as truth tables. 2011-12-22 14:26:47 -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 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 07405ca1c5 Integrated new proof-logging into proof-based gate-level abstraction. 2011-12-08 22:42:50 -08:00
Alan Mishchenko 360c705fc4 Added recording of AIG subgraphs. 2011-12-06 12:42:00 -08:00
Alan Mishchenko d2db956a61 Started experiments with a new solver. 2011-11-25 18:08:48 -08:00
Alan Mishchenko 0a5d856cec Making GLA PBA and GLA CBA communicate information. 2011-11-22 19:07:00 -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 fa96b8d798 Do not allow interpolation with constraints. 2011-11-12 17:18:49 -08:00
Alan Mishchenko c1ac6b9b3e Dump inductive invariant or last interpolant after interpolation. 2011-11-12 16:56:41 -08:00
Alan Mishchenko 3beb36778e Enabled counter-example minimization in 'write_counter'. 2011-11-11 20:56:05 -08:00
Alan Mishchenko 9a89e3f9f5 Changing defaults in gate-level abstraction. 2011-11-06 23:35:15 -08:00
Alan Mishchenko d2ced9f82e Changes to read multi-output testcases described using AIGER 1.9. 2011-11-06 23:15:27 -08:00
Alan Mishchenko f08be2742e C++ portability changes. 2011-10-27 23:34:11 -07:00
Alan Mishchenko bc81cf2dae Improvements to the new abstraction code. 2011-10-27 14:20:47 -07:00
Alan Mishchenko 0f77840520 New proof-based abstraction code. 2011-10-25 18:32:06 +08:00
Alan Mishchenko f7fd329787 Improvements to the QBF solver. 2011-10-25 17:22:33 +08:00
Alan Mishchenko f96f3fa583 Improvements to the QBF solver. 2011-10-24 18:05:45 +08:00
Alan Mishchenko 9ec9d9f315 New abstraction code. 2011-10-19 23:45:11 +07:00
Alan Mishchenko 19ce8396f0 New abstraction code. 2011-10-19 16:03:15 +07:00
Alan Mishchenko 397bebf8a5 New abstraction code. 2011-10-19 15:42:55 +07:00
Alan Mishchenko 6f0b87dd5c New abstraction code. 2011-10-15 22:04:05 +03:00
Alan Mishchenko 924ec940fe Changes to the matching procedure. 2011-10-06 15:48:27 +07:00
Alan Mishchenko e6e6a3cf9e Changes to the matching procedure. 2011-10-01 17:00:59 +07:00
Alan Mishchenko 519b03e8e8 Changes to the matching procedure and new abstraction code. 2011-09-27 15:10:53 +07:00
Alan Mishchenko 976f5f5a12 Changes to Boolean matching. 2011-09-24 20:15:54 -07:00
Alan Mishchenko d080336bb5 Added new feature to bmc3. 2011-09-23 22:35:03 -07:00
Alan Mishchenko 8f74276edb Initial changes to enable gate-level abstraction. 2011-09-22 09:37:44 -07:00
Alan Mishchenko 8248691d84 Added limit on the number of flops to add in one iteration of &abs_refine. 2011-09-12 16:46:37 -05:00
Alan Mishchenko 583bc4d71a Added limit on the number of flops to add in one iteration of &abs_cba. 2011-09-11 20:31:25 -05:00
Alan Mishchenko 11ed724766 Added timeout to &abc_pba. 2011-09-02 17:09:07 +07:00
Alan Mishchenko f8fb154229 Change 'testcex' to modify the PO number. 2011-08-27 22:44:21 +07:00
Alan Mishchenko 2adf8dc2fd Sequential cleanup with symbolic/ternary simulation. 2011-08-25 17:21:17 +07:00
Alan Mishchenko df6d509023 Sequential cleanup with symbolic/ternary simulation. 2011-08-25 14:14:50 +07:00
Alan Mishchenko 3469b605e1 Sequential cleanup with symbolic/ternary simulation. 2011-08-24 17:39:57 +07:00
Alan Mishchenko d79cd4db44 Experiments with SPFD-based decomposition. 2011-08-21 15:05:44 +07:00
Alan Mishchenko 21dfaedebd Experiments with SPFD-based decomposition + new K-map print-out. 2011-08-20 20:18:31 +07:00
Alan Mishchenko b71b5bbc23 Bug fix in CBA and PBA. 2011-08-18 14:38:02 +07:00
Alan Mishchenko 48ae2c448f Bug fix in CBA and PBA. 2011-08-17 20:49:41 +07:00
Alan Mishchenko 3344a46b26 Added switch '-t' to 'miter' to create regular miter from dual-output miter. 2011-08-14 19:22:30 +07:00
Alan Mishchenko 94726c981b Other changes to enable new features in the mapper (bug fix). 2011-08-06 13:28:22 +08:00