From f2abd6b8a9b59e28769662bfc6e6e6670de20faa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 11 May 2013 17:01:13 -0700 Subject: Preprocessing SOPs given to 'fx' to be D1C-free and SCC-free. Handling the case of non-prime SOPs. --- src/base/abc/abc.h | 8 +- src/base/abc/abcFanOrder.c | 188 ++++++++++++++++++++++++++++----------------- src/base/abci/abc.c | 4 +- src/base/abci/abcFx.c | 18 ++++- 4 files changed, 139 insertions(+), 79 deletions(-) diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e408a58f..a2b2fdf5 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -503,11 +503,13 @@ static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At #define Abc_ObjForEachFanout( pObj, pFanout, i ) \ for ( i = 0; (i < Abc_ObjFanoutNum(pObj)) && (((pFanout) = Abc_ObjFanout(pObj, i)), 1); i++ ) // cubes and literals -#define Abc_SopForEachCube( pSop, nFanins, pCube ) \ - for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 ) #define Abc_CubeForEachVar( pCube, Value, i ) \ for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ ) - +#define Abc_SopForEachCube( pSop, nFanins, pCube ) \ + for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 ) +#define Abc_SopForEachCubePair( pSop, nFanins, pCube, pCube2 ) \ + Abc_SopForEachCube( pSop, nFanins, pCube ) \ + Abc_SopForEachCube( pCube + (nFanins) + 3, nFanins, pCube2 ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// diff --git a/src/base/abc/abcFanOrder.c b/src/base/abc/abcFanOrder.c index dd1cfc79..bdeb6d87 100644 --- a/src/base/abc/abcFanOrder.c +++ b/src/base/abc/abcFanOrder.c @@ -231,77 +231,6 @@ void Abc_NtkOrderFaninsByLitCountAndCubeCount( Abc_Ntk_t * pNtk ) Vec_StrFree( vStore ); } -/**Function************************************************************* - - Synopsis [Checks if the network is SCC-free.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Abc_CubeContain( char * pCube1, char * pCube2, int nVars ) -{ - int v, fCont12 = 1, fCont21 = 1; - for ( v = 0; v < nVars; v++ ) - { - if ( pCube1[v] == pCube2[v] ) - continue; - if ( pCube1[v] == '-' ) - fCont21 = 0; - else if ( pCube2[v] == '-' ) - fCont12 = 0; - else - return 0; - if ( !fCont21 && !fCont21 ) - return 0; - } - assert( fCont21 || fCont12 ); - return (fCont21 << 1) | fCont12; -} -int Abc_NodeMakeSCCFree( Abc_Obj_t * pNode, Vec_Ptr_t * vCubes ) -{ - char * pSop = (char *)pNode->pData; - char * pCube, * pCube2; - int i, k, Status, nCount = 0; - int nVars = Abc_ObjFaninNum(pNode); - Vec_PtrClear( vCubes ); - Abc_SopForEachCube( pSop, nVars, pCube ) - Vec_PtrPush( vCubes, pCube ); - Vec_PtrForEachEntry( char *, vCubes, pCube, i ) - if ( pCube != NULL ) - Vec_PtrForEachEntryStart( char *, vCubes, pCube2, k, i+1 ) - if ( pCube2 != NULL ) - { - Status = Abc_CubeContain( pCube, pCube2, nVars ); - nCount += (int)(Status > 0); - if ( Status & 1 ) - Vec_PtrWriteEntry( vCubes, k, NULL ); - else if ( Status & 2 ) - Vec_PtrWriteEntry( vCubes, i, NULL ); - } - if ( nCount == 0 ) - return 0; - return 1; -} -void Abc_NtkMakeSCCFree( Abc_Ntk_t * pNtk ) -{ - Vec_Ptr_t * vCubes; - Abc_Obj_t * pNode; - int i; - assert( Abc_NtkHasSop(pNtk) ); - vCubes = Vec_PtrAlloc( 1000 ); - Abc_NtkForEachNode( pNtk, pNode, i ) - if ( Abc_NodeMakeSCCFree( pNode, vCubes ) ) - { - printf( "Node %d is not SCC-free.\n", i ); - break; - } - Vec_PtrFree( vCubes ); -} - /**Function************************************************************* Synopsis [Split large nodes by dividing their SOPs in half.] @@ -424,6 +353,123 @@ void Abc_NtkSortSops( Abc_Ntk_t * pNtk ) Abc_NtkSortCubes( pNtk ); } +/**Function************************************************************* + + Synopsis [Makes cover legitimate for "fast_extract".] + + Description [Iteratively removes distance-1 and contained cubes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_CubeContain( char * pCube1, char * pCube2, int nVars ) +{ + int v, fCont12 = 1, fCont21 = 1; + for ( v = 0; v < nVars; v++ ) + { + if ( pCube1[v] == pCube2[v] ) + continue; + if ( pCube1[v] == '-' ) + fCont21 = 0; + else if ( pCube2[v] == '-' ) + fCont12 = 0; + else + return 0; + if ( !fCont21 && !fCont21 ) + return 0; + } + assert( fCont21 || fCont12 ); + return (fCont21 << 1) | fCont12; +} +int Abc_NodeMakeSCCFree( Abc_Obj_t * pNode ) +{ + char * pSop = (char *)pNode->pData; + char * pCube, * pCube2, * pSopNew; + int nVars = Abc_ObjFaninNum(pNode); + int Status, nCount = 0; + Abc_SopForEachCubePair( pSop, nVars, pCube, pCube2 ) + { + if ( pCube[0] == 'z' || pCube2[0] == 'z' ) + continue; + Status = Abc_CubeContain( pCube, pCube2, nVars ); + nCount += (int)(Status > 0); + if ( Status & 1 ) + pCube2[0] = 'z'; + else if ( Status & 2 ) + pCube[0] = 'z'; + } + if ( nCount == 0 ) + return 0; + // create new cover + pSopNew = (char *)pNode->pData; + Abc_SopForEachCube( pSop, nVars, pCube ) + { + if ( pCube[0] == 'z' ) + continue; + memcpy( pSopNew, pCube, nVars + 3 ); + pSopNew += nVars + 3; + } + *pSopNew = 0; + return 1; +} +void Abc_NodeMakeDist1Free( Abc_Obj_t * pNode ) +{ + char * pSop = (char *)pNode->pData; + char * pCube, * pCube2; + int i, nVars = Abc_ObjFaninNum(pNode); + Abc_SopForEachCube( pSop, nVars, pCube ) + Abc_SopForEachCube( pCube + nVars + 3, nVars, pCube2 ) + { + int Counter = 0, iDiff = -1; + for ( i = 0; i < nVars; i++ ) + if ( pCube[i] != pCube2[i] ) + Counter++, iDiff = i; + if ( Counter == 1 && ((pCube[iDiff] == '0' && pCube2[iDiff] == '1') || (pCube[iDiff] == '1' && pCube2[iDiff] == '0')) ) + pCube[iDiff] = pCube2[iDiff] = '-'; + } +} +void Abc_NodeCheckDist1Free( Abc_Obj_t * pNode ) +{ + char * pSop = (char *)pNode->pData; + char * pCube, * pCube2; + int i, nVars = Abc_ObjFaninNum(pNode); + Abc_SopForEachCube( pSop, nVars, pCube ) + Abc_SopForEachCube( pSop, nVars, pCube2 ) + { + int Counter = 0; + if ( pCube == pCube2 ) + continue; + for ( i = 0; i < nVars; i++ ) + if ( pCube[i] != pCube2[i] ) + Counter++; + assert( Counter > 1 ); + } +} +int Abc_NodeMakeLegit( Abc_Obj_t * pNode ) +{ + int i, fChanges = 1; + for ( i = 0; fChanges; i++ ) + { + Abc_NodeMakeDist1Free( pNode ); + fChanges = Abc_NodeMakeSCCFree( pNode ); + } +// Abc_NodeCheckDist1Free( pNode ); + return i > 1; +} +int Abc_NtkMakeLegit( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter = 0; + assert( Abc_NtkHasSop(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + Counter += Abc_NodeMakeLegit( pNode ); + if ( Counter ) + Abc_Print( 1, "%d nodes were made dist1-cube-free and/or single-cube-containment-free.\n", Counter ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6de6a637..bd18200c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9625,8 +9625,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) */ if ( pNtk ) { - extern void Abc_NtkTestTim( Abc_Ntk_t * pNtk, int fVerbose ); - Abc_NtkTestTim( pNtk, fVerbose ); + extern void Abc_NtkMakeLegit( Abc_Ntk_t * pNtk ); + Abc_NtkMakeLegit( pNtk ); } return 0; usage: diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index c515afb1..953f87f3 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -134,12 +134,14 @@ static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { ret ***********************************************************************/ Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk ) { + extern int Abc_NtkMakeLegit( Abc_Ntk_t * pNtk ); Vec_Wec_t * vCubes; Vec_Int_t * vCube; Abc_Obj_t * pNode; char * pCube, * pSop; int nVars, i, v, Lit; assert( Abc_NtkIsSopLogic(pNtk) ); + Abc_NtkMakeLegit( pNtk ); vCubes = Vec_WecAlloc( 1000 ); Abc_NtkForEachNode( pNtk, pNode, i ) { @@ -597,7 +599,7 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu pBeg1++, pBeg2++, Counter++; else if ( *pBeg1 < *pBeg2 ) Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); - else + else { if ( Vec_IntSize(vCubeFree) == 0 ) fAttr0 = 1, fAttr1 = 0; @@ -608,7 +610,12 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); while ( pBeg2 < pEnd2 ) Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); - assert( Vec_IntSize(vCubeFree) > 1 ); // the cover is not SCC-free + if ( Vec_IntSize(vCubeFree) == 0 ) + printf( "The SOP has duplicated cubes.\n" ); + else if ( Vec_IntSize(vCubeFree) == 1 ) + printf( "The SOP has contained cubes.\n" ); + else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) ) + printf( "The SOP has distance-1 cubes or it is not a prime cover. Please make sure the result verifies.\n" ); assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) ); return Counter; } @@ -807,7 +814,7 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, else if ( !fRemove ) Vec_QuePush( p->vPrio, iDiv ); } - } + } } void Fx_ManCreateDivisors( Fx_Man_t * p ) { @@ -936,6 +943,11 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 ); assert( Lit0 >= 0 && Lit1 >= 0 ); + // if the input cover is not prime, it may happen that we are extracting divisor (x + !x) + // although it is not strictly correct, it seems to be fine to just skip such divisors + if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) ) + return; + // collect single-cube-divisor cubes Vec_IntClear( p->vCubesS ); if ( Vec_IntSize(vDiv) == 2 ) -- cgit v1.2.3