luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
2,082 Commits 27 Branches 57 Tags 58 MiB
Commit Graph

2035 Commits

Author SHA1 Message Date
Alan Mishchenko ccf3caddb8 Bug fix in 'blockpo'. 2013-05-07 18:39:24 -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 f321b27bb7 SAT sweeping under constraints. 2013-05-06 00:44:21 -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 98cf5698a1 New fast extract. 2013-05-05 18:57:51 -07:00
Alan Mishchenko 7a78e30390 New fast extract. 2013-05-05 14:33:28 -07:00
Alan Mishchenko a1ceb7617c Making changes suggested by Mark Jarvin. 2013-05-05 09:06:53 -07:00
Alan Mishchenko eacfad7622 Changing the queue to work in the same the array of costs is realloced. 2013-05-05 09:04:14 -07:00
Alan Mishchenko 7d3301584a New fast extract. 2013-05-05 01:56:16 -07:00
Alan Mishchenko a762c695d7 New fast extract. 2013-05-05 01:54:11 -07:00
Alan Mishchenko 7f700af6e2 C++ compiler errors. 2013-05-04 20:44:28 -07:00
Alan Mishchenko cd4043ba7f C++ compiler errors. 2013-05-04 20:41:40 -07:00
Alan Mishchenko 79f782c0e8 C++ compiler errors. 2013-05-04 20:37:14 -07:00
Alan Mishchenko a11370946b C++ compiler errors. 2013-05-04 20:36:20 -07:00
Alan Mishchenko af6442a3ed C++ compiler errors. 2013-05-04 20:34:25 -07:00
Alan Mishchenko 744d35d029 C++ compiler errors. 2013-05-04 20:32:38 -07:00
Alan Mishchenko 4aff2d134d C++ compiler errors. 2013-05-04 20:28:05 -07:00
Alan Mishchenko 13ee4998c3 C++ compiler errors. 2013-05-04 20:24:53 -07:00
Alan Mishchenko 3945d382fe Adding new API to the queue. 2013-05-04 20:24:35 -07:00
Alan Mishchenko 36d5ef4e62 Making changes suggested by Mark Jarvin. 2013-05-04 11:10:25 -07:00
Alan Mishchenko 95571be503 Changes to the ABC data-structures to allow for larger designs. 2013-05-04 10:48:46 -07:00
Alan Mishchenko 14f761950d Fix to return equiv classes after improving &iso. 2013-05-03 21:53:13 -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 0ca8a245da Reading/writing MiniAIG and several minor changes. 2013-05-03 17:53:03 -07:00
Alan Mishchenko fcd377405a Compiler warnings. 2013-05-03 15:48:05 -07:00
Alan Mishchenko 6a49d1f4c6 Reading/writing MiniAIG and several minor changes. 2013-05-03 15:45:50 -07:00
Alan Mishchenko e782bbb842 Commenting out a warning. 2013-05-02 14:07:55 -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 266667d8b2 Improving local BDD construction from local SOPs and local AIGs. 2013-04-28 16:33:42 -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 2044caa97e Compiler warnings. 2013-04-28 15:12:55 -07:00
Alan Mishchenko 48d867f77d Modified command 'eliminate' to perform traditional 'eliminate -1'. 2013-04-28 15:02:03 -07:00
Alan Mishchenko 8db0b9c0c6 Improving local BDD construction from local SOPs and local AIGs. 2013-04-28 12:34: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 613e8b2ad6 SAT sweeping under constraints. 2013-04-27 18:37:39 -07:00
Alan Mishchenko 324d73c29a New fast extract. 2013-04-27 15:23:12 -07:00
Alan Mishchenko ae9a4407c4 Adding rollback for the other solver. 2013-04-25 16:02:40 -07:00
Alan Mishchenko ecf75a075b Compiler warnings. 2013-04-25 15:37:31 -07:00
Alan Mishchenko fb6c9e8564 Compiler warnings. 2013-04-25 15:36:07 -07:00
Alan Mishchenko 486eacc542 SAT sweeping under constraints. 2013-04-25 15:32:30 -07:00
Alan Mishchenko 005f0e39d2 Adding command &filter_equiv to filter candidate equivalence classes using indexes of disproved POs after handling SRM as a multi-output miter. 2013-04-22 13:39:55 -07:00
Alan Mishchenko 85ea8e95c6 Fixing the way packing information is written. 2013-04-19 23:40:17 -07:00
Alan Mishchenko 30cfee7d19 Typo in the comments. 2013-04-19 11:41:18 -07:00
Alan Mishchenko ca4145c7ef Typo in the comments. 2013-04-19 11:21:39 -07:00
Alan Mishchenko e0462d8d2e Adding print-out of SOP literals with 'ps -f'. 2013-04-19 09:35:30 -07:00
Alan Mishchenko df198d2cef Enabled 'cec' to be applied to networks derived from BLIF with EXDCs. 2013-04-18 18:32:58 -07:00
Alan Mishchenko c80fce00fe Enabled reading the EXDC network by the default BLIF reader. 2013-04-18 17:39:13 -07:00
Alan Mishchenko 96b784ecd7 Fixing both AIGER readers (read_aiger and &r) to work with AIGER 1.9 (except for liveness properties). 2013-04-18 00:05:11 -07:00
Alan Mishchenko 61ecc9c633 Fixing both AIGER readers (read_aiger and &r) to work with AIGER 1.9 (except for liveness properties). 2013-04-17 23:48:58 -07:00
Alan Mishchenko f6fb5600b1 Moves the code of create_abc_array to line 724. 2013-04-17 23:35:51 -07:00
Alan Mishchenko 05c8df33f2 Compiler warning. 2013-04-17 22:23:29 -07:00
Alan Mishchenko 6502aa82d6 Compiler warning. 2013-04-17 22:21: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 bdae7c625a Adding callback to bmc3, sim3, pdr in the multi-output mode. 2013-04-17 20:46:14 -07:00
Alan Mishchenko 7808ee8e70 Adding parameter structure for rarity simulation. 2013-04-17 19:40:02 -07:00
Alan Mishchenko 95d9aae3e7 Bug fix in '&reachy' having to do with incorrect handling of resource limits. 2013-04-17 18:36:54 -07:00
Alan Mishchenko 9b6efa34ad Bug fix in 'write_pla'. 2013-04-15 22:59:54 -07:00
Alan Mishchenko 45d82477b7 Saving network name in 'blockpo'. 2013-04-12 00:10:21 -07:00
Alan Mishchenko 3b1c632b15 Bug fix in 'blockpo'. 2013-04-11 11:03:26 -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 f1cd879786 New MFS package. 2013-04-03 13:01:49 -07:00
Alan Mishchenko 0a8a505638 New MFS package. 2013-04-03 12:40:41 -07:00
Alan Mishchenko e4cf178041 New MFS package. 2013-04-03 12:39:24 -07:00
Alan Mishchenko 23229e03bf Fixing the format mismatch in writing mapped GIA. 2013-04-02 23:03:30 -07:00
Alan Mishchenko 7e85276780 New MFS package. 2013-04-02 22:22:49 -07:00
Alan Mishchenko b902b00779 Small changes to LMS code. 2013-04-01 21:41:53 -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 2c275b8c71 Compiler warnings. 2013-03-31 23:14:12 -07:00
Alan Mishchenko 2650f94598 Shrink for 6-LUTs. 2013-03-31 23:09:51 -07:00
Alan Mishchenko 017c35baf2 Updating bmc3 printout to show the number of failed outputs. 2013-03-30 17:43:15 -07:00
Alan Mishchenko 900bdfac17 Bug fix in the printout of &popart. 2013-03-30 17:11:37 -07:00
Alan Mishchenko 4cb042f8c5 Bug fix in the printout of &popart. 2013-03-30 16:59:22 -07:00
Alan Mishchenko ca7c801150 Improving verbose printout of 'sim3' when solving multiple outputs. 2013-03-30 15:15:26 -07:00
Alan Mishchenko be8125f364 Updating 'pdr' to report the number of failed POs. 2013-03-30 14:31:09 -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 851c8551c0 Compiler warnings. 2013-03-30 12:31:39 -07:00
Alan Mishchenko 7f11278705 Compiler warnings. 2013-03-30 12:30:04 -07:00
Alan Mishchenko d3a4dce10e Updating bmc3 printout to show the number of failed outputs. 2013-03-30 12:24:30 -07:00
Alan Mishchenko cc7d3e3747 Added dumping QDIMACS files in command 'qbf'. 2013-03-28 22:21:05 -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 4c00829900 Modified SCL gate library to read/write gate formula. 2013-03-26 20:19:50 -07:00
Alan Mishchenko dfb065fa55 Fixing the dump of SAT solver into a CNF file. 2013-03-26 18:42:47 -07:00
Alan Mishchenko d010231043 The result of merging. 2013-03-26 17:29:26 -07:00
Alan Mishchenko e5054fa757 Making sure 'pdr -a' return UNDEC if it did not finish proving the remaining outputs to be UNSAT. 2013-03-26 16:57:42 -07:00
Alan Mishchenko d80071be84 Fixing a bug in &cycle, which could generate an unreachable state. 2013-03-26 16:04:33 -07:00
Alan Mishchenko 17af45424f Commenting out undesirable warnings/assertions. 2013-03-26 14:32:21 -07:00
Alan Mishchenko 93b1031664 Replacing unsafe Aig_ManObjNum() by Aig_ManObjNumMax(). 2013-03-19 12:42:17 +01:00
Alan Mishchenko a96436e890 Commenting out assertion that fails in 'dch', not sure why. 2013-03-14 19:07:33 +01:00
Alan Mishchenko a3b8b0a59d Fixing gap timeout in 'bmc3'. 2013-03-13 12:02:41 +01:00
Alan Mishchenko bf795e57cf Handling special case in 'fold' when the network is combinational. 2013-03-13 11:47:17 +01:00
Alan Mishchenko ec2973947c PO partitioning algorithm. 2013-03-09 13:37:37 -08:00
Alan Mishchenko 1eb4059f05 PO partitioning algorithm. 2013-03-09 13:33:12 -08:00
Alan Mishchenko b30d55b749 PO partitioning algorithm. 2013-03-09 12:49:36 -08:00
Alan Mishchenko 10729d50d4 Modified Python API iso_eq_classes to be eq_classes. 2013-03-09 12:26:11 -08:00
Alan Mishchenko eee8ceb0fa PO partitioning algorithm. 2013-03-09 12:19:11 -08:00
Alan Mishchenko ae091e695e Integrating box library. 2013-03-08 18:58:54 -08:00
Alan Mishchenko 467f8b651a Making 'bmc3' with switch '-a' not save CEXes. 2013-03-07 22:04:35 -08:00
Alan Mishchenko 7adc34ad9e Fixing gap timeout in 'pdr'. 2013-03-07 21:51:26 -08:00
Alan Mishchenko a3bdba6875 Modified command 'init' to allow for specific init values. 2013-03-07 20:38:55 -08:00
Alan Mishchenko 1ce537e992 Misc changes. 2013-03-07 13:04:16 -08:00
Alan Mishchenko 1a6354c22f Improvements to the hierarchy/timing manager. 2013-03-05 17:01:41 -08:00
Alan Mishchenko dcc8907161 Improvements to the hierarchy/timing manager. 2013-03-05 16:53:18 -08:00
Alan Mishchenko 4ff5203f4c Improvements to the hierarchy/timing manager. 2013-03-05 13:13:15 -08:00
Alan Mishchenko 0c9337f627 User-controlable SAT sweeper. 2013-03-04 00:33:36 -08:00
Alan Mishchenko c959cf1ba1 User-controlable SAT sweeper. 2013-03-03 22:43:01 -08:00
Alan Mishchenko b680f12256 User-controlable SAT sweeper. 2013-02-27 13:52:45 -05:00
Alan Mishchenko a27a7bc827 User-controlable SAT sweeper and other small changes. 2013-02-27 12:12:23 -05:00
Alan Mishchenko 236be84149 User-controlable SAT sweeper. 2013-02-27 09:40:45 -05:00
Alan Mishchenko 12253f47ce User-controlable SAT sweeper. 2013-02-26 17:10:37 -05:00
Alan Mishchenko c98119594e User-controlable SAT sweeper. 2013-02-26 16:59:21 -05:00
Alan Mishchenko 88c273c25e User-controlable SAT sweeper. 2013-02-26 15:52:26 -05:00
Alan Mishchenko ceca5da3e9 User-controlable SAT sweeper. 2013-02-26 15:46:54 -05:00
Alan Mishchenko 458c0538d6 User-controlable SAT sweeper. 2013-02-26 15:38:37 -05:00
Alan Mishchenko a1c543c6c9 User-controlable SAT sweeper. 2013-02-26 15:23:04 -05:00
Alan Mishchenko 044d2f0aba User-controlable SAT sweeper. 2013-02-26 14:44:59 -05:00
Alan Mishchenko fc77972625 User-controlable SAT sweeper. 2013-02-26 14:41:09 -05:00
Alan Mishchenko 70ccd477cf User-controlable SAT sweeper. 2013-02-26 14:25:24 -05:00
Alan Mishchenko ef472c6c57 User-controlable SAT sweeper. 2013-02-26 14:18:42 -05:00
Alan Mishchenko 6e65cd1431 User-controlable SAT sweeper. 2013-02-26 14:13:23 -05:00
Alan Mishchenko b1c0b338a0 User-controlable SAT sweeper. 2013-02-26 12:24:07 -05:00
Alan Mishchenko c4b64ed8cc User-controlable SAT sweeper. 2013-02-26 12:21:21 -05:00
Alan Mishchenko 59bc3cb9d9 User-controlable SAT sweeper. 2013-02-26 11:26:40 -05:00
Alan Mishchenko 8e68df2c6a User-controlable SAT sweeper. 2013-02-26 11:23:30 -05:00
Alan Mishchenko d8d1f6c376 User-controlable SAT sweeper. 2013-02-26 10:46:04 -05:00
Alan Mishchenko 7e293ebe08 User-controlable SAT sweeper. 2013-02-25 22:07:32 -05:00
Alan Mishchenko fe3b2e250b User-controlable SAT sweeper. 2013-02-25 17:49:59 -05:00
Alan Mishchenko 95ea102d97 Started PO partitioning command. 2013-02-25 08:20:44 -05:00
Alan Mishchenko 69dd1337b0 Started PO partitioning command. 2013-02-24 09:27:25 -08:00
Alan Mishchenko fdba646b64 Integrating sweeping information. 2013-02-23 17:13:42 -08:00
Alan Mishchenko 7802db98af Integrating sweeping information. 2013-02-23 16:08:10 -08:00
Alan Mishchenko 8281b56e9e Compiler warnings. 2013-02-23 14:01:09 -08:00
Alan Mishchenko 1c744cf10a K-hot STG encoding. 2013-02-23 13:53:22 -08:00
Alan Mishchenko a37737114e Result of merging with the previous change. 2013-02-23 13:12:53 -08:00
Alan Mishchenko e5c60e2b92 K-hot STG encoding. 2013-02-23 12:49:43 -08:00
Alan Mishchenko 2e14b73af6 Allowing for Verilog names of the type slash-<name>-space-[N]. 2013-02-22 13:49:07 -08:00
Alan Mishchenko 91ca83e864 Adding new features to 'dualrail'. 2013-02-21 22:51:25 -08:00
Alan Mishchenko dfe5f511b2 Adding new features to 'dualrail'. 2013-02-21 22:46:53 -08:00
Alan Mishchenko f33c3007b2 Compiler warnings. 2013-02-21 12:22:58 -08:00
Alan Mishchenko dd52905fa3 Enabling two-timeframe property check in the interpolation procedure. 2013-02-21 12:10:35 -08:00
Alan Mishchenko 24823dce0c Integrating sweeping information. 2013-02-20 23:34:27 -08:00
Alan Mishchenko e11c5aa3a0 Integrating sweeping information. 2013-02-20 23:23:50 -08:00
Alan Mishchenko b096809458 Integrating sweeping information. 2013-02-20 23:22:01 -08:00
Alan Mishchenko aa7daf1e51 Integrating sweeping information. 2013-02-20 17:13:29 -08:00
Alan Mishchenko 3e59c102e8 Integrating sweeping information. 2013-02-20 16:21:15 -08:00
Alan Mishchenko 466c4e9992 Integrating hierarchy information (reporting incorrect topological order). 2013-02-20 14:23:00 -08:00
Alan Mishchenko f4c305fc46 Adding STG generation (&era -d) and STG encoding (&read_stg <file>). 2013-02-20 12:52:11 -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 cda61cb2fa Integrating sweeping information. 2013-02-18 23:18:42 -08:00
Alan Mishchenko d415a1adce Integrating packing information. 2013-02-17 19:10:54 -08:00
Alan Mishchenko baa944e6a2 Added 'gap timeout' to pdr. 2013-02-16 14:54:11 -08:00
Alan Mishchenko 4dc7eb6f73 Added 'gap timeout' to bmc3 and sim3. 2013-02-16 13:33:43 -08:00
Alan Mishchenko fd0ff0171e Added 'gap timeout' to bmc3 and sim3. 2013-02-15 16:47:18 -08:00
Alan Mishchenko 8866a1aa6d Fixing performance problem in 'cone -s' 2013-02-13 19:42:11 -08:00
Alan Mishchenko f402293bcd Integration of timing manager. 2013-02-06 19:36:05 +07:00
Alan Mishchenko 930369f36f Integration of timing manager. 2013-02-03 18:02:22 +08:00
Alan Mishchenko 61f8112da0 Corner-case bug fix in PDR. 2013-02-01 23:56:02 +08:00
Alan Mishchenko 6a0dca4535 Integration of timing manager. 2013-02-01 23:55:12 +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
Baruch Sterin e6be7ddfe6 pyabc: allow returning large result from sub processes 2013-01-30 23:50:53 -08:00
Alan Mishchenko e9286513fd Fixing compilation problems on Linux-32 related to constants of type unsigned long long. 2013-01-31 11:07:28 +07:00
Alan Mishchenko 686f8fdaa6 Integration of timing manager. 2013-01-30 19:04:45 +07:00
Alan Mishchenko a2eb6f9a07 Added a fix for the writing an AIG that is not normalized. 2013-01-30 17:26:04 +07:00
Alan Mishchenko 7e598cd231 Fixing compilation problems on Linux-32 related to constants of type unsigned long long. 2013-01-30 16:15:53 +07:00
Baruch Sterin aaacf57304 pyabc: fix _cex_put to not call Abc_CexDup() twice 2013-01-25 12:50:11 -08:00
Baruch Sterin 43d5435124 pyabc: deal better with null counter examples and remove special case handling 2013-01-25 03:36:57 -08:00
Alan Mishchenko 4aa434ad11 Updated CEX code to handle trivial CEX of the type (Abc_Cex_t*)1. 2013-01-25 14:16:31 +07:00
Alan Mishchenko 557448400e Added new Python API is_const_po( int iPoNum ), which returns 0/1 if current network is an AIG and the given PO has const 0/1 function. 2013-01-25 10:25:34 +07:00
Alan Mishchenko fde8c8b2d0 Added switch &trim -V <num> to remove const POs with specific value <num>. 2013-01-25 10:02:11 +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 aa9c87cf8d Extending verification status file format to allow for SAT status without CEX. 2013-01-25 05:59:56 +07:00
Alan Mishchenko 4bd54729d7 Integration of timing manager. 2013-01-25 05:57:52 +07:00
Alan Mishchenko 4efc89d342 Enabled detecting CEXes in multiple POs without stopping (sim3 -a). 2013-01-23 16:50:45 +07:00
Alan Mishchenko dfd871c24d Integration of timing manager. 2013-01-23 13:57:05 +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 70655d5d31 Integration of timing manager. 2013-01-23 01:34:34 +07:00
Alan Mishchenko 8287b05a09 Reintroduced the old abstraction procedure Saig_ManCexAbstractionFlops() formerly called from &abs_start for backward compatibility. 2013-01-08 14:46:13 +08:00
Alan Mishchenko 19749cb8f8 Fixing C++ compilation issues. 2013-01-08 14:19:42 +08:00
Alan Mishchenko a3b5a6ab4a Fixing C++ compilation issues. 2013-01-08 14:18:13 +08:00
Alan Mishchenko 1b6662ce4a Fixing C++ compilation issues. 2013-01-08 14:16:59 +08:00
Alan Mishchenko 562b612691 Fixing C++ compilation issues. 2013-01-08 14:15:39 +08: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 621599fce6 Fixing C++ compilation issues. 2013-01-08 13:28:58 +08:00
Alan Mishchenko 25e27a3a3e Fixing C++ compilation issues. 2013-01-08 13:27:00 +08:00
Alan Mishchenko 1780130f08 Fixing C++ compilation issues. 2013-01-08 13:25:06 +08:00
Alan Mishchenko 394bc276d2 Fixing C++ compilation issues. 2013-01-08 13:23:52 +08:00
Alan Mishchenko b6ab511310 Fixing C++ compilation issues. 2013-01-08 13:19:55 +08:00
Alan Mishchenko 08a9f58aba Fixing C++ compilation issues. 2013-01-08 13:17:15 +08:00
Alan Mishchenko 81a1d97079 Fixing C++ compilation issues. 2013-01-08 13:14:45 +08:00
Alan Mishchenko a8dad4ed61 Fixing C++ compilation issues. 2013-01-08 13:12:28 +08:00
Alan Mishchenko a2c718fcd7 Technology mapper. 2013-01-08 06:44:48 +08:00
Alan Mishchenko a0819f62ab Adding support of flops to the conversion of MiniAIG into ABC network. 2013-01-08 06:42:25 +08:00
Alan Mishchenko 64e907d153 Technology mapper. 2013-01-08 05:51:36 +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 62a4e2f157 Improvements to DSD manager. 2012-12-15 23:19:37 -08:00
Alan Mishchenko bfad654205 Assembling timing/hierarchy manager from input data. 2012-12-15 17:39:34 -08:00
Alan Mishchenko 82050bbe11 Assembling timing/hierarchy manager from input data. 2012-12-13 15:18:53 -08:00
Alan Mishchenko 5ef3c1db3a Unifification of custom extensions. 2012-12-13 10:17:56 -08:00
Alan Mishchenko b2bd941a7e Unifification of custom extensions. 2012-12-13 10:15:32 -08:00
Alan Mishchenko 5a8f8b8aa4 Unifification of custom extensions. 2012-12-13 10:11:39 -08:00
Alan Mishchenko f0d961c825 Unifification of custom extensions. 2012-12-13 10:02:35 -08:00
Alan Mishchenko 72d1151231 Improvements to DSD manager. 2012-12-11 22:37:34 -08:00
Alan Mishchenko ff62cd8349 Improvements to DSD manager. 2012-12-10 18:36:20 -08:00
Alan Mishchenko f35848ed97 Improvements to DSD manager. 2012-12-10 18:03:32 -08:00
Alan Mishchenko da9d1761c9 Improvements to DSD manager. 2012-12-10 17:27:38 -08:00
Alan Mishchenko ad67f4ef25 Assembling timing/hierarchy manager from input data. 2012-12-10 16:04:01 -08:00
Alan Mishchenko 2575a5d683 Unifification of custom extensions. 2012-12-10 13:56:40 -08:00
Alan Mishchenko f7b7ab59cf Retiring old 'fpga' command and package. 2012-12-10 01:14:55 -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 8355eb1d41 Enabling multi-output solving in 'pdr'. 2012-12-09 17:52:34 -08:00
Alan Mishchenko ce63869fe7 Enabling multi-output solving in 'pdr'. 2012-12-09 17:33:44 -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 9fc1cd0b3f Enabling multi-output solving in 'pdr'. 2012-12-09 15:12:40 -08:00
Alan Mishchenko 58d4012a55 Enabling multi-output solving in 'pdr'. 2012-12-09 14:46:16 -08:00
Alan Mishchenko 9f396a0d7e Enabling multi-output solving in 'pdr'. 2012-12-09 10:11:52 -08:00
Alan Mishchenko 8a08453af2 Corner-case bug fix in &rpm. 2012-12-09 10:05:34 -08:00
Alan Mishchenko b65ae7349a Enabling multi-output solving in 'pdr'. 2012-12-09 09:47:48 -08:00
Alan Mishchenko 79aa1f00d6 Deriving CEX after phase/tempor/reparam. 2012-12-09 08:19:00 -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 5d74635f7b Restoring correct behavior of 'tempor' after a change in counting BMC frames in 'bmc2'. 2012-12-07 22:07:47 -08:00
Alan Mishchenko 7b9132311e Removed useless code from the sizing package. 2012-12-04 18:59:09 -08:00
Alan Mishchenko 8c04d9501f Making 'scorr -c' applicable to seq benchmarks without constraints. 2012-12-04 18:35:44 -08:00
Alan Mishchenko fe694d38e3 DSD manager. 2012-12-02 15:59:54 -08:00
Alan Mishchenko f1749fa594 Enabling additional stat printouts. 2012-12-02 01:44:17 -08:00
Alan Mishchenko 4d67a04b19 Enabling additional stat printouts. 2012-12-02 01:25:53 -08:00
Alan Mishchenko a797ea0cc7 Enabling additional stat printouts. 2012-12-02 00:00:29 -08:00
Alan Mishchenko 86fcba60c2 Enabling command &append for combiming multiple AIGs. 2012-12-01 23:13:24 -08:00
Alan Mishchenko 01bea8ef3a Enabling additional stat printouts. 2012-12-01 22:16:22 -08:00
Alan Mishchenko 2469058bb4 Counter-example analysis and optimization. 2012-12-01 19:49:19 -08:00
Alan Mishchenko 9b6ec8e84f Counter-example analysis and optimization. 2012-11-30 17:24:09 -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 c48e3c7ab4 Counter-example analysis and optimization. 2012-11-29 13:34:07 -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 d671adbb86 DSD manager. 2012-11-16 17:04:01 -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 ddab80aea4 Isolating BMC code into a separate package. 2012-11-14 14:00:47 -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 abefcf8fc8 DSD manager. 2012-11-13 20:44:34 -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 e779b8c889 Improved DSD. 2012-11-11 21:37:27 -08:00
Alan Mishchenko e52dc77430 Improved DSD. 2012-11-11 14:40:42 -08:00
Alan Mishchenko 1116313d28 Improved DSD. 2012-11-11 14:38:24 -08:00
Alan Mishchenko 21e6a59ed8 Improved DSD. 2012-11-11 13:26:36 -08:00
Alan Mishchenko 1bef28e6c6 Improved DSD. 2012-11-10 20:45:16 -08:00
Alan Mishchenko ee789ba902 Improved DSD. 2012-11-10 19:37:53 -08:00
Alan Mishchenko e0f27f5ac3 Improved DSD. 2012-11-10 17:26:01 -08:00
Alan Mishchenko fdcbb2cf37 Performance bug fix in choice generation. 2012-11-09 12:43:03 -08:00
Alan Mishchenko aa2c7c0546 Enabling verbose report of dumping abstraction in GLA. 2012-11-07 12:05:39 -08:00
Alan Mishchenko 36d8c000a4 Slightly improved cut computation. 2012-11-06 22:08:54 -08:00
Alan Mishchenko 5ed242ac54 Improved DSD. 2012-11-06 20:41:15 -08:00
Alan Mishchenko ac343478e7 Improved DSD. 2012-11-06 20:28:27 -08:00
Alan Mishchenko 2fbb4b1826 Improved DSD. 2012-11-06 20:27:31 -08:00
Alan Mishchenko db7852bba7 Improvements to LMS code. 2012-11-06 18:04:23 -08:00
Alan Mishchenko 3f7f497351 Improved DSD. 2012-11-06 16:32:58 -08:00
Alan Mishchenko cb5e2308b2 Improved DSD. 2012-11-03 14:27:28 -07:00
Alan Mishchenko 7ba37f4901 Improved DSD. 2012-11-03 00:38:17 -07:00
Alan Mishchenko 7e9f0df3f7 Bug fix in semi-canonical form computation. 2012-11-02 21:55:29 -07:00
Alan Mishchenko c899645b10 Adding dumping truth tables from LMS manager. 2012-11-02 18:59:14 -07:00
Alan Mishchenko b9c22ba99a Improved DSD. 2012-11-02 14:24:22 -07:00
Alan Mishchenko 96d3348d8f Fixing out-of-bound problem when collecting GIA nodes. 2012-11-02 12:02:16 -07:00