Skip to content

A
abc
Commit 283abd47 by Alan Mishchenko
Options

New MFS package.

parent ac037cbb
Showing with 598 additions and 180 deletions
src/base/abci/abc.c
......@@ -4469,7 +4469,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Sfm_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMClaevwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMNClaevwh" ) ) != EOF )
{
switch ( c )
{
......@@ -4517,6 +4517,17 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nWinSizeMax < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nDivNumMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nDivNumMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
......@@ -4573,12 +4584,13 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfs2 [-WFDMC <num>] [-laevwh]\n" );
Abc_Print( -2, "usage: mfs2 [-WFDMNC <num>] [-laevwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
Abc_Print( -2, "\t-N <num> : the max number of divisors to consider (0 = no limit) [default = %d]\n", pPars->nDivNumMax );
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-l : allow logic level to increase [default = %s]\n", !pPars->fFixLevel? "yes": "no" );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
src/opt/mfs/mfsResub.c
......@@ -164,7 +164,7 @@ p->timeGia += clock() - clk;
***********************************************************************/
int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
{
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;// || pNode->Id == 556;
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
unsigned * pData;
int pCands[MFS_FANIN_MAX];
int RetValue, iVar, i, nCands, nWords, w;
......@@ -176,9 +176,9 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
// clean simulation info
Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
p->nCexes = 0;
if ( fVeryVerbose )
if ( p->pPars->fVeryVerbose )
{
printf( "\n" );
// printf( "\n" );
printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n",
pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
iFanin, Abc_ObjFaninNum(pNode),
......@@ -201,8 +201,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
return 0;
if ( RetValue == 1 )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
if ( p->pPars->fVeryVerbose )
printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
p->nNodesResub++;
p->nNodesGainedLevel++;
if ( fSkipUpdate )
......@@ -223,7 +223,7 @@ p->timeInt += clock() - clk;
if ( fVeryVerbose )
{
for ( i = 0; i < 8; i++ )
for ( i = 0; i < 9; i++ )
printf( " " );
for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
printf( "%d", i % 10 );
......@@ -239,7 +239,7 @@ p->timeInt += clock() - clk;
{
if ( fVeryVerbose )
{
printf( "%3d: %2d ", p->nCexes, iVar );
printf( "%3d: %3d ", p->nCexes, iVar );
for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
{
pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
......@@ -276,8 +276,8 @@ p->timeInt += clock() - clk;
return 0;
if ( RetValue == 1 )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
if ( p->pPars->fVeryVerbose )
printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
p->nNodesResub++;
p->nNodesGainedLevel++;
if ( fSkipUpdate )
......@@ -296,6 +296,8 @@ p->timeInt += clock() - clk;
if ( p->nCexes >= p->pPars->nDivMax )
break;
}
if ( p->pPars->fVeryVerbose )
printf( "Node %d: Cannot find replacement for fanin %d.\n", pNode->Id, iFanin );
return 0;
}
......
src/opt/sfm/sfm.h
......@@ -45,7 +45,8 @@ struct Sfm_Par_t_
int nTfoLevMax; // the maximum fanout levels
int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum depth to try
int nWinSizeMax; // the maximum number of divisors
int nDivNumMax; // the maximum number of divisors
int nWinSizeMax; // the maximum window size
int nBTLimit; // the maximum number of conflicts in one SAT run
int fFixLevel; // does not allow level to increase
int fArea; // performs optimization for area
......
src/opt/sfm/sfmCnf.c
......@@ -117,6 +117,37 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
SeeAlso []
***********************************************************************/
Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
{
Vec_Wec_t * vCnfs;
Vec_Str_t * vCnf, * vCnfBase;
word uTruth;
int i;
vCnf = Vec_StrAlloc( 100 );
vCnfs = Vec_WecStart( p->nObjs );
Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
{
Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
vCnfBase->nSize = Vec_StrSize(vCnf);
}
Vec_StrFree( vCnf );
return vCnfs;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
{
Vec_Int_t * vClause;
......
src/opt/sfm/sfmCore.c
......@@ -47,8 +47,9 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
memset( pPars, 0, sizeof(Sfm_Par_t) );
pPars->nTfoLevMax = 2; // the maximum fanout levels
pPars->nFanoutMax = 10; // the maximum number of fanouts
pPars->nDepthMax = 0; // the maximum depth to try
pPars->nWinSizeMax = 500; // the maximum number of divisors
pPars->nDepthMax = 0; // the maximum depth to try
pPars->nDivNumMax = 200; // the maximum number of divisors
pPars->nWinSizeMax = 500; // the maximum window size
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->fFixLevel = 0; // does not allow level to increase
pPars->fArea = 0; // performs optimization for area
......@@ -62,26 +63,169 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_NtkPrepare( Sfm_Ntk_t * p )
void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
{
p->vLeaves = Vec_IntAlloc( 1000 );
p->vRoots = Vec_IntAlloc( 1000 );
p->vNodes = Vec_IntAlloc( 1000 );
p->vTfo = Vec_IntAlloc( 1000 );
p->vDivs = Vec_IntAlloc( 100 );
p->vDivIds = Vec_IntAlloc( 1000 );
p->vDiffs = Vec_IntAlloc( 1000 );
p->vLits = Vec_IntAlloc( 100 );
p->vClauses = Vec_WecAlloc( 100 );
p->vFaninMap = Vec_IntAlloc( 10 );
printf( "Attempts : " );
printf( "Remove %5d (%6.2f%%) ", p->nRemoves, 100.0*p->nRemoves/p->nTryRemoves );
printf( "Resub %5d (%6.2f%%) ", p->nResubs, 100.0*p->nResubs /p->nTryResubs );
printf( "\n" );
printf( "Reduction: " );
printf( "Nodes %5d (%6.2f%%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
printf( "Edges %5d (%6.2f%%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
printf( "\n" );
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
ABC_PRTP( "Div", p->timeDiv , p->timeTotal );
ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
}
/**Function*************************************************************
Synopsis [Performs resubstitution for the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
{
int fSkipUpdate = 1;
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
int i, iFanin, iVar = -1;
word uTruth, uSign, uMask;
clock_t clk;
assert( Sfm_ObjIsNode(p, iNode) );
assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
if ( fRemoveOnly )
p->nTryRemoves++;
else
p->nTryResubs++;
// report init stats
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n",
iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode),
Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 );
// clean simulation info
p->nCexes = 0;
Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 );
// try removing the critical fanin
clk = clock();
Vec_IntClear( p->vDivIds );
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( i != f )
Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
uTruth = Sfm_ComputeInterpolant( p );
p->timeSat += clock() - clk;
// analyze outcomes
if ( uTruth == SFM_SAT_UNDEC )
return 0;
if ( uTruth == SFM_SAT_SAT )
goto finish;
if ( fRemoveOnly )
return 0;
if ( fVeryVerbose )
{
for ( i = 0; i < 9; i++ )
printf( " " );
for ( i = 0; i < Vec_IntSize(p->vDivs); i++ )
printf( "%d", i % 10 );
printf( "\n" );
}
while ( 1 )
{
if ( fVeryVerbose )
{
printf( "%3d: %3d ", p->nCexes, iVar );
Vec_WrdForEachEntry( p->vDivCexes, uSign, i )
printf( "%d", Abc_InfoHasBit((unsigned *)&uSign, p->nCexes-1) );
printf( "\n" );
}
// find the next divisor to try
uMask = (~(word)0) >> (64 - p->nCexes);
Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar )
if ( uSign == uMask )
break;
if ( iVar == Vec_IntSize(p->vDivs) )
return 0;
// try replacing the critical fanin
clk = clock();
Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) );
uTruth = Sfm_ComputeInterpolant( p );
p->timeSat += clock() - clk;
// analyze outcomes
if ( uTruth == SFM_SAT_UNDEC )
return 0;
if ( uTruth == SFM_SAT_SAT )
goto finish;
if ( p->nCexes == 64 )
return 0;
// remove the last variable
Vec_IntPop( p->vDivIds );
}
finish:
if ( p->pPars->fVeryVerbose )
{
if ( iVar == -1 )
printf( "Node %d: Fanin %d can be removed. ", iNode, f );
else
printf( "Node %d: Fanin %d can be replaced by divisor %d. ", iNode, f, iVar );
Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" );
}
if ( iVar == -1 )
p->nRemoves++;
else
p->nResubs++;
if ( fSkipUpdate )
return 1;
// update the network
Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
return 1;
}
int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin;
// prepare SAT solver
Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose );
Sfm_NtkWindowToSolver( p );
Sfm_NtkPrepareDivisors( p, iNode );
// try replacing area critical fanins
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 )
{
if ( Sfm_NodeResubSolve( p, iNode, i, 0 ) )
return 1;
}
// try removing redundant edges
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( !(Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1) )
{
if ( Sfm_NodeResubSolve( p, iNode, i, 1 ) )
return 1;
}
/*
// try replacing area critical fanins while adding two new fanins
if ( Sfm_ObjFaninNum(p, iNode) < p->nFaninMax )
Abc_ObjForEachFanin( pNode, pFanin, i )
if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
{
if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
return 1;
}
*/
return 0;
}
/**Function*************************************************************
......@@ -96,19 +240,25 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
***********************************************************************/
int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{
// int i;
int i;
p->timeTotal = clock();
p->pPars = pPars;
Sfm_NtkPrepare( p );
Sfm_ComputeInterpolantCheck( p );
/*
p->nTotalNodesBeg = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins);
Sfm_NtkForEachNode( p, i )
{
// printf( "Node %d:\n", i );
// Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
// printf( "\n" );
Sfm_NtkWindow( p, i, 1 );
if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
continue;
if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
continue;
Sfm_NodeResub( p, i );
}
*/
p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins);
p->timeTotal = clock() - p->timeTotal;
if ( pPars->fVerbose )
Sfm_NtkPrintStats( p );
return 0;
}
......
src/opt/sfm/sfmNtk.c
......@@ -107,46 +107,21 @@ void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
SeeAlso []
***********************************************************************/
void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
static inline int Sfm_ObjCreateLevel( Vec_Int_t * vArray, Vec_Int_t * vLevels )
{
Vec_Int_t * vArray;
int i, k, Fanin, * pLevels;
Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
pLevels = Vec_IntArray( vLevels );
Vec_WecForEachLevel( vFanins, vArray, i )
Vec_IntForEachEntry( vArray, Fanin, k )
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[Fanin] + 1 );
int k, Fanin, Level = 0;
Vec_IntForEachEntry( vArray, Fanin, k )
Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) + 1 );
return Level;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
{
Vec_Wec_t * vCnfs;
Vec_Str_t * vCnf, * vCnfBase;
word uTruth;
Vec_Int_t * vArray;
int i;
vCnf = Vec_StrAlloc( 100 );
vCnfs = Vec_WecStart( p->nObjs );
Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
{
Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
vCnfBase->nSize = Vec_StrSize(vCnf);
}
Vec_StrFree( vCnf );
return vCnfs;
assert( Vec_IntSize(vLevels) == 0 );
Vec_IntGrow( vLevels, Vec_WecSize(vFanins) );
Vec_WecForEachLevel( vFanins, vArray, i )
Vec_IntPush( vLevels, Sfm_ObjCreateLevel(vArray, vLevels) );
}
/**Function*************************************************************
......@@ -177,15 +152,31 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
// attributes
Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
Sfm_CreateLevel( &p->vFanins, &p->vLevels );
Vec_IntFill( &p->vCounts, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds2, p->nObjs, 0 );
Vec_IntFill( &p->vId2Var, p->nObjs, -1 );
Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
Vec_IntFill( &p->vCounts, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds2, p->nObjs, 0 );
Vec_IntFill( &p->vId2Var, p->nObjs, -1 );
Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
p->vCover = Vec_IntAlloc( 1 << 16 );
p->vCnfs = Sfm_CreateCnf( p );
return p;
}
void Sfm_NtkPrepare( Sfm_Ntk_t * p )
{
p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
p->vLeaves = Vec_IntAlloc( 1000 );
p->vRoots = Vec_IntAlloc( 1000 );
p->vNodes = Vec_IntAlloc( 1000 );
p->vTfo = Vec_IntAlloc( 1000 );
p->vFans = Vec_IntAlloc( 100 );
p->vOrder = Vec_IntAlloc( 100 );
p->vDivVars = Vec_IntAlloc( 100 );
p->vDivs = Vec_IntAlloc( 100 );
p->vDivIds = Vec_IntAlloc( 1000 );
p->vLits = Vec_IntAlloc( 100 );
p->vClauses = Vec_WecAlloc( 100 );
p->vFaninMap = Vec_IntAlloc( 10 );
}
void Sfm_NtkFree( Sfm_Ntk_t * p )
{
// user data
......@@ -203,14 +194,17 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
Vec_WecFree( p->vCnfs );
Vec_IntFree( p->vCover );
// other data
Vec_WrdFreeP( &p->vDivCexes );
Vec_IntFreeP( &p->vLeaves );
Vec_IntFreeP( &p->vRoots );
Vec_IntFreeP( &p->vNodes );
Vec_IntFreeP( &p->vTfo );
Vec_IntFreeP( &p->vFans );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vDivVars );
Vec_IntFreeP( &p->vDivs );
Vec_IntFreeP( &p->vDivIds );
Vec_IntFreeP( &p->vLits );
Vec_IntFreeP( &p->vDiffs );
Vec_WecFreeP( &p->vClauses );
Vec_IntFreeP( &p->vFaninMap );
if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
......@@ -220,6 +214,72 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
/**Function*************************************************************
Synopsis [Performs resubstitution for the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
{
int RetValue;
RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin );
assert( RetValue );
RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );
assert( RetValue );
}
void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
{
if ( iFanin < 0 )
return;
assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 );
assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 );
Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin );
Vec_IntPush( Sfm_ObjFoArray(p, iFanin), iNode );
}
void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin;
if ( Sfm_ObjFanoutNum(p, iNode) > 0 )
return;
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
{
int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue );
if ( Sfm_ObjFanoutNum(p, iFanin) == 0 )
Sfm_NtkDeleteObj_rec( p, iFanin );
}
Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
}
void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
{
int i, iFanout;
int LevelNew = Sfm_ObjCreateLevel( Sfm_ObjFiArray(p, iNode), &p->vLevels );
if ( LevelNew == Sfm_ObjLevel(p, iNode) )
return;
Sfm_ObjSetLevel( p, iNode, LevelNew );
Sfm_ObjForEachFanout( p, iNode, iFanout, i )
Sfm_NtkUpdateLevel_rec( p, iFanout );
}
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
{
int iFanin = Sfm_ObjFanin( p, iNode, f );
// replace old fanin by new fanin
Sfm_NtkRemoveFanin( p, iNode, iFanin );
Sfm_NtkAddFanin( p, iNode, iFaninNew );
// recursively remove MFFC
Sfm_NtkDeleteObj_rec( p, iFanin );
// update logic level
Sfm_NtkUpdateLevel_rec( p, iNode );
// update truth table
Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
}
/**Function*************************************************************
Synopsis [Public APIs of this network.]
Description []
......
src/opt/sfm/sfmSat.c
......@@ -42,6 +42,28 @@ static word s_Truths6[6] = {
/**Function*************************************************************
Synopsis [Creates order of objects in the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_NtkOrderObjects( Sfm_Ntk_t * p )
{
int i, iNode;
assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes)) );
Vec_IntClear( p->vOrder );
Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
Vec_IntPush( p->vOrder, iNode );
Vec_IntForEachEntryStart( p->vDivs, iNode, i, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) )
Vec_IntPush( p->vOrder, iNode );
}
/**Function*************************************************************
Synopsis [Converts a window into a SAT solver.]
Description []
......@@ -51,14 +73,15 @@ static word s_Truths6[6] = {
SeeAlso []
***********************************************************************/
void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
{
Vec_Int_t * vClause;
int RetValue, Lit, iNode = -1, iFanin, i, k, c;
int RetValue, Lit, iNode = -1, iFanin, i, k;
clock_t clk = clock();
sat_solver * pSat0 = sat_solver_new();
sat_solver * pSat1 = sat_solver_new();
sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
// create SAT variables
p->nSatVars = 1;
Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
......@@ -67,29 +90,26 @@ void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
Vec_IntForEachEntryReverse( p->vDivs, iNode, i )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
// add CNF clauses
for ( c = 0; c < 2; c++ )
// add CNF clauses for the TFI
Sfm_NtkOrderObjects( p );
Vec_IntForEachEntry( p->vOrder, iNode, i )
{
Vec_Int_t * vObjs = c ? p->vDivs : p->vNodes;
Vec_IntForEachEntryReverse( vObjs, iNode, i )
// collect fanin variables
Vec_IntClear( p->vFaninMap );
Sfm_ObjForEachFanin( p, iNode, iFanin, k )
Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
// generate CNF
Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
// add clauses
Vec_WecForEachLevel( p->vClauses, vClause, k )
{
// collect fanin variables
Vec_IntClear( p->vFaninMap );
Sfm_NodeForEachFanin( p, iNode, iFanin, k )
Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
// generate CNF
Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
// add clauses
Vec_WecForEachLevel( p->vClauses, vClause, k )
{
if ( Vec_IntSize(vClause) == 0 )
break;
RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue );
RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue );
}
if ( Vec_IntSize(vClause) == 0 )
break;
RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue );
RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue );
}
}
// get the last node
......@@ -110,70 +130,73 @@ void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
assert( p->pSat1 == NULL );
p->pSat0 = pSat0;
p->pSat1 = pSat1;
p->timeCnf += clock() - clk;
}
/**Function*************************************************************
Synopsis [Takes SAT solver and returns interpolant.]
Description [If interpolant does not exist, returns diff SAT variables.]
Description [If interpolant does not exist, records difference variables.]
SideEffects []
SeeAlso []
***********************************************************************/
word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivIds, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
{
word uTruth = 0, uCube;
word * pSign, uCube, uTruth = 0;
int status, i, Div, iVar, nFinal, * pFinal;
int nVars = sat_solver_nvars(pSatOn);
int nVars = sat_solver_nvars( p->pSat1 );
int iNewLit = Abc_Var2Lit( nVars, 0 );
int RetValue;
sat_solver_setnvars( pSatOn, nVars + 1 );
sat_solver_setnvars( p->pSat1, nVars + 1 );
while ( 1 )
{
// find onset minterm
status = sat_solver_solve( pSatOn, &iNewLit, &iNewLit + 1, nBTLimit, 0, 0, 0 );
status = sat_solver_solve( p->pSat1, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SFM_SAT_UNDEC;
if ( status == l_False )
return uTruth;
assert( status == l_True );
// collect literals
Vec_IntClear( vLits );
Vec_IntForEachEntry( vDivIds, Div, i )
// Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
Vec_IntPush( vLits, sat_solver_var_literal(pSatOn, Div) );
// collect divisor literals
Vec_IntClear( p->vLits );
Vec_IntForEachEntry( p->vDivIds, Div, i )
Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat1, Div) );
// check against offset
status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
status = sat_solver_solve( p->pSat0, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SFM_SAT_UNDEC;
if ( status == l_True )
{
Vec_IntClear( vDiffs );
for ( i = 0; i < nVars; i++ )
Vec_IntPush( vDiffs, sat_solver_var_value(pSatOn, i) ^ sat_solver_var_value(pSatOff, i) );
return SFM_SAT_SAT;
}
break;
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( pSatOff, &pFinal );
nFinal = sat_solver_final( p->pSat0, &pFinal );
uCube = ~(word)0;
Vec_IntClear( vLits );
Vec_IntPush( vLits, Abc_LitNot(iNewLit) );
Vec_IntClear( p->vLits );
Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) );
for ( i = 0; i < nFinal; i++ )
{
Vec_IntPush( vLits, pFinal[i] );
iVar = Vec_IntFind( vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
Vec_IntPush( p->vLits, pFinal[i] );
iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
RetValue = sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
assert( RetValue );
status = sat_solver_addclause( p->pSat1, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
assert( status );
}
assert( 0 );
return 0;
assert( status == l_True );
// store the counter-example
Vec_IntForEachEntry( p->vDivVars, iVar, i )
if ( sat_solver_var_value(p->pSat1, iVar) ^ sat_solver_var_value(p->pSat0, iVar) ) // insert 1
{
pSign = Vec_WrdEntryP( p->vDivCexes, i );
assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
}
p->nCexes++;
return SFM_SAT_SAT;
}
/**Function*************************************************************
......@@ -187,6 +210,7 @@ word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_
SeeAlso []
***********************************************************************/
/*
void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
{
int iNode = 3;
......@@ -196,8 +220,8 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
// int i;
// Sfm_NtkForEachNode( p, i )
{
Sfm_NtkWindow( p, iNode, 1 );
Sfm_NtkWin2Sat( p );
Sfm_NtkCreateWindow( p, iNode, 1 );
Sfm_NtkWindowToSolver( p );
// collect SAT variables of divisors
Vec_IntClear( p->vDivIds );
......@@ -218,6 +242,7 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
sat_solver_delete( p->pSat1 ); p->pSat1 = NULL;
}
}
*/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/opt/sfm/sfmWin.c
......@@ -33,6 +33,71 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Returns the MFFC size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sfm_ObjRef_rec( Sfm_Ntk_t * p, int iObj )
{
int i, iFanin, Value, Count;
if ( Sfm_ObjIsPi(p, iObj) )
return 0;
assert( Sfm_ObjIsNode(p, iObj) );
Value = Sfm_ObjRefIncrement(p, iObj);
if ( Value > 1 )
return 0;
assert( Value == 1 );
Count = 1;
Sfm_ObjForEachFanin( p, iObj, iFanin, i )
Count += Sfm_ObjRef_rec( p, iFanin );
return Count;
}
int Sfm_ObjRef( Sfm_Ntk_t * p, int iObj )
{
int i, iFanin, Count = 1;
Sfm_ObjForEachFanin( p, iObj, iFanin, i )
Count += Sfm_ObjRef_rec( p, iFanin );
return Count;
}
int Sfm_ObjDeref_rec( Sfm_Ntk_t * p, int iObj )
{
int i, iFanin, Value, Count;
if ( Sfm_ObjIsPi(p, iObj) )
return 0;
assert( Sfm_ObjIsNode(p, iObj) );
Value = Sfm_ObjRefDecrement(p, iObj);
if ( Value > 0 )
return 0;
assert( Value == 0 );
Count = 1;
Sfm_ObjForEachFanin( p, iObj, iFanin, i )
Count += Sfm_ObjDeref_rec( p, iFanin );
return Count;
}
int Sfm_ObjDeref( Sfm_Ntk_t * p, int iObj )
{
int i, iFanin, Count = 1;
Sfm_ObjForEachFanin( p, iObj, iFanin, i )
Count += Sfm_ObjDeref_rec( p, iFanin );
return Count;
}
int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj )
{
int Count1, Count2;
assert( Sfm_ObjIsNode( p, iObj ) );
Count1 = Sfm_ObjDeref( p, iObj );
Count2 = Sfm_ObjRef( p, iObj );
assert( Count1 == Count2 );
return Count1;
}
/**Function*************************************************************
Synopsis [Working with traversal IDs.]
Description []
......@@ -70,7 +135,7 @@ int Sfm_NtkCheckOverlap_rec( Sfm_Ntk_t * p, int iThis, int iNode )
if ( Sfm_ObjIsTravIdCurrent(p, iThis) )
return 1;
Sfm_ObjSetTravIdCurrent2(p, iThis);
Sfm_NodeForEachFanin( p, iThis, iFanin, i )
Sfm_ObjForEachFanin( p, iThis, iFanin, i )
if ( Sfm_NtkCheckOverlap_rec(p, iFanin, iNode) )
return 1;
return 0;
......@@ -97,7 +162,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
int i, iFanout;
if ( Sfm_ObjFanoutNum(p, iNode) >= p->pPars->nFanoutMax )
return 0;
Sfm_NodeForEachFanout( p, iNode, iFanout, i )
Sfm_ObjForEachFanout( p, iNode, iFanout, i )
if ( !Sfm_NtkCheckOverlap( p, iFanout, iNode ) )
return 0;
return 1;
......@@ -117,7 +182,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
{
int i, iFanout;
Sfm_NodeForEachFanout( p, iNode, iFanout, i )
Sfm_ObjForEachFanout( p, iNode, iFanout, i )
{
// skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level
if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
......@@ -162,13 +227,14 @@ void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
Vec_IntPush( p->vLeaves, iNode );
return;
}
Sfm_NodeForEachFanin( p, iNode, iFanin, i )
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkCollectTfi_rec( p, iFanin );
Vec_IntPush( p->vNodes, iNode );
}
int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
{
int i, iTemp;
clock_t clk = clock();
/*
if ( iNode == 7 )
{
......@@ -187,7 +253,7 @@ int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Vec_IntClear( p->vTfo ); // roots
if ( Sfm_NtkCheckFanouts(p, iNode) )
{
Sfm_NodeForEachFanout( p, iNode, iTemp, i )
Sfm_ObjForEachFanout( p, iNode, iTemp, i )
{
if ( Sfm_ObjIsPo(p, iTemp) )
continue;
......@@ -197,15 +263,16 @@ int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
}
else
Vec_IntPush( p->vRoots, iNode );
p->timeWin += clock() - clk;
// collect divisors of the TFI nodes
clk = clock();
Vec_IntClear( p->vDivs );
Vec_IntAppend( p->vDivs, p->vLeaves );
Vec_IntAppend( p->vDivs, p->vNodes );
Sfm_NtkIncrementTravId2( p );
Vec_IntForEachEntry( p->vLeaves, iTemp, i )
Sfm_NtkAddDivisors( p, iTemp );
Vec_IntForEachEntry( p->vNodes, iTemp, i )
Sfm_NtkAddDivisors( p, iTemp );
Vec_IntForEachEntry( p->vDivs, iTemp, i )
Sfm_NtkAddDivisors( p, iTemp );
p->timeDiv += clock() - clk;
if ( !fVerbose )
return 1;
......@@ -222,7 +289,42 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
{
int i;
Sfm_NtkForEachNode( p, i )
Sfm_NtkWindow( p, i, 1 );
Sfm_NtkCreateWindow( p, i, 1 );
}
/**Function*************************************************************
Synopsis [Removes node and its fanins from the array of divisors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin, k = 0;
// mark fanins
Sfm_NtkIncrementTravId( p );
Sfm_ObjSetTravIdCurrent( p, iNode );
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_ObjSetTravIdCurrent( p, iFanin );
// compact divisors
Vec_IntClear( p->vDivVars );
Vec_IntForEachEntry( p->vDivs, iFanin, i )
if ( !Sfm_ObjIsTravIdCurrent( p, iFanin ) )
{
Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iFanin) );
Vec_IntWriteEntry( p->vDivs, k++, iFanin );
}
assert( Vec_IntSize(p->vDivs) == k + Sfm_ObjFaninNum(p, iNode) + 1 );
Vec_IntShrink( p->vDivs, k );
// collect fanins
// Vec_IntClear( p->vFans );
// Sfm_ObjForEachFanin( p, iNode, iFanin, i )
// Vec_IntPush( p->vFans, iFanin );
}
////////////////////////////////////////////////////////////////////////
......
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