abc70930: src/base/abc/abcFunc.c Source File

00001 
00021 #include "abc.h"
00022 #include "main.h"
00023 #include "mio.h"
00024 
00028 
00029 #define ABC_MUX_CUBES   100000
00030 
00031 static int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
00032 static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
00033 static Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop );
00034 
00038 
00050 int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
00051 {
00052     Abc_Obj_t * pNode;
00053     DdManager * dd;
00054     int nFaninsMax, i;
00055  
00056     assert( Abc_NtkHasSop(pNtk) ); 
00057 
00058     // start the functionality manager
00059     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
00060     if ( nFaninsMax == 0 )
00061         printf( "Warning: The network has only constant nodes.\n" );
00062 
00063     dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00064 
00065     // convert each node from SOP to BDD
00066     Abc_NtkForEachNode( pNtk, pNode, i )
00067     {
00068         assert( pNode->pData );
00069         pNode->pData = Abc_ConvertSopToBdd( dd, pNode->pData );
00070         if ( pNode->pData == NULL )
00071         {
00072             printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
00073             return 0;
00074         }
00075         Cudd_Ref( pNode->pData );
00076     }
00077 
00078     Extra_MmFlexStop( pNtk->pManFunc );
00079     pNtk->pManFunc = dd;
00080 
00081     // update the network type
00082     pNtk->ntkFunc = ABC_FUNC_BDD;
00083     return 1;
00084 }
00085 
00097 DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
00098 {
00099     DdNode * bSum, * bCube, * bTemp, * bVar;
00100     char * pCube;
00101     int nVars, Value, v;
00102 
00103     // start the cover
00104     nVars = Abc_SopGetVarNum(pSop);
00105     bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
00106     if ( Abc_SopIsExorType(pSop) )
00107     {
00108         for ( v = 0; v < nVars; v++ )
00109         {
00110             bSum  = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
00111             Cudd_RecursiveDeref( dd, bTemp );
00112         }
00113     }
00114     else
00115     {
00116         // check the logic function of the node
00117         Abc_SopForEachCube( pSop, nVars, pCube )
00118         {
00119             bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
00120             Abc_CubeForEachVar( pCube, Value, v )
00121             {
00122                 if ( Value == '0' )
00123                     bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
00124                 else if ( Value == '1' )
00125                     bVar = Cudd_bddIthVar( dd, v );
00126                 else
00127                     continue;
00128                 bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
00129                 Cudd_RecursiveDeref( dd, bTemp );
00130             }
00131             bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
00132             Cudd_Ref( bSum );
00133             Cudd_RecursiveDeref( dd, bTemp );
00134             Cudd_RecursiveDeref( dd, bCube );
00135         }
00136     }
00137     // complement the result if necessary
00138     bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
00139     Cudd_Deref( bSum );
00140     return bSum;
00141 }
00142 
00154 void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
00155 {
00156     DdManager * dd;
00157     DdNode * bFunc;
00158     Vec_Str_t * vCube;
00159     Abc_Obj_t * pNode;
00160     int nFaninsMax, fFound, i;
00161 
00162     assert( Abc_NtkHasSop(pNtk) );
00163 
00164     // check if there are nodes with complemented SOPs
00165     fFound = 0;
00166     Abc_NtkForEachNode( pNtk, pNode, i )
00167         if ( Abc_SopIsComplement(pNode->pData) )
00168         {
00169             fFound = 1;
00170             break;
00171         }
00172     if ( !fFound )
00173         return;
00174 
00175     // start the BDD package
00176     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
00177     if ( nFaninsMax == 0 )
00178         printf( "Warning: The network has only constant nodes.\n" );
00179     dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00180 
00181     // change the cover of negated nodes
00182     vCube = Vec_StrAlloc( 100 );
00183     Abc_NtkForEachNode( pNtk, pNode, i )
00184         if ( Abc_SopIsComplement(pNode->pData) )
00185         {
00186             bFunc = Abc_ConvertSopToBdd( dd, pNode->pData );  Cudd_Ref( bFunc );
00187             pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
00188             Cudd_RecursiveDeref( dd, bFunc );
00189             assert( !Abc_SopIsComplement(pNode->pData) );
00190         }
00191     Vec_StrFree( vCube );
00192     Extra_StopManager( dd );
00193 }
00194 
00195 
00196 
00197 
00198 
00210 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
00211 {
00212     Abc_Obj_t * pNode;
00213     Extra_MmFlex_t * pManNew;
00214     DdManager * dd = pNtk->pManFunc;
00215     DdNode * bFunc;
00216     Vec_Str_t * vCube;
00217     int i, fMode;
00218 
00219     if ( fDirect )
00220         fMode = 1;
00221     else
00222         fMode = -1;
00223 
00224     assert( Abc_NtkHasBdd(pNtk) );
00225     if ( dd->size > 0 )
00226     Cudd_zddVarsFromBddVars( dd, 2 );
00227     // create the new manager
00228     pManNew = Extra_MmFlexStart();
00229 
00230     // go through the objects
00231     vCube = Vec_StrAlloc( 100 );
00232     Abc_NtkForEachNode( pNtk, pNode, i )
00233     {
00234         assert( pNode->pData );
00235         bFunc = pNode->pData;
00236         pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
00237         if ( pNode->pNext == NULL )
00238         {
00239             Extra_MmFlexStop( pManNew );
00240             Abc_NtkCleanNext( pNtk );
00241 //            printf( "Converting from BDDs to SOPs has failed.\n" );
00242             Vec_StrFree( vCube );
00243             return 0;
00244         }
00245     }
00246     Vec_StrFree( vCube );
00247 
00248     // update the network type
00249     pNtk->ntkFunc = ABC_FUNC_SOP;
00250     // set the new manager
00251     pNtk->pManFunc = pManNew;
00252     // transfer from next to data
00253     Abc_NtkForEachNode( pNtk, pNode, i )
00254     {
00255         Cudd_RecursiveDeref( dd, pNode->pData );
00256         pNode->pData = pNode->pNext;
00257         pNode->pNext = NULL;
00258     }
00259 
00260     // check for remaining references in the package
00261     Extra_StopManager( dd );
00262     return 1;
00263 }
00264 
00276 char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
00277 {
00278     int fVerify = 0;
00279     char * pSop;
00280     DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
00281     int nCubes, nCubes0, nCubes1, fPhase;
00282 
00283     assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
00284     if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
00285     {
00286         if ( fMode == -1 ) // if the phase is not known, write constant 1
00287             fMode = 1;
00288         Vec_StrFill( vCube, nFanins, '-' );
00289         Vec_StrPush( vCube, '\0' );
00290         if ( pMan )
00291             pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
00292         else
00293             pSop = ALLOC( char, nFanins + 4 );
00294         if ( bFuncOn == Cudd_ReadOne(dd) )
00295             sprintf( pSop, "%s %d\n", vCube->pArray, fMode );
00296         else
00297             sprintf( pSop, "%s %d\n", vCube->pArray, !fMode );
00298         return pSop;
00299     }
00300 
00301 
00302     if ( fMode == -1 )
00303     { // try both phases
00304         assert( fAllPrimes == 0 );
00305 
00306         // get the ZDD of the negative polarity
00307         bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 );
00308         Cudd_Ref( zCover0 );
00309         Cudd_Ref( bCover );
00310         Cudd_RecursiveDeref( dd, bCover );
00311         nCubes0 = Abc_CountZddCubes( dd, zCover0 );
00312 
00313         // get the ZDD of the positive polarity
00314         bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover1 );
00315         Cudd_Ref( zCover1 );
00316         Cudd_Ref( bCover );
00317         Cudd_RecursiveDeref( dd, bCover );
00318         nCubes1 = Abc_CountZddCubes( dd, zCover1 );
00319 
00320         // compare the number of cubes
00321         if ( nCubes1 <= nCubes0 )
00322         { // use positive polarity
00323             nCubes = nCubes1;
00324             zCover = zCover1;
00325             Cudd_RecursiveDerefZdd( dd, zCover0 );
00326             fPhase = 1;
00327         }
00328         else
00329         { // use negative polarity
00330             nCubes = nCubes0;
00331             zCover = zCover0;
00332             Cudd_RecursiveDerefZdd( dd, zCover1 );
00333             fPhase = 0;
00334         }
00335     }
00336     else if ( fMode == 0 )
00337     {
00338         // get the ZDD of the negative polarity
00339         if ( fAllPrimes )
00340         {
00341             zCover = Extra_zddPrimes( dd, Cudd_Not(bFuncOnDc) ); 
00342             Cudd_Ref( zCover );
00343         }
00344         else
00345         {
00346             bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
00347             Cudd_Ref( zCover );
00348             Cudd_Ref( bCover );
00349             Cudd_RecursiveDeref( dd, bCover );
00350         }
00351         nCubes = Abc_CountZddCubes( dd, zCover );
00352         fPhase = 0;
00353     }
00354     else if ( fMode == 1 )
00355     {
00356         // get the ZDD of the positive polarity
00357         if ( fAllPrimes )
00358         {
00359             zCover = Extra_zddPrimes( dd, bFuncOnDc ); 
00360             Cudd_Ref( zCover );
00361         }
00362         else
00363         {
00364             bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
00365             Cudd_Ref( zCover );
00366             Cudd_Ref( bCover );
00367             Cudd_RecursiveDeref( dd, bCover );
00368         }
00369         nCubes = Abc_CountZddCubes( dd, zCover );
00370         fPhase = 1;
00371     }
00372     else
00373     {
00374         assert( 0 );
00375     }
00376 
00377     if ( nCubes > ABC_MUX_CUBES )
00378     {
00379         Cudd_RecursiveDerefZdd( dd, zCover );
00380         printf( "The number of cubes exceeded the predefined limit (%d).\n", ABC_MUX_CUBES );
00381         return NULL;
00382     }
00383 
00384     // allocate memory for the cover
00385     if ( pMan )
00386         pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
00387     else 
00388         pSop = ALLOC( char, (nFanins + 3) * nCubes + 1 );
00389     pSop[(nFanins + 3) * nCubes] = 0;
00390     // create the SOP
00391     Vec_StrFill( vCube, nFanins, '-' );
00392     Vec_StrPush( vCube, '\0' );
00393     Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
00394     Cudd_RecursiveDerefZdd( dd, zCover );
00395 
00396     // verify
00397     if ( fVerify )
00398     {
00399         bFuncNew = Abc_ConvertSopToBdd( dd, pSop );  Cudd_Ref( bFuncNew );
00400         if ( bFuncOn == bFuncOnDc )
00401         {
00402             if ( bFuncNew != bFuncOn )
00403                 printf( "Verification failed.\n" );
00404         }
00405         else
00406         {
00407             if ( !Cudd_bddLeq(dd, bFuncOn, bFuncNew) || !Cudd_bddLeq(dd, bFuncNew, bFuncOnDc) )
00408                 printf( "Verification failed.\n" );
00409         }
00410         Cudd_RecursiveDeref( dd, bFuncNew );
00411     }
00412     return pSop;
00413 }
00414 
00426 void Abc_ConvertZddToSop_rec( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase, int * pnCubes )
00427 {
00428     DdNode * zC0, * zC1, * zC2;
00429     int Index;
00430 
00431     if ( zCover == dd->zero )
00432         return;
00433     if ( zCover == dd->one )
00434     {
00435         char * pCube;
00436         pCube = pSop + (*pnCubes) * (nFanins + 3);
00437         sprintf( pCube, "%s %d\n", vCube->pArray, fPhase );
00438         (*pnCubes)++;
00439         return;
00440     }
00441     Index = zCover->index/2;
00442     assert( Index < nFanins );
00443     extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
00444     vCube->pArray[Index] = '0';
00445     Abc_ConvertZddToSop_rec( dd, zC0, pSop, nFanins, vCube, fPhase, pnCubes );
00446     vCube->pArray[Index] = '1';
00447     Abc_ConvertZddToSop_rec( dd, zC1, pSop, nFanins, vCube, fPhase, pnCubes );
00448     vCube->pArray[Index] = '-';
00449     Abc_ConvertZddToSop_rec( dd, zC2, pSop, nFanins, vCube, fPhase, pnCubes );
00450 }
00451 
00463 int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase )
00464 {
00465     int nCubes = 0;
00466     Abc_ConvertZddToSop_rec( dd, zCover, pSop, nFanins, vCube, fPhase, &nCubes );
00467     return nCubes;
00468 }
00469 
00470 
00482 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
00483 {
00484     assert( Abc_NtkHasBdd(pNode->pNtk) ); 
00485     *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
00486     *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 );
00487 }
00488 
00489 
00490 
00491 
00503 void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
00504 {
00505     DdNode * zC0, * zC1, * zC2;
00506     if ( zCover == dd->zero )
00507         return;
00508     if ( zCover == dd->one )
00509     {
00510         (*pnCubes)++;
00511         return;
00512     }
00513     if ( (*pnCubes) > ABC_MUX_CUBES )
00514         return;
00515     extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
00516     Abc_CountZddCubes_rec( dd, zC0, pnCubes );
00517     Abc_CountZddCubes_rec( dd, zC1, pnCubes );
00518     Abc_CountZddCubes_rec( dd, zC2, pnCubes );
00519 }
00520 
00532 int Abc_CountZddCubes( DdManager * dd, DdNode * zCover )
00533 {
00534     int nCubes = 0;
00535     Abc_CountZddCubes_rec( dd, zCover, &nCubes );
00536     return nCubes;
00537 }
00538 
00539 
00551 int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
00552 {
00553     Abc_Obj_t * pNode;
00554     Hop_Man_t * pMan;
00555     int i;
00556 
00557     assert( Abc_NtkHasSop(pNtk) ); 
00558 
00559     // start the functionality manager
00560     pMan = Hop_ManStart();
00561 
00562     // convert each node from SOP to BDD
00563     Abc_NtkForEachNode( pNtk, pNode, i )
00564     {
00565         assert( pNode->pData );
00566         pNode->pData = Abc_ConvertSopToAig( pMan, pNode->pData );
00567         if ( pNode->pData == NULL )
00568         {
00569             printf( "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
00570             return 0;
00571         }
00572     }
00573     Extra_MmFlexStop( pNtk->pManFunc );
00574     pNtk->pManFunc = pMan;
00575 
00576     // update the network type
00577     pNtk->ntkFunc = ABC_FUNC_AIG;
00578     return 1;
00579 }
00580 
00581 
00593 Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
00594 {
00595     Hop_Obj_t * pAnd, * pSum;
00596     int i, Value, nFanins;
00597     char * pCube;
00598     // get the number of variables
00599     nFanins = Abc_SopGetVarNum(pSop);
00600     // go through the cubes of the node's SOP
00601     pSum = Hop_ManConst0(pMan);
00602     Abc_SopForEachCube( pSop, nFanins, pCube )
00603     {
00604         // create the AND of literals
00605         pAnd = Hop_ManConst1(pMan);
00606         Abc_CubeForEachVar( pCube, Value, i )
00607         {
00608             if ( Value == '1' )
00609                 pAnd = Hop_And( pMan, pAnd, Hop_IthVar(pMan,i) );
00610             else if ( Value == '0' )
00611                 pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
00612         }
00613         // add to the sum of cubes
00614         pSum = Hop_Or( pMan, pSum, pAnd );
00615     }
00616     // decide whether to complement the result
00617     if ( Abc_SopIsComplement(pSop) )
00618         pSum = Hop_Not(pSum);
00619     return pSum;
00620 }
00621 
00633 Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
00634 {
00635     extern Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop );
00636     int fUseFactor = 1;
00637     // consider the constant node
00638     if ( Abc_SopGetVarNum(pSop) == 0 )
00639         return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
00640     // consider the special case of EXOR function
00641     if ( Abc_SopIsExorType(pSop) )
00642         return Hop_NotCond( Hop_CreateExor(pMan, Abc_SopGetVarNum(pSop)), Abc_SopIsComplement(pSop) );
00643     // decide when to use factoring
00644     if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
00645         return Dec_GraphFactorSop( pMan, pSop );
00646     return Abc_ConvertSopToAigInternal( pMan, pSop );
00647 }
00648 
00660 int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk )
00661 {
00662     Abc_Obj_t * pNode;
00663     Hop_Man_t * pMan;
00664     DdManager * dd;
00665     int nFaninsMax, i;
00666 
00667     assert( Abc_NtkHasAig(pNtk) ); 
00668 
00669     // start the functionality manager
00670     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
00671     if ( nFaninsMax == 0 )
00672         printf( "Warning: The network has only constant nodes.\n" );
00673 
00674     dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00675 
00676     // set the mapping of elementary AIG nodes into the elementary BDD nodes
00677     pMan = pNtk->pManFunc;
00678     assert( Hop_ManPiNum(pMan) >= nFaninsMax ); 
00679     for ( i = 0; i < nFaninsMax; i++ )
00680     {
00681         Hop_ManPi(pMan, i)->pData = Cudd_bddIthVar(dd, i);
00682         Cudd_Ref( Hop_ManPi(pMan, i)->pData );
00683     }
00684 
00685     // convert each node from SOP to BDD
00686     Abc_NtkForEachNode( pNtk, pNode, i )
00687     {
00688         assert( pNode->pData );
00689         pNode->pData = Abc_ConvertAigToBdd( dd, pNode->pData );
00690         if ( pNode->pData == NULL )
00691         {
00692             printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
00693             return 0;
00694         }
00695         Cudd_Ref( pNode->pData );
00696     }
00697 
00698     // dereference intermediate BDD nodes
00699     for ( i = 0; i < nFaninsMax; i++ )
00700         Cudd_RecursiveDeref( dd, Hop_ManPi(pMan, i)->pData );
00701 
00702     Hop_ManStop( pNtk->pManFunc );
00703     pNtk->pManFunc = dd;
00704 
00705     // update the network type
00706     pNtk->ntkFunc = ABC_FUNC_BDD;
00707     return 1;
00708 }
00709 
00721 void Abc_ConvertAigToBdd_rec1( DdManager * dd, Hop_Obj_t * pObj )
00722 {
00723     assert( !Hop_IsComplement(pObj) );
00724     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00725         return;
00726     Abc_ConvertAigToBdd_rec1( dd, Hop_ObjFanin0(pObj) ); 
00727     Abc_ConvertAigToBdd_rec1( dd, Hop_ObjFanin1(pObj) );
00728     pObj->pData = Cudd_bddAnd( dd, (DdNode *)Hop_ObjChild0Copy(pObj), (DdNode *)Hop_ObjChild1Copy(pObj) ); 
00729     Cudd_Ref( pObj->pData );
00730     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00731     Hop_ObjSetMarkA( pObj );
00732 }
00733 
00745 void Abc_ConvertAigToBdd_rec2( DdManager * dd, Hop_Obj_t * pObj )
00746 {
00747     assert( !Hop_IsComplement(pObj) );
00748     if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
00749         return;
00750     Abc_ConvertAigToBdd_rec2( dd, Hop_ObjFanin0(pObj) ); 
00751     Abc_ConvertAigToBdd_rec2( dd, Hop_ObjFanin1(pObj) );
00752     Cudd_RecursiveDeref( dd, pObj->pData );
00753     pObj->pData = NULL;
00754     assert( Hop_ObjIsMarkA(pObj) ); // loop detection
00755     Hop_ObjClearMarkA( pObj );
00756 }
00757 
00769 DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
00770 {
00771     DdNode * bFunc;
00772     // check the case of a constant
00773     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
00774         return Cudd_NotCond( Cudd_ReadOne(dd), Hop_IsComplement(pRoot) );
00775     // construct BDD
00776     Abc_ConvertAigToBdd_rec1( dd, Hop_Regular(pRoot) );
00777     // hold on to the result
00778     bFunc = Cudd_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  Cudd_Ref( bFunc );
00779     // dereference BDD
00780     Abc_ConvertAigToBdd_rec2( dd, Hop_Regular(pRoot) );
00781     // return the result
00782     Cudd_Deref( bFunc );
00783     return bFunc;
00784 }
00785 
00786 
00787 
00799 int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj )
00800 {
00801     int Counter = 0;
00802     assert( !Hop_IsComplement(pObj) );
00803     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00804         return 0;
00805     Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); 
00806     Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
00807     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00808     Hop_ObjSetMarkA( pObj );
00809     return Counter + 1;
00810 }
00811 
00823 unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
00824 {
00825     unsigned * pTruth, * pTruth0, * pTruth1;
00826     int i;
00827     assert( !Hop_IsComplement(pObj) );
00828     if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
00829         return pObj->pData;
00830     // compute the truth tables of the fanins
00831     pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
00832     pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
00833     // creat the truth table of the node
00834     pTruth  = Vec_IntFetch( vTruth, nWords );
00835     if ( Hop_ObjIsExor(pObj) )
00836         for ( i = 0; i < nWords; i++ )
00837             pTruth[i] = pTruth0[i] ^ pTruth1[i];
00838     else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
00839         for ( i = 0; i < nWords; i++ )
00840             pTruth[i] = pTruth0[i] & pTruth1[i];
00841     else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
00842         for ( i = 0; i < nWords; i++ )
00843             pTruth[i] = pTruth0[i] & ~pTruth1[i];
00844     else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
00845         for ( i = 0; i < nWords; i++ )
00846             pTruth[i] = ~pTruth0[i] & pTruth1[i];
00847     else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
00848         for ( i = 0; i < nWords; i++ )
00849             pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
00850     assert( Hop_ObjIsMarkA(pObj) ); // loop detection
00851     Hop_ObjClearMarkA( pObj );
00852     pObj->pData = pTruth;
00853     return pTruth;
00854 }
00855 
00869 unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
00870 {
00871     static unsigned uTruths[8][8] = { // elementary truth tables
00872         { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
00873         { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
00874         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
00875         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
00876         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
00877         { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
00878         { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
00879         { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
00880     };
00881     Hop_Obj_t * pObj;
00882     unsigned * pTruth, * pTruth2;
00883     int i, nWords, nNodes;
00884     Vec_Ptr_t * vTtElems;
00885 
00886     // if the number of variables is more than 8, allocate truth tables
00887     if ( nVars > 8 )
00888         vTtElems = Vec_PtrAllocTruthTables( nVars );
00889     else
00890         vTtElems = NULL;
00891 
00892     // clear the data fields and set marks
00893     nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
00894     // prepare memory
00895     nWords = Hop_TruthWordNum( nVars );
00896     Vec_IntClear( vTruth );
00897     Vec_IntGrow( vTruth, nWords * (nNodes+1) );
00898     pTruth = Vec_IntFetch( vTruth, nWords );
00899     // check the case of a constant
00900     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
00901     {
00902         assert( nNodes == 0 );
00903         if ( Hop_IsComplement(pRoot) )
00904             Extra_TruthClear( pTruth, nVars );
00905         else
00906             Extra_TruthFill( pTruth, nVars );
00907         return pTruth;
00908     }
00909     // set elementary truth tables at the leaves
00910     assert( nVars <= Hop_ManPiNum(p) );
00911 //    assert( Hop_ManPiNum(p) <= 8 ); 
00912     if ( fMsbFirst )
00913     {
00914         Hop_ManForEachPi( p, pObj, i )
00915         {
00916             if ( vTtElems )
00917                 pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
00918             else               
00919                 pObj->pData = (void *)uTruths[nVars-1-i];
00920         }
00921     }
00922     else
00923     {
00924         Hop_ManForEachPi( p, pObj, i )
00925         {
00926             if ( vTtElems )
00927                 pObj->pData = Vec_PtrEntry(vTtElems, i);
00928             else               
00929                 pObj->pData = (void *)uTruths[i];
00930         }
00931     }
00932     // clear the marks and compute the truth table
00933     pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
00934     // copy the result
00935     Extra_TruthCopy( pTruth, pTruth2, nVars );
00936     if ( vTtElems )
00937         Vec_PtrFree( vTtElems );
00938     return pTruth;
00939 }
00940 
00941 
00953 void Abc_ConvertAigToAig_rec( Abc_Ntk_t * pNtkAig, Hop_Obj_t * pObj )
00954 {
00955     assert( !Hop_IsComplement(pObj) );
00956     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
00957         return;
00958     Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin0(pObj) ); 
00959     Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin1(pObj) );
00960     pObj->pData = Abc_AigAnd( pNtkAig->pManFunc, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) ); 
00961     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
00962     Hop_ObjSetMarkA( pObj );
00963 }
00964 
00976 Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld )
00977 {
00978     Hop_Man_t * pHopMan;
00979     Hop_Obj_t * pRoot;
00980     Abc_Obj_t * pFanin;
00981     int i;
00982     // get the local AIG
00983     pHopMan = pObjOld->pNtk->pManFunc;
00984     pRoot = pObjOld->pData;
00985     // check the case of a constant
00986     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
00987         return Abc_ObjNotCond( Abc_AigConst1(pNtkAig), Hop_IsComplement(pRoot) );
00988     // assign the fanin nodes
00989     Abc_ObjForEachFanin( pObjOld, pFanin, i )
00990     {
00991         assert( pFanin->pCopy != NULL );
00992         Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
00993     }
00994     // construct the AIG
00995     Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
00996     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
00997     // return the result
00998     return Abc_ObjNotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
00999 }
01000 
01001 
01013 int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
01014 {
01015     extern void * Abc_FrameReadLibGen();                    
01016     Abc_Obj_t * pNode;
01017     char * pSop;
01018     int i;
01019 
01020     assert( Abc_NtkHasMapping(pNtk) );
01021     // update the functionality manager
01022     assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
01023     pNtk->pManFunc = Extra_MmFlexStart();
01024     pNtk->ntkFunc  = ABC_FUNC_SOP;
01025     // update the nodes
01026     Abc_NtkForEachNode( pNtk, pNode, i )
01027     {
01028         pSop = Mio_GateReadSop(pNode->pData);
01029         assert( Abc_SopGetVarNum(pSop) == Abc_ObjFaninNum(pNode) );
01030         pNode->pData = Abc_SopRegister( pNtk->pManFunc, pSop );
01031     }
01032     return 1;
01033 }
01034 
01046 int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk )
01047 {
01048     return 1;
01049 }
01050 
01062 int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
01063 {
01064     assert( !Abc_NtkIsStrash(pNtk) );
01065     if ( Abc_NtkHasSop(pNtk) )
01066     {
01067         if ( !fDirect )
01068             return 1;
01069         if ( !Abc_NtkSopToBdd(pNtk) )
01070             return 0;
01071         return Abc_NtkBddToSop(pNtk, fDirect);
01072     }
01073     if ( Abc_NtkHasMapping(pNtk) )
01074         return Abc_NtkMapToSop(pNtk);
01075     if ( Abc_NtkHasBdd(pNtk) )
01076         return Abc_NtkBddToSop(pNtk, fDirect);
01077     if ( Abc_NtkHasAig(pNtk) )
01078     {
01079         if ( !Abc_NtkAigToBdd(pNtk) )
01080             return 0;
01081         return Abc_NtkBddToSop(pNtk, fDirect);
01082     }
01083     assert( 0 );
01084     return 0;
01085 }
01086 
01098 int Abc_NtkToBdd( Abc_Ntk_t * pNtk )
01099 {
01100     assert( !Abc_NtkIsStrash(pNtk) );
01101     if ( Abc_NtkHasBdd(pNtk) )
01102         return 1;
01103     if ( Abc_NtkHasMapping(pNtk) )
01104     {
01105         Abc_NtkMapToSop(pNtk);
01106         return Abc_NtkSopToBdd(pNtk);
01107     }
01108     if ( Abc_NtkHasSop(pNtk) )
01109         return Abc_NtkSopToBdd(pNtk);
01110     if ( Abc_NtkHasAig(pNtk) )
01111         return Abc_NtkAigToBdd(pNtk);
01112     assert( 0 );
01113     return 0;
01114 }
01115 
01127 int Abc_NtkToAig( Abc_Ntk_t * pNtk )
01128 {
01129     assert( !Abc_NtkIsStrash(pNtk) );
01130     if ( Abc_NtkHasAig(pNtk) )
01131         return 1;
01132     if ( Abc_NtkHasMapping(pNtk) )
01133     {
01134         Abc_NtkMapToSop(pNtk);
01135         return Abc_NtkSopToAig(pNtk);
01136     }
01137     if ( Abc_NtkHasBdd(pNtk) )
01138     {
01139         if ( !Abc_NtkBddToSop(pNtk,0) )
01140             return 0;
01141         return Abc_NtkSopToAig(pNtk);
01142     }
01143     if ( Abc_NtkHasSop(pNtk) )
01144         return Abc_NtkSopToAig(pNtk);
01145     assert( 0 );
01146     return 0;
01147 }
01148 
01149 
01153 
01154