summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abci/abc.c21
-rw-r--r--src/base/abci/abcPrint.c14
-rw-r--r--src/proof/cec/cecSplit.c30
4 files changed, 49 insertions, 18 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 215d66be..62df9450 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -795,7 +795,7 @@ extern ABC_DLL float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf );
extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops );
extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
-extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk, int fUsePis );
extern ABC_DLL void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk, int fMffc );
extern ABC_DLL void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
extern ABC_DLL void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 812e1820..0ce72bd6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1407,17 +1407,17 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
- int fMffc;
- int fVerbose;
-
- // set defaults
- fMffc = 0;
- fVerbose = 0;
+ int fUsePis = 0;
+ int fMffc = 0;
+ int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "imvh" ) ) != EOF )
{
switch ( c )
{
+ case 'i':
+ fUsePis ^= 1;
+ break;
case 'm':
fMffc ^= 1;
break;
@@ -1430,23 +1430,22 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
-
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
-
// print the nodes
if ( fVerbose )
- Abc_NtkPrintFanio( stdout, pNtk );
+ Abc_NtkPrintFanio( stdout, pNtk, fUsePis );
else
Abc_NtkPrintFanioNew( stdout, pNtk, fMffc );
return 0;
usage:
- Abc_Print( -2, "usage: print_fanio [-mvh]\n" );
+ Abc_Print( -2, "usage: print_fanio [-imvh]\n" );
Abc_Print( -2, "\t prints the statistics about fanins/fanouts of all nodes\n" );
+ Abc_Print( -2, "\t-i : toggles considering fanouts of primary inputs only [default = %s]\n", fUsePis? "yes": "no" );
Abc_Print( -2, "\t-m : toggles printing MFFC sizes instead of fanouts [default = %s]\n", fMffc? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose way of printing the stats [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 06e459fe..7358a519 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -524,7 +524,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
+void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk, int fUsePis )
{
Abc_Obj_t * pNode;
int i, k, nFanins, nFanouts;
@@ -558,6 +558,18 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
vFanins->pArray[nFanins]++;
vFanouts->pArray[nFanouts]++;
}
+ if ( fUsePis )
+ {
+ Vec_IntFill( vFanouts, Vec_IntSize(vFanouts), 0 );
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ {
+ if ( Abc_NtkIsNetlist(pNtk) )
+ nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
+ else
+ nFanouts = Abc_ObjFanoutNum(pNode);
+ vFanouts->pArray[nFanouts]++;
+ }
+ }
fprintf( pFile, "The distribution of fanins and fanouts in the network:\n" );
fprintf( pFile, " Number Nodes with fanin Nodes with fanout\n" );
for ( k = 0; k < vFanins->nSize; k++ )
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 4a502895..eef0fc77 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -203,7 +203,7 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-int Gia_SplitCofVar2( Gia_Man_t * p )
+int Gia_SplitCofVar2( Gia_Man_t * p, int * pnFanouts, int * pnCost )
{
Gia_Obj_t * pObj;
int i, iBest = -1, CostBest = -1;
@@ -213,15 +213,17 @@ int Gia_SplitCofVar2( Gia_Man_t * p )
if ( CostBest < Gia_ObjRefNum(p, pObj) )
iBest = i, CostBest = Gia_ObjRefNum(p, pObj);
assert( iBest >= 0 );
+ *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
+ *pnCost = -1;
return iBest;
}
-int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead )
+int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead, int * pnFanouts, int * pnCost )
{
Gia_Man_t * pPart;
int Cost0, Cost1, CostBest = ABC_INFINITY;
int * pOrder, i, iBest = -1;
if ( LookAhead == 1 )
- return Gia_SplitCofVar2( p );
+ return Gia_SplitCofVar2( p, pnFanouts, pnCost );
pOrder = Gia_PermuteSpecialOrder( p );
LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
for ( i = 0; i < LookAhead; i++ )
@@ -251,6 +253,8 @@ int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead )
}
ABC_FREE( pOrder );
assert( iBest >= 0 );
+ *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
+ *pnCost = CostBest;
return iBest;
}
@@ -428,11 +432,19 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
// determine cofactoring variable
int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0);
- int iVar = Gia_SplitCofVar( pLast, LookAhead );
+ int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
// cofactor
Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
if ( pLast->vCofVars == NULL )
pLast->vCofVars = Vec_IntAlloc( 100 );
+ // print results
+ if ( fVerbose )
+ {
+// Cec_GiaSplitPrintRefs( pLast );
+ printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
+ iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
+// Cec_GiaSplitPrintRefs( pPart );
+ }
// create variable
pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
@@ -630,13 +642,21 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
if ( ThData[i].Result == -1 ) // UNDEC
{
// determine cofactoring variable
- int iVar = Gia_SplitCofVar( pLast, LookAhead );
+ int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
// cofactor
Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
Vec_PtrPush( vStack, pPart );
+ // print results
+ if ( fVerbose )
+ {
+// Cec_GiaSplitPrintRefs( pLast );
+ printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
+ iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
+// Cec_GiaSplitPrintRefs( pPart );
+ }
// cofactor
pPart = Gia_ManDupCofactor( pLast, iVar, 1 );
pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 11:06:00 +0000