#include "abc.h"
#include "main.h"
#include "mio.h"
Go to the source code of this file.
#define ABC_MUX_CUBES 100000 |
CFile****************************************************************
FileName [abcFunc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Transformations between different functionality representations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [
] DECLARATIONS ///
Function*************************************************************
Synopsis [Converts the network from AIG to BDD representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 976 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 953 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Converts the network from AIG to BDD representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 769 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 721 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Dereference BDDs and unmark AIG nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 745 of file abcFunc.c.
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 }
unsigned* Abc_ConvertAigToTruth | ( | Hop_Man_t * | p, | |
Hop_Obj_t * | pRoot, | |||
int | nVars, | |||
Vec_Int_t * | vTruth, | |||
int | fMsbFirst | |||
) |
Function*************************************************************
Synopsis [Computes truth table of the node.]
Description [Assumes that the structural support is no more than 8 inputs. Uses array vTruth to store temporary truth tables. The returned pointer should be used immediately.]
SideEffects []
SeeAlso []
Definition at line 869 of file abcFunc.c.
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 }
int Abc_ConvertAigToTruth_rec1 | ( | Hop_Obj_t * | pObj | ) |
Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 799 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
Definition at line 823 of file abcFunc.c.
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 }
char* Abc_ConvertBddToSop | ( | Extra_MmFlex_t * | pMan, | |
DdManager * | dd, | |||
DdNode * | bFuncOn, | |||
DdNode * | bFuncOnDc, | |||
int | nFanins, | |||
int | fAllPrimes, | |||
Vec_Str_t * | vCube, | |||
int | fMode | |||
) |
Function*************************************************************
Synopsis [Converts the node from BDD to SOP representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 276 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Converts the network from AIG to BDD representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 633 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
Definition at line 593 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Converts the node from SOP to BDD representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 97 of file abcFunc.c.
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 }
int Abc_ConvertZddToSop | ( | DdManager * | dd, | |
DdNode * | zCover, | |||
char * | pSop, | |||
int | nFanins, | |||
Vec_Str_t * | vCube, | |||
int | fPhase | |||
) | [static] |
Function*************************************************************
Synopsis [Derive the BDD for the function in the cut.]
Description []
SideEffects []
SeeAlso []
Definition at line 463 of file abcFunc.c.
00464 { 00465 int nCubes = 0; 00466 Abc_ConvertZddToSop_rec( dd, zCover, pSop, nFanins, vCube, fPhase, &nCubes ); 00467 return nCubes; 00468 }
void Abc_ConvertZddToSop_rec | ( | DdManager * | dd, | |
DdNode * | zCover, | |||
char * | pSop, | |||
int | nFanins, | |||
Vec_Str_t * | vCube, | |||
int | fPhase, | |||
int * | pnCubes | |||
) |
Function*************************************************************
Synopsis [Derive the SOP from the ZDD representation of the cubes.]
Description []
SideEffects []
SeeAlso []
Definition at line 426 of file abcFunc.c.
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 }
Function*************************************************************
Synopsis [Count the number of paths in the ZDD.]
Description []
SideEffects []
SeeAlso []
Definition at line 532 of file abcFunc.c.
00533 { 00534 int nCubes = 0; 00535 Abc_CountZddCubes_rec( dd, zCover, &nCubes ); 00536 return nCubes; 00537 }
Function*************************************************************
Synopsis [Count the number of paths in the ZDD.]
Description []
SideEffects []
SeeAlso []
Definition at line 503 of file abcFunc.c.
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 }
void Abc_NodeBddToCnf | ( | Abc_Obj_t * | pNode, | |
Extra_MmFlex_t * | pMmMan, | |||
Vec_Str_t * | vCube, | |||
int | fAllPrimes, | |||
char ** | ppSop0, | |||
char ** | ppSop1 | |||
) |
Function*************************************************************
Synopsis [Computes the SOPs of the negative and positive phase of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 482 of file abcFunc.c.
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 }
int Abc_NtkAigToBdd | ( | Abc_Ntk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Converts the network from AIG to BDD representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 660 of file abcFunc.c.
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 }
int Abc_NtkBddToSop | ( | Abc_Ntk_t * | pNtk, | |
int | fDirect | |||
) |
Function*************************************************************
Synopsis [Converts the network from BDD to SOP representation.]
Description [If the flag is set to 1, forces the direct phase of all covers.]
SideEffects []
SeeAlso []
Definition at line 210 of file abcFunc.c.
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 }
void Abc_NtkLogicMakeDirectSops | ( | Abc_Ntk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Removes complemented SOP covers.]
Description []
SideEffects []
SeeAlso []
Definition at line 154 of file abcFunc.c.
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 }
int Abc_NtkMapToSop | ( | Abc_Ntk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Unmaps the network.]
Description []
SideEffects []
SeeAlso []
Definition at line 1013 of file abcFunc.c.
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 }
int Abc_NtkSopToAig | ( | Abc_Ntk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Converts the network from SOP to AIG representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 551 of file abcFunc.c.
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 }
int Abc_NtkSopToBdd | ( | Abc_Ntk_t * | pNtk | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Converts the network from SOP to BDD representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 50 of file abcFunc.c.
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 }
int Abc_NtkSopToBlifMv | ( | Abc_Ntk_t * | pNtk | ) |
int Abc_NtkToAig | ( | Abc_Ntk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Convers logic network to the SOP form.]
Description []
SideEffects []
SeeAlso []
Definition at line 1127 of file abcFunc.c.
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 }
int Abc_NtkToBdd | ( | Abc_Ntk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Convers logic network to the SOP form.]
Description []
SideEffects []
SeeAlso []
Definition at line 1098 of file abcFunc.c.
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 }
int Abc_NtkToSop | ( | Abc_Ntk_t * | pNtk, | |
int | fDirect | |||
) |
Function*************************************************************
Synopsis [Convers logic network to the SOP form.]
Description []
SideEffects []
SeeAlso []
Definition at line 1062 of file abcFunc.c.
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 }