From 95f183796014544c59f8e75d1824890b1489922c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 7 Aug 2024 10:07:39 -0700 Subject: [PATCH] Ongoing development related to Boolean decomposition. --- src/aig/gia/giaClp.c | 8 +++ src/base/abci/abc.c | 110 +++++++++++++++++++++++++++++-- src/bdd/extrab/extraLutCas.h | 122 ++++++++++++++++++++++++++++++++++- 3 files changed, 235 insertions(+), 5 deletions(-) diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c index 873cea2eb..feadd38d7 100644 --- a/src/aig/gia/giaClp.c +++ b/src/aig/gia/giaClp.c @@ -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 ) @@ -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 //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a78706032..eff7259a4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ); @@ -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 ); @@ -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 or -L , 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 [] @@ -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 ) { @@ -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; @@ -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 ) { @@ -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; diff --git a/src/bdd/extrab/extraLutCas.h b/src/bdd/extrab/extraLutCas.h index df7a14010..1308c2bee 100644 --- a/src/bdd/extrab/extraLutCas.h +++ b/src/bdd/extrab/extraLutCas.h @@ -32,7 +32,9 @@ #include #include +#include "aig/miniaig/miniaig.h" #include "bdd/cudd/cuddInt.h" +#include "bdd/dsd/dsd.h" ABC_NAMESPACE_HEADER_START @@ -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 [] @@ -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 */