diff options
| -rw-r--r-- | src/base/abci/abc.c | 175 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/opt/sfm/sfm.h | 2 | ||||
| -rw-r--r-- | src/opt/sfm/sfmDec.c | 629 |
4 files changed, 618 insertions, 190 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8133440b..c5300f69 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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" ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 2d60c730..a223d682 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -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" ); } diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 1d97cd8b..38744ae1 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -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 diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c index b4376718..fd9109c3 100644 --- a/src/opt/sfm/sfmDec.c +++ b/src/opt/sfm/sfmDec.c @@ -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; @@ -74,6 +80,32 @@ struct Sfm_Dec_t_ /**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 [] Description [] @@ -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) ) - { - Vec_IntPush( vTfo, Abc_ObjId(pNode) ); + Abc_NodeSetTravIdCurrent( pObj ); + if ( Abc_ObjIsCo(pObj) || Abc_ObjLevel(pObj) > nLevelMax ) return; + assert( Abc_ObjIsNode( pObj ) ); + if ( Abc_ObjFanoutNum(pObj) <= nFanoutMax ) + { + 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; - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - return; - Abc_NodeSetTravIdCurrent( pNode ); - if ( Abc_ObjIsCi(pNode) ) + 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 ) { - pNode->iTemp = Vec_IntSize(vTfi); - Vec_IntPush( vTfi, Abc_ObjId(pNode) ); - Vec_IntPush( vTypes, 1 ); - return; + Vec_IntPush( vTfi, Abc_ObjId(pObj) ); + return (pObj->iTemp = CiLabel); } - 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 ); + 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_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_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 ( 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, 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 ); } |