diff options
| -rw-r--r-- | src/base/abci/abc.c | 24 | ||||
| -rw-r--r-- | src/map/mio/mio.h | 1 | ||||
| -rw-r--r-- | src/map/mio/mioApi.c | 1 | ||||
| -rw-r--r-- | src/opt/sfm/sfm.h | 3 | ||||
| -rw-r--r-- | src/opt/sfm/sfmDec.c | 440 |
5 files changed, 364 insertions, 105 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2170b703..ee0021cf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -5160,7 +5160,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Sfm_ParSetDefault3( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "OIFLHDMCNdazovwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "OIFLHDMCNPdazospvwh" ) ) != EOF ) { switch ( c ) { @@ -5266,6 +5266,17 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nNodesMax < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->iNodeOne = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->iNodeOne < 0 ) + goto usage; + break; case 'a': pPars->fArea ^= 1; break; @@ -5275,6 +5286,12 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fRrOnly ^= 1; break; + case 's': + pPars->fUseSim ^= 1; + break; + case 'p': + pPars->fPrintDecs ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -5302,7 +5319,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: mfs3 [-OIFLHDMCN <num>] [-azovwh]\n" ); + Abc_Print( -2, "usage: mfs3 [-OIFLHDMCNP <num>] [-azospvwh]\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 (1 <= num) [default = %d]\n", pPars->nTfiLevMax ); @@ -5313,9 +5330,12 @@ usage: 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-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-P <num> : one particular node to try (0 = none) [default = %d]\n", pPars->iNodeOne ); Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); Abc_Print( -2, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); Abc_Print( -2, "\t-o : toggle using old implementation for comparison [default = %s]\n", pPars->fRrOnly? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using simulation [default = %s]\n", pPars->fUseSim? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle printing decompositions [default = %s]\n", pPars->fPrintDecs? "yes": "no" ); 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"); diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index 9dd72d93..ef1f4258 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -146,6 +146,7 @@ extern Mio_Gate_t * Mio_GateReadTwin ( Mio_Gate_t * pGate ); extern int Mio_GateReadPinNum ( Mio_Gate_t * pGate ); extern double Mio_GateReadDelayMax ( Mio_Gate_t * pGate ); extern char * Mio_GateReadSop ( Mio_Gate_t * pGate ); +extern Vec_Int_t * Mio_GateReadExpr ( Mio_Gate_t * pGate ); extern word Mio_GateReadTruth ( Mio_Gate_t * pGate ); extern int Mio_GateReadValue ( Mio_Gate_t * pGate ); extern char * Mio_GateReadPinName ( Mio_Gate_t * pGate, int iPin ); diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c index 6716bfb9..ba84c178 100644 --- a/src/map/mio/mioApi.c +++ b/src/map/mio/mioApi.c @@ -174,6 +174,7 @@ Mio_Gate_t * Mio_GateReadTwin ( Mio_Gate_t * pGate ) { return int Mio_GateReadPinNum ( Mio_Gate_t * pGate ) { return pGate->nInputs; } double Mio_GateReadDelayMax( Mio_Gate_t * pGate ) { return pGate->dDelayMax; } char * Mio_GateReadSop ( Mio_Gate_t * pGate ) { return pGate->pSop; } +Vec_Int_t * Mio_GateReadExpr ( Mio_Gate_t * pGate ) { return pGate->vExpr; } word Mio_GateReadTruth ( Mio_Gate_t * pGate ) { return pGate->nInputs <= 6 ? pGate->uTruth : 0; } word * Mio_GateReadTruthP ( Mio_Gate_t * pGate ) { return pGate->nInputs <= 6 ? NULL: pGate->pTruth; } int Mio_GateReadValue ( Mio_Gate_t * pGate ) { return pGate->Value; } diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index fc2a9e54..f3557de0 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -53,11 +53,14 @@ struct Sfm_Par_t_ int nGrowthLevel; // the maximum allowed growth in level int nBTLimit; // the maximum number of conflicts in one SAT run int nNodesMax; // the maximum number of nodes to try + int iNodeOne; // one particular node to try int nFirstFixed; // the number of first nodes to be treated as fixed int fRrOnly; // perform redundance removal int fArea; // performs optimization for area int fMoreEffort; // performs high-affort minimization int fZeroCost; // enable zero-cost replacement + int fUseSim; // enable simulation + int fPrintDecs; // enable printing decompositions int fVerbose; // enable basic stats int fVeryVerbose; // enable detailed stats }; diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c index e3ee4ec8..2e986c84 100644 --- a/src/opt/sfm/sfmDec.c +++ b/src/opt/sfm/sfmDec.c @@ -24,6 +24,7 @@ #include "base/abc/abc.h" #include "misc/util/utilTruth.h" #include "opt/dau/dau.h" +#include "map/mio/exp.h" ABC_NAMESPACE_IMPL_START @@ -54,11 +55,16 @@ struct Sfm_Dec_t_ int nMffc; // the number of divisors int AreaMffc; // the area of gates in MFFC int iTarget; // target node + word uCareSet; // computed careset 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 + Vec_Int_t vObjMffc; // MFFC nodes + Vec_Int_t vObjInMffc; // inputs of MFFC nodes + Vec_Wrd_t vObjSims; // simulation patterns + Vec_Wrd_t vObjSims2; // simulation patterns // solver sat_solver * pSat; // reusable solver Vec_Wec_t vClauses; // CNF clauses for the node @@ -95,6 +101,7 @@ struct Sfm_Dec_t_ int nSatCalls; int nSatCallsSat; int nSatCallsUnsat; + int nSatCallsOver; int nTimeOuts; int nNoDecs; int nMaxDivs; @@ -103,6 +110,16 @@ struct Sfm_Dec_t_ word nAllWin; }; +#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 +#define SFM_MASK_PIVOT 16 // the target node + +static inline Sfm_Dec_t * Sfm_DecMan( Abc_Obj_t * p ) { return (Sfm_Dec_t *)p->pNtk->pData; } +static inline word Sfm_DecObjSim( Sfm_Dec_t * p, Abc_Obj_t * pObj ) { return Vec_WrdEntry(&p->vObjSims, Abc_ObjId(pObj)); } +static inline word Sfm_DecObjSim2( Sfm_Dec_t * p, Abc_Obj_t * pObj ) { return Vec_WrdEntry(&p->vObjSims2, Abc_ObjId(pObj)); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -175,6 +192,10 @@ void Sfm_DecStop( Sfm_Dec_t * p ) Vec_WecErase( &p->vObjFanins ); Vec_IntErase( &p->vObjMap ); Vec_IntErase( &p->vObjDec ); + Vec_IntErase( &p->vObjMffc ); + Vec_IntErase( &p->vObjInMffc ); + Vec_WrdErase( &p->vObjSims ); + Vec_WrdErase( &p->vObjSims2 ); // solver sat_solver_delete( p->pSat ); Vec_WecErase( &p->vClauses ); @@ -199,6 +220,168 @@ void Sfm_DecStop( Sfm_Dec_t * p ) SeeAlso [] ***********************************************************************/ +static inline word Sfm_ObjSimulate( Abc_Obj_t * pObj ) +{ + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + Vec_Int_t * vExpr = Mio_GateReadExpr( (Mio_Gate_t *)pObj->pData ); + Abc_Obj_t * pFanin; int i; word uFanins[6]; + Abc_ObjForEachFanin( pObj, pFanin, i ) + uFanins[i] = Sfm_DecObjSim( p, pFanin ); + return Exp_Truth6( Abc_ObjFaninNum(pObj), vExpr, uFanins ); +} +static inline word Sfm_ObjSimulate2( Abc_Obj_t * pObj ) +{ + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + Vec_Int_t * vExpr = Mio_GateReadExpr( (Mio_Gate_t *)pObj->pData ); + Abc_Obj_t * pFanin; int i; word uFanins[6]; + Abc_ObjForEachFanin( pObj, pFanin, i ) + if ( (pFanin->iTemp & SFM_MASK_PIVOT) ) + uFanins[i] = Sfm_DecObjSim2( p, pFanin ); + else + uFanins[i] = Sfm_DecObjSim( p, pFanin ); + return Exp_Truth6( Abc_ObjFaninNum(pObj), vExpr, uFanins ); +} +static inline void Sfm_NtkSimulate( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; int i; word uTemp; + Sfm_Dec_t * p = Sfm_DecMan( Abc_NtkPi(pNtk, 0) ); + Vec_WrdFill( &p->vObjSims, 2*Abc_NtkObjNumMax(pNtk), 0 ); + Vec_WrdFill( &p->vObjSims2, 2*Abc_NtkObjNumMax(pNtk), 0 ); + Gia_ManRandomW(1); + assert( p->pPars->fUseSim ); + Abc_NtkForEachCi( pNtk, pObj, i ) + { + Vec_WrdWriteEntry( &p->vObjSims, Abc_ObjId(pObj), (uTemp = Gia_ManRandomW(0)) ); + //printf( "Inpt = %5d : ", Abc_ObjId(pObj) ); + //Extra_PrintBinary( stdout, (unsigned *)&uTemp, 64 ); + //printf( "\n" ); + } + vNodes = Abc_NtkDfs( pNtk, 1 ); + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + { + Vec_WrdWriteEntry( &p->vObjSims, Abc_ObjId(pObj), (uTemp = Sfm_ObjSimulate(pObj)) ); + //printf( "Obj = %5d : ", Abc_ObjId(pObj) ); + //Extra_PrintBinary( stdout, (unsigned *)&uTemp, 64 ); + //printf( "\n" ); + } + Vec_PtrFree( vNodes ); +} +static inline void Sfm_ObjSimulateNode( Abc_Obj_t * pObj ) +{ + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + if ( !p->pPars->fUseSim ) + return; + Vec_WrdWriteEntry( &p->vObjSims, Abc_ObjId(pObj), Sfm_ObjSimulate(pObj) ); + if ( (pObj->iTemp & SFM_MASK_PIVOT) ) + Vec_WrdWriteEntry( &p->vObjSims2, Abc_ObjId(pObj), Sfm_ObjSimulate2(pObj) ); +} +static inline void Sfm_ObjFlipNode( Abc_Obj_t * pObj ) +{ + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + if ( !p->pPars->fUseSim ) + return; + Vec_WrdWriteEntry( &p->vObjSims2, Abc_ObjId(pObj), ~Sfm_DecObjSim(p, pObj) ); +} +static inline word Sfm_ObjFindCareSet( Abc_Ntk_t * pNtk, Vec_Int_t * vRoots ) +{ + Sfm_Dec_t * p = Sfm_DecMan( Abc_NtkPi(pNtk, 0) ); + Abc_Obj_t * pObj; int i; word Res = 0; + if ( !p->pPars->fUseSim ) + return 0; + Abc_NtkForEachObjVec( vRoots, pNtk, pObj, i ) + Res |= Sfm_DecObjSim(p, pObj) ^ Sfm_DecObjSim2(p, pObj); + return Res; +} +static inline void Sfm_ObjSetupSimInfo( Abc_Obj_t * pObj ) +{ + int nPatKeep = 24; + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + word uCareSet = p->uCareSet; + word uValues = Sfm_DecObjSim(p, pObj); + int c, d, i, Indexes[2][64]; + assert( p->iTarget == pObj->iTemp ); + assert( p->pPars->fUseSim ); + // find what patterns go to on-set/off-set + p->nPats[0] = p->nPats[1] = 0; + p->uMask[0] = p->uMask[1] = 0; + Vec_WrdFill( &p->vSets[0], p->nDivs, 0 ); + Vec_WrdFill( &p->vSets[1], p->nDivs, 0 ); + if ( uCareSet == 0 ) + return; + for ( i = 0; i < 64; i++ ) + if ( (uCareSet >> i) & 1 ) + { + c = !((uValues >> i) & 1); + Indexes[c][p->nPats[c]++] = i; + } + for ( c = 0; c < 2; c++ ) + { + p->nPats[c] = Abc_MinInt( p->nPats[c], nPatKeep ); + p->uMask[c] = Abc_Tt6Mask( p->nPats[c] ); + } + // write patterns + for ( d = 0; d < p->nDivs; d++ ) + { + word uSim = Vec_WrdEntry( &p->vObjSims, Vec_IntEntry(&p->vObjMap, d) ); + for ( c = 0; c < 2; c++ ) + for ( i = 0; i < p->nPats[c]; i++ ) + if ( (uSim >> Indexes[c][i]) & 1 ) + *Vec_WrdEntryP(&p->vSets[c], d) |= ((word)1 << i); + } + //printf( "Node %d : Onset = %d. Offset = %d.\n", pObj->Id, p->nPats[0], p->nPats[1] ); +} +static inline void Sfm_ObjSetdownSimInfo( Abc_Obj_t * pObj ) +{ + int nPatKeep = 32; + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + int c, d; word uSim, uSims[2], uMask; + assert( p->pPars->fUseSim ); + for ( d = 0; d < p->nDivs; d++ ) + { + uSim = Vec_WrdEntry( &p->vObjSims, Vec_IntEntry(&p->vObjMap, d) ); + for ( c = 0; c < 2; c++ ) + { + uMask = p->nPats[c] < nPatKeep ? p->uMask[c] : Abc_Tt6Mask(nPatKeep); + uSims[c] = (Vec_WrdEntry(&p->vSets[c], d) & uMask) | (uSim & ~uMask); + uSim >>= 32; + } + uSim = (uSims[0] & 0xFFFFFFFF) | (uSims[1] << 32); + Vec_WrdWriteEntry( &p->vObjSims, Vec_IntEntry(&p->vObjMap, d), uSim ); + } +} +/* +void Sfm_ObjSetdownSimInfo( Abc_Obj_t * pObj ) +{ + int nPatKeep = 32; + Sfm_Dec_t * p = Sfm_DecMan( pObj ); + word uSim, uMaskKeep[2]; + int c, d, nKeeps[2]; + for ( c = 0; c < 2; c++ ) + { + nKeeps[c] = Abc_MaxInt(p->nPats[c], nPatKeep); + uMaskKeep[c] = Abc_Tt6Mask( nKeeps[c] ); + } + for ( d = 0; d < p->nDivs; d++ ) + { + uSim = Vec_WrdEntry( &p->vObjSims, Vec_IntEntry(&p->vObjMap, d) ) << (nKeeps[0] + nKeeps[1]); + uSim |= (Vec_WrdEntry(&p->vSets[0], d) & uMaskKeep[0]) | ((Vec_WrdEntry(&p->vSets[1], d) & uMaskKeep[1]) << nKeeps[0]); + Vec_WrdWriteEntry( &p->vObjSims, Vec_IntEntry(&p->vObjMap, d), uSim ); + } +} +*/ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Sfm_DecPrepareSolver( Sfm_Dec_t * p ) { Vec_Int_t * vRoots = &p->vObjRoots; @@ -395,7 +578,10 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst ) p->nSatCallsSat++; p->timeSatSat += Abc_Clock() - clk; if ( p->nPats[c] == 64 ) + { + p->nSatCallsOver++; continue; + } // record this status for ( k = 0; k < p->nDivs; k++ ) if ( sat_solver_var_value(p->pSat, k) ) @@ -609,7 +795,10 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu p->nSatCallsSat++; p->timeSatSat += Abc_Clock() - clk; if ( p->nPats[c] == 64 ) - return -2;//continue; + { + p->nSatCallsOver++; + continue;//return -2;//continue; + } for ( i = 0; i < p->nDivs; i++ ) if ( sat_solver_var_value(p->pSat, i) ) *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]); @@ -623,8 +812,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu { word MaskAll = p->uMask[c] & Masks[c]; word MaskCur = Vec_WrdEntry(&p->vSets[c], d) & Masks[c]; - assert( MaskAll ); - if ( MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros + if ( MaskAll != 0 && MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros continue; p->nSatCalls++; pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c ); @@ -643,7 +831,10 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu p->nSatCallsSat++; p->timeSatSat += Abc_Clock() - clk; if ( p->nPats[c] == 64 ) + { + p->nSatCallsOver++; return -2;//continue; + } // record this status for ( i = 0; i < p->nDivs; i++ ) if ( sat_solver_var_value(p->pSat, i) ) @@ -662,8 +853,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu { word MaskAll = p->uMask[c] & Masks[c]; word MaskCur = Vec_WrdEntry(&p->vSets[c], d) & Masks[c]; - assert( MaskAll ); - if ( MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros + if ( MaskAll != 0 && MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros continue; p->nSatCalls++; pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c ); @@ -684,7 +874,10 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu p->nSatCallsSat++; p->timeSatSat += Abc_Clock() - clk; if ( p->nPats[c] == 64 ) - return -2;//continue; + { + p->nSatCallsOver++; + continue;//return -2;//continue; + } // record this status for ( i = 0; i < p->nDivs; i++ ) if ( sat_solver_var_value(p->pSat, i) ) @@ -709,7 +902,6 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu } /* // try using all implications at once -// if ( p->pPars->fVeryVerbose && p->iTarget == 56 ) for ( c = 0; c < 2; c++ ) { if ( Vec_IntSize(&p->vImpls[!c]) < 2 ) @@ -764,14 +956,16 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu p->nSatCallsSat++; p->timeSatSat += Abc_Clock() - clk; if ( p->nPats[c] == 64 ) - return -2;//continue; + { + p->nSatCallsOver++; + continue;//return -2;//continue; + } for ( i = 0; i < p->nDivs; i++ ) if ( sat_solver_var_value(p->pSat, i) ) *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]); p->uMask[c] |= ((word)1 << p->nPats[c]++); } */ - // find the best cofactoring variable Var = -1, CostMin = ABC_INFINITY; for ( c = 0; c < 2; c++ ) @@ -790,9 +984,12 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu } if ( Var == -1 && fCofactor ) { - for ( Var = p->nDivs - 1; Var >= 0; Var-- ) + //for ( Var = p->nDivs - 1; Var >= 0; Var-- ) + Vec_IntForEachEntry( &p->vObjInMffc, Var, i ) if ( Vec_IntFind(&p->vObjDec, Var) == -1 ) break; + if ( i == Vec_IntSize(&p->vObjInMffc) ) + Var = -1; fCofactor = 0; } @@ -836,21 +1033,27 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu } return -2; } -int Sfm_DecPeformDec2( Sfm_Dec_t * p ) +int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj ) { word uTruth[SFM_DEC_MAX][SFM_WORD_MAX], Masks[2]; int pSupp[SFM_DEC_MAX][2*SFM_SUPP_MAX]; int nSupp[SFM_DEC_MAX], pAssump[SFM_WIN_MAX]; - int fVeryVerbose = p->pPars->fVeryVerbose; + int fVeryVerbose = p->pPars->fPrintDecs || p->pPars->fVeryVerbose; int nDecs = Abc_MaxInt(p->pPars->nDecMax, 1); int i, iBest = -1, RetValue, Prev = 0; - assert( p->pPars->nDecMax <= SFM_DEC_MAX ); - p->nPats[0] = p->nPats[1] = 0; - p->uMask[0] = p->uMask[1] = 0; - Vec_WrdFill( &p->vSets[0], p->nDivs, 0 ); - Vec_WrdFill( &p->vSets[1], p->nDivs, 0 ); + if ( p->pPars->fUseSim ) + Sfm_ObjSetupSimInfo( pObj ); + else + { + p->nPats[0] = p->nPats[1] = 0; + p->uMask[0] = p->uMask[1] = 0; + Vec_WrdFill( &p->vSets[0], p->nDivs, 0 ); + Vec_WrdFill( &p->vSets[1], p->nDivs, 0 ); + } + //Sfm_DecPrint( p, NULL ); if ( fVeryVerbose ) printf( "\nNode %4d : MFFC %2d\n", p->iTarget, p->nMffc ); + assert( p->pPars->nDecMax <= SFM_DEC_MAX ); for ( i = 0; i < nDecs; i++ ) { // reduce the variable array @@ -875,6 +1078,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p ) if ( nSupp[iBest] < 2 ) break; } + if ( p->pPars->fUseSim ) + Sfm_ObjSetdownSimInfo( pObj ); if ( iBest == -1 ) { if ( fVeryVerbose ) @@ -886,8 +1091,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p ) { if ( fVeryVerbose ) printf( "Best %d: %d ", iBest, nSupp[iBest] ); - if ( fVeryVerbose ) - Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] ); +// if ( fVeryVerbose ) +// Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] ); } // return -1; RetValue = Sfm_LibImplement( p->pLib, uTruth[iBest][0], pSupp[iBest], nSupp[iBest], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost ); @@ -921,7 +1126,7 @@ void Abc_NtkUpdateIncLevel_rec( Abc_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Testbench for AIG minimization.] + Synopsis [] Description [] @@ -930,11 +1135,22 @@ void Abc_NtkUpdateIncLevel_rec( Abc_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -#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 - +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; +} void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pObj, Vec_Int_t * vTfo, int nLevelMax, int nFanoutMax ) { Abc_Obj_t * pFanout; int i; @@ -958,7 +1174,7 @@ void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pObj, Vec_Int_t * vTfo, int nLevelMax } int Abc_NtkDfsOne_rec( Abc_Obj_t * pObj, Vec_Int_t * vTfi, int nLevelMin, int CiLabel ) { - Abc_Obj_t * pFanin; int i, Mask = 0; + Abc_Obj_t * pFanin; int i; if ( Abc_NodeIsTravIdCurrent( pObj ) ) return pObj->iTemp; Abc_NodeSetTravIdCurrent( pObj ); @@ -968,10 +1184,12 @@ int Abc_NtkDfsOne_rec( Abc_Obj_t * pObj, Vec_Int_t * vTfi, int nLevelMin, int Ci return (pObj->iTemp = CiLabel); } assert( Abc_ObjIsNode(pObj) ); + pObj->iTemp = Abc_ObjFaninNum(pObj) ? 0 : CiLabel; Abc_ObjForEachFanin( pObj, pFanin, i ) - Mask |= Abc_NtkDfsOne_rec( pFanin, vTfi, nLevelMin, CiLabel ); + pObj->iTemp |= Abc_NtkDfsOne_rec( pFanin, vTfi, nLevelMin, CiLabel ); Vec_IntPush( vTfi, Abc_ObjId(pObj) ); - return (pObj->iTemp = (Abc_ObjFaninNum(pObj) ? Mask : CiLabel)); + Sfm_ObjSimulateNode( pObj ); + return pObj->iTemp; } void Sfm_DecAddNode( Abc_Obj_t * pObj, Vec_Int_t * vMap, Vec_Int_t * vGates, int fSkip, int fVeryVerbose ) { @@ -982,61 +1200,64 @@ void Sfm_DecAddNode( Abc_Obj_t * pObj, Vec_Int_t * vMap, Vec_Int_t * vGates, int 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 nLevelMin, int nMffcMax, int fVeryVerbose, int * pAreaMffc ) +static inline int Sfm_DecNodeIsMffc( Abc_Obj_t * p, int nLevelMin ) { - Abc_Obj_t * pFanin, * pFanin2; - int i, k, nMffc = 1; - *pAreaMffc = (int)(MIO_NUM * Mio_GateReadArea((Mio_Gate_t *)pPivot->pData)); - pPivot->iTemp |= SFM_MASK_MFFC; -if ( fVeryVerbose ) -printf( "Mffc = %d.\n", pPivot->Id ); + return Abc_ObjIsNode(p) && Abc_ObjFanoutNum(p) == 1 && Abc_NodeIsTravIdCurrent(p) && (Abc_ObjLevel(p) >= nLevelMin || Abc_ObjFaninNum(p) == 0); +} +void Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nLevelMin, int nMffcMax, int fVeryVerbose, Vec_Int_t * vMffc, Vec_Int_t * vInMffc ) +{ + Abc_Obj_t * pFanin, * pFanin2, * pFanin3, * pObj; int i, k, n; + assert( nMffcMax > 0 ); + // collect MFFC + Vec_IntFill( vMffc, 1, Abc_ObjId(pPivot) ); Abc_ObjForEachFanin( pPivot, pFanin, i ) - if ( Abc_ObjIsNode(pFanin) && (Abc_ObjLevel(pFanin) >= nLevelMin || Abc_ObjFaninNum(pFanin) == 0) && Abc_ObjFanoutNum(pFanin) == 1 && Abc_NodeIsTravIdCurrent(pFanin) ) - { - if ( nMffc == nMffcMax ) - return nMffc; - *pAreaMffc += (int)(MIO_NUM * Mio_GateReadArea((Mio_Gate_t *)pFanin->pData)); - pFanin->iTemp |= SFM_MASK_MFFC; - nMffc++; -if ( fVeryVerbose ) -printf( "Mffc = %d.\n", pFanin->Id ); - } + if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) + Vec_IntPush( vMffc, Abc_ObjId(pFanin) ); Abc_ObjForEachFanin( pPivot, pFanin, i ) - if ( Abc_ObjIsNode(pFanin) && (Abc_ObjLevel(pFanin) >= nLevelMin || Abc_ObjFaninNum(pFanin) == 0) && Abc_ObjFanoutNum(pFanin) == 1 && Abc_NodeIsTravIdCurrent(pFanin) ) - { - if ( nMffc == nMffcMax ) - return nMffc; + if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) Abc_ObjForEachFanin( pFanin, pFanin2, k ) - if ( Abc_ObjIsNode(pFanin2) && (Abc_ObjLevel(pFanin2) >= nLevelMin || Abc_ObjFaninNum(pFanin2) == 0) && Abc_ObjFanoutNum(pFanin2) == 1 && Abc_NodeIsTravIdCurrent(pFanin2) ) - { - if ( nMffc == nMffcMax ) - return nMffc; - *pAreaMffc += (int)(MIO_NUM * Mio_GateReadArea((Mio_Gate_t *)pFanin2->pData)); - pFanin2->iTemp |= SFM_MASK_MFFC; - nMffc++; -if ( fVeryVerbose ) -printf( "Mffc = %d.\n", pFanin2->Id ); - } - } - return nMffc; + if ( Sfm_DecNodeIsMffc(pFanin2, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) + Vec_IntPush( vMffc, Abc_ObjId(pFanin2) ); + Abc_ObjForEachFanin( pPivot, pFanin, i ) + if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) + Abc_ObjForEachFanin( pFanin, pFanin2, k ) + if ( Sfm_DecNodeIsMffc(pFanin2, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) + Abc_ObjForEachFanin( pFanin2, pFanin3, n ) + if ( Sfm_DecNodeIsMffc(pFanin3, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) + Vec_IntPush( vMffc, Abc_ObjId(pFanin3) ); + // mark MFFC + assert( Vec_IntSize(vMffc) <= nMffcMax ); + Abc_NtkForEachObjVec( vMffc, pPivot->pNtk, pObj, i ) + pObj->iTemp |= SFM_MASK_MFFC; + pPivot->iTemp |= SFM_MASK_PIVOT; + // collect MFFC inputs + Vec_IntClear(vInMffc); + Abc_NtkForEachObjVec( vMffc, pPivot->pNtk, pObj, i ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + if ( Abc_NodeIsTravIdCurrent(pFanin) && pFanin->iTemp == SFM_MASK_PI ) + Vec_IntPushUnique( vInMffc, Abc_ObjId(pFanin) ); } -int Abc_NtkDfsCheck_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPivot ) + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sfm_DecMffcArea( Abc_Ntk_t * pNtk, Vec_Int_t * vMffc ) { - 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; + Abc_Obj_t * pObj; + int i, nAreaMffc = 0; + Abc_NtkForEachObjVec( vMffc, pNtk, pObj, i ) + nAreaMffc += (int)(MIO_NUM * Mio_GateReadArea((Mio_Gate_t *)pObj->pData)); + return nAreaMffc; } -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, int * pnAreaMffc ) +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, Vec_Int_t * vMffc, Vec_Int_t * vInMffc ) { int fVeryVerbose = 0;//pPars->fVeryVerbose; Vec_Int_t * vLevel; @@ -1066,13 +1287,14 @@ printf( "\n\nTarget %d\n", Abc_ObjId(pPivot) ); Abc_NtkIncrementTravId( pNtk ); Abc_NtkDfsOne_rec( pPivot, vTfi, nLevelMin, SFM_MASK_PI ); nTfiSize = Vec_IntSize(vTfi); + Sfm_ObjFlipNode( pPivot ); // additinally mark MFFC - *pnMffc = Sfm_DecMarkMffc( pPivot, nLevelMin, pPars->nMffcMax, fVeryVerbose, pnAreaMffc ); - assert( *pnMffc <= pPars->nMffcMax ); + Sfm_DecMarkMffc( pPivot, nLevelMin, pPars->nMffcMax, fVeryVerbose, vMffc, vInMffc ); + assert( Vec_IntSize(vMffc) <= pPars->nMffcMax ); if ( fVeryVerbose ) -printf( "Mffc size = %d. Mffc area = %.2f\n", *pnMffc, *pnAreaMffc*MIO_NUMINV ); +printf( "Mffc size = %d. Mffc area = %.2f. InMffc size = %d.\n", Vec_IntSize(vMffc), Sfm_DecMffcArea(pNtk, vMffc)*MIO_NUMINV, Vec_IntSize(vInMffc) ); // collect TFI(TFO) - Abc_NtkForEachObjVec( vTfo, pNtk, pObj, i ) + Abc_NtkForEachObjVec( vRoots, 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 ) @@ -1082,7 +1304,7 @@ printf( "Mffc size = %d. Mffc area = %.2f\n", *pnMffc, *pnAreaMffc*MIO_NUMINV ); pFanin->iTemp = SFM_MASK_FANIN; // collect nodes supported only on TFI fanins and not MFFC if ( fVeryVerbose ) -printf( "\nDivs: " ); +printf( "\nDivs:\n" ); Vec_IntClear( vMap ); Vec_IntClear( vGates ); Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i ) @@ -1091,13 +1313,13 @@ printf( "\nDivs: " ); nDivs = Vec_IntSize(vMap); // add other nodes that are not in TFO and not in MFFC if ( fVeryVerbose ) -printf( "\nSides: " ); +printf( "\nSides:\n" ); Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i ) if ( pObj->iTemp == (SFM_MASK_PI | SFM_MASK_INPUT) || pObj->iTemp == SFM_MASK_FANIN ) Sfm_DecAddNode( pObj, vMap, vGates, pObj->iTemp == SFM_MASK_FANIN, fVeryVerbose ); // add the TFO nodes if ( fVeryVerbose ) -printf( "\nTFO: " ); +printf( "\nTFO:\n" ); Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i ) if ( pObj->iTemp >= SFM_MASK_MFFC ) Sfm_DecAddNode( pObj, vMap, vGates, 0, fVeryVerbose ); @@ -1114,9 +1336,19 @@ printf( "\n" ); Abc_ObjForEachFanin( pObj, pFanin, k ) Vec_IntPush( vLevel, pFanin->iTemp ); } + // compute care set + Sfm_DecMan(pPivot)->uCareSet = Sfm_ObjFindCareSet(pPivot->pNtk, vRoots); + + //printf( "care = %5d : ", Abc_ObjId(pPivot) ); + //Extra_PrintBinary( stdout, (unsigned *)&Sfm_DecMan(pPivot)->uCareSet, 64 ); + //printf( "\n" ); + // remap roots Abc_NtkForEachObjVec( vRoots, pNtk, pObj, i ) Vec_IntWriteEntry( vRoots, i, pObj->iTemp ); + // remap inputs to MFFC + Abc_NtkForEachObjVec( vInMffc, pNtk, pObj, i ) + Vec_IntWriteEntry( vInMffc, i, pObj->iTemp ); /* // check Abc_NtkForEachObjVec( vMap, pNtk, pObj, i ) @@ -1202,10 +1434,10 @@ void Sfm_DecInsert( Abc_Ntk_t * pNtk, Abc_Obj_t * pPivot, int Limit, Vec_Int_t * } void Sfm_DecPrintStats( Sfm_Dec_t * p ) { - printf( "Node = %d. Try = %d. Change = %d. Const0 = %d. Const1 = %d. Buf = %d. Inv = %d. Gate = %d. AndOr = %d.\n", - p->nTotalNodesBeg, p->nNodesTried, p->nNodesChanged, p->nNodesConst0, p->nNodesConst1, p->nNodesBuf, p->nNodesInv, p->nNodesResyn, p->nNodesAndOr ); - printf( "MaxDiv = %d. MaxWin = %d. AveDiv = %d. AveWin = %d. Calls = %d. (Sat = %d. Unsat = %d.) T/O = %d. NoDec = %d.\n", - p->nMaxDivs, p->nMaxWin, (int)(p->nAllDivs/Abc_MaxInt(1, p->nNodesTried)), (int)(p->nAllWin/Abc_MaxInt(1, p->nNodesTried)), p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nTimeOuts, p->nNoDecs ); + printf( "Node = %d. Try = %d. Change = %d. Const0 = %d. Const1 = %d. Buf = %d. Inv = %d. Gate = %d. AndOr = %d. NoDec = %d.\n", + p->nTotalNodesBeg, p->nNodesTried, p->nNodesChanged, p->nNodesConst0, p->nNodesConst1, p->nNodesBuf, p->nNodesInv, p->nNodesResyn, p->nNodesAndOr, p->nNoDecs ); + printf( "MaxDiv = %d. MaxWin = %d. AveDiv = %d. AveWin = %d. Calls = %d. (Sat = %d. Unsat = %d.) Over = %d. T/O = %d.\n", + p->nMaxDivs, p->nMaxWin, (int)(p->nAllDivs/Abc_MaxInt(1, p->nNodesTried)), (int)(p->nAllWin/Abc_MaxInt(1, p->nNodesTried)), p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsOver, p->nTimeOuts ); p->timeTotal = Abc_Clock() - p->timeStart; p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat; @@ -1249,15 +1481,18 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars ) Sfm_Dec_t * p = Sfm_DecStart( pPars ); Abc_Obj_t * pObj; abctime clk; - int i = 0, Limit, RetValue, Count = 0, nStop = Abc_NtkObjNumMax(pNtk); - //int iNode = 8;//70; //2341;//8;//70; + int i = 0, Limit, RetValue, nStop = Abc_NtkObjNumMax(pNtk); printf( "Remapping parameters: " ); printf( "TFO = %d. ", pPars->nTfoLevMax ); printf( "TFI = %d. ", pPars->nTfiLevMax ); - printf( "FanMax = %d. ", pPars->nFanoutMax ); + printf( "FanMax = %d. ", pPars->nFanoutMax ); printf( "MffcMin = %d. ", pPars->nMffcMin ); printf( "MffcMax = %d. ", pPars->nMffcMax ); - printf( "Zero-cost = %s. ", pPars->fZeroCost ? "yes" : "no" ); + printf( "DecMax = %d. ", pPars->nDecMax ); + printf( "Sim = %s. ", pPars->fUseSim ? "yes" : "no" ); + printf( "0-cost = %s. ", pPars->fZeroCost ? "yes" : "no" ); + if ( pPars->iNodeOne ) + printf( "Pivot = %d. ", pPars->iNodeOne ); printf( "\n" ); // enter library assert( Abc_NtkIsMappedLogic(pNtk) ); @@ -1279,22 +1514,25 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars ) if ( pPars->fVerbose ) p->nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk); // iterate over nodes + pNtk->pData = p; Abc_NtkLevel( pNtk ); + if ( p->pPars->fUseSim ) + Sfm_NtkSimulate( pNtk ); Abc_NtkForEachNode( pNtk, pObj, i ) - //for ( ; (pObj = Abc_NtkObj(pNtk, iNode)); ) { if ( i >= nStop || (pPars->nNodesMax && i > pPars->nNodesMax) ) break; if ( pPars->nMffcMin > 1 && Abc_NodeMffcLabel(pObj) < pPars->nMffcMin ) continue; + if ( pPars->iNodeOne && i != pPars->iNodeOne ) + continue; + pPars->fVeryVerbose = pPars->iNodeOne && i == pPars->iNodeOne; p->nNodesTried++; - //if ( i == pPars->nNodesMax ) - // pPars->fVeryVerbose = 1; - //pPars->fVeryVerbose = (i % 500 == 0); - clk = Abc_Clock(); - p->nDivs = Sfm_DecExtract( pNtk, pPars, pObj, &p->vObjRoots, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vTemp, &p->vTemp2, &p->nMffc, &p->AreaMffc ); + p->nDivs = Sfm_DecExtract( pNtk, pPars, pObj, &p->vObjRoots, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vTemp, &p->vTemp2, &p->vObjMffc, &p->vObjInMffc ); p->timeWin += Abc_Clock() - clk; + p->nMffc = Vec_IntSize(&p->vObjMffc); + p->AreaMffc = Sfm_DecMffcArea(pNtk, &p->vObjMffc); p->nMaxDivs = Abc_MaxInt( p->nMaxDivs, p->nDivs ); p->nAllDivs += p->nDivs; p->iTarget = pObj->iTemp; @@ -1310,7 +1548,7 @@ clk = Abc_Clock(); if ( pPars->fRrOnly ) RetValue = Sfm_DecPeformDec( p ); else - RetValue = Sfm_DecPeformDec2( p ); + RetValue = Sfm_DecPeformDec2( p, pObj ); if ( p->pPars->fVeryVerbose ) printf( "\n\n" ); p->timeSat += Abc_Clock() - clk; @@ -1319,11 +1557,6 @@ p->timeSat += Abc_Clock() - clk; p->nNodesChanged++; Abc_NtkCountStats( p, Limit ); Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands, p->GateBuffer, p->GateInvert, &p->vGateFuncs ); -//if ( pPars->fVeryVerbose ) -//printf( "This was modification %d\n", Count ); - //if ( Count == 2 ) - // break; - Count++; } if ( pPars->fVerbose ) p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk); @@ -1332,6 +1565,7 @@ p->timeSat += Abc_Clock() - clk; if ( pPars->fVerbose ) Sfm_DecPrintStats( p ); Sfm_DecStop( p ); + pNtk->pData = NULL; } //////////////////////////////////////////////////////////////////////// |