From b83985c25bf7845986f88335178068f99d500fe3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 22 Mar 2024 21:42:12 +0100 Subject: [PATCH 1/4] Add `&mfs -r` for re-import testing --- src/aig/gia/giaMfs.c | 3 +++ src/base/abci/abc.c | 6 +++++- src/opt/sfm/sfm.h | 1 + src/opt/sfm/sfmCore.c | 1 + 4 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index a0e6caed4..b1e657f73 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -517,6 +517,8 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) } // collect information pNtk = Gia_ManExtractMfs( p ); + if (pPars->fTestReimport) + goto reimport; // perform optimization nNodes = Sfm_NtkPerform( pNtk, pPars ); if ( nNodes == 0 ) @@ -529,6 +531,7 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) } else { + reimport: pNew = Gia_ManInsertMfs( p, pNtk, pPars->fAllBoxes ); if( pPars->fVerbose ) Abc_Print( 1, "The network has %d nodes changed by \"&mfs\".\n", nNodes ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cf5b341f3..f0fa728c2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -49096,7 +49096,7 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nDepthMax = 100; pPars->nWinSizeMax = 2000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaeblvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaeblvwhr" ) ) != EOF ) { switch ( c ) { @@ -49192,6 +49192,9 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': pPars->fUseDcs ^= 1; break; + case 'r': + pPars->fTestReimport ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -49261,6 +49264,7 @@ usage: Abc_Print( -2, "\t-l : toggle deriving don't-cares [default = %s]\n", pPars->fUseDcs? "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-r : toggle testing re-importing the network unchanged [default = %s]\n", pPars->fTestReimport? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index f9c95c83e..9cdf1bc67 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -73,6 +73,7 @@ struct Sfm_Par_t_ int fDelayVerbose; // enable delay stats int fVerbose; // enable basic stats int fVeryVerbose; // enable detailed stats + int fTestReimport; // enable testing of re-import }; //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index f363e1cb0..c0dc70dd5 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -58,6 +58,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) pPars->fAllBoxes = 0; // enable preserving all boxes pPars->fVerbose = 0; // enable basic stats pPars->fVeryVerbose = 0; // enable detailed stats + pPars->fTestReimport = 0; // enable testing of re-import } /**Function************************************************************* From fda490235eace499ccee78501d0fd1c268e64b52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 22 Mar 2024 22:01:08 +0100 Subject: [PATCH 2/4] &mfs: Fix issues with traversal when re-importing network The former implementation of `Sfm_NtkDfs` was trying to serialize the network while ordering all box inputs ahead of the box outputs. This is sometimes impossible, leaving the result unordered, which led to crashes in the `&mfs` code when it was reintegrating the result into the GIA structure: ABC: Assertion failed: iLitNew >= 0 (src/aig/gia/giaMfs.c: Gia_ManInsertMfs: 388) With a small change to `Gia_ManInsertMfs` which does the reintegration we don't really need the ordering to see through boxes, ordering on the paths between boxes is sufficient. Relaxing the ordering requirement, we make `Sfm_NtkDfs` robust. --- src/aig/gia/giaMfs.c | 15 ++++++++---- src/opt/sfm/sfmWin.c | 58 +++++++++++++++++++++++++++++--------------- 2 files changed, 49 insertions(+), 24 deletions(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index b1e657f73..e5d7c37ee 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -381,6 +381,15 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) continue; } Vec_IntClear( vLeaves ); + + // handle internal CIs first, before we go looking for vLeaves + if ( iGroup != -1 && Abc_LitIsCompl(iGroup) ) + { + //Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); + iLitNew = Gia_ManAppendCi( pNew ); + goto done; + } + Vec_IntForEachEntry( vArray, Fanin, k ) { iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 ); @@ -405,17 +414,13 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) else iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 ); } - else if ( Abc_LitIsCompl(iGroup) ) // internal CI - { - //Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); - iLitNew = Gia_ManAppendCi( pNew ); - } else // internal CO { assert( pTruth[0] == uTruthVar || pTruth[0] == ~uTruthVar ); iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar) ); //printf("Group = %d. po = %d\n", iGroup>>1, iMfsId ); } +done: Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); } Vec_IntFree( vCover ); diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 53f9a71ef..2e1681991 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -142,18 +142,19 @@ void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * v return; if ( Vec_IntEntry(vGroupMap, iNode) >= 0 ) { - int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) ); - Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); - Vec_IntForEachEntry( vGroup, iNode, i ) - assert( Sfm_ObjIsNode(p, iNode) ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Sfm_ObjSetTravIdCurrent( p, iNode ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Sfm_ObjForEachFanin( p, iNode, iFanin, k ) - Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Vec_IntPush( vNodes, iNode ); - Vec_IntPush( vBoxesLeft, iGroup ); + int iGroup = Abc_Lit2Var(Vec_IntEntry(vGroupMap, iNode)); + Vec_Int_t * vGroup = Vec_WecEntry(vGroups, iGroup); + assert(Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iNode))); + Vec_IntPush(vBoxesLeft, iGroup); + Vec_IntForEachEntry(vGroup, iNode, i) + { + // ignore inputs + if ( !Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iNode))) + continue; + assert(Sfm_ObjIsNode(p, iNode)); + Sfm_ObjSetTravIdCurrent(p, iNode); + Vec_IntPush(vNodes, iNode); + } } else { @@ -170,14 +171,33 @@ Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMa Vec_IntClear( vBoxesLeft ); vNodes = Vec_IntAlloc( p->nObjs ); Sfm_NtkIncrementTravId( p ); - if ( fAllBoxes ) - { - Vec_Int_t * vGroup; - Vec_WecForEachLevel( vGroups, vGroup, i ) - Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); + + assert(!fAllBoxes); // TODO + + Sfm_NtkForEachPo( p, i ) { + int iFanin = Sfm_ObjFanin(p, i, 0); + // detect fake PO modeling blackbox input + if (Vec_IntEntry(vGroupMap, iFanin) >= 0 && !Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iFanin))) + continue; + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); } - Sfm_NtkForEachPo( p, i ) - Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); + + for (i = 0; i < Vec_IntSize( vBoxesLeft ); i++) + { + int k, j, iNode, iFanin; + int iGroup = Vec_IntEntry( vBoxesLeft, i ); + Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); + Vec_IntForEachEntry( vGroup, iNode, k ) + { + // ignore outputs + if ( Abc_LitIsCompl( Vec_IntEntry(vGroupMap, iNode)) ) + continue; + Sfm_ObjForEachFanin( p, iNode, iFanin, j ) + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); + Vec_IntPush( vNodes, iNode ); + } + } + return vNodes; } 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 3/4] &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 ); From 1107634fa60253eb359f71f0a80dc32d6ba60459 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 22 Mar 2024 22:47:40 +0100 Subject: [PATCH 4/4] &mfs: Make it no biggie when a network is all blackboxes, no whiteboxes --- src/aig/gia/giaMfs.c | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index 91241aaff..654e53f30 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -153,12 +153,16 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) // skip POs due to box inputs Counter += nBbIns; assert( Counter == nMfsVars ); + // add functions of the boxes if ( p->pAigExtra ) { - int iBbIn = 0, iBbOut = 0; assert( Gia_ManCiNum(p->pAigExtra) < 16 ); Gia_ObjComputeTruthTableStart( p->pAigExtra, Gia_ManCiNum(p->pAigExtra) ); + } + + { + int iBbIn = 0, iBbOut = 0; curCi = nRealPis; curCo = 0; for ( k = 0; k < nBoxes; k++ ) @@ -168,6 +172,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) // iterate through box outputs if ( !Tim_ManBoxIsBlack(pManTime, k) ) //&& Tim_ManBoxInputNum(pManTime, k) <= 6 ) { + assert(p->pAigExtra); // collect truth table leaves Vec_IntClear( vLeaves ); for ( i = 0; i < nBoxIns; i++ ) @@ -267,14 +272,18 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) curCi += nBoxOuts; } curCo += nRealPos; - Gia_ObjComputeTruthTableStop( p->pAigExtra ); // verify counts assert( curCi == Gia_ManCiNum(p) ); assert( curCo == Gia_ManCoNum(p) ); - assert( curCi - nRealPis == Gia_ManCoNum(p->pAigExtra) ); assert( iBbIn == nBbIns ); assert( iBbOut == nBbOuts ); } + + if (p->pAigExtra) { + Gia_ObjComputeTruthTableStop( p->pAigExtra ); + assert( curCi - nRealPis == Gia_ManCoNum(p->pAigExtra) ); + } + // finalize Vec_IntFree( vLeaves ); return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vDenied, vTruths, vStarts, vTruths2 ); @@ -512,11 +521,6 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) int nFaninMax, nNodes; assert( Gia_ManRegNum(p) == 0 ); assert( p->vMapping != NULL ); - if ( p->pManTime != NULL && p->pAigExtra == NULL ) - { - Abc_Print( 1, "Timing manager is given but there is no GIA of boxes.\n" ); - return NULL; - } if ( p->pManTime != NULL && p->pAigExtra != NULL && Gia_ManCiNum(p->pAigExtra) > 15 ) { Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing white-boxes with more than 15 inputs.\n" );