From d7fc8fe98f99febca56b2ca8118d71fc0cde5793 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 22 Mar 2024 22:42:43 +0100 Subject: [PATCH] &mfs: Handle blackboxes robustly When the network is being handed over to the "sfm" core, all blackboxes are modeled by inserting new PIs, POs, and those being connected by buffers to the nodes representing the CIs, COs. Make two changes: * Robustly deny the fake PIs from being considered when shopping for LUT fanin substitutions. Such reconnection occurring would trip up the code reintegrating the result. * Make sure the buffer connecting the fake-PO to the CO doesn't get rewritten as part of the `mfs` transformation, and extend this protection to any whitebox models. --- src/aig/gia/giaMfs.c | 13 +++++++++++-- src/base/abci/abcMfs.c | 4 ++-- src/opt/sfm/sfm.h | 2 +- src/opt/sfm/sfmCore.c | 12 ++++++------ src/opt/sfm/sfmInt.h | 2 ++ src/opt/sfm/sfmNtk.c | 6 ++++-- 6 files changed, 26 insertions(+), 13 deletions(-) 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 );