diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index e5d7c37ee..91241aaff 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -58,6 +58,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_Wec_t * vFanins; // mfs data Vec_Str_t * vFixed; // mfs data Vec_Str_t * vEmpty; // mfs data + Vec_Str_t * vDenied; // mfs data Vec_Wrd_t * vTruths; // mfs data Vec_Int_t * vArray; Vec_Int_t * vStarts; @@ -81,9 +82,14 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) vFanins = Vec_WecStart( nMfsVars ); vFixed = Vec_StrStart( nMfsVars ); vEmpty = Vec_StrStart( nMfsVars ); + vDenied = Vec_StrStart( nMfsVars ); vTruths = Vec_WrdStart( nMfsVars ); vStarts = Vec_IntStart( nMfsVars ); vTruths2 = Vec_WrdAlloc( 10000 ); + // deny the PIs which are modeling blackbox outputs from being considered + // in substitutions + for (int i = 0; i < nBbOuts; i++) + Vec_StrWriteEntry( vDenied, i, (char)1 ); // set internal PIs Gia_ManCleanCopyArray( p ); Gia_ManForEachCiId( p, Id, i ) @@ -232,6 +238,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_IntFill( vArray, 1, iBbOut++ ); Vec_StrWriteEntry( vFixed, Counter, (char)1 ); Vec_StrWriteEntry( vEmpty, Counter, (char)1 ); + Vec_StrWriteEntry( vDenied, Counter, (char)1 ); Vec_WrdWriteEntry( vTruths, Counter, uTruths6[0] ); } for ( i = 0; i < nBoxIns; i++ ) @@ -240,7 +247,9 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) pObj = Gia_ManCo( p, curCo + i ); Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); // connect it with the special primary output (iBbIn) - vArray = Vec_WecEntry( vFanins, nMfsVars - nBbIns + iBbIn++ ); + int poNum = nMfsVars - nBbIns + iBbIn++; + vArray = Vec_WecEntry( vFanins, poNum ); + Vec_StrWriteEntry( vFixed, poNum, (char)1 ); assert( Vec_IntSize(vArray) == 0 ); Vec_IntFill( vArray, 1, Counter ); } @@ -268,7 +277,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) } // finalize Vec_IntFree( vLeaves ); - return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths, vStarts, vTruths2 ); + return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vDenied, vTruths, vStarts, vTruths2 ); } /**Function************************************************************* diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index 0533d189f..69c04c2c3 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -216,7 +216,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed ) // for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ ) // if ( rand() % 10 == 0 ) // Vec_StrWriteEntry( vFixed, i, (char)1 ); - return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); + return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, NULL, vTruths, vStarts, vTruths2 ); } Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) { @@ -285,7 +285,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) Abc_NtkForEachNode( pNtk, pObj, i ) if ( i >= iPivot ) Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 ); - return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); + return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, NULL, vTruths, vStarts, vTruths2 ); } /**Function************************************************************* diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 9cdf1bc67..5fd564fce 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -89,7 +89,7 @@ struct Sfm_Par_t_ extern void Sfm_ParSetDefault( Sfm_Par_t * pPars ); extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ); /*=== sfmNtk.c ==========================================================*/ -extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); +extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Str_t * vDenied, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); extern void Sfm_NtkFree( Sfm_Ntk_t * p ); extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ); extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index c0dc70dd5..87c11e615 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -115,7 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) int fSkipUpdate = 0; int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556; int i, iFanin, iVar = -1; - int iFaninRem = -1, iFaninSkip = -1; + int iFaninRem = -1; int nFanins = Sfm_ObjFaninNum(p, iNode); word uTruth, uSign, uMask; abctime clk; @@ -138,9 +138,6 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) else iFaninRem = iFanin; assert( iFaninRem != -1 ); - // find fanin to skip - if ( Sfm_ObjIsFixed(p, iFaninRem) && Sfm_ObjFaninNum(p, iFaninRem) == 1 ) - iFaninSkip = Sfm_ObjFanin(p, iFaninRem, 0); clk = Abc_Clock(); uTruth = Sfm_ComputeInterpolant( p ); p->timeSat += Abc_Clock() - clk; @@ -176,11 +173,10 @@ p->timeSat += Abc_Clock() - clk; // find the next divisor to try uMask = (~(word)0) >> (64 - p->nCexes); Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar ) - if ( uSign == uMask && Vec_IntEntry(p->vDivs, iVar) != iFaninSkip ) + if ( uSign == uMask && !Sfm_ObjIsDenied(p, Vec_IntEntry(p->vDivs, iVar)) ) break; if ( iVar == Vec_IntSize(p->vDivs) ) return 0; - assert( Vec_IntEntry(p->vDivs, iVar) != iFaninSkip ); // try replacing the critical fanin Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) ); clk = Abc_Clock(); @@ -289,6 +285,10 @@ p->timeSat += Abc_Clock() - clk; int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) { int i, iFanin; + + if (Sfm_NodeReadFixed(p, iNode)) + return 0; + p->nNodesTried++; // prepare SAT solver if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) ) diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index ae4bb60a8..6f86a5c6a 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -81,6 +81,7 @@ struct Sfm_Ntk_t_ // user data Vec_Str_t * vFixed; // persistent objects Vec_Str_t * vEmpty; // transparent objects + Vec_Str_t * vDenied; // denied objects Vec_Wrd_t * vTruths; // truth tables Vec_Wec_t vFanins; // fanins Vec_Int_t * vStarts; // offsets @@ -157,6 +158,7 @@ static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos >= p->nObjs; } static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; } static inline int Sfm_ObjIsFixed( Sfm_Ntk_t * p, int i ) { return Vec_StrEntry(p->vFixed, i); } +static inline int Sfm_ObjIsDenied( Sfm_Ntk_t * p, int i ) { return p->vDenied && Vec_StrEntry(p->vDenied, i); } static inline int Sfm_ObjAddsLevelArray( Vec_Str_t * p, int i ) { return p == NULL || Vec_StrEntry(p, i) == 0; } static inline int Sfm_ObjAddsLevel( Sfm_Ntk_t * p, int i ) { return Sfm_ObjAddsLevelArray(p->vEmpty, i); } diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 70afd91aa..9f32cbb58 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -58,7 +58,7 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * assert( Fanin + nPos < Vec_WecSize(vFanins) ); // POs have one fanout if ( i + nPos >= Vec_WecSize(vFanins) ) - assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 ); + assert( Vec_IntSize(vArray) == 1 ); } } @@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v SeeAlso [] ***********************************************************************/ -Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) +Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Str_t * vDenied, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) { Sfm_Ntk_t * p; int i; Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed ); @@ -177,6 +177,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t p->vFixed = vFixed; p->vEmpty = vEmpty; p->vTruths = vTruths; + p->vDenied = vDenied; p->vFanins = *vFanins; p->vStarts = vStarts; p->vTruths2 = vTruths2; @@ -221,6 +222,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) // user data Vec_StrFree( p->vFixed ); Vec_StrFreeP( &p->vEmpty ); + Vec_StrFreeP( &p->vDenied ); Vec_WrdFree( p->vTruths ); Vec_WecErase( &p->vFanins ); Vec_IntFree( p->vStarts );