Commit Graph

687 Commits

Author SHA1 Message Date
Alan Mishchenko cac32a32c7 Enabled switch 'fx -N <num>' to extract a fixed number of divisors. 2013-05-09 12:51:18 -07:00
Alan Mishchenko 22806448c1 Adding comment about using 'dprove' for sequential synthesis. 2013-05-09 12:01:29 -07:00
Alan Mishchenko 7c7d527755 Changing per-output runtime limit to be in miliseconds. 2013-05-09 11:35:04 -07:00
Alan Mishchenko a735d95a5b SAT sweeping under constraints (bug fix). 2013-05-07 18:11:29 -07:00
Alan Mishchenko 51db560206 Procedures for sorting fanins of the nodes. 2013-05-06 18:51:48 -07:00
Alan Mishchenko f02888635f Procedures for sorting fanins of the nodes. 2013-05-06 18:19:20 -07:00
Alan Mishchenko 05f7cd9ed2 Integration of the liveness property prover developed by Sayak Ray. 2013-05-05 21:08:55 -07:00
Alan Mishchenko 7a78e30390 New fast extract. 2013-05-05 14:33:28 -07:00
Alan Mishchenko 13ee4998c3 C++ compiler errors. 2013-05-04 20:24:53 -07:00
Alan Mishchenko 50df0813fb Allowing 'constr' to reset remove currently defined constraints. 2013-05-03 19:59:18 -07:00
Alan Mishchenko 50095be5ac Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>). 2013-05-03 19:58:25 -07:00
Alan Mishchenko a59968ce8c Adding runtime limit per output to multi-output BMC (bmc3 -H <num_sec>). 2013-05-03 18:26:18 -07:00
Alan Mishchenko 6a49d1f4c6 Reading/writing MiniAIG and several minor changes. 2013-05-03 15:45:50 -07:00
Alan Mishchenko bc50421928 Minor changes and improvement in PO partitioning (command &popart). 2013-05-01 12:45:34 -07:00
Alan Mishchenko 1f573cfe58 Compiler warnings. 2013-05-01 00:13:29 -07:00
Alan Mishchenko b94766bce5 Faster isomorphism detection (command &iso). 2013-05-01 00:10:53 -07:00
Alan Mishchenko c53eb0b9e1 Changing the print-out of &iso. 2013-04-30 10:46:07 -07:00
Alan Mishchenko 3b1ebbaa28 SAT sweeping under constraints. 2013-04-28 19:17:59 -07:00
Alan Mishchenko 9e1765216b Added option 'int -I <filename>' to specify file names to dump invariants. 2013-04-28 16:55:25 -07:00
Alan Mishchenko 58e1041ad8 Modified command 'eliminate' to perform traditional 'eliminate -1'. 2013-04-28 16:21:58 -07:00
Alan Mishchenko a33821ab38 Added alias for 'eliminate'. 2013-04-28 15:41:29 -07:00
Alan Mishchenko 48d867f77d Modified command 'eliminate' to perform traditional 'eliminate -1'. 2013-04-28 15:02:03 -07:00
Alan Mishchenko b09926e8e2 SAT sweeping under constraints. 2013-04-28 01:25:29 -07:00
Alan Mishchenko 17a0d944b3 SAT sweeping under constraints. 2013-04-27 22:38:01 -07:00
Alan Mishchenko 324d73c29a New fast extract. 2013-04-27 15:23:12 -07:00
Alan Mishchenko 486eacc542 SAT sweeping under constraints. 2013-04-25 15:32:30 -07:00
Alan Mishchenko 06ba3d3e6c Adding command &filter_equiv to filter candidate equivalence classes using indexes of disproved POs after handling SRM as a multi-output miter. 2013-04-17 22:18:43 -07:00
Alan Mishchenko 7808ee8e70 Adding parameter structure for rarity simulation. 2013-04-17 19:40:02 -07:00
Alan Mishchenko 45d82477b7 Saving network name in 'blockpo'. 2013-04-12 00:10:21 -07:00
Alan Mishchenko 4876f1e21c Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output mode. 2013-04-09 16:26:28 -07:00
Alan Mishchenko f99e5cd9d6 Shrink for 6-LUTs. 2013-04-01 20:21:34 -07:00
Alan Mishchenko 28f12c5f06 Shrink for 6-LUTs. 2013-04-01 19:25:21 -07:00
Alan Mishchenko 5ec77b66e1 Updating 'sim3' to move the design into the last rare state. 2013-04-01 18:41:56 -07:00
Alan Mishchenko 48fce79453 Updating 'sim3' to move the design into the last rare state. 2013-04-01 18:39:42 -07:00
Alan Mishchenko 2650f94598 Shrink for 6-LUTs. 2013-03-31 23:09:51 -07:00
Alan Mishchenko ca7c801150 Improving verbose printout of 'sim3' when solving multiple outputs. 2013-03-30 15:15:26 -07:00
Alan Mishchenko 05ea180902 Compiler warnings. 2013-03-30 14:20:10 -07:00
Alan Mishchenko 1d4674e548 Compiler warnings. 2013-03-30 14:17:10 -07:00
Alan Mishchenko 270d36ac05 Improved 'trim' and added 'dropsat' to replace sat POs by constant 0. 2013-03-30 14:11:39 -07:00
Alan Mishchenko 5ace683835 Updating bmc3 printout to show the number of failed outputs. 2013-03-30 13:02:32 -07:00
Alan Mishchenko b7cd22786e Changed to 'print_level' to be less verbose by default. 2013-03-28 20:09:08 -07:00
Alan Mishchenko fdb8d83f7a Adding command &miter2 to derive a specified sequential miter. 2013-03-28 12:30:27 -07:00
Alan Mishchenko 7a2132b237 Added dumping QDIMACS files in command 'qbf'. 2013-03-27 17:21:08 -07:00
Alan Mishchenko 272089221a Removing hard-coded limit on the number of solving iterations in command 'qbf'. 2013-03-27 12:51:57 -07:00
Alan Mishchenko e64cad10e2 Adding command &miter2 to derive a specified sequential miter. 2013-03-27 12:43:00 -07:00
Alan Mishchenko bf795e57cf Handling special case in 'fold' when the network is combinational. 2013-03-13 11:47:17 +01:00
Alan Mishchenko 1eb4059f05 PO partitioning algorithm. 2013-03-09 13:33:12 -08:00
Alan Mishchenko eee8ceb0fa PO partitioning algorithm. 2013-03-09 12:19:11 -08:00
Alan Mishchenko a3bdba6875 Modified command 'init' to allow for specific init values. 2013-03-07 20:38:55 -08:00
Alan Mishchenko 0c9337f627 User-controlable SAT sweeper. 2013-03-04 00:33:36 -08:00
Alan Mishchenko a27a7bc827 User-controlable SAT sweeper and other small changes. 2013-02-27 12:12:23 -05:00
Alan Mishchenko 69dd1337b0 Started PO partitioning command. 2013-02-24 09:27:25 -08:00
Alan Mishchenko 1c744cf10a K-hot STG encoding. 2013-02-23 13:53:22 -08:00
Alan Mishchenko dfe5f511b2 Adding new features to 'dualrail'. 2013-02-21 22:46:53 -08:00
Alan Mishchenko dd52905fa3 Enabling two-timeframe property check in the interpolation procedure. 2013-02-21 12:10:35 -08:00
Alan Mishchenko a82b0a8ad5 New command &cycle, which is faster than 'cycle'. 2013-02-19 23:51:13 -08:00
Alan Mishchenko 59fe3268a7 Adding STG generation (&era -d) and STG encoding (&read_stg <file>). 2013-02-19 23:07:29 -08:00
Alan Mishchenko 99a9718355 Integrating sweeping information. 2013-02-19 12:56:36 -08:00
Alan Mishchenko baa944e6a2 Added 'gap timeout' to pdr. 2013-02-16 14:54:11 -08:00
Alan Mishchenko fd0ff0171e Added 'gap timeout' to bmc3 and sim3. 2013-02-15 16:47:18 -08:00
Alan Mishchenko 930369f36f Integration of timing manager. 2013-02-03 18:02:22 +08:00
Alan Mishchenko 30ec58fcda Added switch 'zeropo -s' to skip comb sweep after removing a PO. 2013-02-01 03:57:17 +07:00
Alan Mishchenko 853222ee7b Fixed a corner-case when 'sim3 -a' does not work for costant POs. 2013-01-25 06:49:49 +07:00
Alan Mishchenko edd4b2a29c Added switch &trim -V <num> to remove const POs with specific value <num>. 2013-01-25 06:19:51 +07:00
Alan Mishchenko 6863688789 Enabled detecting CEXes in multiple POs without stopping (sim3 -a). 2013-01-23 12:37:44 +07:00
Alan Mishchenko ac1207abea Enabled detecting CEXes in multiple POs without stopping (sim3 -a). 2013-01-23 02:07:50 +07:00
Alan Mishchenko a625caa17d Fixing C++ compilation issues. 2013-01-08 13:56:20 +08:00
Alan Mishchenko f26e760e9d Fixing C++ compilation issues. 2013-01-08 13:33:17 +08:00
Alan Mishchenko 79f3ecb15f Technology mapper. 2013-01-08 05:50:37 +08:00
Alan Mishchenko e1a5556e8c New unrolling manager. 2012-12-24 08:16:19 +07:00
Alan Mishchenko 82050bbe11 Assembling timing/hierarchy manager from input data. 2012-12-13 15:18:53 -08:00
Alan Mishchenko 2575a5d683 Unifification of custom extensions. 2012-12-10 13:56:40 -08:00
Alan Mishchenko dc843b03c9 Renaming If_Lut_t into If_LibLut_t. 2012-12-10 01:07:41 -08:00
Alan Mishchenko 5eedc74a15 Adding box library. 2012-12-10 00:59:54 -08:00
Alan Mishchenko 8761942258 Renaming multi-output mode enable switch 'bmc3 -s' to be 'bmc3 -a'. 2012-12-09 16:56:43 -08:00
Alan Mishchenko 58d4012a55 Enabling multi-output solving in 'pdr'. 2012-12-09 14:46:16 -08:00
Alan Mishchenko b65ae7349a Enabling multi-output solving in 'pdr'. 2012-12-09 09:47:48 -08:00
Alan Mishchenko 0058cefee3 Deriving CEX after phase/tempor/reparam. 2012-12-09 00:19:18 -08:00
Alan Mishchenko a68593c4f2 Deriving CEX after phase/tempor/reparam. 2012-12-08 12:44:08 -08:00
Alan Mishchenko 8e5d771feb Deriving CEX after phase/tempor/reparam. 2012-12-08 12:38:31 -08:00
Alan Mishchenko 86fcba60c2 Enabling command &append for combiming multiple AIGs. 2012-12-01 23:13:24 -08:00
Alan Mishchenko cd32ae50c4 Counter-example analysis and optimization. 2012-11-30 17:22:44 -08:00
Alan Mishchenko f1a5288904 Counter-example analysis and optimization. 2012-11-30 11:38:05 -08:00
Alan Mishchenko 661265984c Counter-example analysis and optimization. 2012-11-28 16:18:39 -08:00
Alan Mishchenko b2fd119933 DSD manager. 2012-11-20 21:34:40 -08:00
Alan Mishchenko ffbe3bc576 DSD manager. 2012-11-19 23:42:05 -08:00
Alan Mishchenko a0052e22b4 Added switch 'cexcut -m' to generate bad states for all frames after G. 2012-11-15 16:00:29 -08:00
Alan Mishchenko c2e467d55b Added switch 'cexcut -n' to generate only one bad state. 2012-11-15 10:59:57 -08:00
Alan Mishchenko 2eb2402b01 Added command 'cexcut' and 'cexmerge'. 2012-11-14 20:50:18 -08:00
Alan Mishchenko 9173799c96 Added command 'cexcut' and 'cexmerge'. 2012-11-14 18:22:13 -08:00
Alan Mishchenko be29f37baa Added command 'cexcut' and 'cexmerge'. 2012-11-14 18:20:35 -08:00
Alan Mishchenko 9d5d804610 Added command 'cexcut' and 'cexmerge'. 2012-11-14 16:09:49 -08:00
Alan Mishchenko d8e0403296 Added command 'cexsave' and 'cexload'. 2012-11-14 14:33:27 -08:00
Alan Mishchenko be7a4e4259 Isolating BMC code into a separate package. 2012-11-14 13:55:24 -08:00
Alan Mishchenko aba8ff4ba0 Modifying parameter limits to allow mapping into 2-LUTs. 2012-11-14 12:56:45 -08:00
Alan Mishchenko 30b8c3d422 Made print-out of frontier cut an option ('-c') in '&ps'. 2012-11-12 14:08:10 -08:00
Alan Mishchenko 566c7d7152 Extending GIA to represent pintypes and pins. 2012-11-12 13:57:51 -08:00
Alan Mishchenko ee789ba902 Improved DSD. 2012-11-10 19:37:53 -08:00
Alan Mishchenko 7ba37f4901 Improved DSD. 2012-11-03 00:38:17 -07:00
Alan Mishchenko c899645b10 Adding dumping truth tables from LMS manager. 2012-11-02 18:59:14 -07:00