summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/cut/cut.h2
-rw-r--r--src/opt/cut/cutNode.c7
-rw-r--r--src/opt/lpk/lpkAbcDsd.c7
-rw-r--r--src/opt/lpk/lpkCore.c4
-rw-r--r--src/opt/mfs/mfs.h1
-rw-r--r--src/opt/mfs/mfsCore.c248
-rw-r--r--src/opt/mfs/mfsCore_.c388
-rw-r--r--src/opt/mfs/mfsInt.h5
-rw-r--r--src/opt/mfs/mfsMan.c25
-rw-r--r--src/opt/mfs/mfsResub.c67
-rw-r--r--src/opt/mfs/mfsResub_.c560
-rw-r--r--src/opt/sim/simSwitch.c2
12 files changed, 1295 insertions, 21 deletions
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index dee05dfc..faa249f2 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -64,8 +64,10 @@ struct Cut_ParamsStruct_t_
int fGlobal; // compute only global cuts
int fLocal; // compute only local cuts
int fRecord; // record the cut computation flow
+ int fRecordAig; // record the cut functions
int fFancy; // perform fancy computations
int fMap; // computes delay of FPGA mapping with cuts
+ int fAdjust; // removed useless fanouts of XORs/MUXes
int fVerbose; // the verbosiness flag
};
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 2d17020b..633219fd 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -393,6 +393,13 @@ p->timeMerge += clock() - clk;
Vec_IntPush( p->vCutPairs, ((pCut->Num1 << 16) | pCut->Num0) );
Vec_IntWriteEntry( p->vNodeCuts, Node, Vec_IntSize(p->vCutPairs) - Vec_IntEntry(p->vNodeStarts, Node) );
}
+ if ( p->pParams->fRecordAig )
+ {
+ extern void Aig_RManRecord( unsigned * pTruth, int nVarsInit );
+ Cut_ListForEachCut( pList, pCut )
+ if ( Cut_CutReadLeaveNum(pCut) > 4 )
+ Aig_RManRecord( Cut_CutReadTruth(pCut), Cut_CutReadLeaveNum(pCut) );
+ }
// check if the node is over the list
if ( p->nNodeCuts == p->pParams->nKeepMax )
p->nCutsLimit++;
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
index 46d9179a..a1cd9def 100644
--- a/src/opt/lpk/lpkAbcDsd.c
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -287,7 +287,12 @@ void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth,
if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving
continue;
if ( fVerbose )
-Lpk_PrintSetOne( uBoundSet );
+{
+Lpk_PrintSetOne( uBoundSet & 0xFFFF );
+//printf( "\n" );
+//Lpk_PrintSetOne( uBoundSet >> 16 );
+//printf( "\n" );
+}
assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
if ( nVarsBS == 1 )
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 78356d81..d8dd15b7 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -387,6 +387,10 @@ p->timeCuts += clock() - clk;
p->nCutsUseful += p->nEvals;
for ( i = 0; i < p->nEvals; i++ )
{
+ if ( p->pObj->Id == 1478 )
+ {
+ int x = 0;
+ }
// get the cut
pCut = p->pCuts + p->pEvals[i];
if ( p->pPars->fFirst && i == 1 )
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 9550a31b..bddb9328 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -54,6 +54,7 @@ struct Mfs_Par_t_
int fSwapEdge; // performs edge swapping
int fOneHotness; // adds one-hotness conditions
int fDelay; // performs optimization for delay
+ int fPower; // performs power-aware optimization
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 3444bab1..e8820acd 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -9,7 +9,7 @@
Synopsis [Core procedures of this package.]
Author [Alan Mishchenko]
-
+
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
@@ -24,6 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+extern int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -33,7 +35,7 @@
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -57,13 +59,176 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
}
+/*
+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;
+ } else if ( pProbab[pFanin->Id] >= 0.3 )
+ {
+ if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+ return 1;
+ }
+ }
+ return 0;
+}
+*/
+
+int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
+{
+// int clk;
+// Abc_Obj_t * pFanin;
+ float * pProbab = (float *)p->vProbs->pArray;
+// int i;
+
+ p->nNodesTried++;
+ // prepare data structure for this node
+ Mfs_ManClean( p );
+ // compute window roots, window support, and window nodes
+ 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) );
+ if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+ return 1;
+ // compute the divisors of the window
+ p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+ p->nTotalDivs += Vec_PtrSize(p->vDivs);
+ // construct AIG for the window
+ p->pAigWin = Abc_NtkConstructAig( p, pNode );
+ // translate it into CNF
+ p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
+ // create the SAT problem
+ p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
+ if ( p->pSat == NULL )
+ {
+ p->nNodesBad++;
+ return 1;
+ }
+ return 0;
+}
+
+/*
+int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+ int clk;
+ Abc_Obj_t * pFanin;
+ float * pProbab = (float *)p->vProbs->pArray;
+ int i;
+
+ if (Abc_WinNode(p, pNode) // something wrong
+ return 1;
+
+ // solve the SAT problem
+ // Abc_NtkMfsEdgePower( p, pNode );
+ // try replacing area critical fanins
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+ return 1;
+
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( pProbab[pFanin->Id] >= 0.1 && 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 ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
+ return 1;
+ }
+ return 0;
+
+ return 1;
+}
+*/
+
+Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
+{
+ int i, k;
+ Abc_Obj_t *pFanin, *pNode;
+ Abc_Ntk_t *pNtk = p->pNtk;
+ int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
+ float * pProbab = (float *)p->vProbs->pArray;
+
+ Abc_NtkForEachNode( pNtk, pNode, k )
+ {
+ if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
+ continue;
+ if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
+ continue;
+ if (Abc_WinNode(p, pNode) ) // something wrong
+ continue;
+
+ // solve the SAT problem
+ // Abc_NtkMfsEdgePower( p, pNode );
+ // try replacing area critical fanins
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( pProbab[pFanin->Id] >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+ continue;
+ }
+
+ Abc_NtkForEachNode( pNtk, pNode, k )
+ {
+ if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
+ continue;
+ if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
+ continue;
+ if (Abc_WinNode(p, pNode) ) // something wrong
+ continue;
+
+ // solve the SAT problem
+ // Abc_NtkMfsEdgePower( p, pNode );
+ // try replacing area critical fanins
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( pProbab[pFanin->Id] >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+ continue;
+ }
+
+ Abc_NtkForEachNode( pNtk, pNode, k )
+ {
+ if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
+ continue;
+ if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
+ continue;
+ if (Abc_WinNode(p, pNode) ) // something wrong
+ continue;
+
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( pProbab[pFanin->Id] >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+ continue;
+ }
+/*
+ Abc_NtkForEachNode( pNtk, pNode, k )
+ {
+ if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
+ continue;
+ if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax - 2)
+ continue;
+ if (Abc_WinNode(p, pNode) ) // something wrong
+ continue;
+
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
+ continue;
+ }
+*/
+}
/**Function*************************************************************
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -74,7 +239,7 @@ int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
int clk;
p->nNodesTried++;
// prepare data structure for this node
- Mfs_ManClean( p );
+ Mfs_ManClean( p );
// compute window roots, window support, and window nodes
clk = clock();
p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
@@ -105,7 +270,9 @@ clk = clock();
return 1;
}
// solve the SAT problem
- if ( p->pPars->fSwapEdge )
+ if ( p->pPars->fPower )
+ Abc_NtkMfsEdgePower( p, pNode );
+ else if ( p->pPars->fSwapEdge )
Abc_NtkMfsEdgeSwapEval( p, pNode );
else
{
@@ -122,7 +289,7 @@ p->timeSat += clock() - clk;
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -132,7 +299,8 @@ int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Hop_Obj_t * pObj;
int RetValue;
- 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;
+ 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, clk;
p->nNodesTried++;
@@ -173,14 +341,15 @@ p->timeSat += clock() - clk;
}
// minimize the local function of the node using bi-decomposition
assert( p->nFanins == Abc_ObjFaninNum(pNode) );
- pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
+ 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;
+ pNode->pData = pObj;
}
return 1;
}
@@ -190,7 +359,7 @@ p->timeSat += clock() - clk;
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -198,7 +367,7 @@ p->timeSat += clock() - clk;
***********************************************************************/
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
ProgressBar * pProgress;
@@ -242,16 +411,32 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
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 );
+#if 0
+ printf( "Total switching before = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
+#else
+ p->TotalSwitchingBeg = Abc_NtkMfsTotalSwitching(pNtk);
+#endif
+ }
+
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",
+ 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 );
+ p->pCare = Abc_NtkToDar( pTemp, 0, 0 );
Abc_NtkDelete( pTemp );
p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
}
@@ -273,7 +458,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pData = (void *)(PORT_PTRUINT_T)i;
}
-
+
// compute levels
Abc_NtkLevel( pNtk );
Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
@@ -284,6 +469,14 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
p->nTotalEdgesBeg = nTotalEdgesBeg;
if ( pPars->fResub )
{
+#if 0
+ printf( "TotalSwitching (%7.2f --> ", Abc_NtkMfsTotalSwitching(pNtk) );
+#endif
+ if (pPars->fPower)
+ {
+ Abc_NtkMfsPowerResub( p, pPars);
+ } else
+ {
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
{
@@ -299,9 +492,15 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
Abc_NtkMfsNode( p, pObj );
}
Extra_ProgressBarStop( pProgress );
+#if 0
+ printf( " %7.2f )\n", Abc_NtkMfsTotalSwitching(pNtk) );
+#endif
}
- else
+ } else
{
+#if 0
+ printf( "Total switching before = %7.2f, ----> ", Abc_NtkMfsTotalSwitching(pNtk) );
+#endif
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
vLevels = Abc_NtkLevelize( pNtk );
Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
@@ -320,22 +519,27 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
continue;
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
- else
+ 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 %% ",
+ /*
+ 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 );
+#if 0
+ printf( " %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
+#endif
}
Abc_NtkStopReverseLevels( pNtk );
@@ -357,6 +561,16 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
pObj->pData = NULL;
}
+ if ( pPars->fPower )
+ {
+#if 1
+ p->TotalSwitchingEnd = Abc_NtkMfsTotalSwitching(pNtk);
+// printf( "Total switching after = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
+#else
+ printf( "Total switching after = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
+#endif
+ }
+
// free the manager
p->timeTotal = clock() - clk;
Mfs_ManStop( p );
diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c
new file mode 100644
index 00000000..66b497f6
--- /dev/null
+++ b/src/opt/mfs/mfsCore_.c
@@ -0,0 +1,388 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// 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->nDivMax = 250;
+ 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 )
+{
+ int 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);
+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, 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, 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 node be processed.\n", 8 );
+ nFaninMax = 8;
+ }
+ }
+ else
+ {
+ if ( nFaninMax > MFS_FANIN_MAX )
+ {
+ printf( "Nodes with more than %d fanins will node 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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index df8a4848..9eb6e4a4 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -81,6 +81,8 @@ struct Mfs_Man_t_
Vec_Ptr_t * vFanins; // the new set of fanins
int nTotConfLim; // total conflict limit
int nTotConfLevel; // total conflicts on this level
+ // switching activity
+ Vec_Int_t * vProbs;
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
@@ -102,6 +104,8 @@ struct Mfs_Man_t_
int nTotalNodesEnd;
int nTotalEdgesBeg;
int nTotalEdgesEnd;
+ float TotalSwitchingBeg;
+ float TotalSwitchingEnd;
// statistics
int timeWin;
int timeDiv;
@@ -137,6 +141,7 @@ extern void Mfs_ManClean( Mfs_Man_t * p );
/*=== mfsResub.c ==========================================================*/
extern void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p );
extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index d0642368..9a043ed8 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -108,6 +108,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
{
if ( p->pPars->fResub )
{
+/*
printf( "Reduction in nodes = %5d. (%.2f %%) ",
p->nTotalNodesBeg-p->nTotalNodesEnd,
100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
@@ -123,6 +124,28 @@ void Mfs_ManPrint( Mfs_Man_t * p )
else
Abc_NtkMfsPrintResubStats( p );
// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
+*/
+ printf( "@@@------- Node( %4d, %4.2f%% ), ",
+ p->nTotalNodesBeg-p->nTotalNodesEnd,
+ 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
+ printf( "Edge( %4d, %4.2f%% ), ",
+ p->nTotalEdgesBeg-p->nTotalEdgesEnd,
+ 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+ if (p->pPars->fPower)
+ printf( "Power( %5.2f, %4.2f%%) ",
+ p->TotalSwitchingBeg - p->TotalSwitchingEnd,
+ 100.0*(p->TotalSwitchingBeg-p->TotalSwitchingEnd)/p->TotalSwitchingBeg );
+ printf( "\n" );
+#if 0
+ printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
+ Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
+#endif
+ if ( p->pPars->fSwapEdge )
+ printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n",
+ p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
+ else
+ Abc_NtkMfsPrintResubStats( p );
+// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
}
else
{
@@ -168,6 +191,8 @@ void Mfs_ManStop( Mfs_Man_t * p )
Aig_ManStop( p->pCare );
if ( p->vSuppsInv )
Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv );
+ if ( p->vProbs )
+ Vec_IntFree( p->vProbs );
Mfs_ManClean( p );
Int_ManFree( p->pMan );
Vec_IntFree( p->vMem );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index b6c7299b..e9ea2c40 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -80,8 +80,8 @@ void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p )
nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
}
}
- printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n",
- nAreaCrits, nAreaExpanse );
+// printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n",
+// nAreaCrits, nAreaExpanse );
}
/**Function*************************************************************
@@ -209,6 +209,8 @@ p->timeInt += clock() - clk;
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 );
@@ -225,6 +227,13 @@ p->timeInt += clock() - clk;
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.15 )
+ continue;
+ }
pData = Vec_PtrEntry( p->vDivCexes, iVar );
for ( w = 0; w < nWords; w++ )
if ( pData[w] != ~0 )
@@ -345,6 +354,10 @@ p->timeInt += clock() - clk;
iVar = iVar2 = -1;
while ( 1 )
{
+#if 1 // sjang
+ float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL);
+ assert( (pProbab != NULL) == p->pPars->fPower );
+#endif
if ( fVeryVerbose )
{
printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
@@ -363,9 +376,27 @@ p->timeInt += clock() - clk;
for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
{
pData = Vec_PtrEntry( p->vDivCexes, iVar );
+#if 1 // sjang
+ 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.12 )
+ continue;
+ }
+#endif
for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
{
pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 );
+#if 1 // sjang
+ if ( p->pPars->fPower )
+ {
+ Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar2);
+ // only accept the divisor if it is "cool"
+ if ( pProbab[Abc_ObjId(pDiv)] >= 0.12 )
+ continue;
+ }
+#endif
for ( w = 0; w < nWords; w++ )
if ( (pData[w] | pData2[w]) != ~0 )
break;
@@ -434,6 +465,38 @@ int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
/**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.35 )
+ {
+ if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+ return 1;
+ } else if ( pProbab[pFanin->Id] >= 0.25 ) // sjang
+ {
+ if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+ return 1;
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs resubstitution for the node.]
Description []
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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
index 218d4d59..baabc320 100644
--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@@ -97,7 +97,7 @@ float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords )
int nOnes, nTotal;
nTotal = 32 * nSimWords;
nOnes = Sim_UtilCountOnes( pSimInfo, nSimWords );
- return (float)2.0 * nOnes * (nTotal - nOnes) / nTotal / nTotal;
+ return (float)2.0 * nOnes / nTotal * (nTotal - nOnes) / nTotal;
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 06:52:26 +0000