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 +++++++++++++++++++++ src/base/abci/abc.c | 65 ++++++++++++++++++++++++ src/base/abci/abcBidec.c | 126 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcIf.c | 86 ++----------------------------- src/base/abci/module.make | 1 + src/map/if/ifTime.c | 2 +- src/map/if/ifTruth.c | 4 +- src/opt/lpk/lpkCore.c | 21 ++++++++ src/opt/mfs/mfsCore.c | 44 +++++++++++++--- src/opt/mfs/mfsInt.h | 8 ++- src/opt/mfs/mfsMan.c | 6 +++ src/opt/mfs/mfsSat.c | 12 +++++ 18 files changed, 519 insertions(+), 137 deletions(-) create mode 100644 src/base/abci/abcBidec.c (limited to 'src') 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************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f366a612..4262cd0d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -93,6 +93,7 @@ static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -275,6 +276,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 ); Cmd_CommandAdd( pAbc, "Various", "aig", Abc_CommandAig, 0 ); Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 ); + Cmd_CommandAdd( pAbc, "Various", "bidec", Abc_CommandBidec, 1 ); Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); @@ -5191,6 +5193,69 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBidec( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fVerbose; + extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + // get the new network + if ( !Abc_NtkIsAigLogic(pNtk) ) + { + fprintf( pErr, "Bi-decomposition only works when node functions are AIGs (run \"aig\").\n" ); + return 1; + } + Abc_NtkBidecResyn( pNtk, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: bidec [-vh]\n" ); + fprintf( pErr, "\t applies bi-decomposition to local functions of the nodes\n" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c new file mode 100644 index 00000000..ad332314 --- /dev/null +++ b/src/base/abci/abcBidec.c @@ -0,0 +1,126 @@ +/**CFile**************************************************************** + + FileName [abcBidec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Interface to bi-decomposition.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +#include "bdc.h" +#include "bdcInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Resynthesizes nodes using bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ) +{ + unsigned * pTruth; + Bdc_Fun_t * pFunc; + int i; + assert( nVars <= 16 ); + // derive truth table + pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 ); + if ( Hop_IsComplement(pRoot) ) + Extra_TruthNot( pTruth, pTruth, nVars ); + // decompose truth table + Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 ); + // convert back into HOP + Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop ); + for ( i = 0; i < nVars; i++ ) + Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i ); + for ( i = nVars + 1; i < p->nNodes; i++ ) + { + pFunc = Bdc_FunWithId( p, i ); + pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) ); + } + return Bdc_FunCopyHop(p->pRoot); +} + +/**Function************************************************************* + + Synopsis [Resynthesizes nodes using bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Bdc_Par_t Pars = {0}, * pPars = &Pars; + Bdc_Man_t * p; + Abc_Obj_t * pObj; + Vec_Int_t * vTruth; + int i, nGainTotal = 0, nNodes1, nNodes2; + int clk = clock(); + assert( Abc_NtkIsLogic(pNtk) ); + if ( !Abc_NtkToAig(pNtk) ) + return; + pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk ); + pPars->fVerbose = fVerbose; + if ( pPars->nVarsMax > 15 ) + { + if ( fVerbose ) + printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" ); + pPars->nVarsMax = 15; + } + vTruth = Vec_IntAlloc( 0 ); + p = Bdc_ManAlloc( pPars ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + if ( Abc_ObjFaninNum(pObj) > 15 ) + continue; + nNodes1 = Hop_DagSize(pObj->pData); + pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, NULL ); + nNodes2 = Hop_DagSize(pObj->pData); + nGainTotal += nNodes1 - nNodes2; + } + Bdc_ManFree( p ); + Vec_IntFree( vTruth ); + if ( fVerbose ) + { + printf( "Total gain in AIG nodes = %d. ", nGainTotal ); + PRT( "Total runtime", clock() - clk ); + } +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index a20925b2..35ec473f 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -34,7 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk ); extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ); -extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk ); +extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) return NULL; If_ManStop( pIfMan ); if ( pPars->fBidec && pPars->nLutSize <= 8 ) - Abc_NtkBidecResyn( pNtkNew ); + Abc_NtkBidecResyn( pNtkNew, 0 ); // duplicate EXDC if ( pNtk->pExdc ) @@ -256,7 +256,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); // if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays ) -// If_CutRotatePins( pIfMan, pCutBest ); + If_CutRotatePins( pIfMan, pCutBest ); if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) @@ -551,86 +551,6 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk ) } -#include "bdc.h" -#include "bdcInt.h" - -static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); } - -/**Function************************************************************* - - Synopsis [Resynthesizes nodes using bi-decomposition.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth ) -{ - unsigned * pTruth; - Bdc_Fun_t * pFunc; - int i; - // derive truth table - pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 ); - if ( Hop_IsComplement(pRoot) ) - Extra_TruthNot( pTruth, pTruth, nVars ); - // decompose truth table - Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 ); - // convert back into HOP - Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop ); - for ( i = 0; i < nVars; i++ ) - Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i ); - for ( i = nVars + 1; i < p->nNodes; i++ ) - { - pFunc = Bdc_FunWithId( p, i ); - pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) ); - } - return Bdc_FunCopyHop(p->pRoot); -} - -/**Function************************************************************* - - Synopsis [Resynthesizes nodes using bi-decomposition.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk ) -{ - Bdc_Par_t Pars = {0}, * pPars = &Pars; - Bdc_Man_t * p; - Abc_Obj_t * pObj; - Vec_Int_t * vTruth; - int i, nGainTotal = 0, nNodes1, nNodes2; - int clk = clock(); - pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk ); - if ( pPars->nVarsMax > 8 ) - { - printf( "Resynthesis is not performed.\n" ); - return; - } - vTruth = Vec_IntAlloc( 0 ); - p = Bdc_ManAlloc( pPars ); - Abc_NtkForEachNode( pNtk, pObj, i ) - { - nNodes1 = Hop_DagSize(pObj->pData); - pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth ); - nNodes2 = Hop_DagSize(pObj->pData); - nGainTotal += nNodes1 - nNodes2; - } -// printf( "LUTs = %d. Total gain in AIG nodes = %d. ", Abc_NtkNodeNum(pNtk), nGainTotal ); -// PRT( "Time", clock() - clk ); - Bdc_ManFree( p ); - Vec_IntFree( vTruth ); -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 55b724b8..a2f879e3 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -2,6 +2,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcAttach.c \ src/base/abci/abcAuto.c \ src/base/abci/abcBalance.c \ + src/base/abci/abcBidec.c \ src/base/abci/abcBmc.c \ src/base/abci/abcCas.c \ src/base/abci/abcClpBdd.c \ diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 33bbdf74..59322cad 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -238,7 +238,7 @@ void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut ) float PinDelays[32]; // int PinPerm[32]; int i; - assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth ); +// assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth ); If_CutForEachLeaf( p, pCut, pLeaf, i ) PinDelays[i] = If_ObjCutBest(pLeaf)->Delay; If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) ); diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c index a3a7e1ee..637a42b4 100644 --- a/src/map/if/ifTruth.c +++ b/src/map/if/ifTruth.c @@ -146,16 +146,18 @@ void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDe for ( i = 0; i < nVars - 1; i++ ) { if ( pDelays[i] >= pDelays[i+1] ) +// if ( pDelays[i] <= pDelays[i+1] ) continue; tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp; Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp; + if ( pOut && pIn ) If_TruthSwapAdjacentVars( pOut, pIn, nVars, i ); pTemp = pOut; pOut = pIn; pIn = pTemp; fChange = 1; Counter++; } } - if ( Counter & 1 ) + if ( pOut && pIn && (Counter & 1) ) If_TruthCopy( pOut, pIn, nVars ); } diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index 34911c20..80080d50 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -500,6 +500,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) Lpk_Man_t * p; Abc_Obj_t * pObj; double Delta; +// int * pnFanouts, nObjMax; int i, Iter, nNodes, nNodesPrev, clk = clock(); assert( Abc_NtkIsLogic(pNtk) ); @@ -554,6 +555,14 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) p->nTotalNets = Abc_NtkGetTotalFanins(pNtk); p->nTotalNodes = Abc_NtkNodeNum(pNtk); } +/* + // save the number of fanouts of all objects + nObjMax = Abc_NtkObjNumMax( pNtk ); + pnFanouts = ALLOC( int, nObjMax ); + memset( pnFanouts, 0, sizeof(int) * nObjMax ); + Abc_NtkForEachObj( pNtk, pObj, i ) + pnFanouts[pObj->Id] = Abc_ObjFanoutNum(pObj); +*/ // iterate over the network nNodesPrev = p->nNodesTotal; @@ -604,6 +613,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) break; } Abc_NtkStopReverseLevels( pNtk ); +/* + // report the fanout changes + Abc_NtkForEachObj( pNtk, pObj, i ) + { + if ( i >= nObjMax ) + continue; + if ( Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] == 0 ) + continue; + printf( "%d ", Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] ); + } + printf( "\n" ); +*/ if ( pPars->fVerbose ) { diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 4e4f7490..bde2ad42 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -100,7 +100,10 @@ p->timeSat += clock() - clk; ***********************************************************************/ int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { - int clk; + Hop_Obj_t * pObj; + extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ); + + int nGain, clk; p->nNodesTried++; // prepare data structure for this node Mfs_ManClean( p ); @@ -128,6 +131,16 @@ clk = clock(); // solve the SAT problem Abc_NtkMfsSolveSat( p, pNode ); p->timeSat += clock() - clk; + // minimize the local function of the node using bi-decomposition + assert( p->nFanins == Abc_ObjFaninNum(pNode) ); + pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare ); + nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj); + if ( nGain >= 0 ) + { + p->nNodesDec++; + p->nNodesGained += nGain; + pNode->pData = pObj; + } return 1; } @@ -146,6 +159,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ); + Bdc_Par_t Pars = {0}, * pDecPars = &Pars; ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; @@ -157,8 +171,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) nFaninMax = Abc_NtkGetFaninMax(pNtk); if ( nFaninMax > MFS_FANIN_MAX ) { - printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX ); - return 1; + printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX ); + nFaninMax = MFS_FANIN_MAX; } // perform the network sweep Abc_NtkSweep( pNtk, 0 ); @@ -186,11 +200,16 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { if ( p->pCare != NULL ) printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); - else - printf( "Performing optimization without constraints.\n" ); +// else +// printf( "Performing optimization without constraints.\n" ); } if ( !pPars->fResub ) - printf( "Currently don't-cares are not used but the stats are printed.\n" ); + { + pDecPars->nVarsMax = nFaninMax; + pDecPars->fVerbose = pPars->fVerbose; + p->vTruth = Vec_IntAlloc( 0 ); + p->pManDec = Bdc_ManAlloc( pDecPars ); + } // label the register outputs if ( p->pCare ) @@ -211,15 +230,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) continue; + if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) + continue; if ( !p->pPars->fVeryVerbose ) Extra_ProgressBarUpdate( pProgress, i, NULL ); if ( pPars->fResub ) Abc_NtkMfsResub( p, pObj ); - else + else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) Abc_NtkMfsNode( p, pObj ); } Extra_ProgressBarStop( pProgress ); Abc_NtkStopReverseLevels( pNtk ); + + // perform the sweeping + if ( !pPars->fResub ) + { + extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose ); + Abc_NtkSweep( pNtk, 0 ); + Abc_NtkBidecResyn( pNtk, 0 ); + } + p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk); p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk); diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 91395d03..f4da45ef 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -35,12 +35,13 @@ extern "C" { #include "cnf.h" #include "satSolver.h" #include "satStore.h" +#include "bdc.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#define MFS_FANIN_MAX 10 +#define MFS_FANIN_MAX 12 typedef struct Mfs_Man_t_ Mfs_Man_t; struct Mfs_Man_t_ @@ -64,6 +65,11 @@ struct Mfs_Man_t_ int nCexes; // the numbe rof current counter-examples int nSatCalls; int nSatCexes; + // used for bidecomposition + Vec_Int_t * vTruth; + Bdc_Man_t * pManDec; + int nNodesDec; + int nNodesGained; // solving data Aig_Man_t * pAigWin; // window AIG with constraints Cnf_Dat_t * pCnf; // the CNF for the window diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 17ca40fc..f1b3f44c 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -131,6 +131,8 @@ void Mfs_ManPrint( Mfs_Man_t * p ) 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); // printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", // 1.0-(p->dTotalRatios/p->nNodesTried) ); + printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d.\n", + p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained ); } /* PRTP( "Win", p->timeWin , p->timeTotal ); @@ -158,6 +160,10 @@ void Mfs_ManStop( Mfs_Man_t * p ) { if ( p->pPars->fVerbose ) Mfs_ManPrint( p ); + if ( p->vTruth ) + Vec_IntFree( p->vTruth ); + if ( p->pManDec ) + Bdc_ManFree( p->pManDec ); if ( p->pCare ) Aig_ManStop( p->pCare ); if ( p->vSuppsInv ) diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index efb09b39..2529e207 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -110,6 +110,18 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) Extra_PrintBinary( stdout, p->uCare, (1<nFanins) ); printf( "\n" ); } + + // map the care + if ( p->nFanins > 4 ) + return; + if ( p->nFanins == 4 ) + p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16); + if ( p->nFanins == 3 ) + p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24); + if ( p->nFanins == 2 ) + p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) | + (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28); + assert( p->nFanins != 1 ); } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3