luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Deleting unused files.

This commit is contained in:
Alan Mishchenko 2024-12-23 17:03:29 -08:00
parent b81df1744f
commit cc894c5905
2 changed files with 0 additions and 961 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

394
src/opt/mfs/mfsCore_.c
View File

@ -1,394 +0,0 @@
/**CFile****************************************************************
FileName [mfsCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Core procedures of this package.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
{
memset( pPars, 0, sizeof(Mfs_Par_t) );
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
pPars->nWinSizeMax = 300;
pPars->nGrowthLevel = 0;
pPars->nBTLimit = 5000;
pPars->fResub = 1;
pPars->fArea = 0;
pPars->fMoreEffort = 0;
pPars->fSwapEdge = 0;
pPars->fOneHotness = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
clock_t clk;
p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
// compute window roots, window support, and window nodes
clk = clock();
p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->timeWin += clock() - clk;
if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
return 1;
// compute the divisors of the window
clk = clock();
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
p->timeDiv += clock() - clk;
// construct AIG for the window
clk = clock();
p->pAigWin = Abc_NtkConstructAig( p, pNode );
p->timeAig += clock() - clk;
// translate it into CNF
clk = clock();
p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
if ( p->pSat == NULL )
{
p->nNodesBad++;
return 1;
}
// solve the SAT problem
if ( p->pPars->fPower )
Abc_NtkMfsEdgePower( p, pNode );
else if ( p->pPars->fSwapEdge )
Abc_NtkMfsEdgeSwapEval( p, pNode );
else
{
Abc_NtkMfsResubNode( p, pNode );
if ( p->pPars->fMoreEffort )
Abc_NtkMfsResubNode2( p, pNode );
}
p->timeSat += clock() - clk;
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Hop_Obj_t * pObj;
int RetValue;
float dProb;
extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb );
int nGain;
clock_t clk;
p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
// compute window roots, window support, and window nodes
clk = clock();
p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->timeWin += clock() - clk;
// count the number of patterns
// p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode );
// construct AIG for the window
clk = clock();
p->pAigWin = Abc_NtkConstructAig( p, pNode );
p->timeAig += clock() - clk;
// translate it into CNF
clk = clock();
p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) );
p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
if ( p->pSat && p->pPars->fOneHotness )
Abc_NtkAddOneHotness( p );
if ( p->pSat == NULL )
return 0;
// solve the SAT problem
RetValue = Abc_NtkMfsSolveSat( p, pNode );
p->nTotConfLevel += p->pSat->stats.conflicts;
p->timeSat += clock() - clk;
if ( RetValue == 0 )
{
p->nTimeOutsLevel++;
p->nTimeOuts++;
return 0;
}
// minimize the local function of the node using bi-decomposition
assert( p->nFanins == Abc_ObjFaninNum(pNode) );
dProb = p->pPars->fPower? ((float *)p->vProbs->pArray)[pNode->Id] : -1.0;
pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare, dProb );
nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj);
if ( nGain >= 0 )
{
p->nNodesDec++;
p->nNodesGained += nGain;
p->nNodesGainedLevel += nGain;
pNode->pData = pObj;
}
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
ProgressBar * pProgress;
Mfs_Man_t * p;
Abc_Obj_t * pObj;
Vec_Vec_t * vLevels;
Vec_Ptr_t * vNodes;
int i, k, nNodes, nFaninMax;
clock_t clk = clock(), clk2;
int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
assert( Abc_NtkIsLogic(pNtk) );
nFaninMax = Abc_NtkGetFaninMax(pNtk);
if ( pPars->fResub )
{
if ( nFaninMax > 8 )
{
printf( "Nodes with more than %d fanins will not be processed.\n", 8 );
nFaninMax = 8;
}
}
else
{
if ( nFaninMax > MFS_FANIN_MAX )
{
printf( "Nodes with more than %d fanins will not be processed.\n", MFS_FANIN_MAX );
nFaninMax = MFS_FANIN_MAX;
}
}
// perform the network sweep
Abc_NtkSweep( pNtk, 0 );
// convert into the AIG
if ( !Abc_NtkToAig(pNtk) )
{
fprintf( stdout, "Converting to AIGs has failed.\n" );
return 0;
}
assert( Abc_NtkHasAig(pNtk) );
// start the manager
p = Mfs_ManAlloc( pPars );
p->pNtk = pNtk;
p->nFaninMax = nFaninMax;
// precomputer power-aware metrics
if ( pPars->fPower )
{
extern Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne );
if ( pPars->fResub )
p->vProbs = Abc_NtkPowerEstimate( pNtk, 0 );
else
p->vProbs = Abc_NtkPowerEstimate( pNtk, 1 );
printf( "Total switching before = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
}
if ( pNtk->pExcare )
{
Abc_Ntk_t * pTemp;
if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n",
Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) );
else
{
pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
p->pCare = Abc_NtkToDar( pTemp, 0, 0 );
Abc_NtkDelete( pTemp );
p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
}
}
if ( p->pCare != NULL )
printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
// prepare the BDC manager
if ( !pPars->fResub )
{
pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
pDecPars->fVerbose = pPars->fVerbose;
p->vTruth = Vec_IntAlloc( 0 );
p->pManDec = Bdc_ManAlloc( pDecPars );
}
// label the register outputs
if ( p->pCare )
{
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pData = (void *)(PORT_PTRUINT_T)i;
}
// compute levels
Abc_NtkLevel( pNtk );
Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// compute don't-cares for each node
nNodes = 0;
p->nTotalNodesBeg = nTotalNodesBeg;
p->nTotalEdgesBeg = nTotalEdgesBeg;
if ( pPars->fResub )
{
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
continue;
if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
continue;
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else
Abc_NtkMfsNode( p, pObj );
}
Extra_ProgressBarStop( pProgress );
}
else
{
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
vLevels = Abc_NtkLevelize( pNtk );
Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
{
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
p->nNodesGainedLevel = 0;
p->nTotConfLevel = 0;
p->nTimeOutsLevel = 0;
clk2 = clock();
Vec_PtrForEachEntry( vNodes, pObj, i )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
break;
if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
continue;
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else
Abc_NtkMfsNode( p, pObj );
}
nNodes += Vec_PtrSize(vNodes);
if ( pPars->fVerbose )
{
printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %% ",
k, Vec_PtrSize(vNodes),
1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
PRT( "Time", clock() - clk2 );
}
}
Extra_ProgressBarStop( pProgress );
Vec_VecFree( vLevels );
}
Abc_NtkStopReverseLevels( pNtk );
// perform the sweeping
if ( !pPars->fResub )
{
extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
// Abc_NtkSweep( pNtk, 0 );
// Abc_NtkBidecResyn( pNtk, 0 );
}
p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
// undo labesl
if ( p->pCare )
{
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pData = NULL;
}
if ( pPars->fPower )
printf( "Total switching after = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
// free the manager
p->timeTotal = clock() - clk;
Mfs_ManStop( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

567
src/opt/mfs/mfsResub_.c
View File

@ -1,567 +0,0 @@
/**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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// 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;
clock_t 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, nWords, fBreak;
clock_t clk;
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 ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END