Skip to content

A
abc
Commit f2abd6b8 by Alan Mishchenko
Options

Preprocessing SOPs given to 'fx' to be D1C-free and SCC-free. Handling the case of non-prime SOPs.

parent cac32a32
Showing with 139 additions and 79 deletions
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 ///
......
src/base/abc/abcFanOrder.c
......@@ -233,77 +233,6 @@ void Abc_NtkOrderFaninsByLitCountAndCubeCount( Abc_Ntk_t * pNtk )
/**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.]
Description []
......@@ -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 ///
////////////////////////////////////////////////////////////////////////
......
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:
......
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 )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment