Commit Graph
1150 Commits
Author SHA1 Message Date
Alan Mishchenko d65d8528b6 New BMC engine. 2013-10-27 22:39:58 -07:00
Alan Mishchenko 3b30fb2a11 Multi-output property solver. 2013-10-26 23:05:13 -07:00
Alan Mishchenko 9437664596 Multi-output property solver. 2013-10-26 21:29:57 -07:00
Alan Mishchenko 47afd0f4f4 Multi-output property solver. 2013-10-23 16:26:13 -07:00
Alan Mishchenko 8ad1729aa9 Adding new synthesis scripts. 2013-10-23 10:44:11 -07:00
Alan Mishchenko cb4631e64e Compiler warnings. 2013-10-17 18:04:07 -07:00
Alan Mishchenko 4ab7905b72 Fix for writing choices into a BLIF file. 2013-10-16 13:33:51 -07:00
Alan Mishchenko f9900a4c3b Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe. 2013-10-15 09:04:27 -07:00
Alan Mishchenko 1692c1a57a Improvements to buffering and sizing. 2013-10-13 23:08:52 -07:00
Alan Mishchenko f8410b532b Improvements to buffering and sizing. 2013-10-12 22:51:43 -07:00
Alan Mishchenko 2c7f39026a Extending truth table support in &jf for more than 6 inputs. 2013-10-10 14:45:19 -07:00
Alan Mishchenko 33695bed11 Improvements to the canonical form computation. 2013-10-10 12:35:27 -07:00
Alan Mishchenko 12aab154c3 CNF generating using new mapper. 2013-10-10 01:18:15 -07:00
Alan Mishchenko 6ea3a35b03 Upgrading 'mfs2' to consider some nodes as having no level. 2013-10-09 22:30:38 -07:00
Alan Mishchenko 7d56aabab6 Upgrading 'mfs2' to consider some nodes as having no level. 2013-10-09 22:30:03 -07:00
Alan Mishchenko 608fe4e3bd Towards better Boolean matching. 2013-10-09 21:31:57 -07:00
Alan Mishchenko 51fb9e4ed4 Towards better Boolean matching. 2013-10-09 18:58:49 -07:00
Alan Mishchenko 8a03e530c2 Resubstitution code. 2013-10-06 15:57:17 -07:00
Alan Mishchenko a4a1053d98 Towards better Boolean matching. 2013-10-05 22:44:02 -07:00
Alan Mishchenko c59121f4e0 Bug fix and performance improvement in &iso. 2013-10-03 16:33:41 -07:00
Alan Mishchenko 6132d7cb10 Experiment with the AIG package. 2013-10-03 12:25:27 -07:00
Alan Mishchenko cfa7be1a07 Integrating synthesis into the new BMC engine. 2013-10-02 22:58:23 -07:00
Alan Mishchenko 38e577f5df Enabling counter-example generation in the new BMC engine. 2013-10-02 21:41:01 -07:00
Alan Mishchenko 7b99370e0a Changing default values. 2013-10-02 14:36:33 -07:00
Alan Mishchenko 19c361e387 Changes in specialized matching. 2013-10-02 12:55:20 -07:00
Alan Mishchenko 16f7903697 Changes in specialized matching. 2013-10-01 00:43:43 -07:00
Alan Mishchenko 1fb7ef8153 Converting mapped AIG into strashed AIG. 2013-09-30 22:41:55 -07:00
Alan Mishchenko cb845d4488 Changing default values. 2013-09-30 13:39:14 -07:00
Alan Mishchenko 846da1d2c7 Changing default values. 2013-09-30 13:33:39 -07:00
Alan Mishchenko 726e70392c Changing default values. 2013-09-30 01:00:25 -07:00
Alan Mishchenko 62439be84d New logic sharing extraction. 2013-09-29 23:14:00 -07:00
Alan Mishchenko 2a83a97164 Changing default values. 2013-09-28 23:56:08 -07:00
Alan Mishchenko 797cb49584 Changing default values. 2013-09-28 23:14:43 -07:00
Alan Mishchenko 68011de615 Improving printouts in sharing extraction. 2013-09-28 22:42:01 -07:00
Alan Mishchenko 5f97f5cffa New logic sharing extraction. 2013-09-28 20:19:53 -07:00
Alan Mishchenko 61ee156b72 New logic sharing extraction. 2013-09-28 18:35:38 -07:00
Alan Mishchenko a7fcdf20ab Performance balancing command &b. 2013-09-27 18:50:23 -07:00
Alan Mishchenko 4a74b7ced9 Generation of plain AIG after mapping. 2013-09-27 14:45:55 -07:00
Alan Mishchenko 940cf7f98b Generation of plain AIG after mapping. 2013-09-27 13:30:36 -07:00
Alan Mishchenko debbf4d807 Bug fix. 2013-09-27 10:09:57 -07:00
Alan Mishchenko 531657105b Improving DAG-aware unmapping. 2013-09-25 15:29:01 -07:00
Alan Mishchenko ee11ee1833 Changes to enable decomposition of non-DSD functions. 2013-09-25 13:18:21 -07:00
Alan Mishchenko cab8301065 Changing switch -R <num> in &gla to mean the max allowed size of abstraction. Adding switch -Q <num> to stop when the number of objects exceeds num % _during_refinement_. 2013-09-23 10:57:15 -07:00
Alan Mishchenko eec94a70f1 Adding API to return the mapped network. 2013-09-22 23:18:40 -07:00
Alan Mishchenko d61bedc627 Adding API to return the mapped network. 2013-09-22 16:23:57 -07:00
Alan Mishchenko cfebcae125 Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement. 2013-09-21 17:55:59 -04:00
Alan Mishchenko d4bd7846c3 Added bridge integration for multi-output 'bmc3 -a'. 2013-09-17 23:19:54 -07:00
Alan Mishchenko efa6b54b5e Debugging and finetuning the flow. 2013-09-17 21:47:39 -07:00
Alan Mishchenko 73a997a8bd Adding commands to set and print timing constraints. 2013-09-17 14:47:34 -07:00
Alan Mishchenko 7d3976a763 Unifying standard cell library representations. 2013-09-17 13:16:20 -07:00