From 9268c100237e67b404c6528bf435d1f60f185329 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 May 2013 00:45:22 -0700 Subject: New MFS package. --- src/base/abci/abcMfs.c | 34 ++++++++++++++++++++++++---------- src/opt/mfs/mfsCore.c | 4 ++-- src/opt/mfs/mfsCore_.c | 2 +- src/opt/sfm/sfm.h | 1 + src/opt/sfm/sfmCnf.c | 4 ++-- src/opt/sfm/sfmCore.c | 21 +++++++++++++-------- src/opt/sfm/sfmNtk.c | 8 ++++++++ src/opt/sfm/sfmSat.c | 10 ++++++++-- src/opt/sfm/sfmWin.c | 21 ++++++++------------- 9 files changed, 67 insertions(+), 38 deletions(-) diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index 5259ea03..9c0513de 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -53,7 +53,11 @@ Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk ) Abc_NtkForEachPi( pNtk, pObj, i ) pObj->iTemp = i; Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + { pObj->iTemp = Abc_NtkPiNum(pNtk) + i; +//printf( "%d->%d ", pObj->Id, pObj->iTemp ); + } +//printf( "\n" ); Abc_NtkForEachPo( pNtk, pObj, i ) pObj->iTemp = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + i; return vNodes; @@ -119,6 +123,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) Vec_Int_t * vMap, * vArray; Abc_Obj_t * pNode; int i, k, Fanin; + word * pTruth; // map new IDs into old nodes vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); Abc_NtkForEachPi( pNtk, pNode, i ) @@ -131,18 +136,27 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) Abc_ObjRemoveFanins( pNode ); // create new fanins Abc_NtkForEachNode( pNtk, pNode, i ) - if ( pNode->iTemp > 0 && !Sfm_NodeReadFixed(p, pNode->iTemp) ) + { + if ( pNode->iTemp == 0 || Sfm_NodeReadFixed(p, pNode->iTemp) ) + continue; + if ( !Sfm_NodeReadUsed(p, pNode->iTemp) ) { - vArray = Sfm_NodeReadFanins( p, pNode->iTemp ); - if ( Vec_IntSize(vArray) == 0 ) - { - Abc_NtkDeleteObj( pNode ); - continue; - } - Vec_IntForEachEntry( vArray, Fanin, k ) - Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) ); - pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)Sfm_NodeReadTruth(p, pNode->iTemp) ); + Abc_NtkDeleteObj( pNode ); + continue; } + // update fanins + vArray = Sfm_NodeReadFanins( p, pNode->iTemp ); + Vec_IntForEachEntry( vArray, Fanin, k ) + Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) ); + // update function + pTruth = Sfm_NodeReadTruth( p, pNode->iTemp ); + if ( pTruth[0] == 0 ) + pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" ); + else if ( ~pTruth[0] == 0 ) + pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" ); + else + pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth ); + } Vec_IntFree( vMap ); } diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index fe7a1852..9e50333f 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -101,7 +101,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode) return 1; // compute the divisors of the window p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); - p->nTotalDivs += Vec_PtrSize(p->vDivs); + p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode); // construct AIG for the window p->pAigWin = Abc_NtkConstructAig( p, pNode ); // translate it into CNF @@ -250,7 +250,7 @@ p->timeWin += clock() - clk; // compute the divisors of the window clk = clock(); p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); - p->nTotalDivs += Vec_PtrSize(p->vDivs); + p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode); p->timeDiv += clock() - clk; // construct AIG for the window clk = clock(); diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c index ceee04cf..49105da6 100644 --- a/src/opt/mfs/mfsCore_.c +++ b/src/opt/mfs/mfsCore_.c @@ -89,7 +89,7 @@ p->timeWin += clock() - clk; // compute the divisors of the window clk = clock(); p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); - p->nTotalDivs += Vec_PtrSize(p->vDivs); + p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode); p->timeDiv += clock() - clk; // construct AIG for the window clk = clock(); diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index b67fc8df..f6380e65 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -73,6 +73,7 @@ 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 ); extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ); +extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i ); /*=== sfmSat.c ==========================================================*/ diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c index 126b6ca0..f04a6970 100644 --- a/src/opt/sfm/sfmCnf.c +++ b/src/opt/sfm/sfmCnf.c @@ -122,12 +122,12 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ) Vec_Wec_t * vCnfs; Vec_Str_t * vCnf, * vCnfBase; word uTruth; - int i; + int i, nCubes; vCnf = Vec_StrAlloc( 100 ); vCnfs = Vec_WecStart( p->nObjs ); Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos ) { - Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); + nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) ); diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 35c092fa..acdee9c1 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -48,8 +48,8 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) pPars->nTfoLevMax = 2; // the maximum fanout levels pPars->nFanoutMax = 10; // the maximum number of fanouts pPars->nDepthMax = 0; // the maximum depth to try - pPars->nDivNumMax = 200; // the maximum number of divisors - pPars->nWinSizeMax = 500; // the maximum window size + pPars->nDivNumMax = 300; // the maximum number of divisors + pPars->nWinSizeMax = 300; // the maximum window size pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run pPars->fFixLevel = 1; // does not allow level to increase pPars->fArea = 0; // performs optimization for area @@ -111,14 +111,18 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) clock_t clk; assert( Sfm_ObjIsNode(p, iNode) ); assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) ); + if ( iNode == 211 ) + { + int i = 0; + } if ( fRemoveOnly ) p->nTryRemoves++; else p->nTryResubs++; // report init stats if ( p->pPars->fVeryVerbose ) - printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n", - iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), + printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin = %d/%d. MFFC = %d\n", + iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 ); // clean simulation info p->nCexes = 0; @@ -187,9 +191,9 @@ finish: if ( p->pPars->fVeryVerbose ) { if ( iVar == -1 ) - printf( "Node %d: Fanin %d can be removed. ", iNode, f ); + printf( "Node %d: Fanin %d (%d) can be removed. ", iNode, f, Sfm_ObjFanin(p, iNode, f) ); else - printf( "Node %d: Fanin %d can be replaced by divisor %d. ", iNode, f, iVar ); + printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d. ", iNode, f, Sfm_ObjFanin(p, iNode, f), iVar ); Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" ); } if ( iVar == -1 ) @@ -205,9 +209,10 @@ finish: int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) { int i, iFanin; - p->nNodesTried++; // prepare SAT solver - Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ); + if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) ) + return 0; + p->nNodesTried++; Sfm_NtkWindowToSolver( p ); Sfm_NtkPrepareDivisors( p, iNode ); // try replacing area critical fanins diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 29463de6..53ec4153 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -243,6 +243,10 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin ) void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode ) { int i, iFanin; + if ( iNode == 202 ) + { + int s = 0; + } if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) ) return; assert( Sfm_ObjIsNode(p, iNode) ); @@ -304,6 +308,10 @@ int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ) { return (int)Vec_StrEntry( p->vFixed, i ); } +int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i ) +{ + return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index f5355503..4a06dde6 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -123,8 +123,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 ); assert( RetValue ); // finalize - sat_solver_compress( pSat0 ); - sat_solver_compress( pSat1 ); + RetValue = sat_solver_simplify( pSat0 ); + assert( RetValue ); + RetValue = sat_solver_simplify( pSat1 ); + if ( RetValue == 0 ) + { + Sat_SolverWriteDimacs( pSat1, "test.cnf", NULL, NULL, 0 ); + } + assert( RetValue ); // return the result if ( p->pSat0 ) sat_solver_delete( p->pSat0 ); if ( p->pSat1 ) sat_solver_delete( p->pSat1 ); diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 893a4592..54cf924d 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -179,7 +179,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode ) SeeAlso [] ***********************************************************************/ -void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode ) +void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax ) { int i, iFanout; Sfm_ObjForEachFanout( p, iNode, iFanout, i ) @@ -187,7 +187,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode ) // skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax || - (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= Sfm_ObjLevel(p, iNode)) ) + (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) ) continue; // handle single-input nodes if ( Sfm_ObjFaninNum(p, iFanout) == 1 ) @@ -235,23 +235,18 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) { int i, iTemp; clock_t clk = clock(); -/* - if ( iNode == 7 ) - { - int iLevel = Sfm_ObjLevel(p, iNode); - int s = 0; - } -*/ assert( Sfm_ObjIsNode( p, iNode ) ); Vec_IntClear( p->vLeaves ); // leaves Vec_IntClear( p->vNodes ); // internal Vec_IntClear( p->vDivs ); // divisors + Vec_IntClear( p->vRoots ); // roots + Vec_IntClear( p->vTfo ); // roots // collect transitive fanin Sfm_NtkIncrementTravId( p ); Sfm_NtkCollectTfi_rec( p, iNode ); + if ( Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) > p->pPars->nWinSizeMax ) + return 0; // collect TFO (currently use only one level of TFO) - Vec_IntClear( p->vRoots ); // roots - Vec_IntClear( p->vTfo ); // roots if ( Sfm_NtkCheckFanouts(p, iNode) ) { Sfm_ObjForEachFanout( p, iNode, iTemp, i ) @@ -271,8 +266,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Vec_IntAppend( p->vDivs, p->vNodes ); Sfm_NtkIncrementTravId2( p ); Vec_IntForEachEntry( p->vDivs, iTemp, i ) - if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) - Sfm_NtkAddDivisors( p, iTemp ); + if ( iTemp != iNode && Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) + Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); p->nTotalDivs += Vec_IntSize(p->vDivs); p->timeDiv += clock() - clk; if ( !fVerbose ) -- cgit v1.2.3