Commit Graph

2142 Commits

Author SHA1 Message Date
Alan Mishchenko 3d8dc1217c Integrating input driving cell constraint into buffering/sizing. 2013-09-17 23:00:59 -07:00
Alan Mishchenko efa6b54b5e Debugging and finetuning the flow. 2013-09-17 21:47:39 -07:00
Alan Mishchenko c62f380eff Debugging and finetuning the flow. 2013-09-17 16:59:22 -07:00
Alan Mishchenko a2d97cf2b6 Debugging and finetuning the flow. 2013-09-17 16:43:42 -07:00
Alan Mishchenko 73a997a8bd Adding commands to set and print timing constraints. 2013-09-17 14:47:34 -07:00
Alan Mishchenko ca39b892f0 Compiler warning about unused variable. 2013-09-17 13:22:16 -07:00
Alan Mishchenko 7d3976a763 Unifying standard cell library representations. 2013-09-17 13:16:20 -07:00
Alan Mishchenko 5df166fce1 Changing dynamic CNF loading code to perform loading before propagate() as opposed to when the literal first implied in enqueue(). 2013-09-16 23:43:47 -07:00
Alan Mishchenko 105648bf7c Adding switch to enable reuse of proof-obligations in the last timeframe. 2013-09-16 22:57:50 -07:00
Alan Mishchenko 2ba12a76ff Adding new switch to &if to relax the delay. 2013-09-16 22:50:39 -07:00
Alan Mishchenko e446cfca15 Added bridge integration for multi-output 'pdr -a'. 2013-09-16 14:54:11 -07:00
Alan Mishchenko 653dc8cff5 Added bridge integration for multi-output 'pdr -a'. 2013-09-16 14:46:07 -07:00
Alan Mishchenko 3b1cf0976c Added bridge integration for multi-output 'pdr -a'. 2013-09-16 14:39:37 -07:00
Alan Mishchenko e87f0dd679 Bug fix in PDR. 2013-09-16 08:49:37 -07:00
Alan Mishchenko 5d2dc04144 Bug fix in XOR balancing. 2013-09-15 23:18:43 -07:00
Alan Mishchenko 549fd2ed15 Infrastructure to support full Liberty format and unitification of library representations. 2013-09-15 18:31:02 -07:00
Alan Mishchenko 931e5882b1 Infrastructure to support full Liberty format and unitification of library representations. 2013-09-15 18:28:29 -07:00
Alan Mishchenko ff5d3591d1 Infrastructure to support full Liberty format and unitification of library representations. 2013-09-15 18:23:49 -07:00
Alan Mishchenko d1fed2dd89 Fixing return value of 'pdr -a'. 2013-09-15 11:02:53 -07:00
Alan Mishchenko ab5c1692db Handling the case when all outputs are undecided in 'pdr -a' with per-output timeout. 2013-09-14 12:23:46 -07:00
Alan Mishchenko 60fae35d36 Fixing several bugs, which led to unsound results produced by 'pdr -a' with per-output timeout. 2013-09-13 19:44:54 -07:00
Alan Mishchenko a4087e45f0 Enabling additional printouts in 'pdr'. 2013-09-13 17:36:29 -07:00
Alan Mishchenko 27be3d0185 Added command &struct for profiling non-dec structures. 2013-09-13 17:25:31 -07:00
Alan Mishchenko dfb43b2f58 Fix a bug in 'zeropo'. 2013-09-13 09:52:54 -07:00
Alan Mishchenko 5b6b7c5bbe Removing duplicated typedef line. 2013-09-13 09:39:50 -07:00
Alan Mishchenko bee107443d Improvements to the new technology mapper. 2013-09-12 23:59:18 -07:00
Alan Mishchenko 7312ff3c4a Improvements to the new technology mapper. 2013-09-12 23:14:39 -07:00
Alan Mishchenko 75fee10708 Improvements to the new technology mapper. 2013-09-12 22:37:26 -07:00
Alan Mishchenko 14606c473e Improvements to the new technology mapper. 2013-09-12 17:53:41 -07:00
Alan Mishchenko 0a346a36a2 Improvements to the new technology mapper. 2013-09-12 14:52:58 -07:00
Alan Mishchenko 9b02a26a80 Improvements to the new technology mapper. 2013-09-12 14:47:45 -07:00
Alan Mishchenko 68df9f0f59 Improvements to the new technology mapper. 2013-09-12 00:39:19 -07:00
Alan Mishchenko 61abba9571 Improvements to the new technology mapper. 2013-09-11 23:49:05 -07:00
Alan Mishchenko 211ac730c6 Improvements to the new technology mapper. 2013-09-11 18:19:36 -07:00
Alan Mishchenko 5d6f05a9a2 Improvements to the new technology mapper. 2013-09-11 16:47:08 -07:00
Alan Mishchenko b1b0202c05 Command '&slice' to cut out the bottom part of the AIG. 2013-09-11 14:38:08 -07:00
Alan Mishchenko deb7b6ac4f Corrected variable naming in clause2_proofid(). 2013-09-11 13:34:32 -07:00
Alan Mishchenko 66b1d4de54 Small performance bug in new 'fx'. 2013-09-11 13:10:31 -07:00
Alan Mishchenko 299099a443 Updates for the new BMC engine. 2013-09-10 23:14:20 -07:00
Alan Mishchenko 26c0e9370a Updates for the new BMC engine. 2013-09-10 22:16:28 -07:00
Alan Mishchenko 0e256dc2c2 Updates for the new BMC engine. 2013-09-10 22:12:42 -07:00
Alan Mishchenko 8430b6dad4 New API to return the set of all reachable states as an AIG. 2013-09-10 14:51:47 -07:00
Alan Mishchenko 9d01c98e62 Added sorting equiv classes by the index of their representatives. 2013-09-10 13:27:39 -07:00
Alan Mishchenko 60540f3c61 Moving #include to the top of the file in 'giaUtil.c'. 2013-09-10 13:21:17 -07:00
Alan Mishchenko d4c70cb6c1 Updates for the new BMC engine. 2013-09-09 23:12:01 -07:00
Alan Mishchenko 2fa9645b08 Improvements to the new technology mapper. 2013-09-09 14:00:47 -07:00
Alan Mishchenko 34e037898c Improvements to the new technology mapper. 2013-09-09 11:46:45 -07:00
Alan Mishchenko 649222e4d0 Improvements to the new technology mapper. 2013-09-09 10:44:19 -07:00
Alan Mishchenko c05e141d1f Improvements to the new technology mapper. 2013-09-09 10:31:21 -07:00
Alan Mishchenko fba43b5065 Improvements to the new technology mapper. 2013-09-09 00:24:56 -07:00