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

1499 Commits

Author SHA1 Message Date
Alan Mishchenko 2f3a9f91e5 Bug fix when &vta returns empty absraction. 2012-06-29 12:38:36 -07:00
Alan Mishchenko 5d5ff3b99e Bug fix in &gla -d. 2012-06-29 12:19:48 -07:00
Alan Mishchenko a3a1810ab0 Improving printouts in &vta and &gla. 2012-06-28 23:56:45 -07:00
Alan Mishchenko 051cc64ee2 Gate level abstraction (command &gla). 2012-06-28 23:06:07 -07:00
Alan Mishchenko 311486d910 Gate level abstraction (command &gla). 2012-06-28 17:06:02 -07:00
Alan Mishchenko 520c436d28 Gate level abstraction (command &gla). 2012-06-28 16:44:03 -07:00
Alan Mishchenko 27c3ff1f9b New computation of tents for GIA package. 2012-06-28 10:41:15 -07:00
Alan Mishchenko 7629fd6aea Added min-cut-based refinement of gate-level abstraction (command &gla_refine). 2012-06-24 18:45:42 -07:00
Alan Mishchenko 735a831e13 Added memory reporting to &vta. 2012-06-22 10:30:22 -07:00
Alan Mishchenko 3c0a9e0862 Switch -A <file_name> to specify file name for dumping abstrated model with &vta -d. 2012-06-21 20:20:26 -07:00
Alan Mishchenko 675b0892a8 Reporing memory usage by the SAT solver in 'bmc3'. 2012-06-15 09:51:33 -07:00
Alan Mishchenko 2f1f0ac93d Minor change to prevent assertion failure when verifying required times. 2012-06-15 08:45:12 -07:00
Alan Mishchenko 082d27ede8 Added option to compile on windows without DLL support. 2012-06-15 08:39:46 -07:00
Alan Mishchenko 98d9d5a61f Added warning when a command is missing 2012-06-15 08:37:56 -07:00
Alan Mishchenko 034fc5a14d Misc changes. 2012-05-21 23:52:05 +07:00
Alan Mishchenko 77b83074e0 Changing 'if' to allow for delay optimization on sequential paths only. 2012-05-20 22:18:23 +07:00
Alan Mishchenko c6af9094c0 Changing 'if' to allow for delay optimization on sequential paths only. 2012-05-20 17:27:53 +07:00
Alan Mishchenko 38214f01c2 Do not allow quitting bmc3 after exploring 2^<num_ff> frames if jump-forward is enabled. 2012-05-20 16:41:01 +07:00
Alan Mishchenko 6ecc71f8f9 Misc changes. 2012-05-19 16:37:32 +07:00
Alan Mishchenko 37a3e07d91 Prevent network from being unmapped after equivalence checking. 2012-05-15 15:36:51 +07:00
Alan Mishchenko 54670783e0 Better resolution of CO drivers. Should impact the QoR after 'if'. 2012-05-15 15:28:42 +07:00
Alan Mishchenko 76539c1956 Added generation of multipliers in 'gen'. 2012-05-15 09:34:24 +07:00
Alan Mishchenko 675437b214 Preventing 'show' from unmapping the network. 2012-05-14 19:55:40 +07:00
Alan Mishchenko e37fb952da Included copyright statement into 'main.c'. 2012-05-11 09:26:36 +07:00
Alan Mishchenko 7452455155 Changing the rules of assigning the names when AIG is converted into a logic network. 2012-05-11 08:35:54 +07:00
Alan Mishchenko aa087d2513 Making sure cec -n and dsec -n do not remove the I/O names in the current network. 2012-05-08 13:37:19 +08:00
Alan Mishchenko 50fac8a098 Bug fix in fraig_restore. 2012-05-06 22:52:56 +08:00
Alan Mishchenko d4399dbf92 Misc changes. 2012-05-03 19:54:40 +08:00
Alan Mishchenko 32b0762546 Preventing &iso from removing fanoutless PIs. 2012-05-03 04:54:06 +08:00
Alan Mishchenko e6b16e27d1 Misc changes. 2012-05-02 17:42:56 +08:00
Alan Mishchenko a9807a759e Bug fixes in previous bug fixes related to &trim. 2012-05-01 09:04:23 +08:00
Alan Mishchenko 959ac60956 Misc changes. 2012-05-01 08:04:31 +08:00
Alan Mishchenko e9b7c703b3 Added supporting dual-output seq miters in &trim (bug fix). 2012-04-30 23:38:34 +08:00
Alan Mishchenko 2c6faa0607 Compilation problem caused by multiple declarations. 2012-04-28 16:04:17 +07:00
Alan Mishchenko 490e84c4bc Adding on-the-fly truth-table minimization. 2012-04-28 12:09:38 +07:00
Alan Mishchenko 334911a116 Added supporting dual-output seq miters in &trim. 2012-04-28 05:36:38 +07:00
Alan Mishchenko d1e82047ff Added supporting dual-output seq miters in &iso. 2012-04-28 05:08:07 +07:00
Alan Mishchenko 78855cc952 Added supporting dual-output seq miters in &trim. 2012-04-28 04:19:26 +07:00
Alan Mishchenko 8a89f1c3f6 Added supporting dual-output seq miters in &iso. 2012-04-28 02:24:34 +07:00
Alan Mishchenko 2bf7454b41 Added supporting dual-output seq miters in &iso. 2012-04-28 02:21:06 +07:00
Alan Mishchenko a4baba2c83 Misc changes. 2012-04-27 16:26:41 +07:00
Alan Mishchenko 590202e327 Set the failed output index if ORing of outputs was done in 'int'. 2012-04-27 16:14:40 +07:00
Alan Mishchenko ce03d5ab28 Writing status file vta.status when dumping intermediate abstraction in &vta. 2012-04-27 08:26:40 +07:00
Alan Mishchenko 5f5dda9030 Updating the counter of finished frames when dumping intermediate abstraction in &vta. 2012-04-27 07:46:02 +07:00
Alan Mishchenko 92da248e9a Disallow the circiut-based solver in &scorr to run with more than 1000 conflicts. 2012-04-24 15:49:40 -07:00
Alan Mishchenko b8088b901d Misc changes. 2012-04-22 23:33:50 -07:00
Alan Mishchenko 74d0ffee69 Misc changes. 2012-04-22 19:14:22 -07:00
Baruch Sterin c4911370bb pyabc: minor fixes to make API changes work 2012-04-20 15:40:28 -07:00
Alan Mishchenko e822a1f8c7 Added Python APIs for node/level counts. 2012-04-20 10:32:29 -07:00
Alan Mishchenko 73789120c1 Misc changes. 2012-04-20 10:12:29 -07:00
Alan Mishchenko 3f6bb881c0 Adding dumping abstractions in &vta. 2012-04-15 14:51:06 -07:00
Alan Mishchenko 5c683fc164 Adding iterative refinement to 'addbuffs'. 2012-04-14 15:06:41 -07:00
Alan Mishchenko 92ad58ffa2 Adding iterative refinement to 'addbuffs'. 2012-04-13 18:20:44 -07:00
Alan Mishchenko 7e21f01269 Updated used message for 'back_reach'. 2012-04-13 15:41:31 -07:00
Alan Mishchenko 85f6d2526e Bug fix in SOP balancing with structural choices. 2012-04-12 20:19:47 -07:00
Alan Mishchenko b1a57b2ae9 Adding iterative refinement to 'addbuffs'. 2012-04-11 16:29:08 -07:00
Alan Mishchenko 0184dab4de Adding iterative refinement to 'addbuffs'. 2012-04-11 16:00:09 -07:00
Alan Mishchenko 0d802453e4 Adding reverse order to 'addbuffs'. 2012-04-11 08:09:31 -07:00
Alan Mishchenko f16457aaf5 Added/moved several APIs. 2012-04-10 00:28:36 -07:00
Alan Mishchenko f380bb5ac1 Improving printouts of critical path. 2012-04-09 20:01:40 -07:00
Alan Mishchenko b9913732c4 Improving printouts of critical path. 2012-04-09 18:59:36 -07:00
Alan Mishchenko 0509440a45 Improving printouts of critical path. 2012-04-09 15:06:33 -07:00
Alan Mishchenko e908ff1cb9 Improving printouts of critical path. 2012-04-09 11:46:42 -07:00
Alan Mishchenko d898059460 Added dumping abstracted model in &vta. 2012-04-07 18:38:20 -07:00
Alan Mishchenko 48b47300e3 Added dumping abstracted model in &vta. 2012-04-07 12:43:17 -07:00
Alan Mishchenko c3d3ccf349 Better interface with the new code. 2012-04-06 22:03:00 -07:00
Alan Mishchenko 2c21e2de0d Improving printouts of critical path. 2012-04-06 13:31:03 -07:00
Alan Mishchenko 5de8e60b9f Improving printouts of critical path. 2012-04-06 12:52:26 -07:00
Alan Mishchenko 8c1513dfbc Improving printouts of critical path. 2012-04-06 00:45:58 -07:00
Alan Mishchenko 993c2027d8 Added several new APIs. 2012-03-31 16:33:22 -07:00
Alan Mishchenko 9520736621 Added several new APIs to GIA and for file management. 2012-03-30 21:09:08 -07:00
Alan Mishchenko 9eb1be8e53 Bug fix in 'addbuffs'. 2012-03-29 15:48:45 -07:00
Alan Mishchenko 38494b41a6 Moving Vec_Set_t to the vector directory. 2012-03-28 10:19:12 -07:00
Alan Mishchenko 265e3e5cd4 Moving Vec_Set_t to the vector directory. 2012-03-28 10:13:42 -07:00
Alan Mishchenko 3992e344ea Logic sharing for multi-input gates (silencing a warning). 2012-03-27 21:59:13 -07:00
Alan Mishchenko a21f2986aa Enabling mapping into multi-input AND/OR gates. 2012-03-27 20:15:02 -07:00
Alan Mishchenko 08253a50eb Logic sharing for multi-input gates (bug fix). 2012-03-26 20:21:05 -07:00
Alan Mishchenko c2ab4426e4 Important bug fix in XOR balancing (balance -x). 2012-03-26 15:01:54 -07:00
Alan Mishchenko a4144cf0d1 Making demiter dump files in the current directory. 2012-03-26 12:55:58 -07:00
Alan Mishchenko 16cf6bf1ca Logic sharing for multi-input gates. 2012-03-26 12:55:20 -07:00
Alan Mishchenko 45f07795ef Logic sharing for multi-input gates. 2012-03-25 23:10:35 -07:00
Alan Mishchenko 8ed3e40a52 Logic sharing for multi-input gates. 2012-03-25 22:47:08 -07:00
Alan Mishchenko 5f075adc19 Logic sharing for multi-input gates. 2012-03-25 16:58:40 -07:00
Alan Mishchenko b4df114e4a Logic sharing for multi-input gates. 2012-03-25 16:49:29 -07:00
Alan Mishchenko 309bcf2dec Logic sharing for multi-input gates. 2012-03-25 01:24:26 -07:00
Alan Mishchenko abb889fe6e Improving printouts of gates and support. 2012-03-24 13:15:37 -07:00
Alan Mishchenko b584fea24a Bug fix in the mapper: using an object after it is deleted. 2012-03-24 11:52:13 -07:00
Alan Mishchenko aede5026b3 Silencing a gcc warning. 2012-03-23 22:55:45 -07:00
Alan Mishchenko 3abd9773a4 Enabled demitering dual-output miters. 2012-03-23 22:52:30 -07:00
Alan Mishchenko 1c31dbe786 Added command 'addbuffs' to create balanced CI/CO paths. 2012-03-23 22:29:25 -07:00
Alan Mishchenko 0792ab0eb6 Additional features for delay optimization 2012-03-21 23:19:49 -07:00
Alan Mishchenko f50ce3dbd9 Switching to a variable-page-size memory manager for clauses and proofs. 2012-03-21 17:13:39 -07:00
Alan Mishchenko 92539a91a0 Added one currently unused iterator. 2012-03-21 15:27:47 -07:00
Alan Mishchenko 0dc699f777 Preventing gcc compilation errors in handling memory pages. 2012-03-21 15:26:09 -07:00
Alan Mishchenko 8f91b30a67 Bug fix to prevent crashing when Abc_Print() is called while ABC is not initialized. 2012-03-20 09:35:33 -07:00
Alan Mishchenko c347f2b90b Alternative way of computing delay in SOP balancing. 2012-03-16 15:43:08 -07:00
Alan Mishchenko aeedc6ace5 Exploration of ISO and minor changes. 2012-03-13 16:12:16 -07:00
Alan Mishchenko 49c13f4f03 Added new procedures to read files. 2012-03-11 23:07:27 -07:00
Alan Mishchenko 795b5a6ce7 Added command 'nodedup' to duplicate nodes with high fanout. 2012-03-11 23:06:14 -07:00
Alan Mishchenko 2e97ffdd1a Updating &test to call full check. 2012-03-10 21:44:32 -08:00
Alan Mishchenko fec988f619 Renamed Aig_ObjPioNum to be Aig_ObjCioId. 2012-03-09 19:59:35 -08:00
Alan Mishchenko c46c957a07 Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)... 2012-03-09 19:50:18 -08:00
Alan Mishchenko 2c8f1a67ec Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ...Ci/Co. 2012-03-09 19:32:44 -08:00
Alan Mishchenko 34078de8d6 Silencing remaining gcc warnings. 2012-03-09 19:18:18 -08:00
Alan Mishchenko 66eb3cf472 Silencing remaining gcc warnings. 2012-03-09 19:08:34 -08:00
Alan Mishchenko 8388f065f4 Do not cancel the current abstraction when a new refinement is discovered in VTA. 2012-03-09 18:57:13 -08:00
Alan Mishchenko 76f3e03cc1 Commenting out verbose statements. 2012-03-08 02:10:20 +01:00
Alan Mishchenko 3634f60d7a Fixing a bug and adding verification of minimized counter-example. 2012-03-06 15:33:16 +01:00
Alan Mishchenko abde9fe948 Fixing a bug and adding verification of minimized counter-example. 2012-03-06 15:30:20 +01:00
Alan Mishchenko f7c7cb5c65 Adding switch '-n' to 'permute' to derive random topological ordering of internal nodes. 2012-03-06 11:53:07 +01:00
Alan Mishchenko 5ad0fea606 Extending memory page size for proof logging. 2012-03-05 09:01:50 +01:00
Niklas Een 12d9aaa7b4 Some fixes for VTA under Bridge. 2012-03-03 11:03:59 -08:00
Niklas Een 5b800e05de Counterexamples now work in Bridge 2012-03-03 10:10:07 -08:00
Niklas Een 929e5e16e6 Some fixes to the Bridge code. More to do. 2012-03-03 08:58:25 -08:00
Niklas Een 1e40c5b79f Removed warning in Abc_Print 2012-03-02 16:28:32 -08:00
Alan Mishchenko 90e95fcb48 Adding features related to the communication bridge. 2012-03-02 15:29:19 -08:00
Alan Mishchenko eb4aa42577 Enabling user-specified required times in 'map'. 2012-03-02 13:50:28 -08:00
Alan Mishchenko a0933b1643 Adding switch -N to 'super' to set an upper bound on the number of supergates generated. 2012-03-02 13:49:49 -08:00
Alan Mishchenko 7e805e5c9a Making GENLIB parser skip LATCHes. 2012-03-02 11:48:13 -08:00
Alan Mishchenko 7fa9de2da4 Redirecting printf messages. 2012-03-02 01:31:44 -08:00
Alan Mishchenko c47dc99a94 Redirecting printf messages. 2012-03-02 01:15:40 -08:00
Alan Mishchenko 4db9c63627 Redirecting printf messages. 2012-03-02 01:06:53 -08:00
Alan Mishchenko 7926d75ecb Adding features related to the communication bridge. 2012-03-02 00:57:48 -08:00
Alan Mishchenko a6f363d461 Created a communication bridge. 2012-03-01 22:36:34 -08:00
Alan Mishchenko 325ac583e6 Created a communication bridge. 2012-03-01 21:20:18 -08:00
Alan Mishchenko 2b39d60f6e Adding switch -N to 'super' to set an upper bound on the number of supergates generated. 2012-03-01 11:18:35 -08:00
Alan Mishchenko b90f1c73ae Adding switch -N to 'super' to set an upper bound on the number of supergates generated. 2012-02-29 16:44:16 -08:00
Alan Mishchenko b30791ba62 Updating 'print_library' to write GENLIB library into a file. 2012-02-29 16:43:28 -08:00
Alan Mishchenko d548040437 Bug fix in a standard cell library generator. 2012-02-29 16:15:31 -08:00
Alan Mishchenko 4b647de7fd Bug fix in a standard cell library generator. 2012-02-29 15:59:18 -08:00
Alan Mishchenko 3e5e7a2544 Added skipping &iso when there is only one PO. 2012-02-29 10:51:05 -08:00
Alan Mishchenko 1bf2b0351a Added skipping &iso when there is only one PO. 2012-02-29 10:38:18 -08:00
Alan Mishchenko d509c0c3a0 Bug fix in 'in' (look at the OR of the interpolants, rather than the last frontier, when K > 1). 2012-02-28 19:14:05 -08:00
Alan Mishchenko 0b1cfe886e Added switch -z to command 'removepo' to enable removing const1 outputs. 2012-02-27 17:50:48 -08:00
Alan Mishchenko c17a22ef8a Disabled verbose print-out in the SAT solvers. 2012-02-26 08:51:14 -08:00
Alan Mishchenko b06908d1e8 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default (bug fix). 2012-02-25 15:54:11 -08:00
Alan Mishchenko 3f525b0d42 Silenced a gcc warning. 2012-02-24 16:18:38 -08:00
Alan Mishchenko b4fe108d86 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. 2012-02-24 16:11:49 -08:00
Alan Mishchenko 3552d39b71 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. 2012-02-24 13:37:31 -08:00
Alan Mishchenko d80f43a185 Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. 2012-02-24 13:21:32 -08:00
Alan Mishchenko 8f4457772a Added a way to disable support for dynamic linking. 2012-02-24 09:44:16 -08:00
Alan Mishchenko c20d29e7e7 Silenced a gcc warning. 2012-02-23 13:49:49 -08:00
Baruch Sterin f42131935e pyabc: silnce more warnings 2012-02-23 13:45:51 -08:00
Baruch Sterin 4ade9fc7c8 pyabc: python 2.6 compatibility fix for previous commit (which silenced warnings) 2012-02-23 13:28:07 -08:00
Baruch Sterin af51bdaf3e pyabc: silenced warnings in gcc 2012-02-23 13:01:17 -08:00
Alan Mishchenko a87a3b4e33 Bug fix in stadard cell library representation. 2012-02-23 11:58:59 -08:00
Baruch Sterin 871684d2a0 pyabc changes with main branch 2012-02-23 11:11:21 -08:00
Baruch Sterin b879786e73 pyabc: added a function pyabc.iso_eq_classes() that retrieves the results of the "&iso" command 2012-02-23 11:09:57 -08:00
Alan Mishchenko 99e7d1d193 Bug fix in stadard cell library representation. 2012-02-23 10:24:01 -08:00
Alan Mishchenko 1d25ae3b1a Experiment with technology mapping. 2012-02-22 17:54:24 -08:00
Alan Mishchenko d2cab85976 Adding flag -s to &put to disable status clearing. 2012-02-22 08:06:22 -08:00
Alan Mishchenko 8ba2398138 Undoing a previuos change to not reset the status after &put. 2012-02-22 00:46:52 -08:00
Alan Mishchenko db3a005402 Experiment with technology mapping. 2012-02-20 21:34:50 -08:00
Alan Mishchenko e60d6c94a3 Experiment with technology mapping. 2012-02-20 21:33:51 -08:00
Alan Mishchenko 18ea60a06b Isomorphism checking code. 2012-02-20 16:43:15 -08:00
Alan Mishchenko 9f71a9f67b Isomorphism checking code. 2012-02-20 16:09:20 -08:00
Alan Mishchenko e43ca9f850 Isomorphism checking code. 2012-02-19 15:05:59 -08:00
Alan Mishchenko 2377ae60e9 Isomorphism checking code. 2012-02-19 14:52:43 -08:00
Alan Mishchenko ea13085fe3 Added printout of BMC tents in &ps. 2012-02-19 13:33:21 -08:00
Alan Mishchenko c2b2e99284 Added QuickSort based on 3-way partitioning. 2012-02-19 13:19:35 -08:00
Alan Mishchenko 596bbbe6dc Added QuickSort based on 3-way partitioning. 2012-02-19 13:16:51 -08:00
Alan Mishchenko 9aab58f601 Isomorphism checking code. 2012-02-19 12:57:58 -08:00
Alan Mishchenko af8cac095d Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity). 2012-02-19 10:41:16 -08:00
Alan Mishchenko c9147d76cc Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity). 2012-02-19 09:55:52 -08:00
Alan Mishchenko 7ca9c116df Isomorphism checking code. 2012-02-18 19:20:02 -08:00
Alan Mishchenko 78cad5e176 Isomorphism checking code. 2012-02-17 23:26:20 -08:00
Alan Mishchenko 97a2e6f29e Isomorphism checking code. 2012-02-17 19:04:28 -08:00
Alan Mishchenko 5d7c568589 Changes to properly save current GIA after &miter -t and not erase the comb cex after &put. 2012-02-17 15:51:12 -08:00
Alan Mishchenko ee9f66e2c4 Isomorphism checking code. 2012-02-17 13:19:09 -08:00
Alan Mishchenko f2a413029c Silencing some of the gcc warnings. 2012-02-17 12:46:08 -08:00
Alan Mishchenko 82cd6ae7cc Silencing some of the gcc warnings. 2012-02-17 00:55:58 -08:00
Alan Mishchenko 32eb2e223d Silencing some of the gcc warnings. 2012-02-17 00:53:07 -08:00
Alan Mishchenko fe2d7d9612 Silencing some of the gcc warnings. 2012-02-17 00:24:38 -08:00
Alan Mishchenko 4743884de4 Silencing some of the gcc warnings. 2012-02-17 00:12:53 -08:00
Alan Mishchenko 2d316b86e2 Silencing some of the gcc warnings. 2012-02-17 00:06:39 -08:00
Alan Mishchenko 97856d021a Silencing some of the gcc warnings. 2012-02-16 23:40:23 -08:00
Alan Mishchenko 791b107e7a Silencing some of the gcc warnings. 2012-02-16 21:53:16 -08:00
Alan Mishchenko 16dc02e7f6 Improved memory management of proof-logging and propagated changes. 2012-02-16 20:54:41 -08:00
Alan Mishchenko f1dba69c57 Improved memory management of proof-logging and propagated changes. 2012-02-16 14:23:52 -08:00
Alan Mishchenko ce945006e1 Changing how BMC report runtime. 2012-02-16 00:28:33 -08:00
Alan Mishchenko 8587ebe797 Variable timeframe abstraction. 2012-02-16 00:11:09 -08:00
Alan Mishchenko ecd14d4daf Isomorphism checking code. 2012-02-15 18:40:05 -08:00
Alan Mishchenko e405d71398 Isomorphism checking code. 2012-02-14 22:16:01 -08:00
Alan Mishchenko a9980135a0 Isomorphism checking code. 2012-02-14 22:15:49 -08:00
Alan Mishchenko faa934e2e6 Added restarts to PDR. 2012-02-14 00:17:01 -08:00
Alan Mishchenko 77b5dc261e Added restarts to PDR. 2012-02-13 23:31:01 -08:00
Alan Mishchenko e0650dce0a Timeout crash fix in 'reachy'. 2012-02-13 21:10:15 -08:00
Alan Mishchenko 59ea100dbf Variable timeframe abstraction. 2012-02-13 20:40:38 -08:00
Alan Mishchenko d931de7feb Variable timeframe abstraction. 2012-02-13 20:03:55 -08:00
Alan Mishchenko 6f4bb33ce1 Variable timeframe abstraction. 2012-02-13 14:35:00 -08:00
Alan Mishchenko f80841a5fd Variable timeframe abstraction. 2012-02-13 14:17:01 -08:00
Alan Mishchenko d0713831a0 Lazy man's logic synthesis. 2012-02-12 17:30:05 -08:00
Alan Mishchenko 9f331ae915 Isomorphism checking code. 2012-02-12 15:45:07 -08:00
Alan Mishchenko d9edb7e549 Variable timeframe abstraction. 2012-02-12 02:16:36 -08:00
Alan Mishchenko 862ebb214d Variable timeframe abstraction. 2012-02-11 22:54:59 -08:00
Alan Mishchenko 49c5beefd4 Variable timeframe abstraction. 2012-02-11 22:30:04 -08:00
Alan Mishchenko 95d7b478fd Variable timeframe abstraction. 2012-02-11 21:56:05 -08:00
Alan Mishchenko 309ab1c12b Variable timeframe abstraction. 2012-02-11 20:48:23 -08:00
Alan Mishchenko d81aa6d697 Variable timeframe abstraction. 2012-02-11 19:32:45 -08:00
Baruch Sterin 33261c33cb pyabc: replace 'bool' with 'int' as it was removed from the rest of ABC 2012-02-11 15:01:55 -08:00
Alan Mishchenko c395afe225 Graph isomorphism checking code. 2012-02-11 14:13:11 -08:00
Alan Mishchenko 112f797c73 Added switch -f to 'print_io' to suppress printing flops. 2012-02-11 00:43:37 -08:00
Alan Mishchenko c5067f7d04 Graph isomorphism checking code. 2012-02-11 00:22:05 -08:00
Alan Mishchenko 71891354b4 Bug fixes in &cec command. 2012-02-10 00:07:31 -08:00
Alan Mishchenko b186f362a7 Bug fix in flop-level abstraction refinement. 2012-02-09 13:38:09 -08:00
Alan Mishchenko 274e8ada94 Removed unused 'bool' definition and unused memory management macros. 2012-02-07 19:59:14 -08:00
Alan Mishchenko 25859eefb6 Graph isomorphism checking code. 2012-02-02 15:45:48 -08:00
Alan Mishchenko 16fd67f0ab Trying to fix a false-positive due to incorrect inductive termination check in 'int' when K is more than 1 (not fixed yet). 2012-02-01 14:54:32 -08:00
Alan Mishchenko 61211df4ff Lazy man's logic synthesis. 2012-02-01 12:24:04 -08:00
Alan Mishchenko 5004aa1940 Graph isomorphism checking code. 2012-01-30 23:16:40 -08:00
Alan Mishchenko 044149593d Graph isomorphism checking code. 2012-01-30 23:11:38 -08:00
Alan Mishchenko 7ea40494eb Graph isomorphism checking code. 2012-01-29 21:22:54 -08:00
Alan Mishchenko e511b87237 Moving Vec_IntPrint to where it belongs. 2012-01-29 21:22:26 -08:00
Alan Mishchenko 5e91f13247 Variable timeframe abstraction. 2012-01-28 23:17:31 -08:00
Alan Mishchenko 095bf1c91b Variable timeframe abstraction. 2012-01-28 23:03:25 -08:00
Alan Mishchenko 5e1c28338b Generation of dual-rail miter. 2012-01-28 21:09:31 -08:00
Alan Mishchenko 99b408fcb1 Generation of dual-rail miter. 2012-01-28 20:10:34 -08:00
Alan Mishchenko 5aeab257ed Generation of dual-rail miter. 2012-01-28 15:05:33 -08:00
Alan Mishchenko a2df331852 Variable timeframe abstraction. 2012-01-28 13:48:48 -08:00
Alan Mishchenko 7a87f20c18 Variable timeframe abstraction. 2012-01-27 00:57:42 -08:00
Alan Mishchenko ce0e8caf79 Variable timeframe abstraction. 2012-01-27 00:48:06 -08:00
Alan Mishchenko c7e855619a Variable timeframe abstraction. 2012-01-24 14:39:49 -08:00
Alan Mishchenko 94d35a2592 Variable timeframe abstraction. 2012-01-24 01:04:56 -08:00
Alan Mishchenko f8e933c718 Variable timeframe abstraction. 2012-01-23 13:45:46 -08:00
Alan Mishchenko c39fd3741a Added returning counter-example after BMC, which was recently added to 'dprove'. 2012-01-23 12:41:55 -08:00
Alan Mishchenko 14457af21a Bug fix for incorrect memory allocation in main SAT solver, leading to crashes in 'dsec' (correction to the previous fix). 2012-01-23 12:21:29 -08:00
Alan Mishchenko 3906e37c12 Bug fix for incorrect memory allocation in main SAT solver, leading to crashes in 'dsec'. 2012-01-22 22:24:23 -08:00
Alan Mishchenko fb918249ca Variable timeframe abstraction. 2012-01-21 22:57:18 -08:00
Baruch Sterin 6e72e2fb35 pyabc: adapt build to recent changes in the rest of ABC 2012-01-21 18:21:03 -08:00
Alan Mishchenko 8014f25f6d Major restructuring of the code. 2012-01-21 04:30:10 -08:00
Alan Mishchenko c44cc5de94 Deleting file added by mistake. 2012-01-20 20:30:24 -08:00
Alan Mishchenko 2c50c2c5c0 Preserving CI/CO varible names when moving between the main space and &-space. 2012-01-20 19:54:26 -08:00
Alan Mishchenko 7d4545126d Variable timeframe abstraction. 2012-01-20 19:04:01 -08:00
Alan Mishchenko 719b06f912 Variable timeframe abstraction. 2012-01-20 17:55:34 -08:00
Alan Mishchenko b9163754b7 New hierarchy manager. 2012-01-20 09:52:38 -08:00
Alan Mishchenko ec1c45fb64 New hierarchy manager. 2012-01-19 21:09:49 -08:00
Alan Mishchenko 215d62f41f New hierarchy manager. 2012-01-19 17:18:11 -08:00
Alan Mishchenko fffd733f94 Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to control BMC frames and conflicts. 2012-01-19 14:24:56 -08:00
Alan Mishchenko 0111d43b54 New hierarchy manager. 2012-01-19 12:02:07 -08:00
Alan Mishchenko 8c62c9db6c Added switch 'write_counter -f' to output flop values in each time frame. 2012-01-18 17:49:13 -08:00
Alan Mishchenko debe445063 New hierarchy manager. 2012-01-18 17:28:59 -08:00
Alan Mishchenko fe6d1ff7da New hierarchy manager. 2012-01-18 02:25:12 -08:00
Alan Mishchenko 2fd746ed94 Removing debug print-outs from the SAT solver. 2012-01-17 23:57:02 -08:00
Alan Mishchenko 2a236864ab Changes to the lazy man's synthesis code. 2012-01-17 23:38:11 -08:00
Alan Mishchenko d8d705c717 New hierarchy manager. 2012-01-17 23:19:47 -08:00
Alan Mishchenko 67300e056b Small bug induced by changes in the SAT solver. 2012-01-17 23:09:19 -08:00
Alan Mishchenko 25914e417a Added notification about exceeding the number of nodes. 2012-01-17 22:40:40 -08:00
Alan Mishchenko 6bff2986a2 New hierarchy manager. 2012-01-17 15:02:25 -08:00
Alan Mishchenko 940d5d66b2 Variable timeframe abstraction. 2012-01-16 22:07:09 -08:00
Alan Mishchenko be5256c926 New hierarchy manager. 2012-01-16 22:06:59 -08:00
Alan Mishchenko 08f6d49fb7 Removing additional printout in the GIA package. 2012-01-16 13:29:47 -08:00
Alan Mishchenko 0695ec5473 New hierarchy manager plus additional printout in the GIA package. 2012-01-16 13:07:51 -08:00
Alan Mishchenko ca28f77f3a Variable timeframe abstraction. 2012-01-16 12:21:53 -08:00
Alan Mishchenko 10478a9cbf Variable timeframe abstraction. 2012-01-15 20:47:58 -08:00
Alan Mishchenko bb4897aba6 Changes to the lazy man's synthesis code. 2012-01-15 12:35:04 -08:00
Alan Mishchenko 1f0e5533dc Several small bug fixes in the mapper. 2012-01-15 09:15:10 -08:00
Alan Mishchenko 60a84f7350 Changes to the lazy man's synthesis code. 2012-01-14 23:39:53 -08:00
Alan Mishchenko 868ed19469 Changes to the lazy man's synthesis code. 2012-01-14 22:37:25 -08:00
Alan Mishchenko ac7e665bf6 Bug fixes in the Verilog parser. 2012-01-14 22:21:23 -08:00
Alan Mishchenko c7e215ca31 New hierarchy manager. 2012-01-14 18:05:12 -08:00
Alan Mishchenko 9c409addca Support computation experiments with different network data-structures. 2012-01-14 18:04:47 -08:00
Alan Mishchenko 4748f6988e Small bug fix in printing DSD for Boolean functions. 2012-01-14 18:03:06 -08:00
Alan Mishchenko 7a3c33e169 New hierarchy manager. 2012-01-13 22:49:08 -08:00
Alan Mishchenko 5fff8354ce New hierarchy manager. 2012-01-13 22:02:04 -08:00
Alan Mishchenko b7ba9aa8dc New hierarchy manager. 2012-01-13 20:58:28 -08:00
Alan Mishchenko 37b8a190ba Improving printout in the SAT solver. 2012-01-13 20:57:26 -08:00
Alan Mishchenko c48925dfb6 Commented out a printout line which cases a warning to be printed. 2012-01-13 19:34:00 -08:00
Alan Mishchenko 1aeaacc03d Added bit vector. 2012-01-13 19:31:58 -08:00
Alan Mishchenko 4bd7efa6cd Added counting hits and misses during structural hashing. 2012-01-13 19:31:13 -08:00
Alan Mishchenko edbff75fff New hierarchy manager. 2012-01-13 18:10:00 -08:00
Alan Mishchenko eecbbea24b New hierarchy manager. 2012-01-13 17:50:21 -08:00
Alan Mishchenko 095345fc4a Added new name manager and modified hierarchy manager to use it. 2012-01-13 15:43:09 -08:00
Alan Mishchenko cb2d12bb04 New hierarchy manager. 2012-01-13 00:34:13 -08:00
Alan Mishchenko 2e1dcdd239 Added model ID inside the design. 2012-01-12 23:29:47 -08:00
Alan Mishchenko 56cc5734a4 Bug fix related to not properly resizing SAT solver's model array. 2012-01-12 07:28:01 -08:00
Alan Mishchenko fadde52dc6 Changes to the lazy man's synthesis code. 2012-01-11 22:08:35 -08:00
Alan Mishchenko 22ae2e452a Gate level abstraction. 2012-01-11 14:51:00 -08:00
Alan Mishchenko 564a3553f0 Gate level abstraction. 2012-01-08 13:15:03 +07:00
Alan Mishchenko 03f772d50a Backward reachability using circuit cofactoring. 2012-01-08 09:35:09 +07:00
Alan Mishchenko d1450e7733 Backward reachability using circuit cofactoring. 2012-01-07 21:12:27 +07:00
Alan Mishchenko c3ab7843bb Backward reachability using circuit cofactoring. 2012-01-07 21:04:36 +07:00
Alan Mishchenko 99cc6ae9d2 Crash fix in 'tempor' in case the leading length is 0. 2012-01-07 20:29:11 +07:00
Alan Mishchenko 36bc5703ad Gate level abstraction. 2012-01-07 12:11:25 +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 10ad89490a Bug fix related to not properly resizing SAT solver's model array. 2012-01-06 11:34:06 +07:00
Alan Mishchenko 26b87c8c55 Added warning when the network from file has no primary inputs. 2012-01-06 01:36:08 +07:00
Alan Mishchenko 5a45a75dca APIs to represent simple gates in CNF. 2012-01-05 19:19:13 +07:00
Alan Mishchenko fd62957d39 Backward reachability using circuit cofactoring. 2012-01-05 18:48:11 +07:00
Alan Mishchenko 32e7b75829 APIs to represent simple gates in CNF. 2012-01-05 13:15:05 +07:00
Alan Mishchenko 660779b53c Configuration changes in the Boolean matching code. 2012-01-05 13:14:04 +07:00
Alan Mishchenko e3a412b2e7 Backward reachability using circuit cofactoring. 2012-01-01 15:58:49 +07:00
Alan Mishchenko aec5d33889 Backward reachability using circuit cofactoring. 2012-01-01 15:58:17 +07:00
Alan Mishchenko 1e20e2ccbc Delay optimization using precomputed library. 2011-12-30 13:11:52 +07:00
Alan Mishchenko 655d452cbb Delay optimization using precomputed library. 2011-12-30 11:36:25 +07:00
Alan Mishchenko 6ed8340226 Delay optimization using precomputed library. 2011-12-30 11:27:12 +07:00
Alan Mishchenko 64b8aa51e9 Delay optimization using precomputed library. 2011-12-30 09:54:30 +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 21df8bf021 Experiments with flattening hierarchy. 2011-12-28 22:16:04 +07:00
Alan Mishchenko c59e2e9c96 Transforming the solver to use different clause representation. 2011-12-23 21:45:23 -08:00
Alan Mishchenko 7facbc3cc9 Transforming the solver to use different clause representation. 2011-12-23 10:23:45 -08:00
Alan Mishchenko 94174d0f04 Transforming the solver to use different clause representation. 2011-12-23 00:43:31 -08:00
Alan Mishchenko 9d2893040e Transforming the solver to use different clause representation. 2011-12-23 00:29:26 -08:00
Alan Mishchenko 844c385e2b Transforming the solver to use different clause representation. 2011-12-22 15:38:06 -08: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 82a2495ce9 Improvements to hierarchical BLIF parser. 2011-12-22 14:26:03 -08:00
Alan Mishchenko b3c9609e82 Improvements to hierarchical BLIF parser. 2011-12-21 12:56:28 -08:00
Alan Mishchenko 3418a8820a Fixed a bug in matching code. 2011-12-17 17:51:13 -08:00
Alan Mishchenko cd4752b565 Added utility to sort lines in a file alphabetically. 2011-12-17 13:57:56 -08:00
Alan Mishchenko 024f9a2b13 Performance improvement in 'dch' for designs having nodes with many fanouts. 2011-12-15 19:32:53 -08:00
Alan Mishchenko f67cb76dff Added optional printout of the hierarchy structure before collapsing. 2011-12-15 19:32:05 -08:00
Alan Mishchenko 8404ecda54 Undoing temporary change to the solver. 2011-12-15 17:05:38 -08:00
Alan Mishchenko 4d000265f6 Temporary change to the solver. 2011-12-15 16:47:28 -08:00
Alan Mishchenko 4a7ef41db2 Adding switch '-W' to fx to control the quality of extracted divisors. 2011-12-15 15:46:32 -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 c80c0cc6c9 Trying to make sorting of nodes platform-indendent. 2011-12-15 13:39:16 -08:00
Alan Mishchenko 9608bcd1d8 Enabling balance again. 2011-12-15 13:39:03 -08:00
Alan Mishchenko 6531899709 Temporarily disabling balance. 2011-12-15 13:24:27 -08:00
Alan Mishchenko c8e4a05fd3 Additional print-outs in dc2. 2011-12-15 13:13:23 -08:00
Alan Mishchenko b63b332bac Trying to make sorting of nodes platform-indendent. 2011-12-15 12:42:42 -08:00
Alan Mishchenko 40ddda3edd Trying to make sorting of nodes platform-indendent. 2011-12-15 12:27:35 -08:00
Alan Mishchenko bc2f199bd3 Started SAT-based reparameterization. 2011-12-13 23:38:41 -08:00
Alan Mishchenko 8fdc5d220f g++ portability changes. 2011-12-13 12:17:03 -08:00
Alan Mishchenko 23af7f9036 Added command &read_blif to read hierarchical BLIF directly into the &-space. 2011-12-12 19:10:33 -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 ed4f4adeee Added the hierarchy printout. 2011-12-11 17:29:25 -08:00
Alan Mishchenko c2a1a9ef37 Implementing rollback in the updated solver. 2011-12-10 14:55:33 -08:00
Alan Mishchenko a2228ee09b Implementing rollback in the updated solver. 2011-12-10 14:45:35 -08:00
Alan Mishchenko 871171ffa4 Implemented rollback in the main SAT solver and updated PDR to use it (saves about 5% of runtime). 2011-12-10 14:06:01 -08:00
Alan Mishchenko 6c766b4f1a Implementing rollback in the updated solver. 2011-12-10 13:11:28 -08:00
Alan Mishchenko dea5708d4e Removing unused files. 2011-12-10 11:30:29 -08:00
Alan Mishchenko f67c0c173d Changes to the main SAT solver: fixing performance bug (resetting decay params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity). 2011-12-09 23:49:30 -08:00
Alan Mishchenko eb35f0ef65 Added support for generating a library of real-life truth-tables. 2011-12-09 01:05:18 -08:00
Alan Mishchenko beb29257bf Added support for generating a library of real-life truth-tables. 2011-12-09 00:38:16 -08:00
Alan Mishchenko 200c5cc659 Added support for generating a library of real-life truth-tables. 2011-12-09 00:37:05 -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 b5c3992b6b Proof-logging in the updated solver. 2011-12-08 19:43:08 -08:00
Alan Mishchenko c985e17d1f Proof-logging in the updated solver. 2011-12-08 15:06:26 -08:00
Alan Mishchenko d1fa7f7a61 Proof-logging in the updated solver. 2011-12-07 22:26:50 -08:00
Alan Mishchenko 565fefec7a Proof-logging in the updated solver. 2011-12-06 21:11:18 -08:00
Alan Mishchenko 35733eb1a1 Added/renamed useful APIs. 2011-12-06 21:10:58 -08:00
Alan Mishchenko 68baf03809 Another attempt to make CUDD platform- and runtime-independent. 2011-12-06 18:58:41 -08:00
Alan Mishchenko 780321cf54 Another attempt to make CUDD platform- and runtime-independent. 2011-12-06 17:48:31 -08:00
Alan Mishchenko 7cce97b4b3 Added new switch to the LUT matching code. 2011-12-06 16:50:04 -08:00
Alan Mishchenko e84dcb7862 g++ portability changes. 2011-12-06 16:06:59 -08:00
Alan Mishchenko ef37d14bc6 Added recording of AIG subgraphs. 2011-12-06 15:37:09 -08:00
Alan Mishchenko f95e73c40b Added recording of AIG subgraphs. 2011-12-06 14:29:32 -08:00
Alan Mishchenko 0f8b68aef8 Performance bug fix in SOP balancing. 2011-12-06 13:15:53 -08:00
Alan Mishchenko 360c705fc4 Added recording of AIG subgraphs. 2011-12-06 12:42:00 -08:00
Alan Mishchenko b4a46eb688 Bug fixes in CUDD 2.4.2. 2011-12-06 07:39:55 -08:00
Alan Mishchenko a24e678a79 Bug fixes in CUDD 2.4.2. 2011-12-06 07:32:17 -08:00
Alan Mishchenko b743298cd5 Proof-logging in the updated solver. 2011-12-05 20:02:46 -08:00
Alan Mishchenko df8b636169 Fixed performance bug in matching code. 2011-12-05 18:27:03 -08:00
Alan Mishchenko 72404d1fdf Proof-logging in the updated solver. 2011-12-05 18:00:49 -08:00
Alan Mishchenko bb96fa361c Proof-logging in the updated solver. 2011-12-05 11:53:57 -08:00
Alan Mishchenko 7a19593d3f Proof-logging in the updated solver. 2011-12-04 23:30:09 -08:00
Alan Mishchenko f0d44a4a93 Proof-logging in the updated solver. 2011-12-04 22:58:24 -08:00
Alan Mishchenko 09d3e1ff77 Proof-logging in the updated solver. 2011-12-04 16:10:11 -08:00
Alan Mishchenko a7031bb3f7 Removing redundant function declarations. 2011-12-02 10:11:39 -05:00
Alan Mishchenko 12869de14b Previusly forgotten debug printout. 2011-12-02 01:08:48 -05:00
Alan Mishchenko 5161978d05 Started proof transformations. 2011-12-01 01:14:32 -05:00
Alan Mishchenko 1c16c45679 Started experiments with a new solver. 2011-11-27 16:28:57 -08:00
Alan Mishchenko fc4ab6bd39 Started experiments with a new solver. 2011-11-26 18:17:39 -08:00
Alan Mishchenko 0cfc97b940 Started experiments with a new solver. 2011-11-26 11:54:01 -08:00
Alan Mishchenko 8ac9515d36 Started experiments with a new solver. 2011-11-26 11:37:27 -08:00
Alan Mishchenko 06416a981f Started experiments with a new solver. 2011-11-26 11:33:37 -08:00
Alan Mishchenko d2db956a61 Started experiments with a new solver. 2011-11-25 18:08:48 -08:00
Alan Mishchenko 0f594b78fa Commented out the default call to UNSAT core verification. 2011-11-25 18:07:41 -08:00
Alan Mishchenko 9726d5a85e Improvement to the SAT solver (skipping binary clauses). 2011-11-25 18:06:36 -08:00
Alan Mishchenko 0a5d856cec Making GLA PBA and GLA CBA communicate information. 2011-11-22 19:07:00 -08:00
Alan Mishchenko ff938c7141 Modifications to the matching procedure 2011-11-22 18:48:03 -08:00
Alan Mishchenko 24408a483c Bug fix in GLA PBA. 2011-11-13 00:17:00 -08:00
Alan Mishchenko c7a7444211 Bug fix in GLA PBA. 2011-11-13 00:10:34 -08:00
Alan Mishchenko 21de666005 Bug fix in GLA PBA. 2011-11-13 00:01:16 -08:00
Alan Mishchenko e43c0d8708 Setting the number of completed time frames. 2011-11-12 23:44:38 -08:00
Alan Mishchenko b695e3334c Setting the number of completed time frames. 2011-11-12 23:42:19 -08:00
Alan Mishchenko 30ea50a3b4 Temporary debugging change. 2011-11-12 23:21:41 -08:00
Alan Mishchenko ca33481f1e Temporary debugging change. 2011-11-12 23:10:08 -08:00
Alan Mishchenko bf97e901d7 Temporary debugging change. 2011-11-12 23:07:19 -08:00
Alan Mishchenko 53b2f056a1 Temporary debugging change. 2011-11-12 23:04:27 -08:00
Alan Mishchenko 926b3adec1 Temporary debugging change. 2011-11-12 23:00:09 -08:00
Alan Mishchenko 4a937ef39f Temporary debugging change. 2011-11-12 22:58:48 -08:00
Alan Mishchenko 03cd9e196b Temporary debugging change. 2011-11-12 22:30:41 -08:00
Alan Mishchenko bca84be597 Temporary debugging change. 2011-11-12 22:26:12 -08:00
Alan Mishchenko cd2f13c09d Making computation in 'fx' run-to-run reproducible. 2011-11-12 22:20:26 -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 b38df9feec Experiment with time reporting in GLA PBA. 2011-11-12 14:18:38 -08:00
Alan Mishchenko 814ee4841b Dump last frame clauses with 'pdr -d' even if the problem is SAT or undecided. 2011-11-12 14:03:00 -08:00
Alan Mishchenko c16f5d6494 Bug fix in GLA PBA. 2011-11-12 13:30:28 -08:00
Alan Mishchenko 3beb36778e Enabled counter-example minimization in 'write_counter'. 2011-11-11 20:56:05 -08:00
Alan Mishchenko 9fe4c74952 Corner-case bug in PDR. 2011-11-11 19:29:15 -08:00
Alan Mishchenko 8e6d4d3fe9 Removing restruction on the number of LUT inputs. 2011-11-10 23:17:08 -08:00
Alan Mishchenko d8dbc712d3 Bug fix in GLA PBA (unfinished). 2011-11-09 15:58:31 -08:00
Alan Mishchenko 0b73c76380 Preventing scripts from aborting if reading has failed. 2011-11-08 17:58:51 -08:00
Alan Mishchenko 55e9c4d0fa Corner case bug in deriving truth table from SOP. 2011-11-08 11:36:35 -08:00
Alan Mishchenko 9a89e3f9f5 Changing defaults in gate-level abstraction. 2011-11-06 23:35:15 -08:00
Alan Mishchenko 986bf053ee Trying to add BMC to random simulation. 2011-11-06 23:16:24 -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 c345a60ee7 Experiments with variable permutation. 2011-11-06 23:14:32 -08:00
Alan Mishchenko 9382c8fdd1 Trying to add BMC to random simulation. 2011-11-06 23:13:52 -08:00
Alan Mishchenko 6a939b6382 Experiments with variable permutation. 2011-11-06 08:26:30 -08:00
Alan Mishchenko cb5be5118b Experiments with variable permutation. 2011-11-06 08:22:05 -08:00
Alan Mishchenko 5c3264643e Temporarily added new runtime computation procedures. 2011-11-03 19:32:56 -05:00
Alan Mishchenko f75e55bb4b Fixed &reachy to perform reparametrization in case reachability is disabled. 2011-11-03 19:32:20 -05:00
Alan Mishchenko 5b75410a5e Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc. 2011-10-31 15:04:47 -05:00
Alan Mishchenko 868a1b9aeb Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc. 2011-10-31 14:59:47 -05:00
Alan Mishchenko f08be2742e C++ portability changes. 2011-10-27 23:34:11 -07:00
Alan Mishchenko 24d27e5524 Improvements to the new abstraction code. 2011-10-27 22:27:00 -07:00
Alan Mishchenko ef288ed5d0 Removed some recently added file, which broke compilation. 2011-10-27 14:28:41 -07:00
Alan Mishchenko 0ff0a552a5 Improvements to the new abstraction code. 2011-10-27 14:23:43 -07:00
Alan Mishchenko bc81cf2dae Improvements to the new abstraction code. 2011-10-27 14:20:47 -07:00
Alan Mishchenko 1dcdba1bee New proof-based abstraction code (bug fix). 2011-10-27 10:10:10 -07:00
Alan Mishchenko 0736f39609 New truth table permutation procedure. 2011-10-26 23:15:42 +08: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 a8e1ba40b9 The result of merging with recent PyABC changes. 2011-10-25 14:05:50 +08:00
Baruch Sterin 15d0d84bb4 pyabc: rearrange files and locations 2011-10-24 15:21:08 -07:00
Baruch Sterin 521ec0fcf9 pyabc: fix command line parser in reachx_cmx.py and abcpy_test.py 2011-10-24 15:21:08 -07:00
Alan Mishchenko f96f3fa583 Improvements to the QBF solver. 2011-10-24 18:05:45 +08:00
Alan Mishchenko 88c36d9d65 New abstraction code (bug fix). 2011-10-23 13:20:24 +07: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 efd310af3e Skip NULL entry when freeing vector of vectors. 2011-10-19 14:22:33 +07:00
Alan Mishchenko 5dbfc74807 Changes to CNF generation code. 2011-10-19 14:21:41 +07:00
Alan Mishchenko 1d0b827603 Changes to CNF generation code. 2011-10-19 11:49:54 +07:00
Alan Mishchenko 12b70d4946 Changes to CNF generation code. 2011-10-17 10:39:05 +03:00
Alan Mishchenko 6f0b87dd5c New abstraction code. 2011-10-15 22:04:05 +03:00
Alan Mishchenko e4bd4d5440 New abstraction code. 2011-10-14 16:49:43 +03:00
Alan Mishchenko c6982485e4 New abstraction code. 2011-10-14 16:48:45 +03:00
Alan Mishchenko ad5ee9ff46 Changes to the matching procedure. 2011-10-12 15:04:41 +03:00
Alan Mishchenko 191de3e885 Changes to the matching procedure. 2011-10-10 22:19:34 +03:00
Alan Mishchenko 657f2acd71 Changes to the matching procedure. 2011-10-10 21:55:32 +03:00
Alan Mishchenko 9daabedff5 Fixing built-in resource limit when converting truth-tables to AIGs. 2011-10-08 23:18:44 +07:00
Alan Mishchenko 924ec940fe Changes to the matching procedure. 2011-10-06 15:48:27 +07:00
Alan Mishchenko d66b586330 Modified write_blif to output LUT structures. 2011-10-04 18:43:23 +07:00
Alan Mishchenko 8c302870f4 Changes to the matching procedure. 2011-10-03 13:34:17 +07:00
Alan Mishchenko 0f9dacb7be Changes to the matching procedure. 2011-10-02 16:39:51 +07:00
Alan Mishchenko e6e6a3cf9e Changes to the matching procedure. 2011-10-01 17:00:59 +07:00
Alan Mishchenko ff4c674dd7 Updated miter status check to detect the case when a PO is equal to a true PI. 2011-10-01 10:51:33 +07:00
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
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
Alan Mishchenko 81620f2e92 Changes to enable CEX minimization. 2011-08-01 12:13:49 +07:00
Alan Mishchenko 02b04efe9c Changes and simplifications in Vec_Vec_t data-structure. 2011-08-01 11:56:19 +07:00
Alan Mishchenko 33f71450d9 Bug fix in &abs_cba. 2011-08-01 11:48:21 +07:00
Alan Mishchenko 48f3db0b2d Reducing print-out in 'bmc3'. 2011-08-01 11:47:13 +07:00
Alan Mishchenko ab3c537072 Undoing previous change in 'resim' (do not initialize flops using their values in the CEX because the number of flops in the CEX can be different). 2011-08-01 11:25:46 +07:00
Alan Mishchenko 88251e97e3 Minor bug fix in 'testcex' (made it consider outputs in direct order). 2011-08-01 11:24:02 +07:00
Alan Mishchenko 34811655f2 Minor bug fix in 'testcex'. 2011-07-31 20:37:38 +07:00
Alan Mishchenko 778215e7ee Added new APIs to the AIG manager. 2011-07-31 20:36:43 +07:00
Alan Mishchenko 0d65c49048 Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed). 2011-07-31 20:22:57 +07:00
Alan Mishchenko d5955db960 Added new APIs to integer vector. 2011-07-31 20:20:10 +07:00
Alan Mishchenko 5303465ed6 Added new sorting procedures. 2011-07-31 16:17:21 +07:00
Alan Mishchenko 4ffe37b34b Added new sorting procedures. 2011-07-31 16:16:49 +07:00
Alan Mishchenko 340e4380e9 Changes to enable smarter simulation (bug fix). 2011-07-30 20:26:17 +07:00
Alan Mishchenko 43d8b8bece Changes to enable smarter simulation. 2011-07-30 20:19:28 +07:00
Alan Mishchenko b8de7a28e0 Changes to enable smarter simulation. 2011-07-30 19:56:52 +07:00
Alan Mishchenko 02711b6392 Added generation of counter-examples to induction in 'ind'. 2011-07-30 19:18:26 +07:00
Alan Mishchenko c60852f4a9 Changes to enable smarter simulation. 2011-07-30 13:37:02 +07:00
Alan Mishchenko 2ea0ded0bc Changes to enable smarter simulation. 2011-07-30 13:30:04 +07:00
Alan Mishchenko e4f15dd003 Changes to enable smarter simulation. 2011-07-30 02:04:54 +07:00
Alan Mishchenko badf8e4742 Improving and updating the abstraction code. 2011-07-29 18:57:54 +07:00
Alan Mishchenko dac71e9b33 Added deriving abstraction in GIA from the precomputed flop map. 2011-07-29 16:21:25 +07:00
Alan Mishchenko ce38474c74 Improving and updating the abstraction code. 2011-07-29 15:38:44 +07:00
Alan Mishchenko 581daaeade Changes to enable smarter simulation. 2011-07-29 14:20:41 +07:00
Alan Mishchenko 9e6d0664cb Other changes to enable new features in the mapper (bug fix). 2011-07-28 15:27:07 +07:00
Alan Mishchenko fddff7a55b Other changes to enable new features in the mapper (bug fix). 2011-07-28 13:50:34 +07:00
Alan Mishchenko 8ed6d8e05f Adding procedures to find the care bits of a counter-example (update). 2011-07-27 20:18:14 +07:00
Alan Mishchenko ff963167fe Added random generation of 64-bit numbers. 2011-07-27 18:30:08 +07:00
Alan Mishchenko 701296451e Determine LUT size form the LUT library if present. 2011-07-27 13:30:17 +07:00
Alan Mishchenko 7184003b42 Adding procedures to find the care bits of a counter-example (update). 2011-07-25 20:52:15 +07:00
Alan Mishchenko e7a5a74b4c Adding procedures to find the care bits of a counter-example. 2011-07-25 20:35:06 +07:00
Alan Mishchenko 67e84b719d Enhancing printing of counter-examples. 2011-07-25 20:33:55 +07:00
Alan Mishchenko c4dd8067fd Bug fix in how seq cleanup handles cand equiv classes. 2011-07-25 19:29:57 +07:00
Alan Mishchenko 9e307901c7 Added support for constraints in AIGER (bug fix). 2011-07-22 20:29:26 +07:00
Alan Mishchenko 76447062cc Adding &equiv3, a new way of refining equivalence classes. 2011-07-22 20:20:19 +07:00
Alan Mishchenko 5b71a8f849 Added support for constraints in AIGER (bug fix). 2011-07-21 22:42:11 +07:00
Alan Mishchenko 5b616990b4 Added support for constraints in AIGER (bug fix). 2011-07-21 22:38:20 +07:00
Alan Mishchenko 9a2a0f2912 Changes to enable smarter simulation. 2011-07-21 17:55:44 +07:00
Alan Mishchenko 515835579e Added support for constraints in AIGER (bug fix). 2011-07-21 13:04:32 +07:00
Alan Mishchenko fdf79ed471 Other changes to enable new features in the mapper (bug fix). 2011-07-21 12:02:07 +07:00
Alan Mishchenko f899bae8f6 Added support for constraints in AIGER (bug fix). 2011-07-20 22:16:06 +07:00
Alan Mishchenko 267f61164a Changes to enable smarter simulation. 2011-07-20 18:40:09 +07:00
Alan Mishchenko ee261ef3f2 Other changes to enable new features in the mapper (bug fix). 2011-07-20 18:23:10 +07:00
Alan Mishchenko bb86d9142e New demitering features. 2011-07-20 13:52:54 +07:00
Alan Mishchenko 3ab9683d26 Added support for constraints in AIGER (bug fix). 2011-07-20 13:45:30 +07:00
Alan Mishchenko 4ca6612821 Fixed assertion failure when mitering with choices. 2011-07-20 11:01:12 +07:00
Alan Mishchenko bc63966e4a Corner case bug fix in 'speedup'. 2011-07-20 10:55:58 +07:00
Alan Mishchenko c511bccb67 Added support for constraints in AIGER. 2011-07-20 10:11:49 +07:00
Alan Mishchenko 5e7de1f80a Added report about exceeding the conflict limit in 'ind'. 2011-07-19 11:16:53 +07:00
Alan Mishchenko fbd6a08e73 Other changes to enable new features in the mapper (bug fix). 2011-07-16 17:49:35 +07:00
Alan Mishchenko 7ad51056bd Diagnostic printout for random simulation 2011-07-16 15:00:39 +07:00
Alan Mishchenko ccaed178ca Fixed a glitch in &dch, which removed the flops. 2011-07-16 12:36:06 +07:00
Alan Mishchenko 302f7d7a97 Other changes to enable new features in the mapper (bug fix). 2011-07-15 18:50:58 +07:00
Alan Mishchenko 96e44e313e Other changes to enable new features in the mapper (bug fix). 2011-07-15 12:27:40 +07:00
Alan Mishchenko 2dd6b9789d Reduced default growth rate of vectors in the SAT solver. 2011-07-13 16:35:53 +07:00
Alan Mishchenko 6a020d6f69 Added switch to PDR to disable expensive generalization step. 2011-07-13 15:13:08 +07:00
Alan Mishchenko 669f390c6d Other changes to enable new features in the mapper (bug fix). 2011-07-13 12:48:51 +07:00
Alan Mishchenko 97b488e72e Fixed memory leak in the AIGER reader. 2011-07-13 10:50:36 +07:00
Alan Mishchenko 73702835c6 Added equivalence class computation for flop outputs only in &equiv2. 2011-07-13 10:13:24 +07:00