From ff6f0943362c30176fd1f961bcbd19e188cee520 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 14 Mar 2008 08:01:00 -0700 Subject: Version abc80314 --- src/aig/bdc/bdcCore.c | 28 ++++++++++-- src/aig/bdc/bdcDec.c | 115 +++++++++++++++++++++++++++++++++++++++++++++--- src/aig/bdc/bdcInt.h | 17 ++++++- src/aig/bdc/bdcTable.c | 33 -------------- src/aig/dar/darRefact.c | 29 ++++++++++++ src/aig/kit/kit.h | 1 + src/aig/kit/kitTruth.c | 58 ++++++++++++++++++++++++ 7 files changed, 237 insertions(+), 44 deletions(-) (limited to 'src/aig') diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c index f0b0f3bc..13275377 100644 --- a/src/aig/bdc/bdcCore.c +++ b/src/aig/bdc/bdcCore.c @@ -48,11 +48,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) p->pPars = pPars; p->nWords = Kit_TruthWordNum( pPars->nVarsMax ); p->nDivsLimit = 200; - // memory - p->vMemory = Vec_IntStart( 1 << 16 ); // internal nodes p->nNodesAlloc = 512; p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc ); + // memory + p->vMemory = Vec_IntStart( 4 * p->nWords * p->nNodesAlloc ); // set up hash table p->nTableSize = (1 << p->pPars->nVarsMax); p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize ); @@ -69,7 +69,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR ); p->pIsfAL = &p->IsfAL; Bdc_IsfStart( p, p->pIsfAL ); p->pIsfAR = &p->IsfAR; Bdc_IsfStart( p, p->pIsfAR ); - return p; + return p; } /**Function************************************************************* @@ -85,6 +85,18 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) ***********************************************************************/ void Bdc_ManFree( Bdc_Man_t * p ) { + if ( p->pPars->fVerbose ) + { + printf( "Bi-decomposition stats: Calls = %d. Nodes = %d. Reuse = %d.\n", + p->numCalls, p->numNodes, p->numReuse ); + printf( "ANDs = %d. ORs = %d. Weak = %d. Muxes = %d. Memory = %.2f K\n", + p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) ); + PRT( "Cache", p->timeCache ); + PRT( "Check", p->timeCheck ); + PRT( "Muxes", p->timeMuxes ); + PRT( "Supps", p->timeSupps ); + PRT( "TOTAL", p->timeTotal ); + } Vec_IntFree( p->vMemory ); Vec_IntFree( p->vSpots ); Vec_PtrFree( p->vTruths ); @@ -118,7 +130,8 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) // add constant 1 pNode = Bdc_FunNew( p ); pNode->Type = BDC_TYPE_CONST1; - pNode->puFunc = NULL; + pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); + Kit_TruthFill( pNode->puFunc, p->nVars ); pNode->uSupp = 0; Bdc_TableAdd( p, pNode ); // add variables @@ -192,6 +205,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p ) int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax ) { Bdc_Isf_t Isf, * pIsf = &Isf; + int clk = clock(); assert( nVars <= p->pPars->nVarsMax ); // set current manager parameters p->nVars = nVars; @@ -213,8 +227,14 @@ int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int n Bdc_SuppMinimize( p, pIsf ); // call decomposition p->pRoot = Bdc_ManDecompose_rec( p, pIsf ); + p->timeTotal += clock() - clk; + p->numCalls++; + p->numNodes += p->nNodesNew; if ( p->pRoot == NULL ) return -1; + if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) ) + printf( "Bdc_ManDecompose(): Internal verification failed.\n" ); +// assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) ); return p->nNodesNew; } diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c index 13a33196..55ce97a0 100644 --- a/src/aig/bdc/bdcDec.c +++ b/src/aig/bdc/bdcDec.c @@ -28,6 +28,82 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Minimizes the support of the ISF.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) +{ + int v, clk; + if ( p->pPars->fVerbose ) + clk = clock(); + // compute support + pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | + Kit_TruthSupport( pIsf->puOff, p->nVars ); + // go through the support variables + for ( v = 0; v < p->nVars; v++ ) + { + if ( (pIsf->uSupp & (1 << v)) == 0 ) + continue; + Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v ); + Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v ); + if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) ) + continue; +// if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) ) +// continue; + // remove the variable + Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars ); + Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars ); +// Kit_TruthExist( pIsf->puOn, p->nVars, v ); +// Kit_TruthExist( pIsf->puOff, p->nVars, v ); + pIsf->uSupp &= ~(1 << v); + } + if ( p->pPars->fVerbose ) + p->timeSupps += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [Minimizes the support of the ISF.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) +{ + int v, clk; + if ( p->pPars->fVerbose ) + clk = clock(); + // go through the support variables + pIsf->uSupp = 0; + for ( v = 0; v < p->nVars; v++ ) + { + if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) && + !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) ) + continue; + if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) ) + { + Kit_TruthExist( pIsf->puOn, p->nVars, v ); + Kit_TruthExist( pIsf->puOff, p->nVars, v ); + continue; + } + pIsf->uSupp |= (1 << v); + } + if ( p->pPars->fVerbose ) + p->timeSupps += clock() - clk; +} + /**Function************************************************************* Synopsis [Updates the ISF of the right after the left was decompoosed.] @@ -418,12 +494,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL // check if there is any reuse for the components if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR ) { + p->numReuse++; + p->numOrs++; Bdc_IsfCopy( pIsfL, p->pIsfOL ); Bdc_IsfCopy( pIsfR, p->pIsfOR ); return BDC_TYPE_OR; } if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR ) { + p->numReuse++; + p->numAnds++; Bdc_IsfCopy( pIsfL, p->pIsfAL ); Bdc_IsfCopy( pIsfR, p->pIsfAR ); return BDC_TYPE_AND; @@ -432,10 +512,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL // compare the two-component costs if ( WeightOr > WeightAnd ) { + if ( WeightOr < BDC_SCALE ) + p->numWeaks++; + p->numOrs++; Bdc_IsfCopy( pIsfL, p->pIsfOL ); Bdc_IsfCopy( pIsfR, p->pIsfOR ); return BDC_TYPE_OR; } + if ( WeightAnd < BDC_SCALE ) + p->numWeaks++; + p->numAnds++; Bdc_IsfCopy( pIsfL, p->pIsfAL ); Bdc_IsfCopy( pIsfR, p->pIsfAR ); return BDC_TYPE_AND; @@ -456,6 +542,9 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd { int Var, VarMin, nSuppMin, nSuppCur; unsigned uSupp0, uSupp1; + int clk; + if ( p->pPars->fVerbose ) + clk = clock(); VarMin = -1; nSuppMin = 1000; for ( Var = 0; Var < p->nVars; Var++ ) @@ -473,7 +562,7 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd { nSuppMin = nSuppCur; VarMin = Var; -// break; + break; } } if ( VarMin >= 0 ) @@ -485,6 +574,8 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd Bdc_SuppMinimize( p, pIsfL ); Bdc_SuppMinimize( p, pIsfR ); } + if ( p->pPars->fVerbose ) + p->timeMuxes += clock() - clk; return VarMin; } @@ -582,6 +673,7 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) Bdc_Fun_t * pFunc, * pFunc0, * pFunc1; Bdc_Isf_t IsfL, * pIsfL = &IsfL; Bdc_Isf_t IsfB, * pIsfR = &IsfB; + int iVar, clk; /* printf( "Init function (%d):\n", LocalCounter ); Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n"); @@ -589,13 +681,27 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n"); */ // check computed results assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) ); - if ( pFunc = Bdc_TableLookup( p, pIsf ) ) + if ( p->pPars->fVerbose ) + clk = clock(); + pFunc = Bdc_TableLookup( p, pIsf ); + if ( p->pPars->fVerbose ) + p->timeCache += clock() - clk; + if ( pFunc ) return pFunc; // decide on the decomposition type + if ( p->pPars->fVerbose ) + clk = clock(); Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR ); + if ( p->pPars->fVerbose ) + p->timeCheck += clock() - clk; if ( Type == BDC_TYPE_MUX ) { - int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR ); + if ( p->pPars->fVerbose ) + clk = clock(); + iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR ); + if ( p->pPars->fVerbose ) + p->timeMuxes += clock() - clk; + p->numMuxes++; pFunc0 = Bdc_ManDecompose_rec( p, pIsfL ); pFunc1 = Bdc_ManDecompose_rec( p, pIsfR ); if ( pFunc0 == NULL || pFunc1 == NULL ) @@ -625,9 +731,6 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n"); // create new gate pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type ); } - if ( pFunc == NULL ) - return NULL; - assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) ); return pFunc; } diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h index 5fda4301..afba0e67 100644 --- a/src/aig/bdc/bdcInt.h +++ b/src/aig/bdc/bdcInt.h @@ -106,6 +106,20 @@ struct Bdc_Man_t_ Bdc_Isf_t * pIsfAR, IsfAR; // internal memory manager Vec_Int_t * vMemory; // memory for internal truth tables + // statistics + int numCalls; + int numNodes; + int numMuxes; + int numAnds; + int numOrs; + int numWeaks; + int numReuse; + // runtime + int timeCache; + int timeCheck; + int timeMuxes; + int timeSupps; + int timeTotal; }; // working with complemented attributes of objects @@ -132,11 +146,12 @@ static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsign /*=== bdcDec.c ==========================================================*/ extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); +extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); +extern int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc ); /*=== bdcTable.c ==========================================================*/ extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); extern void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc ); extern void Bdc_TableClear( Bdc_Man_t * p ); -extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); extern int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth ); #ifdef __cplusplus diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c index b7f10344..3a6ed126 100644 --- a/src/aig/bdc/bdcTable.c +++ b/src/aig/bdc/bdcTable.c @@ -28,39 +28,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Minimizes the support of the ISF.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) -{ - int v; - // compute support - pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | - Kit_TruthSupport( pIsf->puOff, p->nVars ); - // go through the support variables - for ( v = 0; v < p->nVars; v++ ) - { - if ( (pIsf->uSupp & (1 << v)) == 0 ) - continue; - Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v ); - Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v ); - if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) ) - continue; - // remove the variable - Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars ); - Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars ); - pIsf->uSupp &= ~(1 << v); - } -} - /**Function************************************************************* Synopsis [Checks containment of the function in the ISF.] diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index a765ec30..e814840f 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -21,6 +21,9 @@ #include "darInt.h" #include "kit.h" +#include "bdc.h" +#include "bdcInt.h" + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -44,6 +47,9 @@ struct Ref_Man_t_ Kit_Graph_t * pGraphBest; // the best factored form int GainBest; // the best gain int LevelBest; // the level of node with the best gain + // bi-decomposition + Bdc_Par_t DecPars; // decomposition parameters + Bdc_Man_t * pManDec; // decomposition manager // node statistics int nNodesInit; // the initial number of nodes int nNodesTried; // the number of nodes tried @@ -111,6 +117,11 @@ Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) p->vMemory = Vec_IntAlloc( 1 << 16 ); p->vCutNodes = Vec_PtrAlloc( 256 ); p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax ); + // alloc bi-decomposition manager + p->DecPars.nVarsMax = pPars->nLeafMax; + p->DecPars.fVerbose = pPars->fVerbose; + p->DecPars.fVeryVerbose = 0; +// p->pManDec = Bdc_ManAlloc( &p->DecPars ); return p; } @@ -151,6 +162,8 @@ void Dar_ManRefPrintStats( Ref_Man_t * p ) ***********************************************************************/ void Dar_ManRefStop( Ref_Man_t * p ) { + if ( p->pManDec ) + Bdc_ManFree( p->pManDec ); if ( p->pPars->fVerbose ) Dar_ManRefPrintStats( p ); Vec_VecFree( p->vCuts ); @@ -381,6 +394,13 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in if ( RetValue > -1 ) { pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory ); +/* +{ + int RetValue; + RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 ); + printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue ); +} +*/ nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required ); if ( nNodesAdded > -1 ) { @@ -403,9 +423,17 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in // try negative phase Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) ); RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 ); +// Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) ); if ( RetValue > -1 ) { pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory ); +/* +{ + int RetValue; + RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 ); + printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue ); +} +*/ nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required ); if ( nNodesAdded > -1 ) { @@ -426,6 +454,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in Kit_GraphFree( pGraphCur ); } } + return p->GainBest; } diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h index 06a93cf0..23e3ce8d 100644 --- a/src/aig/kit/kit.h +++ b/src/aig/kit/kit.h @@ -564,6 +564,7 @@ extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVa extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar ); extern void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar ); +extern int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar ); extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask ); diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c index dab60132..9ddc7562 100644 --- a/src/aig/kit/kitTruth.c +++ b/src/aig/kit/kitTruth.c @@ -520,6 +520,64 @@ void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar } } +/**Function************************************************************* + + Synopsis [Computes negative cofactor of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar ) +{ + int nWords = Kit_TruthWordNum( nVars ); + int i, k, Step; + + assert( iVar < nVars ); + switch ( iVar ) + { + case 0: + for ( i = 0; i < nWords; i++ ) + if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 ) + return 0; + return 1; + case 1: + for ( i = 0; i < nWords; i++ ) + if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 ) + return 0; + return 1; + case 2: + for ( i = 0; i < nWords; i++ ) + if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F ) + return 0; + return 1; + case 3: + for ( i = 0; i < nWords; i++ ) + if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF ) + return 0; + return 1; + case 4: + for ( i = 0; i < nWords; i++ ) + if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF ) + return 0; + return 1; + default: + Step = (1 << (iVar - 5)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) ) + return 0; + pOnset += 2*Step; + pOffset += 2*Step; + } + return 1; + } +} + /**Function************************************************************* -- cgit v1.2.3