From e8d690f2a4c9abde54bb248a97c0c619b187f238 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 28 Jul 2012 18:30:21 -0700 Subject: Adding command 'testdec'. --- src/bool/bdc/bdc.h | 2 ++ src/bool/bdc/bdcCore.c | 66 +++++++++++++++++++++++++++++++++++-- src/bool/kit/kit.h | 13 ++++---- src/bool/kit/kitDsd.c | 88 ++++++++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 158 insertions(+), 11 deletions(-) (limited to 'src/bool') diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h index a7572fe8..bd0f7d7d 100644 --- a/src/bool/bdc/bdc.h +++ b/src/bool/bdc/bdc.h @@ -67,10 +67,12 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_F /*=== bdcCore.c ==========================================================*/ extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); extern void Bdc_ManFree( Bdc_Man_t * p ); +extern void Bdc_ManDecPrint( Bdc_Man_t * p ); extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax ); extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ); extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ); extern int Bdc_ManNodeNum( Bdc_Man_t * p ); +extern int Bdc_ManAndNum( Bdc_Man_t * p ); extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ); extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ); extern void * Bdc_FuncCopy( Bdc_Fun_t * p ); diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c index fb318e0d..a810146d 100644 --- a/src/bool/bdc/bdcCore.c +++ b/src/bool/bdc/bdcCore.c @@ -46,6 +46,7 @@ ABC_NAMESPACE_IMPL_START Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ) { return Bdc_FunWithId(p, i); } Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ) { return p->pRoot; } int Bdc_ManNodeNum( Bdc_Man_t * p ) { return p->nNodes; } +int Bdc_ManAndNum( Bdc_Man_t * p ) { return p->nNodes-p->nVars-1;} Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ) { return p->pFan0; } Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ) { return p->pFan1; } void * Bdc_FuncCopy( Bdc_Fun_t * p ) { return p->pCopy; } @@ -186,7 +187,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) /**Function************************************************************* - Synopsis [Clears the manager.] + Synopsis [Prints bi-decomposition in a simple format.] Description [] @@ -195,7 +196,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) SeeAlso [] ***********************************************************************/ -void Bdc_ManDecPrint( Bdc_Man_t * p ) +void Bdc_ManDecPrintSimple( Bdc_Man_t * p ) { Bdc_Fun_t * pNode; int i; @@ -211,12 +212,71 @@ void Bdc_ManDecPrint( Bdc_Man_t * p ) printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) ); printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) ); } - Extra_PrintBinary( stdout, pNode->puFunc, (1<nVars) ); +// Extra_PrintBinary( stdout, pNode->puFunc, (1<nVars) ); printf( "\n" ); } printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) ); } +/**Function************************************************************* + + Synopsis [Prints bi-decomposition recursively.] + + Description [This procedure prints bi-decomposition as a factored form. + In doing so, logic sharing, if present, will be replicated several times.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManDecPrint_rec( Bdc_Man_t * p, Bdc_Fun_t * pNode ) +{ + if ( pNode->Type == BDC_TYPE_PI ) + printf( "%c", 'a' + Bdc_FunId(p,pNode) - 1 ); + else if ( pNode->Type == BDC_TYPE_AND ) + { + Bdc_Fun_t * pNode0 = Bdc_FuncFanin0( pNode ); + Bdc_Fun_t * pNode1 = Bdc_FuncFanin1( pNode ); + + if ( Bdc_IsComplement(pNode0) ) + printf( "!" ); + if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI ) + printf( "(" ); + Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode0) ); + if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI ) + printf( ")" ); + + if ( Bdc_IsComplement(pNode1) ) + printf( "!" ); + if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI ) + printf( "(" ); + Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode1) ); + if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI ) + printf( ")" ); + } + else assert( 0 ); +} +void Bdc_ManDecPrint( Bdc_Man_t * p ) +{ + Bdc_Fun_t * pRoot = Bdc_Regular(p->pRoot); + + printf( "F = " ); + if ( pRoot->Type == BDC_TYPE_CONST1 ) // constant 0 + printf( "Constant %d", !Bdc_IsComplement(p->pRoot) ); + else if ( pRoot->Type == BDC_TYPE_PI ) // literal + printf( "%s%d", Bdc_IsComplement(p->pRoot) ? "!" : "", Bdc_FunId(p,pRoot)-1 ); + else + { + if ( Bdc_IsComplement(p->pRoot) ) + printf( "!(" ); + Bdc_ManDecPrint_rec( p, pRoot ); + if ( Bdc_IsComplement(p->pRoot) ) + printf( ")" ); + } + printf( "\n" ); +} + /**Function************************************************************* Synopsis [Performs decomposition of one function.] diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h index dfee532e..8151f1d2 100644 --- a/src/bool/kit/kit.h +++ b/src/bool/kit/kit.h @@ -112,17 +112,17 @@ struct Kit_DsdObj_t_ unsigned Offset : 8; // offset to the truth table unsigned nRefs : 8; // offset to the truth table unsigned nFans : 6; // the number of fanins of this node - unsigned char pFans[0]; // the fanin literals + unsigned short pFans[0]; // the fanin literals }; // DSD network typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t; struct Kit_DsdNtk_t_ { - unsigned char nVars; // at most 16 (perhaps 18?) - unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars) - unsigned char nNodes; // the number of nodes - unsigned char Root; // the root of the tree + unsigned short nVars; // at most 16 (perhaps 18?) + unsigned short nNodesAlloc; // the number of allocated nodes (at most nVars) + unsigned short nNodes; // the number of nodes + unsigned short Root; // the root of the tree unsigned * pMem; // memory for the truth tables (memory manager?) unsigned * pSupps; // supports of the nodes Kit_DsdObj_t** pNodes; // the nodes @@ -142,7 +142,7 @@ struct Kit_DsdMan_t_ Vec_Int_t * vNodes; // temporary array for BDD nodes }; -static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); } +static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 1) + ((nFans & 1) > 0); } static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; } static inline int Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; } static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; } @@ -538,6 +538,7 @@ extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk ); extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk ); extern Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk ); extern unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk ); +extern int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk ); extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] ); diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c index 3df16d8c..d026afbc 100644 --- a/src/bool/kit/kitDsd.c +++ b/src/bool/kit/kitDsd.c @@ -1485,7 +1485,7 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ) SeeAlso [] ***********************************************************************/ -void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, unsigned piLitsRes[] ) +void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] ) { int nSuppSizes[16], Priority[16], pOrder[16]; int i, k, iVarBest, SuppMax, PrioMax; @@ -1825,6 +1825,90 @@ int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size ) return Kit_DsdFindLargeBox_rec( pNtk, Abc_Lit2Var(pNtk->Root), Size ); } +/**Function************************************************************* + + Synopsis [Returns 1 if there is a component with more than 3 inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id ) +{ + Kit_DsdObj_t * pObj; + unsigned iLit, i, RetValue; + pObj = Kit_DsdNtkObj( pNtk, Id ); + if ( pObj == NULL ) + return 0; + if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR ) + return 0; + if ( pObj->nFans < 2 ) // why this happens? - need to figure out + return 0; + assert( pObj->nFans > 1 ); + if ( pObj->Type == KIT_DSD_AND ) + RetValue = ((int)pObj->nFans - 1); + else if ( pObj->Type == KIT_DSD_XOR ) + RetValue = ((int)pObj->nFans - 1) * 3; + else if ( pObj->Type == KIT_DSD_PRIME ) + { + // assuming MUX decomposition + assert( (int)pObj->nFans == 3 ); + RetValue = 3; + } + else assert( 0 ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if there is a component with more than 3 inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk ) +{ + return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if there is a component with more than 3 inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk ) +{ + Kit_DsdObj_t * pObj; + int i, Counter = 0; + for ( i = 0; i < pNtk->nNodes; i++ ) + { + pObj = pNtk->pNodes[i]; + if ( pObj->Type == KIT_DSD_AND ) + Counter += ((int)pObj->nFans - 1); + else if ( pObj->Type == KIT_DSD_XOR ) + Counter += ((int)pObj->nFans - 1) * 3; + else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition + Counter += 3; + } + return Counter; +} + /**Function************************************************************* Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.] @@ -1883,7 +1967,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 ) SeeAlso [] ***********************************************************************/ -void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux ) +void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux ) { Kit_DsdObj_t * pRes, * pRes0, * pRes1; int nWords = Kit_TruthWordNum(pObj->nFans); -- cgit v1.2.3