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

Ongoing development related to Boolean decomposition.

This commit is contained in:
Alan Mishchenko 2024-08-09 18:33:36 -07:00
parent 4156a88dbb
commit 35a1bbbdb4
4 changed files with 303 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

100
src/aig/gia/giaClp.c
View File

@ -404,6 +404,41 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p )
Gia_ManStop( pNew );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintDsdOne( Dsd_Manager_t * pManDsd, int Output, int OffSet )
{
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
Dsd_TreePrint4( vStr, pManDsd, Output );
for ( int i = 0; i < OffSet; i++ )
printf( " " );
printf( "Supp %2d nDsd %2d %s\n", Dsd_TreeSuppSize(pManDsd, Output), Dsd_TreeNonDsdMax(pManDsd, Output), Vec_StrArray(vStr) );
Vec_StrFree( vStr );
fflush( stdout );
}
void Gia_ManPrintDsd( Dsd_Manager_t * pManDsd, int Output, int nOutputs, int OffSet )
{
if ( Output == -1 )
{
for ( int i = 0; i < nOutputs; i++ )
Gia_ManPrintDsdOne( pManDsd, i, OffSet );
}
else
{
assert( Output >= 0 && Output < nOutputs );
Gia_ManPrintDsdOne( pManDsd, Output, OffSet );
}
}
void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
{
DdManager * dd;
@ -425,7 +460,8 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
Cudd_Quit( dd );
return;
}
Dsd_Decompose( pManDsd, (DdNode **)vFuncs->pArray, Gia_ManCoNum(p) );
Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
if ( fVerbose )
{
Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
@ -436,13 +472,75 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
Vec_PtrFreeFree( vNamesCi );
Vec_PtrFreeFree( vNamesCo );
}
else
Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 );
Dsd_ManagerStop( pManDsd );
Gia_ManCollapseDeref( dd, vFuncs );
Extra_StopManager( dd );
}
Vec_Ptr_t * Gia_ManRecurDsdCof( DdManager * dd, Vec_Ptr_t * vFuncs, int iVar )
{
Vec_Ptr_t * vNew = Vec_PtrAlloc( 2 * Vec_PtrSize(vFuncs) ); DdNode * bFunc; int i;
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i ) {
DdNode * bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(Cudd_bddIthVar(dd, iVar)) ); Cudd_Ref( bCof0 );
DdNode * bCof1 = Cudd_Cofactor( dd, bFunc, Cudd_bddIthVar(dd, iVar) ); Cudd_Ref( bCof1 );
Vec_PtrPush( vNew, bCof0 );
Vec_PtrPush( vNew, bCof1 );
}
return vNew;
}
void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose )
{
DdManager * dd;
Dsd_Manager_t * pManDsd;
Vec_Ptr_t * vFuncs, * vAux;
dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
Cudd_AutodynDisable( dd );
if ( vFuncs == NULL )
{
Extra_StopManager( dd );
return;
}
pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
if ( pManDsd == NULL )
{
Gia_ManCollapseDeref( dd, vFuncs );
Cudd_Quit( dd );
return;
}
Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
printf( "Function:\n" );
Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 );
for ( int i = 0; i < 5 && Dsd_TreeNonDsdMax(pManDsd, -1) > 0; i++ )
{
int v, iBestV = -1, DsdMin = ABC_INFINITY, SuppMin = ABC_INFINITY;
for ( v = 0; v < Gia_ManCiNum(p); v++ )
{
Vec_Ptr_t * vTemp = Gia_ManRecurDsdCof( dd, vFuncs, v );
Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vTemp), Vec_PtrSize(vTemp) );
int DsdCur = Dsd_TreeNonDsdMax( pManDsd, -1 );
int SuppCur = Dsd_TreeSuppSize( pManDsd, -1 );
if ( DsdMin > DsdCur || (DsdMin == DsdCur && SuppMin > SuppCur) )
DsdMin = DsdCur, SuppMin = SuppCur, iBestV = v;
Gia_ManCollapseDeref( dd, vTemp );
}
assert( iBestV >= 0 );
vFuncs = Gia_ManRecurDsdCof( dd, vAux = vFuncs, iBestV );
Gia_ManCollapseDeref( dd, vAux );
printf( "Cofactoring variable %c:\n", (int)(iBestV >= 26 ? 'A' - 26 : 'a') + iBestV );
Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
Gia_ManPrintDsd( pManDsd, -1, Vec_PtrSize(vFuncs), (i+1)*2 );
}
Dsd_ManagerStop( pManDsd );
Gia_ManCollapseDeref( dd, vFuncs );
Extra_StopManager( dd );
}
#else

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

@ -54145,13 +54145,14 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDsd )
{
if ( iIn == -1 ) {
Gia_ManCheckDsd( pAbc->pGia, 0, 1 );
printf( "Function = " );
Gia_ManCheckDsd( pAbc->pGia, 0, fVerbose );
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 );
printf( "Cof(%c=%d) = ", 'a' + iIn, c );
Gia_ManCheckDsd( pTemp, 12, fVerbose );
Gia_ManStop( pTemp );
}
}
@ -54159,14 +54160,14 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
}
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, 0, 1 );
printf( " Cof(%c=%d) = ", 'a' + iIn, c );
Gia_ManCheckDsd( pTemp, 0, fVerbose );
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 );
for ( int iIn2 = 0; iIn2 < Gia_ManPiNum(pAbc->pGia); iIn2++ ) if ( iIn2 != iIn )
for ( int c2 = 0; c2 < 2; c2++ ) {
Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn2, c2 );
printf( "Cof(%c=%d,%c=%d) = ", 'a' + iIn, c, 'a' + iIn2, c2 );
Gia_ManCheckDsd( pTemp2, 12, fVerbose );
Gia_ManStop( pTemp2 );
}
}

4
src/bdd/dsd/dsd.h
View File

@ -117,7 +117,11 @@ extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNo
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, int OffSet );
extern void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output );
extern void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output );
extern void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output );
extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
extern int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output );
extern int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output );
/*=== dsdLocal.c =======================================================*/
extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );

189
src/bdd/dsd/dsdTree.c
View File

@ -627,6 +627,195 @@ void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], in
ppNodes[ (*pnNodes)++ ] = pNode;
}
/**Function*************************************************************
Synopsis [Returns the size of the largest non-DSD block.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dsd_TreeNonDsdMax_rec( Dsd_Node_t * pNode )
{
if ( pNode->Type == DSD_NODE_CONST1 )
return 0;
if ( pNode->Type == DSD_NODE_BUF )
return 0;
int MaxBlock = pNode->Type == DSD_NODE_PRIME ? pNode->nDecs : 0;
for ( int i = 0; i < pNode->nDecs; i++ )
{
int MaxThis = Dsd_TreeNonDsdMax_rec( Dsd_Regular( pNode->pDecs[i] ) );
MaxBlock = Abc_MaxInt( MaxBlock, MaxThis );
}
return MaxBlock;
}
int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output )
{
if ( Output == -1 )
{
int i, Res = 0;
for ( i = 0; i < pDsdMan->nRoots; i++ )
Res = Abc_MaxInt( Res, Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ) );
return Res;
}
else
{
assert( Output >= 0 && Output < pDsdMan->nRoots );
return Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) );
}
}
/**Function*************************************************************
Synopsis [Returns the support size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dsd_TreeSuppSize_rec( Dsd_Node_t * pNode )
{
if ( pNode->Type == DSD_NODE_CONST1 )
return 0;
if ( pNode->Type == DSD_NODE_BUF )
return 1;
int nSuppSize = 0;
for ( int i = 0; i < pNode->nDecs; i++ )
nSuppSize += Dsd_TreeSuppSize_rec( Dsd_Regular( pNode->pDecs[i] ) );
return nSuppSize;
}
int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output )
{
if ( Output == -1 )
{
int i, Res = 0;
for ( i = 0; i < pDsdMan->nRoots; i++ )
Res += Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
return Res;
}
else
{
assert( Output >= 0 && Output < pDsdMan->nRoots );
return Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) );
}
}
/**Function*************************************************************
Synopsis [Prints the decompostion tree into a string.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dsd_TreePrint3_rec( Vec_Str_t * p, Dsd_Node_t * pNode )
{
if ( pNode->Type == DSD_NODE_BUF ) {
Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index );
return;
}
if ( pNode->Type == DSD_NODE_PRIME )
Vec_StrPush( p, '{' );
else if ( pNode->Type == DSD_NODE_OR )
Vec_StrPush( p, '(' );
else if ( pNode->Type == DSD_NODE_EXOR )
Vec_StrPush( p, '[' );
else assert( 0 );
for ( int i = 0; i < pNode->nDecs; i++ )
{
Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] );
if ( pInput != pNode->pDecs[i] )
Vec_StrPush( p, '~' );
Dsd_TreePrint3_rec( p, pInput );
}
if ( pNode->Type == DSD_NODE_PRIME )
Vec_StrPush( p, '}' );
else if ( pNode->Type == DSD_NODE_OR )
Vec_StrPush( p, ')' );
else if ( pNode->Type == DSD_NODE_EXOR )
Vec_StrPush( p, ']' );
else assert( 0 );
}
void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output )
{
Vec_Str_t * p = (Vec_Str_t *)pStr;
assert( Output >= 0 && Output < pDsdMan->nRoots );
Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
int fCompl = pNode != pDsdMan->pRoots[Output];
if ( pNode->Type == DSD_NODE_CONST1 )
Vec_StrPush( p, fCompl ? '0' : '1' );
else {
if ( fCompl )
Vec_StrPush( p, '~' );
Dsd_TreePrint3_rec( p, pNode );
}
Vec_StrPush( p, '\0' );
}
/**Function*************************************************************
Synopsis [Prints the decompostion tree into a string.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dsd_TreePrint4_rec( Vec_Str_t * p, Dsd_Node_t * pNode )
{
if ( pNode->Type == DSD_NODE_BUF ) {
Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index );
return;
}
if ( pNode->Type == DSD_NODE_PRIME )
Vec_StrPush( p, '{' );
else if ( pNode->Type == DSD_NODE_OR )
Vec_StrPush( p, '(' );
else if ( pNode->Type == DSD_NODE_EXOR )
Vec_StrPush( p, '[' );
else assert( 0 );
for ( int i = 0; i < pNode->nDecs; i++ )
{
Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] );
if ( (pInput != pNode->pDecs[i]) ^ (pNode->Type == DSD_NODE_OR) ^ (pInput->Type == DSD_NODE_OR) )
Vec_StrPush( p, '~' );
Dsd_TreePrint4_rec( p, pInput );
}
if ( pNode->Type == DSD_NODE_PRIME )
Vec_StrPush( p, '}' );
else if ( pNode->Type == DSD_NODE_OR )
Vec_StrPush( p, ')' );
else if ( pNode->Type == DSD_NODE_EXOR )
Vec_StrPush( p, ']' );
else assert( 0 );
}
void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output )
{
Vec_Str_t * p = (Vec_Str_t *)pStr;
assert( Output >= 0 && Output < pDsdMan->nRoots );
Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
int fCompl = pNode != pDsdMan->pRoots[Output];
if ( pNode->Type == DSD_NODE_CONST1 )
Vec_StrPush( p, fCompl ? '0' : '1' );
else {
if ( fCompl ^ (pNode->Type == DSD_NODE_OR) )
Vec_StrPush( p, '~' );
Dsd_TreePrint4_rec( p, pNode );
}
Vec_StrPush( p, '\0' );
}
/**Function*************************************************************
Synopsis [Prints the decompostion tree into file.]