abc70930: src/base/abci/abcNtbdd.c Source File

00001 
00021 #include "abc.h"
00022 
00026 
00027 static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
00028 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
00029 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
00030 static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose );
00031 
00035 
00052 Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
00053 {
00054     Abc_Ntk_t * pNtk; 
00055     Vec_Ptr_t * vNamesPiFake = NULL;
00056     Abc_Obj_t * pNode, * pNodePi, * pNodePo;
00057     DdNode * bSupp, * bTemp;
00058     char * pName;
00059     int i;
00060 
00061     // supply fake names if real names are not given
00062     if ( pNamePo == NULL )
00063         pNamePo = "F";
00064     if ( vNamesPi == NULL )
00065     {
00066         vNamesPiFake = Abc_NodeGetFakeNames( dd->size );
00067         vNamesPi = vNamesPiFake;
00068     }
00069 
00070     // make sure BDD depends on the variables whose index 
00071     // does not exceed the size of the array with PI names
00072     bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
00073     for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
00074         if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) )
00075             break;
00076     Cudd_RecursiveDeref( dd, bSupp );
00077     if ( bTemp != Cudd_ReadOne(dd) )
00078         return NULL;
00079 
00080     // start the network
00081     pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
00082     pNtk->pName = Extra_UtilStrsav(pNamePo);
00083     // make sure the new manager has enough inputs
00084     Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
00085     // add the PIs corresponding to the names
00086     Vec_PtrForEachEntry( vNamesPi, pName, i )
00087         Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL );
00088     // create the node
00089     pNode = Abc_NtkCreateNode( pNtk );
00090     pNode->pData = Cudd_bddTransfer( dd, pNtk->pManFunc, bFunc ); Cudd_Ref(pNode->pData);
00091     Abc_NtkForEachPi( pNtk, pNodePi, i )
00092         Abc_ObjAddFanin( pNode, pNodePi );
00093     // create the only PO
00094     pNodePo = Abc_NtkCreatePo( pNtk );
00095     Abc_ObjAddFanin( pNodePo, pNode );
00096     Abc_ObjAssignName( pNodePo, pNamePo, NULL );
00097     // make the network minimum base
00098     Abc_NtkMinimumBase( pNtk );
00099     if ( vNamesPiFake )
00100         Abc_NodeFreeNames( vNamesPiFake );
00101     if ( !Abc_NtkCheck( pNtk ) )
00102         fprintf( stdout, "Abc_NtkDeriveFromBdd(): Network check has failed.\n" );
00103     return pNtk;
00104 }
00105 
00106 
00107 
00120 Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk )
00121 {
00122     Abc_Ntk_t * pNtkNew;
00123     assert( Abc_NtkIsBddLogic(pNtk) );
00124     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
00125     Abc_NtkBddToMuxesPerform( pNtk, pNtkNew );
00126     Abc_NtkFinalize( pNtk, pNtkNew );
00127     // make sure everything is okay
00128     if ( !Abc_NtkCheck( pNtkNew ) )
00129     {
00130         printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
00131         Abc_NtkDelete( pNtkNew );
00132         return NULL;
00133     }
00134     return pNtkNew;
00135 }
00136 
00148 void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
00149 {
00150     ProgressBar * pProgress;
00151     Abc_Obj_t * pNode, * pNodeNew;
00152     Vec_Ptr_t * vNodes;
00153     int i;
00154     // perform conversion in the topological order
00155     vNodes = Abc_NtkDfs( pNtk, 0 );
00156     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
00157     Vec_PtrForEachEntry( vNodes, pNode, i )
00158     {
00159         Extra_ProgressBarUpdate( pProgress, i, NULL );
00160         // convert one node
00161         assert( Abc_ObjIsNode(pNode) );
00162         pNodeNew = Abc_NodeBddToMuxes( pNode, pNtkNew );
00163         // mark the old node with the new one
00164         assert( pNode->pCopy == NULL );
00165         pNode->pCopy = pNodeNew;
00166     }
00167     Vec_PtrFree( vNodes );
00168     Extra_ProgressBarStop( pProgress );
00169 }
00170 
00182 Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
00183 {
00184     DdManager * dd = pNodeOld->pNtk->pManFunc;
00185     DdNode * bFunc = pNodeOld->pData;
00186     Abc_Obj_t * pFaninOld, * pNodeNew;
00187     st_table * tBdd2Node;
00188     int i;
00189     // create the table mapping BDD nodes into the ABC nodes
00190     tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
00191     // add the constant and the elementary vars
00192     Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
00193         st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
00194     // create the new nodes recursively
00195     pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
00196     st_free_table( tBdd2Node );
00197     if ( Cudd_IsComplement(bFunc) )
00198         pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
00199     return pNodeNew;
00200 }
00201 
00213 Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node )
00214 {
00215     Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
00216     assert( !Cudd_IsComplement(bFunc) );
00217     if ( bFunc == b1 )
00218         return Abc_NtkCreateNodeConst1(pNtkNew);
00219     if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
00220         return pNodeNew;
00221     // solve for the children nodes
00222     pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
00223     if ( Cudd_IsComplement(cuddE(bFunc)) )
00224         pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
00225     pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
00226     if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
00227         assert( 0 );
00228     // create the MUX node
00229     pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
00230     st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
00231     return pNodeNew;
00232 }
00233 
00234 
00246 DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
00247 {
00248     ProgressBar * pProgress;
00249     Abc_Obj_t * pObj, * pFanin;
00250     Vec_Att_t * pAttMan;
00251     DdManager * dd;
00252     DdNode * bFunc;
00253     int i, k, Counter;
00254 
00255     // remove dangling nodes
00256     Abc_AigCleanup( pNtk->pManFunc );
00257 
00258     // start the manager
00259     assert( Abc_NtkGlobalBdd(pNtk) == NULL );
00260     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00261     pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, dd, Extra_StopManager, NULL, Cudd_RecursiveDeref );
00262     Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
00263 
00264     // set reordering
00265     if ( fReorder )
00266         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
00267 
00268     // assign the constant node BDD
00269     pObj = Abc_AigConst1(pNtk);
00270     if ( Abc_ObjFanoutNum(pObj) > 0 )
00271     {
00272         bFunc = dd->one;
00273         Abc_ObjSetGlobalBdd( pObj, bFunc );   Cudd_Ref( bFunc );
00274     }
00275     // set the elementary variables
00276     Abc_NtkForEachCi( pNtk, pObj, i )
00277         if ( Abc_ObjFanoutNum(pObj) > 0 )
00278         {
00279             bFunc = dd->vars[i];
00280 //            bFunc = dd->vars[Abc_NtkCiNum(pNtk) - 1 - i];
00281             Abc_ObjSetGlobalBdd( pObj, bFunc );  Cudd_Ref( bFunc );
00282         }
00283 
00284     // collect the global functions of the COs
00285     Counter = 0;
00286     // construct the BDDs
00287     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
00288     Abc_NtkForEachCo( pNtk, pObj, i )
00289     {
00290         bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
00291         if ( bFunc == NULL )
00292         {
00293             if ( fVerbose )
00294             printf( "Constructing global BDDs is aborted.\n" );
00295             Abc_NtkFreeGlobalBdds( pNtk, 0 );
00296             Cudd_Quit( dd );
00297             return NULL;
00298         }
00299         bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
00300         Abc_ObjSetGlobalBdd( pObj, bFunc );
00301     }
00302     Extra_ProgressBarStop( pProgress );
00303 
00304 /*
00305     // derefence the intermediate BDDs
00306     Abc_NtkForEachNode( pNtk, pObj, i )
00307         if ( pObj->pCopy ) 
00308         {
00309             Cudd_RecursiveDeref( dd, (DdNode *)pObj->pCopy );
00310             pObj->pCopy = NULL;
00311         }
00312 */
00313 /*
00314     // make sure all nodes are derefed
00315     Abc_NtkForEachObj( pNtk, pObj, i )
00316     {
00317         if ( pObj->pCopy != NULL )
00318             printf( "Abc_NtkBuildGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id );
00319         if ( pObj->vFanouts.nSize > 0 )
00320             printf( "Abc_NtkBuildGlobalBdds() error: Node %d has refs assigned\n", pObj->Id );
00321     }
00322 */
00323     // reset references
00324     Abc_NtkForEachObj( pNtk, pObj, i )
00325         if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
00326             Abc_ObjForEachFanin( pObj, pFanin, k )
00327                 pFanin->vFanouts.nSize++;
00328 
00329     // reorder one more time
00330     if ( fReorder )
00331     {
00332         Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
00333         Cudd_AutodynDisable( dd );
00334     }
00335 //    Cudd_PrintInfo( dd, stdout );
00336     return dd;
00337 }
00338 
00350 DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
00351 {
00352     DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
00353     int fDetectMuxes = 1;
00354     assert( !Abc_ObjIsComplement(pNode) );
00355     if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
00356     {
00357         Extra_ProgressBarStop( pProgress );
00358         if ( fVerbose )
00359         printf( "The number of live nodes reached %d.\n", nBddSizeMax );
00360         fflush( stdout );
00361         return NULL;
00362     }
00363     // if the result is available return
00364     if ( Abc_ObjGlobalBdd(pNode) == NULL )
00365     {
00366         Abc_Obj_t * pNodeC, * pNode0, * pNode1;
00367         pNode0 = Abc_ObjFanin0(pNode);
00368         pNode1 = Abc_ObjFanin1(pNode);
00369         // check for the special case when it is MUX/EXOR
00370         if ( fDetectMuxes && 
00371              Abc_ObjGlobalBdd(pNode0) == NULL && Abc_ObjGlobalBdd(pNode1) == NULL &&
00372              Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 && 
00373              Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 && 
00374              Abc_NodeIsMuxType(pNode) )
00375         {
00376             // deref the fanins
00377             pNode0->vFanouts.nSize--;
00378             pNode1->vFanouts.nSize--;
00379             // recognize the MUX
00380             pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
00381             assert( Abc_ObjFanoutNum(pNodeC) > 1 );
00382             // dereference the control once (the second time it will be derefed when BDDs are computed)
00383             pNodeC->vFanouts.nSize--;
00384 
00385             // compute the result for all branches
00386             bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
00387             if ( bFuncC == NULL )
00388                 return NULL;
00389             Cudd_Ref( bFuncC );
00390             bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
00391             if ( bFunc0 == NULL )
00392                 return NULL;
00393             Cudd_Ref( bFunc0 );
00394             bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
00395             if ( bFunc1 == NULL )
00396                 return NULL;
00397             Cudd_Ref( bFunc1 );
00398 
00399             // complement the branch BDDs
00400             bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjIsComplement(pNode0) );
00401             bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjIsComplement(pNode1) );
00402             // get the final result
00403             bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 );   Cudd_Ref( bFunc );
00404             Cudd_RecursiveDeref( dd, bFunc0 );
00405             Cudd_RecursiveDeref( dd, bFunc1 );
00406             Cudd_RecursiveDeref( dd, bFuncC );
00407             // add the number of used nodes
00408             (*pCounter) += 3;
00409         }
00410         else
00411         {
00412             // compute the result for both branches
00413             bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
00414             if ( bFunc0 == NULL )
00415                 return NULL;
00416             Cudd_Ref( bFunc0 );
00417             bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
00418             if ( bFunc1 == NULL )
00419                 return NULL;
00420             Cudd_Ref( bFunc1 );
00421             bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
00422             bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
00423             // get the final result
00424             bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
00425             Cudd_RecursiveDeref( dd, bFunc0 );
00426             Cudd_RecursiveDeref( dd, bFunc1 );
00427             // add the number of used nodes
00428             (*pCounter)++;
00429         }
00430         // set the result
00431         assert( Abc_ObjGlobalBdd(pNode) == NULL );
00432         Abc_ObjSetGlobalBdd( pNode, bFunc );
00433         // increment the progress bar
00434         if ( pProgress )
00435             Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
00436     }
00437     // prepare the return value
00438     bFunc = Abc_ObjGlobalBdd(pNode);
00439     // dereference BDD at the node
00440     if ( --pNode->vFanouts.nSize == 0 && fDropInternal )
00441     {
00442         Cudd_Deref( bFunc );
00443         Abc_ObjSetGlobalBdd( pNode, NULL );
00444     }
00445     return bFunc;
00446 }
00447 
00459 DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan ) 
00460 { 
00461     return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan ); 
00462 }
00463 
00475 int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk ) 
00476 {
00477     Vec_Ptr_t * vFuncsGlob;
00478     Abc_Obj_t * pObj;
00479     int RetValue, i;
00480     // complement the global functions
00481     vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
00482     Abc_NtkForEachCo( pNtk, pObj, i )
00483         Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
00484     RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
00485     Vec_PtrFree( vFuncsGlob );
00486     return RetValue;
00487 }
00488 
00500 double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
00501 {
00502     /*
00503     Vec_Ptr_t * vNodes;
00504     Abc_Obj_t * pObj, * pNodeR;
00505     DdManager * dd;
00506     DdNode * bFunc;
00507     double Result;
00508     int i;
00509     pNodeR = Abc_ObjRegular(pNode);
00510     assert( Abc_NtkIsStrash(pNodeR->pNtk) );
00511     Abc_NtkCleanCopy( pNodeR->pNtk );
00512     // get the CIs in the support of the node
00513     vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 );
00514     // start the manager
00515     dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00516     Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
00517     // assign elementary BDDs for the CIs
00518     Vec_PtrForEachEntry( vNodes, pObj, i )
00519         pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
00520     // build the BDD of the cone
00521     bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, 1, NULL, NULL, 1 );  Cudd_Ref( bFunc );
00522     bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
00523     // count minterms
00524     Result = Cudd_CountMinterm( dd, bFunc, dd->size );
00525     // get the percentagle
00526     Result *= 100.0;
00527     for ( i = 0; i < dd->size; i++ )
00528         Result /= 2;
00529     // clean up
00530     Cudd_Quit( dd );
00531     Vec_PtrFree( vNodes );
00532     return Result;
00533     */
00534     return 0.0;
00535 }
00536 
00537 
00538 
00539 
00551 void Abc_NtkBddImplicationTest()
00552 {
00553     DdManager * dd;
00554     DdNode * bImp, * bSum, * bTemp;
00555     int nVars = 200;
00556     int nImps = 200;
00557     int i, clk;
00558 clk = clock();
00559     dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00560     Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
00561     bSum = b0;   Cudd_Ref( bSum );
00562     for ( i = 0; i < nImps; i++ )
00563     {
00564         printf( "." );
00565         bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] );  Cudd_Ref( bImp );
00566         bSum = Cudd_bddOr( dd, bTemp = bSum, bImp );     Cudd_Ref( bSum );
00567         Cudd_RecursiveDeref( dd, bTemp );
00568         Cudd_RecursiveDeref( dd, bImp );
00569     }
00570     printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
00571     Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
00572     printf( "The BDD after  = %d.\n", Cudd_DagSize(bSum) );
00573 PRT( "Time", clock() - clk );
00574     Cudd_RecursiveDeref( dd, bSum );
00575     Cudd_Quit( dd );
00576 }
00577 
00581 
00582