luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with functional matching.

This commit is contained in:
Alan Mishchenko 2015-10-08 23:27:56 -07:00
parent 46223f903b
commit 1ca82c87b4
4 changed files with 619 additions and 191 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

175
src/base/abci/abc.c
View File

@ -112,6 +112,7 @@ static int Abc_CommandLutmin ( Abc_Frame_t * pAbc, int argc, cha
//static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -737,6 +738,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs3", Abc_CommandMfs3, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
@ -5137,6 +5139,166 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
extern void Sfm_ParSetDefault3( Sfm_Par_t * pPars );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Sfm_Par_t Pars, * pPars = &Pars;
int c;
// set defaults
Sfm_ParSetDefault3( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "OIFXMLCNdavwh" ) ) != EOF )
{
switch ( c )
{
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTfoLevMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTfoLevMax < 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTfiLevMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTfiLevMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFanoutMax < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMffcMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMffcMax < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWinSizeMax < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nGrowthLevel < -ABC_INFINITY || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBTLimit < 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->nNodesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nNodesMax < 0 )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsMappedLogic(pNtk) )
{
Abc_Print( -1, "This command can only be applied to a mapped logic network.\n" );
return 1;
}
// modify the current network
Abc_NtkPerformMfs3( pNtk, pPars );
return 0;
usage:
Abc_Print( -2, "usage: mfs3 [-OIFXMLCN <num>] [-avwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of mapped networks\n" );
Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (0 <= num) [default = %d]\n", pPars->nTfiLevMax );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
Abc_Print( -2, "\t-X <num> : the max size of max fanout-free cone (MFFC) [default = %d]\n", pPars->nMffcMax );
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-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
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-N <num> : the max number of nodes to try (0 = all) [default = %d]\n", pPars->nNodesMax );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -10825,7 +10987,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
// Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int nCutMax = 1;
int nLeafMax = 4;
int nDivMax = 2;
@ -10914,12 +11076,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
/*
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
*/
/*
if ( Abc_NtkIsStrash(pNtk) )
{
@ -11032,14 +11195,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Cba_PrsReadBlifTest();
// Cba_PrsReadBlifTest();
}
{
extern void Tab_DecomposeTest();
extern void Sfm_DecTestBench( Abc_Ntk_t * pNtk, int iNode );
//Tab_DecomposeTest();
extern void Cnf_AddCardinConstrTest();
//Cnf_AddCardinConstrTest();
Sfm_DecTestBench( pNtk, nDecMax );
}
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );

2
src/base/abci/abcPrint.c
View File

@ -1382,6 +1382,8 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
// print the logic function
if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) )
fprintf( pFile, " %s", (char*)pObj->pData );
else if ( Abc_ObjIsNode(pObj) && Abc_NtkIsMappedLogic(pObj->pNtk) )
fprintf( pFile, " %s\n", Mio_GateReadName((Mio_Gate_t *)pObj->pData) );
else
fprintf( pFile, "\n" );
}

2
src/opt/sfm/sfm.h
View File

@ -43,8 +43,10 @@ typedef struct Sfm_Par_t_ Sfm_Par_t;
struct Sfm_Par_t_
{
int nTfoLevMax; // the maximum fanout levels
int nTfiLevMax; // the maximum fanin levels
int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum depth to try
int nMffcMax; // the maximum MFFC size
int nWinSizeMax; // the maximum window size
int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run

631
src/opt/sfm/sfmDec.c
View File

@ -46,19 +46,25 @@ struct Sfm_Dec_t_
int GateConst1; // special gates
int GateBuffer; // special gates
int GateInvert; // special gates
int GateAnd[4]; // special gates
int GateOr[4]; // special gates
// objects
int nDivs; // the number of divisors
int nMffc; // the number of divisors
int iTarget; // target node
Vec_Int_t vObjTypes; // PI (1), PO (2)
Vec_Int_t vObjRoots; // roots of the window
Vec_Int_t vObjGates; // functionality
Vec_Wec_t vObjFanins; // fanin IDs
Vec_Int_t vObjMap; // object map
Vec_Int_t vObjDec; // decomposition
// solver
sat_solver * pSat; // reusable solver
Vec_Wec_t vClauses; // CNF clauses for the node
Vec_Int_t vPols[2]; // onset/offset polarity
Vec_Int_t vTaken[2]; // onset/offset implied nodes
Vec_Int_t vImpls[2]; // onset/offset implications
Vec_Int_t vCounts[2]; // onset/offset counters
Vec_Wrd_t vSets[2]; // onset/offset patterns
int nPats[3];
int nPats[2]; // CEX count
word uMask[2]; // mask count
// temporary
Vec_Int_t vTemp;
Vec_Int_t vTemp2;
@ -72,6 +78,32 @@ struct Sfm_Dec_t_
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Setup parameter structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
{
memset( pPars, 0, sizeof(Sfm_Par_t) );
pPars->nTfoLevMax = 1000; // the maximum fanout levels
pPars->nTfiLevMax = 1000; // the maximum fanin levels
pPars->nFanoutMax = 30; // the maximum number of fanoutsp
pPars->nMffcMax = 3; // the maximum MFFC size
pPars->nWinSizeMax = 300; // the maximum window size
pPars->nGrowthLevel = 0; // the maximum allowed growth in level
pPars->nBTLimit = 5000; // the maximum number of conflicts in one SAT run
pPars->fArea = 0; // performs optimization for area
pPars->fVerbose = 0; // enable basic stats
pPars->fVeryVerbose = 0; // enable detailed stats
}
/**Function*************************************************************
Synopsis []
@ -83,9 +115,10 @@ struct Sfm_Dec_t_
SeeAlso []
***********************************************************************/
Sfm_Dec_t * Sfm_DecStart()
Sfm_Dec_t * Sfm_DecStart( Sfm_Par_t * pPars )
{
Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 );
p->pPars = pPars;
p->pSat = sat_solver_new();
return p;
}
@ -97,18 +130,18 @@ void Sfm_DecStop( Sfm_Dec_t * p )
Vec_WecErase( &p->vGateCnfs );
Vec_PtrErase( &p->vGateHands );
// objects
Vec_IntErase( &p->vObjTypes );
Vec_IntErase( &p->vObjRoots );
Vec_IntErase( &p->vObjGates );
Vec_WecErase( &p->vObjFanins );
Vec_IntErase( &p->vObjMap );
Vec_IntErase( &p->vObjDec );
// solver
sat_solver_delete( p->pSat );
Vec_WecErase( &p->vClauses );
Vec_IntErase( &p->vPols[0] );
Vec_IntErase( &p->vPols[1] );
Vec_IntErase( &p->vTaken[0] );
Vec_IntErase( &p->vTaken[1] );
Vec_IntErase( &p->vImpls[0] );
Vec_IntErase( &p->vImpls[1] );
Vec_IntErase( &p->vCounts[0] );
Vec_IntErase( &p->vCounts[1] );
Vec_WrdErase( &p->vSets[0] );
Vec_WrdErase( &p->vSets[1] );
// temporary
@ -131,32 +164,25 @@ void Sfm_DecStop( Sfm_Dec_t * p )
int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
{
abctime clk = Abc_Clock();
Vec_Int_t * vRoots = &p->vTemp;
Vec_Int_t * vRoots = &p->vObjRoots;
Vec_Int_t * vFaninVars = &p->vTemp2;
Vec_Int_t * vLevel, * vClause;
int i, k, Type, Gate, iObj, RetValue;
int i, k, Gate, iObj, RetValue;
int nTfiSize = p->iTarget + 1; // including node
int nWinSize = Vec_IntSize(&p->vObjTypes);
int nWinSize = Vec_IntSize(&p->vObjGates);
int nSatVars = 2 * nWinSize - nTfiSize;
assert( nWinSize == Vec_IntSize(&p->vObjGates) );
assert( p->iTarget < nWinSize );
// collect variables of root nodes
Vec_IntClear( vRoots );
Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, p->iTarget )
if ( Type == 2 )
Vec_IntPush( vRoots, i );
assert( Vec_IntSize(vRoots) > 0 );
// create SAT solver
sat_solver_restart( p->pSat );
sat_solver_setnvars( p->pSat, nSatVars + Vec_IntSize(vRoots) );
// add CNF clauses for the TFI
Vec_IntForEachEntryStop( &p->vObjTypes, Type, i, nTfiSize )
Vec_IntForEachEntry( &p->vObjGates, Gate, i )
{
if ( Type == 1 )
if ( Gate == -1 )
continue;
vLevel = Vec_WecEntry( &p->vObjFanins, i );
// generate CNF
Gate = Vec_IntEntry( &p->vObjGates, i );
vLevel = Vec_WecEntry( &p->vObjFanins, i );
Vec_IntPush( vLevel, i );
Sfm_TranslateCnf( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vGateCnfs, Gate), vLevel, -1 );
Vec_IntPop( vLevel );
@ -171,16 +197,15 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
}
}
// add CNF clauses for the TFO
Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, nTfiSize )
Vec_IntForEachEntryStart( &p->vObjGates, Gate, i, nTfiSize )
{
assert( Type != 1 );
assert( Gate != -1 );
vLevel = Vec_WecEntry( &p->vObjFanins, i );
Vec_IntClear( vFaninVars );
Vec_IntForEachEntry( vLevel, iObj, k )
Vec_IntPush( vFaninVars, iObj <= p->iTarget ? iObj : iObj + nWinSize - nTfiSize );
Vec_IntPush( vFaninVars, i + nWinSize - nTfiSize );
// generate CNF
Gate = Vec_IntEntry( &p->vObjGates, i );
Sfm_TranslateCnf( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vGateCnfs, Gate), vFaninVars, p->iTarget );
// add clauses
Vec_WecForEachLevel( &p->vClauses, vClause, k )
@ -192,16 +217,17 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
return 0;
}
}
if ( p->iTarget + 1 < nWinSize )
if ( nTfiSize < nWinSize )
{
// create XOR clauses for the roots
Vec_IntClear( vFaninVars );
Vec_IntForEachEntry( vRoots, iObj, i )
{
Vec_IntPush( vFaninVars, Abc_Var2Lit(nSatVars, 0) );
sat_solver_add_xor( p->pSat, iObj, iObj + nWinSize - nTfiSize, nSatVars++, 0 );
Vec_IntWriteEntry( vRoots, i, Abc_Var2Lit(nSatVars-1, 0) );
}
// make OR clause for the last nRoots variables
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vRoots), Vec_IntLimit(vRoots) );
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
if ( RetValue == 0 )
return 0;
assert( nSatVars == sat_solver_nvars(p->pSat) );
@ -224,55 +250,66 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
SeeAlso []
***********************************************************************/
int Sfm_DecPeformDec( Sfm_Dec_t * p )
int Sfm_DecFindWeight( Sfm_Dec_t * p, int c, int iLit )
{
int fVerbose = 1;
int Value = Vec_IntEntry( &p->vCounts[!c], Abc_Lit2Var(iLit) );
return Abc_LitIsCompl(iLit) ? Value : p->nPats[!c] - Value;
}
int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
{
int fVerbose = p->pPars->fVeryVerbose;
int nBTLimit = 0;
abctime clk = Abc_Clock();
int i, j, k, c, n, Pol, Pol2, Entry, Entry2, status, Lits[3];
int i, k, c, Entry, status, Lits[3], RetValue;
int iLitBest = -1, iCBest = -1, WeightBest = -1, Weight;
*pfConst = -1;
// check stuck-at-0/1 (on/off-set empty)
p->nPats[0] = p->nPats[1] = 0;
p->uMask[0] = p->uMask[1] = 0;
Vec_IntClear( &p->vImpls[0] );
Vec_IntClear( &p->vImpls[1] );
Vec_IntClear( &p->vCounts[0] );
Vec_IntClear( &p->vCounts[1] );
Vec_WrdClear( &p->vSets[0] );
Vec_WrdClear( &p->vSets[1] );
for ( c = 0; c < 2; c++ )
{
Lits[0] = Abc_Var2Lit( p->iTarget, c );
status = sat_solver_solve( p->pSat, Lits, Lits + 1, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return 0;
return -2;
if ( status == l_False )
{
Vec_IntPush( &p->vObjTypes, 0 );
Vec_IntPush( &p->vObjGates, c ? p->GateConst1 : p->GateConst0 );
Vec_WecPushLevel( &p->vObjFanins );
return 1;
*pfConst = c;
return -1;
}
assert( status == l_True );
// record this status
for ( i = 0; i <= p->iTarget; i++ )
{
Vec_IntPush( &p->vPols[c], sat_solver_var_value(p->pSat, i) );
Vec_WrdPush( &p->vSets[c], 0 );
Entry = sat_solver_var_value(p->pSat, i);
Vec_IntPush( &p->vCounts[c], Entry );
Vec_WrdPush( &p->vSets[c], (word)Entry );
}
p->nPats[c]++;
Vec_IntClear( &p->vImpls[c] );
Vec_IntFill( &p->vTaken[c], p->iTarget, 0 );
p->uMask[c] = 1;
}
// proceed checking divisors based on their values
for ( c = 0; c < 2; c++ )
{
Lits[0] = Abc_Var2Lit( p->iTarget, c );
for ( i = 0; i < p->iTarget; i++ )
for ( i = 0; i < p->nDivs; i++ )
{
if ( Vec_WrdEntry(&p->vSets[c], i) ) // diff value is possible
word Column = Vec_WrdEntry(&p->vSets[c], i);
if ( Column != 0 && Column != p->uMask[c] ) // diff value is possible
continue;
Pol = Vec_IntEntry(&p->vPols[c], i);
Lits[1] = Abc_Var2Lit( i, Pol );
Lits[1] = Abc_Var2Lit( i, Column != 0 );
status = sat_solver_solve( p->pSat, Lits, Lits + 2, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return 0;
if ( status == l_False )
{
Vec_IntWriteEntry( &p->vTaken[c], i, 1 );
Vec_IntPushTwo( &p->vImpls[c], Abc_Var2Lit(i, Pol), -1 );
Vec_IntPush( &p->vImpls[c], Abc_LitNot(Lits[1]) );
continue;
}
assert( status == l_True );
@ -280,73 +317,64 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p )
continue;
// record this status
for ( k = 0; k <= p->iTarget; k++ )
if ( sat_solver_var_value(p->pSat, k) ^ Vec_IntEntry(&p->vPols[c], k) )
if ( sat_solver_var_value(p->pSat, k) )
{
Vec_IntAddToEntry( &p->vCounts[c], k, 1 );
*Vec_WrdEntryP(&p->vSets[c], k) |= ((word)1 << p->nPats[c]);
p->nPats[c]++;
}
p->uMask[c] |= ((word)1 << p->nPats[c]++);
}
}
// proceed checking divisor pairs
// find the best decomposition
for ( c = 0; c < 2; c++ )
{
Lits[0] = Abc_Var2Lit( p->iTarget, c );
for ( i = 0; i < p->iTarget; i++ )
if ( !Vec_IntEntry(&p->vTaken[c], i) )
for ( j = 0; j < i; j++ )
if ( !Vec_IntEntry(&p->vTaken[c], j) )
Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
{
word SignI = Vec_WrdEntry(&p->vSets[c], i);
word SignJ = Vec_WrdEntry(&p->vSets[c], j);
for ( n = 0; n < 3; n++ )
Weight = Sfm_DecFindWeight(p, c, Entry);
if ( WeightBest < Weight )
{
if ( ((n&1) ? ~SignI : SignI) & ((n>>1) ? ~SignJ : SignJ) ) // diff value is possible
continue;
Pol = Vec_IntEntry(&p->vPols[c], i) ^ (n&1);
Pol2 = Vec_IntEntry(&p->vPols[c], j) ^ (n>>1);
Lits[1] = Abc_Var2Lit( i, Pol );
Lits[2] = Abc_Var2Lit( j, Pol2 );
status = sat_solver_solve( p->pSat, Lits, Lits + 3, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return 0;
if ( status == l_False )
{
Vec_IntPushTwo( &p->vImpls[c], Abc_Var2Lit(i, Pol), Abc_Var2Lit(j, Pol2) );
continue;
}
assert( status == l_True );
if ( p->nPats[c] == 64 )
continue;
// record this status
for ( k = 0; k <= p->iTarget; k++ )
if ( sat_solver_var_value(p->pSat, k) ^ Vec_IntEntry(&p->vPols[c], k) )
*Vec_WrdEntryP(&p->vSets[c], k) |= ((word)1 << p->nPats[c]);
p->nPats[c]++;
WeightBest = Weight;
iLitBest = Entry;
iCBest = c;
}
}
}
if ( WeightBest == -1 )
return -2;
// add clause
Lits[0] = Abc_Var2Lit( p->iTarget, iCBest );
Lits[1] = iLitBest;
RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
if ( RetValue == 0 )
return -1;
p->timeSat += Abc_Clock() - clk;
// print the results
if ( fVerbose )
if ( !fVerbose )
return Abc_Var2Lit( iLitBest, iCBest );
printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), WeightBest );
for ( c = 0; c < 2; c++ )
{
Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget );
printf( "\n%s-SET of object %d with gate \"%s\" and fanins: ", c ? "OFF": "ON", p->iTarget, Mio_GateReadName((Mio_Gate_t *)Vec_PtrEntry(&p->vGateHands, Vec_IntEntry(&p->vObjGates,p->iTarget))) );
printf( "\n%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ",
c ? "OFF": "ON", p->iTarget, p->nDivs,
Mio_GateReadName((Mio_Gate_t *)Vec_PtrEntry(&p->vGateHands, Vec_IntEntry(&p->vObjGates,p->iTarget))) );
Vec_IntForEachEntry( vLevel, Entry, i )
printf( "%d ", Entry );
printf( "\n" );
printf( "Implications: " );
Vec_IntForEachEntryDouble( &p->vImpls[c], Entry, Entry2, i )
{
if ( Entry2 == -1 )
printf( "%s%d ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry) );
else
printf( "%s%d:%s%d ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Abc_LitIsCompl(Entry2)? "!":"", Abc_Lit2Var(Entry2) );
}
Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindWeight(p, c, Entry) );
printf( "\n" );
printf( " " );
for ( i = 0; i <= p->iTarget; i++ )
printf( "%d", Vec_IntEntry(&p->vPols[c], i) );
printf( "\n\n" );
printf( "%d", i / 10 );
printf( "\n" );
printf( " " );
for ( i = 0; i <= p->iTarget; i++ )
printf( "%d", i % 10 );
@ -360,8 +388,117 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p )
}
printf( "\n" );
}
p->timeSat += Abc_Clock() - clk;
return 1;
return Abc_Var2Lit( iLitBest, iCBest );
}
int Sfm_DecPeformDec( Sfm_Dec_t * p, Mio_Library_t * pLib )
{
Vec_Int_t * vLevel;
int i, Dec, Last, fCompl, Pol, fConst = -1, nNodes = Vec_IntSize(&p->vObjGates);
// perform decomposition
Vec_IntClear( &p->vObjDec );
for ( i = 0; i <= p->nMffc; i++ )
{
Dec = Sfm_DecPeformDecOne( p, &fConst );
if ( Dec == -2 )
{
if ( p->pPars->fVerbose )
printf( "There is no decomposition (or time out occurred).\n" );
return -1;
}
if ( Dec == -1 )
break;
Vec_IntPush( &p->vObjDec, Dec );
}
if ( i == p->nMffc + 1 )
{
if ( p->pPars->fVerbose )
printf( "Area-reducing decomposition is not found.\n" );
return -1;
}
// check constant
if ( Vec_IntSize(&p->vObjDec) == 0 )
{
assert( fConst >= 0 );
// report
if ( p->pPars->fVerbose )
printf( "Create constant %d.\n", fConst );
// add gate
Vec_IntPush( &p->vObjGates, fConst ? p->GateConst1 : p->GateConst0 );
vLevel = Vec_WecPushLevel( &p->vObjFanins );
return Vec_IntSize(&p->vObjDec);
}
// create network
Last = Vec_IntPop( &p->vObjDec );
fCompl = Abc_LitIsCompl(Last);
Last = Abc_LitNotCond( Abc_Lit2Var(Last), fCompl );
if ( Vec_IntSize(&p->vObjDec) == 0 )
{
// report
if ( p->pPars->fVerbose )
// printf( "Create node %d = %s%d.\n", nNodes, (Abc_LitIsCompl(Last) ^ fCompl) ? "!":"", Abc_Lit2Var(Last) );
printf( "Create node %d = %s%d.\n", nNodes, Abc_LitIsCompl(Last) ? "!":"", Abc_Lit2Var(Last) );
// add gate
// Vec_IntPush( &p->vObjGates, (Abc_LitIsCompl(Last) ^ fCompl) ? p->GateInvert : p->GateBuffer );
Vec_IntPush( &p->vObjGates, Abc_LitIsCompl(Last) ? p->GateInvert : p->GateBuffer );
vLevel = Vec_WecPushLevel( &p->vObjFanins );
Vec_IntPush( vLevel, Abc_Lit2Var(Last) );
return Vec_IntSize(&p->vObjDec);
}
Vec_IntForEachEntryReverse( &p->vObjDec, Dec, i )
{
fCompl = Abc_LitIsCompl(Dec);
// Dec = Abc_Lit2Var(Dec);
Dec = Abc_LitNotCond( Abc_Lit2Var(Dec), fCompl );
// add gate
Pol = (Abc_LitIsCompl(Last) << 1) | Abc_LitIsCompl(Dec);
// Pol = Abc_LitIsCompl(Dec);
if ( fCompl )
Vec_IntPush( &p->vObjGates, p->GateOr[Pol] );
else
Vec_IntPush( &p->vObjGates, p->GateAnd[Pol] );
vLevel = Vec_WecPushLevel( &p->vObjFanins );
Vec_IntPush( vLevel, Abc_Lit2Var(Dec) );
Vec_IntPush( vLevel, Abc_Lit2Var(Last) );
// report
if ( p->pPars->fVerbose )
printf( "Create node %s%d = %s%d and %s%d (gate %d).\n",
fCompl? "!":"", nNodes,
Abc_LitIsCompl(Last)? "!":"", Abc_Lit2Var(Last),
Abc_LitIsCompl(Dec)? "!":"", Abc_Lit2Var(Dec),
Pol );
// prepare for the next one
Last = Abc_Var2Lit( nNodes, 0 );
nNodes++;
}
return Vec_IntSize(&p->vObjDec);
}
/**Function*************************************************************
Synopsis [Incremental level update.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkUpdateIncLevel_rec( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanout;
int i, LevelNew = Abc_ObjLevelNew(pObj);
if ( LevelNew == (int)pObj->Level )
return;
pObj->Level = LevelNew;
if ( Abc_ObjIsCo(pObj) )
return;
Abc_ObjForEachFanout( pObj, pFanout, i )
Abc_NtkUpdateIncLevel_rec( pFanout );
}
void Abc_NtkUpdateIncLevel( Abc_Obj_t * pObj )
{
Abc_NtkUpdateIncLevel_rec( pObj );
}
/**Function*************************************************************
@ -375,102 +512,208 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p )
SeeAlso []
***********************************************************************/
void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vTfo )
#define SFM_MASK_PI 1 // supp(node) is contained in supp(TFI(pivot))
#define SFM_MASK_INPUT 2 // supp(node) does not overlap with supp(TFI(pivot))
#define SFM_MASK_FANIN 4 // the same as above (pointed to by node with SFM_MASK_PI | SFM_MASK_INPUT)
#define SFM_MASK_MFFC 8 // MFFC nodes, including the target node
void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pObj, Vec_Int_t * vTfo, int nLevelMax, int nFanoutMax )
{
Abc_Obj_t * pFanout; int i;
if ( Abc_NodeIsTravIdCurrent( pNode ) )
if ( Abc_NodeIsTravIdCurrent( pObj ) )
return;
Abc_NodeSetTravIdCurrent( pNode );
if ( Abc_ObjIsCo(pNode) )
Abc_NodeSetTravIdCurrent( pObj );
if ( Abc_ObjIsCo(pObj) || Abc_ObjLevel(pObj) > nLevelMax )
return;
assert( Abc_ObjIsNode( pObj ) );
if ( Abc_ObjFanoutNum(pObj) <= nFanoutMax )
{
Vec_IntPush( vTfo, Abc_ObjId(pNode) );
return;
Abc_ObjForEachFanout( pObj, pFanout, i )
if ( Abc_ObjIsCo(pFanout) )
break;
if ( i == Abc_ObjFanoutNum(pObj) )
Abc_ObjForEachFanout( pObj, pFanout, i )
Abc_NtkDfsReverseOne_rec( pFanout, vTfo, nLevelMax, nFanoutMax );
}
assert( Abc_ObjIsNode( pNode ) );
Abc_ObjForEachFanout( pNode, pFanout, i )
Abc_NtkDfsReverseOne_rec( pFanout, vTfo );
Vec_IntPush( vTfo, Abc_ObjId(pNode) );
Vec_IntPush( vTfo, Abc_ObjId(pObj) );
pObj->iTemp = 0;
}
void Abc_NtkDfsOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vTfi, Vec_Int_t * vTypes )
int Abc_NtkDfsOne_rec( Abc_Obj_t * pObj, Vec_Int_t * vTfi, int nLevelMin, int CiLabel )
{
Abc_Obj_t * pFanin; int i, Mask = 0;
if ( Abc_NodeIsTravIdCurrent( pObj ) )
return pObj->iTemp;
Abc_NodeSetTravIdCurrent( pObj );
if ( Abc_ObjIsCi(pObj) || Abc_ObjLevel(pObj) < nLevelMin )
{
Vec_IntPush( vTfi, Abc_ObjId(pObj) );
return (pObj->iTemp = CiLabel);
}
assert( Abc_ObjIsNode(pObj) );
Abc_ObjForEachFanin( pObj, pFanin, i )
Mask |= Abc_NtkDfsOne_rec( pFanin, vTfi, nLevelMin, CiLabel );
Vec_IntPush( vTfi, Abc_ObjId(pObj) );
//assert( Mask > 0 );
return (pObj->iTemp = Mask);
}
void Sfm_DecAddNode( Abc_Obj_t * pObj, Vec_Int_t * vMap, Vec_Int_t * vGates, int fSkip, int fVeryVerbose )
{
if ( fVeryVerbose )
printf( "%d:%d(%d) ", Vec_IntSize(vMap), Abc_ObjId(pObj), pObj->iTemp );
if ( fVeryVerbose )
Abc_ObjPrint( stdout, pObj );
Vec_IntPush( vMap, Abc_ObjId(pObj) );
Vec_IntPush( vGates, fSkip ? -1 : Mio_GateReadValue((Mio_Gate_t *)pObj->pData) );
}
int Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nMffcMax, int fVeryVerbose )
{
Abc_Obj_t * pFanin, * pFanin2;
int i, k, nMffc = 1;
pPivot->iTemp |= SFM_MASK_MFFC;
if ( fVeryVerbose )
printf( "Mffc = %d.\n", pPivot->Id );
Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 && Abc_NodeIsTravIdCurrent(pFanin) )
{
if ( nMffc == nMffcMax )
return nMffc;
pFanin->iTemp |= SFM_MASK_MFFC;
nMffc++;
if ( fVeryVerbose )
printf( "Mffc = %d.\n", pFanin->Id );
}
Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 && Abc_NodeIsTravIdCurrent(pFanin) )
{
if ( nMffc == nMffcMax )
return nMffc;
Abc_ObjForEachFanin( pFanin, pFanin2, k )
if ( Abc_ObjIsNode(pFanin2) && Abc_ObjFanoutNum(pFanin2) == 1 && Abc_NodeIsTravIdCurrent(pFanin2) )
{
if ( nMffc == nMffcMax )
return nMffc;
pFanin2->iTemp |= SFM_MASK_MFFC;
nMffc++;
if ( fVeryVerbose )
printf( "Mffc = %d.\n", pFanin2->Id );
}
}
return nMffc;
}
int Abc_NtkDfsCheck_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPivot )
{
Abc_Obj_t * pFanin; int i;
if ( Abc_NodeIsTravIdCurrent( pNode ) )
return;
Abc_NodeSetTravIdCurrent( pNode );
if ( Abc_ObjIsCi(pNode) )
{
pNode->iTemp = Vec_IntSize(vTfi);
Vec_IntPush( vTfi, Abc_ObjId(pNode) );
Vec_IntPush( vTypes, 1 );
return;
}
assert( Abc_ObjIsNode(pNode) );
Abc_ObjForEachFanin( pNode, pFanin, i )
Abc_NtkDfsOne_rec( pFanin, vTfi, vTypes );
pNode->iTemp = Vec_IntSize(vTfi);
Vec_IntPush( vTfi, Abc_ObjId(pNode) );
Vec_IntPush( vTypes, 0 );
if ( pObj == pPivot )
return 0;
if ( Abc_NodeIsTravIdCurrent( pObj ) )
return 1;
Abc_NodeSetTravIdCurrent( pObj );
if ( Abc_ObjIsCi(pObj) )
return 1;
assert( Abc_ObjIsNode(pObj) );
Abc_ObjForEachFanin( pObj, pFanin, i )
if ( !Abc_NtkDfsCheck_rec(pFanin, pPivot) )
return 0;
return 1;
}
int Sfm_DecExtract( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Vec_Int_t * vTypes, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Int_t * vTfo )
int Sfm_DecExtract( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars, Abc_Obj_t * pPivot, Vec_Int_t * vRoots, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Int_t * vTfi, Vec_Int_t * vTfo, int * pnMffc )
{
Vec_Int_t * vLevel;
Abc_Obj_t * pFanin;
int i, k, iObj, iTarget;
assert( Abc_ObjIsNode(pNode) );
// collect transitive fanout including COs
Abc_Obj_t * pObj, * pFanin;
int nLevelMax = pPivot->Level + pPars->nTfoLevMax;
int nLevelMin = pPivot->Level - pPars->nTfiLevMax;
int i, k, nTfiSize, nDivs = -1;
assert( Abc_ObjIsNode(pPivot) );
if ( pPars->fVerbose )
printf( "\n\nTarget %d\n", Abc_ObjId(pPivot) );
// collect TFO nodes
Vec_IntClear( vTfo );
Abc_NtkIncrementTravId( pNtk );
Abc_NtkDfsReverseOne_rec( pNode, vTfo );
// collect transitive fanin
Vec_IntClear( vMap );
Vec_IntClear( vTypes );
Abc_NtkDfsReverseOne_rec( pPivot, vTfo, nLevelMax, pPars->nFanoutMax );
// count internal fanouts
Abc_NtkForEachObjVec( vTfo, pNtk, pObj, i )
Abc_ObjForEachFanin( pObj, pFanin, k )
pFanin->iTemp++;
// comput roots
Vec_IntClear( vRoots );
Abc_NtkForEachObjVec( vTfo, pNtk, pObj, i )
if ( pObj->iTemp != Abc_ObjFanoutNum(pObj) )
Vec_IntPush( vRoots, Abc_ObjId(pObj) );
assert( Vec_IntSize(vRoots) > 0 );
// collect TFI and mark nodes
Vec_IntClear( vTfi );
Abc_NtkIncrementTravId( pNtk );
Abc_NtkDfsOne_rec( pNode, vMap, vTypes );
Vec_IntPop( vMap );
Vec_IntPop( vTypes );
assert( Vec_IntSize(vMap) == Vec_IntSize(vTypes) );
// remember target node
iTarget = Vec_IntSize( vMap );
// add transitive fanout
Vec_IntForEachEntryReverse( vTfo, iObj, i )
{
pNode = Abc_NtkObj( pNtk, iObj );
if ( Abc_ObjIsCo(pNode) )
{
assert( Vec_IntEntry(vTypes, Abc_ObjFanin0(pNode)->iTemp) == 0 ); // CO points to a unique node
Vec_IntWriteEntry( vTypes, Abc_ObjFanin0(pNode)->iTemp, 2 );
continue;
}
pNode->iTemp = Vec_IntSize(vMap);
Vec_IntPush( vMap, Abc_ObjId(pNode) );
Vec_IntPush( vTypes, 0 );
}
assert( Vec_IntSize(vMap) == Vec_IntSize(vTypes) );
// create gates and fanins
Abc_NtkDfsOne_rec( pPivot, vTfi, nLevelMin, SFM_MASK_PI );
nTfiSize = Vec_IntSize(vTfi);
// additinally mark MFFC
*pnMffc = Sfm_DecMarkMffc( pPivot, pPars->nMffcMax, pPars->fVeryVerbose );
assert( *pnMffc <= pPars->nMffcMax );
if ( pPars->fVerbose )
printf( "Mffc size = %d.\n", *pnMffc );
// collect TFI(TFO)
Abc_NtkForEachObjVec( vTfo, pNtk, pObj, i )
Abc_NtkDfsOne_rec( pObj, vTfi, nLevelMin, SFM_MASK_INPUT );
// mark input-only nodes pointed to by mixed nodes
Abc_NtkForEachObjVecStart( vTfi, pNtk, pObj, i, nTfiSize )
if ( pObj->iTemp != SFM_MASK_INPUT )
Abc_ObjForEachFanin( pObj, pFanin, k )
if ( pFanin->iTemp == SFM_MASK_INPUT )
pFanin->iTemp = SFM_MASK_FANIN;
// collect nodes supported only on TFI fanins and not MFFC
Vec_IntClear( vMap );
Vec_IntClear( vGates );
Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i )
if ( pObj->iTemp == SFM_MASK_PI )
Sfm_DecAddNode( pObj, vMap, vGates, Abc_ObjIsCi(pObj) || Abc_ObjLevel(pObj) < nLevelMin, pPars->fVeryVerbose );
nDivs = Vec_IntSize(vMap);
if ( pPars->fVeryVerbose )
printf( "\nFinish divs\n" );
// add other nodes that are not in TFO and not in MFFC
Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i )
if ( pObj->iTemp == (SFM_MASK_PI | SFM_MASK_INPUT) || pObj->iTemp == SFM_MASK_FANIN || pObj->iTemp == 0 ) // const
Sfm_DecAddNode( pObj, vMap, vGates, pObj->iTemp == SFM_MASK_FANIN, pPars->fVeryVerbose );
if ( pPars->fVeryVerbose )
printf( "\nFinish side\n" );
// add the TFO nodes
Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i )
if ( pObj->iTemp >= SFM_MASK_MFFC )
Sfm_DecAddNode( pObj, vMap, vGates, 0, pPars->fVeryVerbose );
assert( Vec_IntSize(vMap) == Vec_IntSize(vGates) );
if ( pPars->fVeryVerbose )
printf( "\nFinish all\n" );
// create node IDs
Vec_WecClear( vFanins );
Vec_IntForEachEntry( vMap, iObj, i )
Abc_NtkForEachObjVec( vMap, pNtk, pObj, i )
{
pObj->iTemp = i;
vLevel = Vec_WecPushLevel( vFanins );
pNode = Abc_NtkObj( pNtk, iObj );
if ( Abc_ObjIsCi(pNode) )
{
Vec_IntPush( vGates, -1 );
continue;
}
Abc_ObjForEachFanin( pNode, pFanin, k )
Vec_IntPush( vLevel, pFanin->iTemp );
Vec_IntPush( vGates, Mio_GateReadValue((Mio_Gate_t *)pNode->pData) );
if ( Vec_IntEntry(vGates, i) >= 0 )
Abc_ObjForEachFanin( pObj, pFanin, k )
Vec_IntPush( vLevel, pFanin->iTemp );
}
return iTarget;
// remap roots
Abc_NtkForEachObjVec( vRoots, pNtk, pObj, i )
Vec_IntWriteEntry( vRoots, i, pObj->iTemp );
/*
// check
Abc_NtkForEachObjVec( vMap, pNtk, pObj, i )
{
if ( i == nDivs )
break;
Abc_NtkIncrementTravId( pNtk );
assert( Abc_NtkDfsCheck_rec(pObj, pPivot) );
}
*/
return nDivs;
}
void Sfm_DecInsert( Abc_Ntk_t * pNtk, int iNode, int Limit, Vec_Int_t * vTypes, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Ptr_t * vGateHandles )
void Sfm_DecInsert( Abc_Ntk_t * pNtk, Abc_Obj_t * pPivot, int Limit, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Ptr_t * vGateHandles )
{
Abc_Obj_t * pTarget = Abc_NtkObj( pNtk, iNode );
Abc_Obj_t * pObjNew = NULL;
int i, k, iObj, Gate;
// assuming that new gates are appended at the end
assert( Limit < Vec_IntSize(vTypes) );
assert( Limit < Vec_IntSize(vGates) );
assert( Limit == Vec_IntSize(vMap) );
// introduce new gates
Vec_IntForEachEntryStart( vGates, Gate, i, Limit )
{
@ -479,20 +722,30 @@ void Sfm_DecInsert( Abc_Ntk_t * pNtk, int iNode, int Limit, Vec_Int_t * vTypes,
Vec_IntForEachEntry( vLevel, iObj, k )
Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, iObj)) );
pObjNew->pData = Vec_PtrEntry( vGateHandles, Gate );
Vec_IntPush( vMap, Abc_ObjId(pObjNew) );
}
// transfer the fanout
Abc_ObjTransferFanout( pTarget, pObjNew );
assert( Abc_ObjFanoutNum(pTarget) == 0 );
Abc_NtkDeleteObj_rec( pTarget, 1 );
Abc_ObjTransferFanout( pPivot, pObjNew );
assert( Abc_ObjFanoutNum(pPivot) == 0 );
Abc_NtkDeleteObj_rec( pPivot, 1 );
// update level
Abc_NtkForEachObjVecStart( vMap, pNtk, pObjNew, i, Limit )
Abc_NtkUpdateIncLevel( pObjNew );
}
void Sfm_DecTestBench( Abc_Ntk_t * pNtk, int iNode )
void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
{
extern void Sfm_LibPreprocess( Mio_Library_t * pLib, Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t * vGateCnfs, Vec_Ptr_t * vGateHands );
Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
Sfm_Dec_t * p = Sfm_DecStart();
Vec_Int_t * vMap = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) ); // Sfm->Ntk
Sfm_Dec_t * p = Sfm_DecStart( pPars );
Abc_Obj_t * pObj;
int i, Limit;
int i, Limit, Count = 0, nStop = Abc_NtkObjNumMax(pNtk);
//int iNode = 2299;//8;//70;
printf( "Running remapping with parameters: " );
printf( "TFO = %d. ", pPars->nTfoLevMax );
printf( "TFI = %d. ", pPars->nTfiLevMax );
printf( "FanMax = %d. ", pPars->nFanoutMax );
printf( "MffcMax = %d. ", pPars->nMffcMax );
printf( "\n" );
// enter library
assert( Abc_NtkIsMappedLogic(pNtk) );
Sfm_LibPreprocess( pLib, &p->vGateSizes, &p->vGateFuncs, &p->vGateCnfs, &p->vGateHands );
@ -500,21 +753,37 @@ void Sfm_DecTestBench( Abc_Ntk_t * pNtk, int iNode )
p->GateConst1 = Mio_GateReadValue( Mio_LibraryReadConst1(pLib) );
p->GateBuffer = Mio_GateReadValue( Mio_LibraryReadBuf(pLib) );
p->GateInvert = Mio_GateReadValue( Mio_LibraryReadInv(pLib) );
p->GateAnd[0] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "and00", NULL) );
p->GateAnd[1] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "and01", NULL) );
p->GateAnd[2] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "and10", NULL) );
p->GateAnd[3] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "and11", NULL) );
p->GateOr[0] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "or00", NULL) );
p->GateOr[1] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "or01", NULL) );
p->GateOr[2] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "or10", NULL) );
p->GateOr[3] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "or11", NULL) );
// iterate over nodes
// Abc_NtkForEachNode( pNtk, pObj, i )
for ( ; pObj = Abc_NtkObj(pNtk, iNode); )
Abc_NtkLevel( pNtk );
Abc_NtkForEachNode( pNtk, pObj, i )
// for ( ; (pObj = Abc_NtkObj(pNtk, iNode)); )
{
p->iTarget = Sfm_DecExtract( pNtk, pObj, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap, &p->vTemp );
Limit = Vec_IntSize( &p->vObjTypes );
if ( i >= nStop )
break;
//if ( Abc_ObjFaninNum(pObj) == 0 || (Abc_ObjFaninNum(pObj) == 1 && Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) > 1) )
// continue;
p->nDivs = Sfm_DecExtract( pNtk, pPars, pObj, &p->vObjRoots, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vTemp, &p->vTemp2, &p->nMffc );
p->iTarget = pObj->iTemp;
Limit = Vec_IntSize( &p->vObjGates );
if ( !Sfm_DecPrepareSolver( p ) )
continue;
if ( !Sfm_DecPeformDec( p ) )
if ( Sfm_DecPeformDec( p, pLib ) == -1 )
continue;
// Sfm_DecInsert( pNtk, p->iTarget, Limit, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap, vGateHandles );
break;
Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands );
if ( pPars->fVerbose )
printf( "This was modification %d\n", Count );
//if ( Count == 2 )
// break;
Count++;
}
Vec_IntFree( vMap );
Sfm_DecStop( p );
}