Skip to content

Commit

Permalink
Ongoing development related to Boolean decomposition.
Browse files Browse the repository at this point in the history
  • Loading branch information
@alanminko
alanminko committed Aug 7, 2024
1 parent b23f998 commit 95f1837
Show file tree
Hide file tree
Showing 3 changed files with 235 additions and 5 deletions.
8 changes: 8 additions & 0 deletions src/aig/gia/giaClp.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -441,6 +441,10 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
Extra_StopManager( dd );
}

void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose )
{
}

#else

Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
Expand All @@ -452,6 +456,10 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
{
}

void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose )
{
}

#endif

////////////////////////////////////////////////////////////////////////
Expand Down
110 changes: 106 additions & 4 deletions src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -427,6 +427,7 @@ static int Abc_CommandAbc9Strash ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Add1Hot ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cofs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv );
Expand Down Expand Up @@ -1221,6 +1222,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&topand", Abc_CommandAbc9Topand, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&add1hot", Abc_CommandAbc9Add1Hot, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cof", Abc_CommandAbc9Cof, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cofs", Abc_CommandAbc9Cofs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 );
Expand Down Expand Up @@ -34229,6 +34231,96 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}

/**Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

***********************************************************************/
int Abc_CommandAbc9Cofs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManDupCofs( Gia_Man_t * p, Vec_Int_t * vVarNums );
Gia_Man_t * pTemp; Vec_Int_t * vVars = NULL;
int c, iVar = 0, nVars = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "VNvh" ) ) != EOF )
{
switch ( c )
{
case 'V':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
goto usage;
}
iVar = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iVar < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nVars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nVars < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cof(): There is no AIG.\n" );
return 1;
}
if ( iVar ) {
Abc_Print( 0, "Cofactoring one variable with ID %d.\n", iVar );
vVars = Vec_IntAlloc( 1 );
Vec_IntPush( vVars, iVar );
}
else if ( nVars ) {
Abc_Print( 0, "Cofactoring the first %d inputs.\n", nVars );
vVars = Vec_IntStartNatural( nVars );
}
else if ( globalUtilOptind < argc ) {
vVars = Vec_IntAlloc( argc );
for ( c = globalUtilOptind; c < argc; c++ )
Vec_IntPush( vVars, atoi(argv[c]) );
}
else {
Abc_Print( -1, "One of the parameters, -V <num> or -L <num>, should be set on the command line.\n" );
goto usage;
}
pTemp = Gia_ManDupCofs( pAbc->pGia, vVars );
Abc_FrameUpdateGia( pAbc, pTemp );
Vec_IntFree( vVars );
return 0;

usage:
Abc_Print( -2, "usage: &cofs [-VN num] [-vh]\n" );
Abc_Print( -2, "\t derives cofactors w.r.t the set of variables\n" );
Abc_Print( -2, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar );
Abc_Print( -2, "\t-N num : cofactoring the given number of first input variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

/**Function*************************************************************

Synopsis []
Expand Down Expand Up @@ -53957,9 +54049,10 @@ 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 OffSet, int fVerbose );
int c, iIn = -1, fDsd = 0, fAll = 0, fVerbose = 0;
extern void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose );
int c, iIn = -1, fDsd = 0, fAll = 0, fRecur = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Vdavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Vdarvh" ) ) != EOF )
{
switch ( c )
{
Expand All @@ -53979,7 +54072,10 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
break;
case 'a':
fAll ^= 1;
break;
break;
case 'r':
fRecur ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
Expand All @@ -53994,6 +54090,11 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9DsdInfo(): There is no AIG.\n" );
return 0;
}
if ( fRecur )
{
Gia_ManRecurDsd( pAbc->pGia, fVerbose );
return 0;
}
if ( fDsd )
{
if ( iIn == -1 ) {
Expand Down Expand Up @@ -54035,10 +54136,11 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;

usage:
Abc_Print( -2, "usage: &dsdinfo [-V num] [-dvh]\n" );
Abc_Print( -2, "usage: &dsdinfo [-V num] [-drvh]\n" );
Abc_Print( -2, "\t computes and displays information related to DSD\n" );
Abc_Print( -2, "\t-V num : the zero-based index of the input variable [default = %d]\n", iIn );
Abc_Print( -2, "\t-d : toggles showing DSD structure [default = %s]\n", fDsd ? "yes": "no" );
Abc_Print( -2, "\t-r : toggles recursive cofactoring to get a full DSD [default = %s]\n", fRecur ? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
Expand Down
122 changes: 121 additions & 1 deletion src/bdd/extrab/extraLutCas.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,9 @@
#include <string.h>
#include <assert.h>

#include "aig/miniaig/miniaig.h"
#include "bdd/cudd/cuddInt.h"
#include "bdd/dsd/dsd.h"

ABC_NAMESPACE_HEADER_START

Expand All @@ -50,6 +52,62 @@ ABC_NAMESPACE_HEADER_START
If the LUT cascade contains a 6-LUT followed by a 4-LUT, the record contains 1+10+8=19 words.
*/

#define Mini_AigForEachNonPo( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( Mini_AigNodeIsPo(p, i) ) {} else

/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_LutCasCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs )
{
DdNode * bFunc; int i;
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
if ( bFunc )
Cudd_RecursiveDeref( dd, bFunc );
Vec_PtrFree( vFuncs );
}
Vec_Ptr_t * Abc_LutCasCollapse( Mini_Aig_t * p, DdManager * dd, int nBddLimit, int fVerbose )
{
DdNode * bFunc0, * bFunc1, * bFunc; int Id, nOuts = 0;
Vec_Ptr_t * vFuncs = Vec_PtrStart( Mini_AigNodeNum(p) );
Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
Mini_AigForEachPi( p, Id )
Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,Id-1) ), Cudd_Ref(Cudd_bddIthVar(dd,Id-1));
Mini_AigForEachAnd( p, Id ) {
bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin0(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin0(p, Id)) );
bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin1(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin1(p, Id)) );
bFunc = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );
if ( bFunc == NULL )
{
Abc_LutCasCollapseDeref( dd, vFuncs );
return NULL;
}
Cudd_Ref( bFunc );
Vec_PtrWriteEntry( vFuncs, Id, bFunc );
}
Mini_AigForEachPo( p, Id ) {
bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin0(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin0(p, Id)) );
Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
}
Mini_AigForEachNonPo( p, Id ) {
bFunc = (DdNode *)Vec_PtrEntry(vFuncs, Id);
Cudd_RecursiveDeref( dd, bFunc );
Vec_PtrWriteEntry( vFuncs, Id, NULL );
}
Mini_AigForEachPo( p, Id )
Vec_PtrWriteEntry( vFuncs, nOuts++, Vec_PtrEntry(vFuncs, Id) );
Vec_PtrShrink( vFuncs, nOuts );
return vFuncs;
}


/**Function*************************************************************
Synopsis []
Expand All @@ -61,12 +119,74 @@ ABC_NAMESPACE_HEADER_START
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_LutCasFakeNames( int nNames )
{
Vec_Ptr_t * vNames;
char Buffer[5];
int i;

vNames = Vec_PtrAlloc( nNames );
for ( i = 0; i < nNames; i++ )
{
if ( nNames < 26 )
{
Buffer[0] = 'a' + i;
Buffer[1] = 0;
}
else
{
Buffer[0] = 'a' + i%26;
Buffer[1] = '0' + i/26;
Buffer[2] = 0;
}
Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
}
return vNames;
}
void Abc_LutCasPrintDsd( DdManager * dd, DdNode * bFunc, int fVerbose )
{
Dsd_Manager_t * pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
Dsd_Decompose( pManDsd, &bFunc, 1 );
if ( fVerbose )
{
Vec_Ptr_t * vNamesCi = Abc_LutCasFakeNames( dd->size );
Vec_Ptr_t * vNamesCo = Abc_LutCasFakeNames( 1 );
char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
Vec_PtrFreeFree( vNamesCi );
Vec_PtrFreeFree( vNamesCo );
}
Dsd_ManagerStop( pManDsd );
}
DdNode * Abc_LutCasBuildBdds( Mini_Aig_t * p, DdManager ** pdd )
{
DdManager * dd = Cudd_Init( Mini_AigPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
Vec_Ptr_t * vFuncs = Abc_LutCasCollapse( p, dd, 10000, 0 );
Cudd_AutodynDisable( dd );
if ( vFuncs == NULL ) {
Extra_StopManager( dd );
return NULL;
}
DdNode * bNode = (DdNode *)Vec_PtrEntry(vFuncs, 0);
Vec_PtrFree(vFuncs);
*pdd = dd;
return bNode;
}
static inline word * Abc_LutCascade( Mini_Aig_t * p, int nLutSize, int fVerbose )
{
DdManager * dd = NULL;
DdNode * bFunc = Abc_LutCasBuildBdds( p, &dd );
if ( bFunc == NULL ) return NULL;
Abc_LutCasPrintDsd( dd, bFunc, 1 );
Cudd_RecursiveDeref( dd, bFunc );
Extra_StopManager( dd );

word * pLuts = NULL;
return pLuts;
}

ABC_NAMESPACE_HEADER_END

#endif /* __EXTRA_H__ */
#endif /* ABC__misc__extra__extra_lutcas_h */

0 comments on commit 95f1837

Please sign in to comment.