Commit Graph

2864 Commits

Author SHA1 Message Date
Alan Mishchenko 7884dd01bc Fixed a corner case bug in dprove when a trivial CEX is not produced. 2011-10-01 10:50:50 +07:00
Alan Mishchenko dbe2b466d7 Added handling of exceeding conflict limit in PushClasses. 2011-10-01 08:00:04 +07:00
Baruch Sterin 16e12f1852 pyabc: fix callbacks into python to work correctly by moving to PyGILEState_Ensure/Release APIs 2011-09-29 17:34:05 -07:00
Baruch Sterin ef0fbf0372 completely silence the "source" command when the -s option is given 2011-10-24 15:21:08 -07:00
Baruch Sterin 9d652062b7 pyabc: fix indentation in pyabc.i 2011-10-24 15:21:08 -07:00
Baruch Sterin e9ef8e97bf Makefile: current LIBS line has a lot of unnecessary and problematic stuff. Replace it with just "-lreadline" 2011-10-24 15:21:08 -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 81b040e61c Fixed minor issues having to do with the number of BDD vars used. 2011-09-18 17:28:00 -07:00
Alan Mishchenko f14f5c9203 Fixing obscure memory problem with 'int' on large designs. 2011-09-17 23:00:50 -07:00
Alan Mishchenko c1edeccc60 64-bit portability changes. 2011-09-17 16:24:40 -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 a7acb2f104 Fixed the problem with blackboxes not preserving their names after duplication. 2011-09-08 21:10:36 +07:00
Alan Mishchenko 70694628d2 Sequential cleanup with symbolic/ternary simulation (bug fix). 2011-09-08 08:53:52 +07:00
Alan Mishchenko a525dfba6c Fixed the problem with incorrect reporting of finished timeframes after &abs_cba. 2011-09-04 01:40:56 +07:00
Alan Mishchenko 11ed724766 Added timeout to &abc_pba. 2011-09-02 17:09:07 +07:00
Alan Mishchenko 8cde0dd33c Bug fix in CBA. 2011-08-31 11:37:59 +07:00
Alan Mishchenko 11dca3aab0 Sequential cleanup with symbolic/ternary simulation (bug fix). 2011-08-30 00:42:02 +07:00
Alan Mishchenko 48bdc5144a Making 'reconcile' ignore the difference in flop count. 2011-08-29 18:46:16 +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 c913fd8849 Other changes to enable new features in the mapper (bug fix). 2011-08-24 09:33:40 +07:00
Alan Mishchenko 19d6e1693a Experiments with SPFD-based decomposition. 2011-08-24 09:33:18 +07:00
Alan Mishchenko 166fba3509 Experiments with SPFD-based decomposition. 2011-08-21 15:09:11 +07:00
Alan Mishchenko d79cd4db44 Experiments with SPFD-based decomposition. 2011-08-21 15:05:44 +07:00
Alan Mishchenko 151fe40242 Experiments with SPFD-based decomposition. 2011-08-20 20:38:44 +07:00
Alan Mishchenko 56035ab9ab Making sure reconcile does not change the PO number. 2011-08-20 20:29:11 +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 23671d65a9 Experiments with SPFD-based decomposition. 2011-08-17 20:48:56 +07:00
Alan Mishchenko e21d307544 Bug fix in interpolation (false positive if property fails in frame 0). 2011-08-14 20:04:08 +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
Alan Mishchenko b9dea5d674 Other changes to enable new features in the mapper (bug fix). 2011-08-06 01:31:07 +08:00
Alan Mishchenko fbb12a06f2 Bug fix in PBA. 2011-08-04 11:31:31 +08:00
Baruch Sterin 825b0b5ee3 added support for getting a cex vector 2011-08-02 02:13:52 -04:00
Alan Mishchenko 49df91f071 Several bug fixes. 2011-08-02 12:58:37 +07:00
Alan Mishchenko 64f31f98bf Added API to access the CEX vector. 2011-08-02 12:01:49 +07:00
Alan Mishchenko 6c6c0b0686 Enabled saving vector of counter-examples in the ABC framework. 2011-08-02 00:31:03 +07:00
Alan Mishchenko 4e9f972489 Changes to enable CEX minimization. 2011-08-01 20:44:13 +07:00
Alan Mishchenko 8af417bab7 Changes to enable smarter simulation (bug fix). 2011-08-01 18:40:34 +07:00
Alan Mishchenko 961f7532d7 Changing the ordering of arguments in two iterators. 2011-08-01 13:47:51 +07:00
Alan Mishchenko 820a147ef1 Removed useless typecasts related to changes in Vec_VecEntry(). 2011-08-01 12:35:34 +07:00
Alan Mishchenko 957b9f0173 Changes to enable CEX minimization. 2011-08-01 12:15:10 +07:00