summaryrefslogtreecommitdiffstats
path: root/src/opt/mfs/mfsResub.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/mfs/mfsResub.c')
-rw-r--r--src/opt/mfs/mfsResub.c307
1 files changed, 269 insertions, 38 deletions
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index ae1132f2..1e9da4d2 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -57,6 +57,35 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
/**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.]
@@ -68,7 +97,7 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
***********************************************************************/
int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
{
- unsigned * pData, * pDataTot;
+ unsigned * pData;
int RetValue, iVar, i;
p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
@@ -77,17 +106,16 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
return 1;
p->nSatCexes++;
// store the counter-example
- pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
- assert( pData[0] == 0 );
Vec_IntForEachEntry( p->vProjVars, iVar, i )
{
- if ( sat_solver_var_value( p->pSat, iVar ) )
- Aig_InfoSetBit( pData, 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 );
+ }
}
- // AND the result with the previous ones
- pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
- for ( i = 0; i < p->nDivWords; i++ )
- pDataTot[i] &= pData[i];
+ p->nCexes++;
return 0;
}
@@ -102,22 +130,19 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
SeeAlso []
***********************************************************************/
-int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
+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 iVar, i, nCands, clk;
+ int iVar, i, nCands, nWords, w, clk;
Abc_Obj_t * pFanin;
Hop_Obj_t * pFunc;
assert( iFanin >= 0 );
// clean simulation info
- Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords );
- pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
- memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
+ Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
p->nCexes = 0;
-
if ( fVeryVerbose )
{
printf( "\n" );
@@ -143,7 +168,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
p->nNodesResub++;
-// p->nNodesGained += Abc_NodeMffcLabel(pNode);
+ if ( fSkipUpdate )
+ return 1;
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
@@ -156,11 +182,6 @@ p->timeInt += clock() - clk;
if ( fOnlyRemove )
return 0;
- // shift variables by 1
- for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
- p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
- p->vFanins->nSize++;
-
if ( fVeryVerbose )
{
for ( i = 0; i < 8; i++ )
@@ -180,37 +201,52 @@ p->timeInt += clock() - clk;
if ( fVeryVerbose )
{
printf( "%3d: %2d ", p->nCexes, iVar );
- pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
-// Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
- printf( "%d", Aig_InfoHasBit(pData, i) );
+ {
+ pData = Vec_PtrEntry( p->vDivCexes, i );
+ printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+ }
printf( "\n" );
}
// find the next divisor to try
- pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+ nWords = Aig_BitWordNum(p->nCexes);
+ assert( nWords <= p->nDivWords );
for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
- if ( Aig_InfoHasBit( pData, iVar ) )
+ {
+ 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 );
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
p->nNodesResub++;
-// p->nNodesGained += Abc_NodeMffcLabel(pNode);
+ if ( fSkipUpdate )
+ return 1;
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
- // update the network
-// Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+ // shift fanins by 1
+ for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+ p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+ p->vFanins->nSize++;
Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
+ // update the network
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
p->timeInt += clock() - clk;
return 1;
}
+ if ( p->nCexes >= p->pPars->nDivMax )
+ break;
}
return 0;
}
@@ -226,16 +262,155 @@ p->timeInt += clock() - clk;
SeeAlso []
***********************************************************************/
-int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
+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 iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
Abc_Obj_t * pFanin;
- int i;
+ 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 ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+ {
+ 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 );
+ }
+ if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+ {
+ if ( fVeryVerbose )
+ printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
+ p->nNodesResub++;
+clk = clock();
+ // derive the function
+ pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+ // 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 )
{
- if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
- return 1;
+ 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 );
+ if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) )
+ {
+ if ( fVeryVerbose )
+ printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
+ p->nNodesResub++;
+clk = clock();
+ // derive the function
+ pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
+ // shift fanins by 1
+ for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+ p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+ p->vFanins->nSize++;
+ // shift fanins by 1
+ for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+ p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+ p->vFanins->nSize++;
+ Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) );
+ Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) );
+ // update the network
+ 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;
}
@@ -250,25 +425,81 @@ int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
+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 ) )
+ 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_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
{
- if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:54:35 +0000