Updating DSD profiling procedures.

This commit is contained in:
Alan Mishchenko 2024-08-01 18:36:20 -07:00
parent 9f864ebe76
commit 1954e2fcaa
6 changed files with 86 additions and 53 deletions

View File

@ -382,7 +382,7 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
Vec_PtrFreeFree( vNamesCi );
Vec_PtrFreeFree( vNamesCo );
}
@ -404,7 +404,7 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p )
Gia_ManStop( pNew );
}
void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose )
void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
{
DdManager * dd;
Dsd_Manager_t * pManDsd;
@ -432,7 +432,7 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose )
Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, OffSet );
Vec_PtrFreeFree( vNamesCi );
Vec_PtrFreeFree( vNamesCo );
}
@ -448,7 +448,7 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
return NULL;
}
void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose )
void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
{
}

View File

@ -3311,15 +3311,15 @@ usage:
***********************************************************************/
int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Abc_Obj_t * pNode;
int c, fCompl = 0, fGlobal = 0, fReorder = 1;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Abc_Obj_t * pNode;
int c, fCompl = 0, fGlobal = 0, fReorder = 1, fWidth = 0;
extern void Abc_NodeShowBdd( Abc_Obj_t * pNode, int fCompl );
extern void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl, int fReorder );
extern void Abc_NtkBddDecExplore( Abc_Obj_t * pNode );
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cgrh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cgrwh" ) ) != EOF )
{
switch ( c )
{
@ -3332,6 +3332,9 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fReorder ^= 1;
break;
case 'w':
fWidth ^= 1;
break;
case 'h':
goto usage;
default:
@ -3343,7 +3346,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
}
if ( fGlobal )
{
@ -3358,7 +3361,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Print( -1, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
return 1;
}
}
if ( argc > globalUtilOptind + 1 )
{
Abc_Print( -1, "Wrong number of auguments.\n" );
@ -3382,11 +3385,14 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
}
Abc_NodeShowBdd( pNode, fCompl );
if ( fWidth )
Abc_NtkBddDecExplore( pNode );
else
Abc_NodeShowBdd( pNode, fCompl );
return 0;
usage:
Abc_Print( -2, "usage: show_bdd [-cgrh] <node>\n" );
Abc_Print( -2, "usage: show_bdd [-cgrwh] <node>\n" );
Abc_Print( -2, " uses DOT and GSVIEW to visualize the global BDDs of primary outputs\n" );
Abc_Print( -2, " in terms of primary inputs or the local BDD of a node in terms of its fanins\n" );
#ifdef WIN32
@ -3397,6 +3403,7 @@ usage:
Abc_Print( -2, "\t-c : toggle visualizing BDD with complemented edges [default = %s].\n", fCompl? "yes": "no" );
Abc_Print( -2, "\t-g : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" );
Abc_Print( -2, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
Abc_Print( -2, "\t-w : toggles printing width profile of the node's BDD [default = %s]\n", fWidth? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@ -53855,10 +53862,10 @@ usage:
int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManPrintDsdMatrix( Gia_Man_t * p, int iIn );
extern void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose );
int c, iIn = -1, fDsd = 0, fVerbose = 0;
extern void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose );
int c, iIn = -1, fDsd = 0, fAll = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Vdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Vdavh" ) ) != EOF )
{
switch ( c )
{
@ -53876,6 +53883,9 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDsd ^= 1;
break;
case 'a':
fAll ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -53893,13 +53903,31 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDsd )
{
if ( iIn == -1 ) {
Gia_ManCheckDsd( pAbc->pGia, 1 );
Gia_ManCheckDsd( pAbc->pGia, 0, 1 );
if ( fAll ) {
for ( iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ )
for ( c = 0; c < 2; c++ ) {
Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c );
printf( "%s %2d = %d:\n", c ? " " : "Var", iIn, c );
Gia_ManCheckDsd( pTemp, 12, 1 );
Gia_ManStop( pTemp );
}
}
return 0;
}
for ( c = 0; c < 2; c++ ) {
Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c );
printf( "Var %2d Cof %d:\n", iIn, c );
Gia_ManCheckDsd( pTemp, 1 );
Gia_ManCheckDsd( pTemp, 0, 1 );
if ( fAll ) {
for ( int iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ )
for ( int c = 0; c < 2; c++ ) {
Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn, c );
printf( "%s %2d = %d:\n", c ? " " : "Var", iIn, c );
Gia_ManCheckDsd( pTemp2, 12, 1 );
Gia_ManStop( pTemp2 );
}
}
Gia_ManStop( pTemp );
}
return 0;

View File

@ -143,7 +143,7 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int
ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
if ( fVerbose )
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1, 0 );
else
Dsd_TreePrint2( stdout, pManDsd, ppNamesCi, ppNamesCo, -1 );
ABC_FREE( ppNamesCi );

View File

@ -585,30 +585,36 @@ Abc_Obj_t * Abc_NtkBddFindCofactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int
SeeAlso []
***********************************************************************/
void Abc_NtkBddDecExploreOne( DdManager * dd, DdNode * bFunc, int nLutSize )
void Abc_NtkBddDecExploreOne( DdManager * dd, DdNode * bFunc, int iOrder )
{
DdManager * ddNew = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
int i, * pProfile = ABC_CALLOC( int, dd->size + 100 );
Cudd_AutodynEnable( ddNew, CUDD_REORDER_SYMM_SIFT );
Vec_Int_t * vPerm = Vec_IntStartNatural( dd->size );
Vec_IntRandomizeOrder( vPerm );
Vec_Int_t * vPerm = Vec_IntStartNatural( dd->size ); if ( iOrder ) Vec_IntRandomizeOrder( vPerm );
DdNode * bFuncNew = Extra_TransferPermute( dd, ddNew, bFunc, Vec_IntArray(vPerm) ); Cudd_Ref(bFuncNew);
Cudd_ReduceHeap( ddNew, CUDD_REORDER_SYMM_SIFT, 1 );
Vec_Ptr_t * vCofs = Abc_NtkBddCofactors( ddNew, bFuncNew, nLutSize );
Vec_Ptr_t * vUniq = Vec_PtrDup( vCofs );
Vec_PtrUniqify( vUniq, (int (*)(const void *, const void *))Vec_PtrSortCompare );
printf( "%d ", Vec_PtrSize(vUniq) );
Cudd_RecursiveDeref( dd, bFuncNew );
Cudd_Quit( ddNew );
if ( iOrder ) Cudd_ReduceHeap( ddNew, CUDD_REORDER_SYMM_SIFT, 1 );
Vec_IntFree( vPerm );
Vec_PtrFree( vCofs );
Vec_PtrFree( vUniq );
}
void Abc_NtkBddDecExplore( DdManager * dd, DdNode * bFunc, int nLutSize )
{
Abc_Random(1);
for ( int i = 0; i < 32; i++ )
Abc_NtkBddDecExploreOne( dd, bFunc, nLutSize );
DdNode * aFuncNew = Cudd_BddToAdd( ddNew, bFuncNew ); Cudd_Ref( aFuncNew );
Extra_ProfileWidth( ddNew, aFuncNew, pProfile, -1 );
if ( iOrder )
printf( "Random order %d:\n", iOrder );
else
printf( "Natural order:\n" );
for ( i = 0; i <= dd->size; i++ )
printf( " %d=%d(%d)[%d]", i, pProfile[i], i-Abc_Base2Log(pProfile[i]), ddNew->perm[i] );
printf( "\n" );
Cudd_RecursiveDeref( ddNew, aFuncNew );
Cudd_RecursiveDeref( ddNew, bFuncNew );
Cudd_Quit( ddNew );
}
void Abc_NtkBddDecExplore( Abc_Obj_t * pNode )
{
DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
DdNode * bFunc = (DdNode *)pNode->pData;
int i; Abc_Random(1);
if ( Abc_ObjIsNode(pNode) )
for ( i = 0; i < 16; i++ )
Abc_NtkBddDecExploreOne( dd, bFunc, i );
}
/**Function*************************************************************
@ -645,8 +651,6 @@ Abc_Obj_t * Abc_NtkBddDecompose( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int nLu
}
}
//if ( dd->size == Abc_ObjFaninNum(pNode) )
//Abc_NtkBddDecExplore( dd, (DdNode *)pNode->pData, nLutSize );
// cofactor w.r.t. the bound set variables
vCofs = Abc_NtkBddCofactors( dd, (DdNode *)pNode->pData, nLutSize );
vUniq = Vec_PtrDup( vCofs );
@ -813,6 +817,7 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fReorder, int
#else
Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fReorder, int fVerbose ) { return NULL; }
void Abc_NtkBddDecExplore( Abc_Obj_t * pNode ) {}
#endif

View File

@ -115,7 +115,7 @@ extern int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot );
extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars );
extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet );
extern void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output );
extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
/*=== dsdLocal.c =======================================================*/

View File

@ -638,7 +638,7 @@ void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], in
SeeAlso []
***********************************************************************/
void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output )
void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet )
{
Dsd_Node_t * pNode;
int SigCounter;
@ -650,14 +650,14 @@ void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[],
for ( i = 0; i < pDsdMan->nRoots; i++ )
{
pNode = Dsd_Regular( pDsdMan->pRoots[i] );
Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], 0, &SigCounter, fShortNames );
Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], OffSet, &SigCounter, fShortNames );
}
}
else
{
assert( Output >= 0 && Output < pDsdMan->nRoots );
pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], 0, &SigCounter, fShortNames );
Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], OffSet, &SigCounter, fShortNames );
}
}
@ -686,7 +686,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
if ( !fComp )
fprintf( pFile, "%s = ", pOutputName );
else
fprintf( pFile, "NOT(%s) = ", pOutputName );
fprintf( pFile, "~%s = ", pOutputName );
pInputNums = ABC_ALLOC( int, pNode->nDecs );
if ( pNode->Type == DSD_NODE_CONST1 )
{
@ -711,7 +711,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
if ( i )
fprintf( pFile, "," );
if ( fCompNew )
fprintf( pFile, " NOT(" );
fprintf( pFile, " ~" );
else
fprintf( pFile, " " );
if ( pInput->Type == DSD_NODE_BUF )
@ -727,8 +727,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
pInputNums[i] = (*pSigCounter)++;
fprintf( pFile, "<%d>", pInputNums[i] );
}
if ( fCompNew )
fprintf( pFile, ")" );
//if ( fCompNew )
// fprintf( pFile, "" );
}
fprintf( pFile, " )\n" );
// call recursively for the following blocks
@ -751,7 +751,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
if ( i )
fprintf( pFile, "," );
if ( fCompNew )
fprintf( pFile, " NOT(" );
fprintf( pFile, " ~" );
else
fprintf( pFile, " " );
if ( pInput->Type == DSD_NODE_BUF )
@ -767,8 +767,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
pInputNums[i] = (*pSigCounter)++;
fprintf( pFile, "<%d>", pInputNums[i] );
}
if ( fCompNew )
fprintf( pFile, ")" );
//if ( fCompNew )
// fprintf( pFile, "" );
}
fprintf( pFile, " )\n" );
// call recursively for the following blocks
@ -791,7 +791,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
if ( i )
fprintf( pFile, "," );
if ( fCompNew )
fprintf( pFile, " NOT(" );
fprintf( pFile, " ~" );
else
fprintf( pFile, " " );
if ( pInput->Type == DSD_NODE_BUF )
@ -807,8 +807,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
pInputNums[i] = (*pSigCounter)++;
fprintf( pFile, "<%d>", pInputNums[i] );
}
if ( fCompNew )
fprintf( pFile, ")" );
//if ( fCompNew )
// fprintf( pFile, "" );
}
fprintf( pFile, " )\n" );
// call recursively for the following blocks
@ -979,7 +979,7 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
if ( !fComp )
fprintf( pFile, "%s = ", pOutputName );
else
fprintf( pFile, "NOT(%s) = ", pOutputName );
fprintf( pFile, "~%s = ", pOutputName );
pInputNums = ABC_ALLOC( int, pNode->nDecs );
if ( pNode->Type == DSD_NODE_CONST1 )
{