Alan Mishchenko
|
eec94a70f1
|
Adding API to return the mapped network.
|
2013-09-22 23:18:40 -07:00 |
Alan Mishchenko
|
d61bedc627
|
Adding API to return the mapped network.
|
2013-09-22 16:23:57 -07:00 |
Alan Mishchenko
|
cfebcae125
|
Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement.
|
2013-09-21 17:55:59 -04:00 |
Alan Mishchenko
|
247dd95dd3
|
Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement.
|
2013-09-21 14:08:38 -04:00 |
Alan Mishchenko
|
d32e51409f
|
Buf fix in Liberty parser.
|
2013-09-19 18:49:18 -04:00 |
Alan Mishchenko
|
080a7420fc
|
Added bridge integration for multi-output 'bmc3 -a'.
|
2013-09-17 23:25:15 -07:00 |
Alan Mishchenko
|
d4bd7846c3
|
Added bridge integration for multi-output 'bmc3 -a'.
|
2013-09-17 23:19:54 -07:00 |
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 |