diff options
Diffstat (limited to 'src/opt/mfs/mfsResub_.c')
| -rw-r--r-- | src/opt/mfs/mfsResub_.c | 560 |
1 files changed, 560 insertions, 0 deletions
diff --git a/src/opt/mfs/mfsResub_.c b/src/opt/mfs/mfsResub_.c new file mode 100644 index 00000000..47600b30 --- /dev/null +++ b/src/opt/mfs/mfsResub_.c @@ -0,0 +1,560 @@ +/**CFile**************************************************************** + + FileName [mfsResub.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures to perform resubstitution.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Updates the network after resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc ) +{ + Abc_Obj_t * pObjNew, * pFanin; + int k; + // create the new node + pObjNew = Abc_NtkCreateNode( pObj->pNtk ); + pObjNew->pData = pFunc; + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Abc_ObjAddFanin( pObjNew, pFanin ); + // replace the old node by the new node +//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj ); +//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew ); + // update the level of the node + Abc_NtkUpdate( pObj, pObjNew, p->vLevels ); +} + +/**Function************************************************************* + + Synopsis [Prints resub candidate stats.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p ) +{ + Abc_Obj_t * pFanin, * pNode; + int i, k, nAreaCrits = 0, nAreaExpanse = 0; + int nFaninMax = Abc_NtkGetFaninMax(p->pNtk); + Abc_NtkForEachNode( p->pNtk, pNode, i ) + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + nAreaCrits++; + nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax); + } + } + printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", + nAreaCrits, nAreaExpanse ); +} + +/**Function************************************************************* + + Synopsis [Tries resubstitution.] + + Description [Returns 1 if it is feasible, or 0 if c-ex is found.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) +{ + unsigned * pData; + int RetValue, iVar, i; + p->nSatCalls++; + RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +// assert( RetValue == l_False || RetValue == l_True ); + if ( RetValue == l_False ) + return 1; + if ( RetValue != l_True ) + { + p->nTimeOuts++; + return -1; + } + p->nSatCexes++; + // store the counter-example + Vec_IntForEachEntry( p->vProjVars, iVar, i ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! + { + assert( Aig_InfoHasBit(pData, p->nCexes) ); + Aig_InfoXorBit( pData, p->nCexes ); + } + } + p->nCexes++; + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate ) +{ + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData; + int pCands[MFS_FANIN_MAX]; + int RetValue, iVar, i, nCands, nWords, w, clk; + Abc_Obj_t * pFanin; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + + // clean simulation info + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); + p->nCexes = 0; + if ( fVeryVerbose ) + { + printf( "\n" ); + printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), + iFanin, Abc_ObjFaninNum(pNode), + Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( i == iFanin ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); + p->nNodesResub++; + p->nNodesGainedLevel++; + if ( fSkipUpdate ) + return 1; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + if ( pFunc == NULL ) + return 0; + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fOnlyRemove ) + return 0; + + if ( fVeryVerbose ) + { + for ( i = 0; i < 8; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ ) + if ( i == iFanin ) + printf( "*" ); + else + printf( "%c", 'a' + i ); + printf( "\n" ); + } + iVar = -1; + while ( 1 ) + { + float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL); + assert( (pProbab != NULL) == p->pPars->fPower ); + if ( fVeryVerbose ) + { + printf( "%3d: %2d ", p->nCexes, iVar ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } + printf( "\n" ); + } + + // find the next divisor to try + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); + for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) + { + if ( p->pPars->fPower ) + { + Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar); + // only accept the divisor if it is "cool" + if ( pProbab[Abc_ObjId(pDiv)] >= 0.2 ) + continue; + } + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( w = 0; w < nWords; w++ ) + if ( pData[w] != ~0 ) + break; + if ( w == nWords ) + break; + } + if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) + return 0; + + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); + p->nNodesResub++; + p->nNodesGainedLevel++; + if ( fSkipUpdate ) + return 1; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 ); + if ( pFunc == NULL ) + return 0; + // update the network + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + if ( p->nCexes >= p->pPars->nDivMax ) + break; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 ) +{ + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData, * pData2; + int pCands[MFS_FANIN_MAX]; + int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak; + Abc_Obj_t * pFanin; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + assert( iFanin2 >= 0 || iFanin2 == -1 ); + + // clean simulation info + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); + p->nCexes = 0; + if ( fVeryVerbose ) + { + printf( "\n" ); + printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), + iFanin, iFanin2, Abc_ObjFaninNum(pNode), + Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( i == iFanin || i == iFanin2 ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 ); + p->nNodesResub++; + p->nNodesGainedLevel++; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + if ( pFunc == NULL ) + return 0; + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fVeryVerbose ) + { + for ( i = 0; i < 11; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ ) + if ( i == iFanin || i == iFanin2 ) + printf( "*" ); + else + printf( "%c", 'a' + i ); + printf( "\n" ); + } + iVar = iVar2 = -1; + while ( 1 ) + { + if ( fVeryVerbose ) + { + printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } + printf( "\n" ); + } + + // find the next divisor to try + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); + fBreak = 0; + for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( iVar2 = 0; iVar2 < iVar; iVar2++ ) + { + pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 ); + for ( w = 0; w < nWords; w++ ) + if ( (pData[w] | pData2[w]) != ~0 ) + break; + if ( w == nWords ) + { + fBreak = 1; + break; + } + } + if ( fBreak ) + break; + } + if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) + return 0; + + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 ); + p->nNodesResub++; + p->nNodesGainedLevel++; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 ); + if ( pFunc == NULL ) + return 0; + // update the network + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) ); + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + assert( Vec_PtrSize(p->vFanins) == nCands + 2 ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + if ( p->nCexes >= p->pPars->nDivMax ) + break; + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Evaluates the possibility of replacing given edge by another edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i; + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Evaluates the possibility of replacing given edge by another edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + float * pProbab = (float *)p->vProbs->pArray; + int i; + // try replacing area critical fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( pProbab[pFanin->Id] >= 0.4 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i; + // try replacing area critical fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } + // try removing redundant edges + if ( !p->pPars->fArea ) + { + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) + return 1; + } + } + if ( Abc_ObjFaninNum(pNode) == p->nFaninMax ) + return 0; + // try replacing area critical fanins while adding two new fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin, * pFanin2; + int i, k; +/* + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } +*/ + if ( Abc_ObjFaninNum(pNode) < 2 ) + return 0; + // try replacing one area critical fanin and one other fanin while adding two new fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + // consider second fanin to remove at the same time + Abc_ObjForEachFanin( pNode, pFanin2, k ) + { + if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) ) + return 1; + } + } + } + return 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |