VIS
|
00001 00018 #include "maig.h" 00019 #include "ntk.h" 00020 #include "cmd.h" 00021 #include "baig.h" 00022 #include "baigInt.h" 00023 #include "heap.h" 00024 #include "ntmaig.h" 00025 #include "ord.h" 00026 00027 static char rcsid[] UNUSED = "$Id: baigBddSweep.c,v 1.13 2005/05/18 18:11:42 jinh Exp $"; 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Constant declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 00034 /*---------------------------------------------------------------------------*/ 00035 /* Stucture declarations */ 00036 /*---------------------------------------------------------------------------*/ 00037 00038 00039 /*---------------------------------------------------------------------------*/ 00040 /* Type declarations */ 00041 /*---------------------------------------------------------------------------*/ 00042 00043 00044 /*---------------------------------------------------------------------------*/ 00045 /* Variable declarations */ 00046 /*---------------------------------------------------------------------------*/ 00047 00048 /*---------------------------------------------------------------------------*/ 00049 /* Macro declarations */ 00050 /*---------------------------------------------------------------------------*/ 00051 00052 00055 /*---------------------------------------------------------------------------*/ 00056 /* Static function prototypes */ 00057 /*---------------------------------------------------------------------------*/ 00058 00059 static int SweepBddCompare(const char *x, const char *y); 00060 static int SweepBddHash(char *x, int size); 00061 00065 /*---------------------------------------------------------------------------*/ 00066 /* Definition of exported functions */ 00067 /*---------------------------------------------------------------------------*/ 00068 void bAig_BuildAigBFSManner( Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep); 00069 void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray); 00070 void bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray); 00071 00083 static int 00084 SweepBddCompare(const char *x, const char *y) 00085 { 00086 return(bdd_ptrcmp((bdd_t *)x, (bdd_t *)y)); 00087 } 00088 00100 static int 00101 SweepBddHash(char *x, int size) 00102 { 00103 00104 return(bdd_ptrhash((bdd_t *)x, size)); 00105 } 00106 00119 void 00120 bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray) 00121 { 00122 array_t *mVarList, *bVarList; 00123 bdd_t *bdd, *func; 00124 int bddIdIndex; 00125 int i, count, sizeLimit, mvfSize; 00126 int maxSize, curSize; 00127 array_t *tnodeArray; 00128 lsGen gen; 00129 st_generator *gen1; 00130 Ntk_Node_t *node; 00131 bAigEdge_t v; 00132 MvfAig_Function_t *mvfAig; 00133 mAig_Manager_t *manager; 00134 mdd_manager *mgr; 00135 st_table *node2MvfAigTable; 00136 st_table * bdd2vertex; 00137 mAigMvar_t mVar; 00138 mAigBvar_t bVar; 00139 int index1, mAigId; 00140 00141 00142 manager = Ntk_NetworkReadMAigManager(network); 00143 00144 mgr = Ntk_NetworkReadMddManager(network); 00145 if(mgr == 0) { 00146 Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 00147 Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 00148 Ord_Unassigned_c, 0, 0); 00149 mgr = Ntk_NetworkReadMddManager(network); 00150 } 00151 node2MvfAigTable = 00152 (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); 00153 00154 bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash); 00155 00156 sizeLimit = 500; 00157 maxSize = manager->nodesArraySize; 00158 00159 tnodeArray = 0; 00160 if(nodeArray == 0) { 00161 bVarList = mAigReadBinVarList(manager); 00162 mVarList = mAigReadMulVarList(manager); 00163 tnodeArray = array_alloc(bAigEdge_t, 0); 00164 Ntk_NetworkForEachLatch(network, gen, node) { 00165 node = Ntk_LatchReadDataInput(node); 00166 st_lookup(node2MvfAigTable, node, &mvfAig); 00167 mvfSize = array_n(mvfAig); 00168 for(i=0; i<mvfSize; i++){ 00169 v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i)); 00170 array_insert_last(bAigEdge_t, tnodeArray, v); 00171 } 00172 00173 mAigId = Ntk_NodeReadMAigId(node); 00174 mVar = array_fetch(mAigMvar_t, mVarList, mAigId); 00175 for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) { 00176 bVar = array_fetch(mAigBvar_t, bVarList, index1++); 00177 v = bVar.node; 00178 v = bAig_GetCanonical(manager, v); 00179 array_insert_last(bAigEdge_t, tnodeArray, v); 00180 } 00181 } 00182 Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 00183 st_lookup(node2MvfAigTable, node, &mvfAig); 00184 mvfSize = array_n(mvfAig); 00185 for(i=0; i<mvfSize; i++){ 00186 v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i)); 00187 array_insert_last(bAigEdge_t, tnodeArray, v); 00188 } 00189 } 00190 } 00191 00192 count = bAigNodeID(manager->nodesArraySize); 00193 for(i=0; i<count; i++) { 00194 manager->bddIdArray[i] = -1; 00195 manager->bddArray[i] = 0; 00196 } 00197 manager->bddArray[0] = bdd_zero(mgr); 00198 00199 bddIdIndex = 0; 00200 for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) { 00201 if(leftChild(i) != 2) continue; 00202 bdd = bdd_get_variable(mgr, bddIdIndex); 00203 manager->bddIdArray[bAigNodeID(i)] = bddIdIndex; 00204 manager->bddArray[bAigNodeID(i)] = bdd; 00205 bddIdIndex++; 00206 } 00207 00208 if(nodeArray) { 00209 for(i=0; i<array_n(nodeArray); i++) { 00210 v = array_fetch(bAigEdge_t, nodeArray, i); 00211 v = bAig_GetCanonical(manager, v); 00212 bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex); 00213 } 00214 } 00215 else { 00216 for(i=0; i<array_n(tnodeArray); i++) { 00217 v = array_fetch(bAigEdge_t, tnodeArray, i); 00218 v = bAig_GetCanonical(manager, v); 00219 bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex); 00220 } 00221 array_free(tnodeArray); 00222 } 00223 00224 count = bAigNodeID(manager->nodesArraySize); 00225 for(i=0; i<count; i++) { 00226 if(manager->bddArray[i]) { 00227 bdd_free(manager->bddArray[i]); 00228 manager->bddArray[i] = 0; 00229 } 00230 } 00231 00232 st_foreach_item(bdd2vertex, gen1, &func, &v) { 00233 bdd_free(func); 00234 } 00235 st_free_table(bdd2vertex); 00236 00237 count = bAigNodeID(manager->nodesArraySize); 00238 curSize = 0; 00239 for(i=0; i<count; i++) { 00240 if(bAigGetPassFlag(manager, i*bAigNodeSize)) { 00241 curSize++; 00242 } 00243 } 00244 /* 00245 fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 00246 maxSize/bAigNodeSize, count, (maxSize-curSize)/bAigNodeSize); 00247 fflush(vis_stdout); 00248 */ 00249 return; 00250 00251 } 00252 00264 void 00265 bAig_BddSweepSub( 00266 bAig_Manager_t *manager, 00267 mdd_manager *mgr, 00268 bAigEdge_t v, 00269 st_table *bdd2vertex, 00270 int sizeLimit, 00271 int *newBddIdIndex) 00272 { 00273 bAigEdge_t left, right, oldV, nv; 00274 bdd_t *leftBdd, *rightBdd; 00275 bdd_t *func, *nfunc, *funcBar, *newBdd; 00276 int newId, size; 00277 00278 if(v == 0 || v == 1) return; 00279 if(manager->bddArray[bAigNodeID(v)]) { 00280 return; 00281 } 00282 00283 left = leftChild(v); 00284 right = rightChild(v); 00285 left = bAig_GetCanonical(manager, left); 00286 right = bAig_GetCanonical(manager, right); 00287 00288 if(left == 2 && right == 2) { 00289 return; 00290 } 00291 00292 bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex); 00293 bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex); 00294 00295 v = bAig_GetCanonical(manager, v); 00296 if(manager->bddArray[bAigNodeID(v)]) { 00297 return; 00298 } 00299 00300 left = leftChild(v); 00301 right = rightChild(v); 00302 left = bAig_GetCanonical(manager, left); 00303 right = bAig_GetCanonical(manager, right); 00304 00305 leftBdd = manager->bddArray[bAigNodeID(left)]; 00306 rightBdd = manager->bddArray[bAigNodeID(right)]; 00307 00308 if(leftBdd == 0) { 00309 bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex); 00310 left = bAig_GetCanonical(manager, left); 00311 leftBdd = manager->bddArray[bAigNodeID(left)]; 00312 } 00313 00314 if(rightBdd == 0) { 00315 bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex); 00316 right = bAig_GetCanonical(manager, right); 00317 rightBdd = manager->bddArray[bAigNodeID(right)]; 00318 } 00319 00325 if(leftBdd == 0 || rightBdd == 0) { 00326 fprintf(vis_stdout, 00327 "ERROR : all the nodes should have bdd node at this moment\n"); 00328 } 00329 00330 func = bdd_and(leftBdd, rightBdd, 00331 !bAig_IsInverted(left), !bAig_IsInverted(right)); 00332 00333 if(bAig_IsInverted(v)) { 00334 funcBar = bdd_not(func); 00335 nfunc = funcBar; 00336 } 00337 else { 00338 nfunc = bdd_dup(func); 00339 } 00340 00341 if(st_lookup(bdd2vertex, nfunc, &oldV)) { 00342 bAig_Merge(manager, oldV, v); 00343 } 00344 else { 00345 funcBar = bdd_not(nfunc); 00346 if(st_lookup(bdd2vertex, funcBar, &oldV)) { 00347 bAig_Merge(manager, bAig_Not(oldV), v); 00348 } 00349 bdd_free(funcBar); 00350 } 00351 bdd_free(nfunc); 00352 00353 v = bAig_NonInvertedEdge(v); 00354 nv = bAig_GetCanonical(manager, v); 00355 v = nv; 00356 00357 if(manager->bddArray[bAigNodeID(v)] == 0) { 00358 size = bdd_size(func); 00359 if(size > sizeLimit) { 00360 newId = *newBddIdIndex; 00361 (*newBddIdIndex) ++; 00362 newBdd = bdd_get_variable(mgr, newId); 00363 manager->bddIdArray[bAigNodeID(v)] = newId; 00364 bdd_free(func); 00365 func = newBdd; 00366 manager->bddArray[bAigNodeID(v)] = func; 00367 st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v)); 00368 } 00369 else { 00370 if(bAig_IsInverted(v)) { 00371 funcBar = bdd_not(func); 00372 manager->bddArray[bAigNodeID(v)] = funcBar; 00373 st_insert(bdd2vertex, (char *)func, (char *)v); 00374 } 00375 else { 00376 manager->bddArray[bAigNodeID(v)] = func; 00377 st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v); 00378 } 00379 } 00380 } 00381 else bdd_free(func); 00382 00383 } 00384 00396 void 00397 bAig_BuildAigBFSManner( 00398 Ntk_Network_t *network, 00399 mAig_Manager_t *manager, 00400 st_table *leaves, 00401 int sweep) 00402 { 00403 array_t *nodeArray, *result; 00404 lsGen gen1; 00405 int iter, maxLevel, level; 00406 int i, j, k; 00407 bAigEdge_t v; 00408 Ntk_Node_t *node, *fanin, *fanout; 00409 st_table *node2mvfAigTable; 00410 array_t *curArray, *nextArray, *tmpArray; 00411 array_t *levelArray, *clevelArray; 00412 MvfAig_Function_t *mvfAig; 00413 int mvfSize; 00414 st_generator *gen; 00415 00416 Ntk_NetworkForEachNode(network, gen1, node) { 00417 Ntk_NodeSetUndef(node, (void *)0); 00418 } 00419 00420 curArray = array_alloc(Ntk_Node_t *, 0); 00421 st_foreach_item(leaves, gen, &node, &fanout) { 00422 array_insert_last(Ntk_Node_t *, curArray, node); 00423 Ntk_NodeSetUndef(node, (void *)1); 00424 } 00425 00426 levelArray = array_alloc(array_t *, 10); 00427 nextArray = array_alloc(Ntk_Node_t *, 0); 00428 iter = 0; 00429 while(1) { 00430 clevelArray = array_alloc(array_t *, 10); 00431 array_insert_last(array_t *, levelArray, clevelArray); 00432 for(i=0; i<array_n(curArray); i++) { 00433 node = array_fetch(Ntk_Node_t *, curArray, i); 00434 Ntk_NodeForEachFanout(node, j, fanout) { 00435 00436 level = (int)(long)Ntk_NodeReadUndef(fanout); 00437 if(level > 0) continue; 00438 00439 maxLevel = 0; 00440 Ntk_NodeForEachFanin(fanout, k, fanin) { 00441 level = (int)(long)Ntk_NodeReadUndef(fanin); 00442 if(level == 0) { 00443 maxLevel = 0; 00444 break; 00445 } 00446 else if(level > maxLevel) { 00447 maxLevel = level; 00448 } 00449 } 00450 00451 if(maxLevel > 0) { 00452 Ntk_NodeSetUndef(fanout, (void *)(long)(maxLevel+1)); 00453 array_insert_last(Ntk_Node_t *, nextArray, fanout); 00454 array_insert_last(Ntk_Node_t *, clevelArray, fanout); 00455 } 00456 } 00457 } 00458 00459 curArray->num = 0; 00460 tmpArray = curArray; 00461 curArray = nextArray; 00462 nextArray = tmpArray; 00463 if(curArray->num == 0) break; 00464 00465 iter++; 00466 } 00467 00468 Ntk_NetworkForEachNode(network, gen1, node) { 00469 Ntk_NodeSetUndef(node, (void *)0); 00470 } 00471 00472 for(i=0; i<array_n(levelArray); i++) { 00473 clevelArray = array_fetch(array_t *, levelArray, i); 00474 result = ntmaig_NetworkBuildMvfAigs(network, clevelArray, leaves); 00475 MvfAig_FunctionArrayFree(result); 00476 node2mvfAigTable = (st_table *) Ntk_NetworkReadApplInfo( 00477 network, MVFAIG_NETWORK_APPL_KEY); 00478 00479 if(i < 50 && sweep) { 00480 nodeArray = array_alloc(bAigEdge_t, 0); 00481 for(j=0; j<array_n(clevelArray); j++) { 00482 node = array_fetch(Ntk_Node_t *, clevelArray, j); 00483 st_lookup(node2mvfAigTable, node, &mvfAig); 00484 mvfSize = array_n(mvfAig); 00485 for(k=0; k<mvfSize; k++){ 00486 v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k)); 00487 array_insert_last(bAigEdge_t, nodeArray, v); 00488 } 00489 } 00490 00491 bAig_BddSweepForceMain(network, nodeArray); 00492 00493 for(j=0; j<array_n(clevelArray); j++) { 00494 node = array_fetch(Ntk_Node_t *, clevelArray, j); 00495 st_lookup(node2mvfAigTable, node, &mvfAig); 00496 mvfSize = array_n(mvfAig); 00497 for(k=0; k<mvfSize; k++){ 00498 v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k)); 00499 array_insert(bAigEdge_t, nodeArray, v, k); 00500 } 00501 } 00502 array_free(nodeArray); 00503 } 00504 00505 array_free(clevelArray); 00506 } 00507 array_free(levelArray); 00508 } 00509 00510 00522 void 00523 bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray) 00524 { 00525 array_t *mVarList, *bVarList; 00526 bdd_t *bdd, *func; 00527 int bddIdIndex; 00528 int i, count, sizeLimit, mvfSize; 00529 int maxSize, curSize; 00530 array_t *tnodeArray; 00531 lsGen gen; 00532 st_generator *gen1; 00533 Ntk_Node_t *node; 00534 bAigEdge_t v; 00535 MvfAig_Function_t *mvfAig; 00536 mAig_Manager_t *manager; 00537 mdd_manager *mgr; 00538 st_table *node2MvfAigTable; 00539 st_table * bdd2vertex; 00540 mAigMvar_t mVar; 00541 mAigBvar_t bVar; 00542 int index1, mAigId; 00543 int newmask, resetNewmask; 00544 int usedAig; 00545 00546 00547 manager = Ntk_NetworkReadMAigManager(network); 00548 00549 mgr = Ntk_NetworkReadMddManager(network); 00550 if(mgr == 0) { 00551 Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 00552 Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 00553 Ord_Unassigned_c, 0, 0); 00554 mgr = Ntk_NetworkReadMddManager(network); 00555 } 00556 node2MvfAigTable = 00557 (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); 00558 00559 bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash); 00560 00561 sizeLimit = 500; 00562 maxSize = manager->nodesArraySize; 00563 00564 tnodeArray = 0; 00565 if(nodeArray == 0) { 00566 bVarList = mAigReadBinVarList(manager); 00567 mVarList = mAigReadMulVarList(manager); 00568 tnodeArray = array_alloc(bAigEdge_t, 0); 00569 Ntk_NetworkForEachLatch(network, gen, node) { 00570 node = Ntk_LatchReadDataInput(node); 00571 st_lookup(node2MvfAigTable, node, &mvfAig); 00572 mvfSize = array_n(mvfAig); 00573 for(i=0; i<mvfSize; i++){ 00574 v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i)); 00575 array_insert_last(bAigEdge_t, tnodeArray, v); 00576 } 00577 00578 mAigId = Ntk_NodeReadMAigId(node); 00579 mVar = array_fetch(mAigMvar_t, mVarList, mAigId); 00580 for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) { 00581 bVar = array_fetch(mAigBvar_t, bVarList, index1++); 00582 v = bVar.node; 00583 v = bAig_GetCanonical(manager, v); 00584 array_insert_last(bAigEdge_t, tnodeArray, v); 00585 } 00586 } 00587 Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 00588 st_lookup(node2MvfAigTable, node, &mvfAig); 00589 mvfSize = array_n(mvfAig); 00590 for(i=0; i<mvfSize; i++){ 00591 v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i)); 00592 array_insert_last(bAigEdge_t, tnodeArray, v); 00593 } 00594 } 00595 } 00596 00597 count = bAigNodeID(manager->nodesArraySize); 00598 for(i=0; i<count; i++) { 00599 manager->bddIdArray[i] = -1; 00600 manager->bddArray[i] = 0; 00601 } 00602 manager->bddArray[0] = bdd_zero(mgr); 00603 00604 bddIdIndex = 0; 00605 for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) { 00606 if(leftChild(i) != 2) continue; 00607 bdd = bdd_get_variable(mgr, bddIdIndex); 00608 manager->bddIdArray[bAigNodeID(i)] = bddIdIndex; 00609 manager->bddArray[bAigNodeID(i)] = bdd; 00610 bddIdIndex++; 00611 } 00612 00613 if(nodeArray) { 00614 for(i=0; i<array_n(nodeArray); i++) { 00615 v = array_fetch(bAigEdge_t, nodeArray, i); 00616 v = bAig_GetCanonical(manager, v); 00617 bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex); 00618 } 00619 } 00620 else { 00621 for(i=0; i<array_n(tnodeArray); i++) { 00622 v = array_fetch(bAigEdge_t, tnodeArray, i); 00623 v = bAig_GetCanonical(manager, v); 00624 bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex); 00625 } 00626 } 00627 00628 count = bAigNodeID(manager->nodesArraySize); 00629 for(i=0; i<count; i++) { 00630 if(manager->bddArray[i]) { 00631 bdd_free(manager->bddArray[i]); 00632 manager->bddArray[i] = 0; 00633 } 00634 } 00635 00636 st_foreach_item(bdd2vertex, gen1, &func, &v) { 00637 bdd_free(func); 00638 } 00639 st_free_table(bdd2vertex); 00640 00641 count = bAigNodeID(manager->nodesArraySize); 00642 curSize = 0; 00643 for(i=0; i<count; i++) { 00644 if(bAigGetPassFlag(manager, i*bAigNodeSize)) { 00645 curSize++; 00646 } 00647 } 00648 00649 00650 newmask = 0x00000100; 00651 resetNewmask = 0xfffffeff; 00652 if(tnodeArray) { 00653 for(i=0; i<array_n(tnodeArray); i++) { 00654 v = array_fetch(int, tnodeArray, i); 00655 bAig_SetMaskTransitiveFanin(manager, v, newmask); 00656 } 00657 00658 usedAig = 0; 00659 for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) { 00660 if(flags(i) & newmask) usedAig++; 00661 } 00662 00663 for(i=0; i<array_n(tnodeArray); i++) { 00664 v = array_fetch(int, tnodeArray, i); 00665 bAig_ResetMaskTransitiveFanin(manager, v, newmask, resetNewmask); 00666 } 00667 array_free(tnodeArray); 00668 fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 00669 maxSize/bAigNodeSize, count, usedAig); 00670 fflush(vis_stdout); 00671 } 00672 00673 } 00674 00686 void 00687 bAig_BddSweepForceSub( 00688 bAig_Manager_t *manager, 00689 mdd_manager *mgr, 00690 bAigEdge_t v, 00691 st_table *bdd2vertex, 00692 int sizeLimit, 00693 int *newBddIdIndex) 00694 { 00695 bAigEdge_t left, right, oldV, nv; 00696 bdd_t *leftBdd, *rightBdd; 00697 bdd_t *func, *nfunc, *funcBar, *newBdd; 00698 int newId, size; 00699 00700 if(v == 0 || v == 1) return; 00701 if(manager->bddArray[bAigNodeID(v)]) { 00702 return; 00703 } 00704 00705 00706 left = leftChild(v); 00707 right = rightChild(v); 00708 left = bAig_GetCanonical(manager, left); 00709 right = bAig_GetCanonical(manager, right); 00710 00711 if(left == 2 && right == 2) { 00712 return; 00713 } 00714 00715 bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex); 00716 bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex); 00717 00718 v = bAig_GetCanonical(manager, v); 00719 if(manager->bddArray[bAigNodeID(v)]) { 00720 return; 00721 } 00722 00723 left = leftChild(v); 00724 right = rightChild(v); 00725 left = bAig_GetCanonical(manager, left); 00726 right = bAig_GetCanonical(manager, right); 00727 00728 leftBdd = manager->bddArray[bAigNodeID(left)]; 00729 rightBdd = manager->bddArray[bAigNodeID(right)]; 00730 00731 if(leftBdd == 0) { 00732 bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex); 00733 left = bAig_GetCanonical(manager, left); 00734 leftBdd = manager->bddArray[bAigNodeID(left)]; 00735 } 00736 00737 if(rightBdd == 0) { 00738 bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex); 00739 right = bAig_GetCanonical(manager, right); 00740 rightBdd = manager->bddArray[bAigNodeID(right)]; 00741 } 00742 00748 if(leftBdd == 0 || rightBdd == 0) { 00749 fprintf(vis_stdout, 00750 "ERROR : all the nodes should have bdd node at this moment\n"); 00751 } 00752 00753 func = bdd_and(leftBdd, rightBdd, 00754 !bAig_IsInverted(left), !bAig_IsInverted(right)); 00755 00756 if(bAig_IsInverted(v)) { 00757 funcBar = bdd_not(func); 00758 nfunc = funcBar; 00759 } 00760 else { 00761 nfunc = bdd_dup(func); 00762 } 00763 00764 if(st_lookup(bdd2vertex, nfunc, &oldV)) { 00765 bAig_Merge(manager, oldV, v); 00766 } 00767 else { 00768 funcBar = bdd_not(nfunc); 00769 if(st_lookup(bdd2vertex, funcBar, &oldV)) { 00770 bAig_Merge(manager, bAig_Not(oldV), v); 00771 } 00772 bdd_free(funcBar); 00773 } 00774 bdd_free(nfunc); 00775 00776 v = bAig_NonInvertedEdge(v); 00777 nv = bAig_GetCanonical(manager, v); 00778 v = nv; 00779 00780 if(manager->bddArray[bAigNodeID(v)] == 0) { 00781 size = bdd_size(func); 00782 if(size > sizeLimit) { 00783 newId = *newBddIdIndex; 00784 (*newBddIdIndex) ++; 00785 newBdd = bdd_get_variable(mgr, newId); 00786 manager->bddIdArray[bAigNodeID(v)] = newId; 00787 bdd_free(func); 00788 func = newBdd; 00789 manager->bddArray[bAigNodeID(v)] = func; 00790 st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v)); 00791 } 00792 else { 00793 if(bAig_IsInverted(v)) { 00794 funcBar = bdd_not(func); 00795 manager->bddArray[bAigNodeID(v)] = funcBar; 00796 st_insert(bdd2vertex, (char *)func, (char *)v); 00797 } 00798 else { 00799 manager->bddArray[bAigNodeID(v)] = func; 00800 st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v); 00801 } 00802 } 00803 } 00804 else bdd_free(func); 00805 00806 return; 00807 }