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

Adding print-out to &splitprove to see impact of cof variable on AIG size.

This commit is contained in:
Alan Mishchenko 2014-06-07 13:04:03 -07:00
parent 8a341c200f
commit 2d38fc1608
4 changed files with 49 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/base/abc/abc.h
View File

@ -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 );

21
src/base/abci/abc.c
View File

@ -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");

14
src/base/abci/abcPrint.c
View File

@ -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++ )

30
src/proof/cec/cecSplit.c
View File

@ -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 );