From a13c64a5b4164b5a10943c0d5283260252be30d0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 6 Feb 2007 08:01:00 -0800 Subject: Version abc70206 --- src/opt/bdc/bdc.h | 6 +- src/opt/bdc/bdcCore.c | 92 +++++++---- src/opt/bdc/bdcDec.c | 415 +++++++++++++++++++++++++++++++++++++++++++++++-- src/opt/bdc/bdcInt.h | 62 +++++--- src/opt/bdc/bdcTable.c | 140 +++++++++++++++++ src/opt/bdc/bdc_.c | 1 - 6 files changed, 648 insertions(+), 68 deletions(-) create mode 100644 src/opt/bdc/bdcTable.c (limited to 'src/opt/bdc') diff --git a/src/opt/bdc/bdc.h b/src/opt/bdc/bdc.h index f0976bfe..71875edb 100644 --- a/src/opt/bdc/bdc.h +++ b/src/opt/bdc/bdc.h @@ -20,7 +20,7 @@ #ifndef __BDC_H__ #define __BDC_H__ - + #ifdef __cplusplus extern "C" { #endif @@ -57,8 +57,8 @@ struct Bdc_Par_t_ /*=== bdcCore.c ==========================================================*/ extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); -extern void Bdc_ManAlloc( Bdc_Man_t * p ); -extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit ); +extern void Bdc_ManFree( Bdc_Man_t * p ); +extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesLimit ); #ifdef __cplusplus diff --git a/src/opt/bdc/bdcCore.c b/src/opt/bdc/bdcCore.c index f120ac3f..157927b1 100644 --- a/src/opt/bdc/bdcCore.c +++ b/src/opt/bdc/bdcCore.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "abc.h" #include "bdcInt.h" //////////////////////////////////////////////////////////////////////// @@ -43,32 +42,50 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) { Bdc_Man_t * p; - int i; + unsigned * pData; + int i, k, nBits; p = ALLOC( Bdc_Man_t, 1 ); memset( p, 0, sizeof(Bdc_Man_t) ); assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 ); p->pPars = pPars; + p->nWords = Kit_TruthWordNum( pPars->nVarsMax ); + p->nDivsLimit = 200; + p->nNodesLimit = 0; // will be set later // memory p->vMemory = Vec_IntStart( 1 << 16 ); // internal nodes - p->nNodesAlloc = 256; + p->nNodesAlloc = 512; p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc ); // set up hash table p->nTableSize = (1 << p->pPars->nVarsMax); p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize ); memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize ); p->vSpots = Vec_IntAlloc( 256 ); - // set up constant 1 and elementary variables - for ( i = 0; i < pPars->nVarsMax; i++ ) + // truth tables + p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords ); + // set elementary truth tables + nBits = (1 << pPars->nVarsMax); + Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars ); + for ( k = 0; k < pPars->nVarsMax; k++ ) { + pData = Vec_PtrEntry( p->vTruths, k+1 ); + Kit_TruthClear( pData, p->nVars ); + for ( i = 0; i < nBits; i++ ) + if ( i & (1 << k) ) + pData[i>>5] |= (1 << (i&31)); } - p->nNodes = pPars->nVarsMax + 1; - // remember the current place in memory - p->nMemStart = Vec_IntSize( p->vMemory ); + p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 ); + p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 ); + p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 ); + p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 ); + // start the internal ISFs + p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL ); + 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; } - /**Function************************************************************* Synopsis [Deallocate resynthesis manager.] @@ -80,15 +97,21 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -void Bdc_ManAlloc( Bdc_Man_t * p ) +void Bdc_ManFree( Bdc_Man_t * p ) { + Vec_IntFree( p->vMemory ); + Vec_IntFree( p->vSpots ); + Vec_PtrFree( p->vTruths ); + free( p->pNodes ); + free( p->pTable ); + free( p ); } /**Function************************************************************* - Synopsis [Sets up the divisors.] + Synopsis [Clears the manager.] - Description [The first n+1 entries are const1 and elem variables.] + Description [] SideEffects [] @@ -97,23 +120,31 @@ void Bdc_ManAlloc( Bdc_Man_t * p ) ***********************************************************************/ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) { - Bdc_Fun_t ** pSpot, * pFunc; unsigned * puTruth; + Bdc_Fun_t * pNode; int i; - // clean hash table - Vec_PtrForEachEntry( p->vSpots, pSpot, i ) - *pSpot = NULL; - // reset nodes - p->nNodes = p->pPars->nVarsMax + 1; - // reset memory - Vec_IntShrink( p->vMemory, p->nMemStart ); - // add new nodes to the hash table + Bdc_TableClear( p ); + Vec_IntClear( p->vMemory ); + // add constant 1 and elementary vars + p->nNodes = p->nNodesNew = 0; + for ( i = 0; i <= p->pPars->nVarsMax; i++ ) + { + pNode = Bdc_FunNew( p ); + pNode->Type = BDC_TYPE_PI; + pNode->puFunc = Vec_PtrEntry( p->vTruths, i ); + pNode->uSupp = i? (1 << (i-1)) : 0; + Bdc_TableAdd( p, pNode ); + } + // add the divisors Vec_PtrForEachEntry( vDivs, puTruth, i ) { - pFunc = Bdc_ManNewNode( p ); - pFunc->Type = BDC_TYPE_PI; - pFunc->puFunc = puTruth; - pFunc->uSupp = Kit_TruthSupport( puTruth, p->nVars ); + pNode = Bdc_FunNew( p ); + pNode->Type = BDC_TYPE_PI; + pNode->puFunc = puTruth; + pNode->uSupp = Kit_TruthSupport( puTruth, p->nVars ); + Bdc_TableAdd( p, pNode ); + if ( i == p->nDivsLimit ) + break; } } @@ -128,25 +159,26 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) SeeAlso [] ***********************************************************************/ -int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit ) +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; // set current manager parameters p->nVars = nVars; p->nWords = Kit_TruthWordNum( nVars ); - p->nNodeLimit = nNodeLimit; Bdc_ManPrepare( p, vDivs ); + p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc; // copy the function + Bdc_IsfStart( p, pIsf ); + Bdc_IsfClean( pIsf ); pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars ); - pIsf->puOn = Vec_IntFetch( p->vMemory, p->nWords ); - pIsf->puOff = Vec_IntFetch( p->vMemory, p->nWords ); Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars ); Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars ); // call decomposition + Bdc_SuppMinimize( p, pIsf ); p->pRoot = Bdc_ManDecompose_rec( p, pIsf ); if ( p->pRoot == NULL ) return -1; - return p->nNodes - (p->pPars->nVarsMax + 1); + return p->nNodesNew; } diff --git a/src/opt/bdc/bdcDec.c b/src/opt/bdc/bdcDec.c index 1fbea911..747fcb14 100644 --- a/src/opt/bdc/bdcDec.c +++ b/src/opt/bdc/bdcDec.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [bdc_.c] + FileName [bdcDec.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Truth-table-based bi-decomposition engine.] - Synopsis [] + Synopsis [Decomposition procedures.] Author [Alan Mishchenko] @@ -14,17 +14,19 @@ Date [Ver. 1.0. Started - January 30, 2007.] - Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] + Revision [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "abc.h" #include "bdcInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ); +static int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -43,31 +45,414 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) { Bdc_Fun_t * pFunc; - Bdc_Isf_t IsfA, * pIsfA = &IsfA; - Bdc_Isf_t IsfB, * pIsfB = &IsfB; - int Type; - Bdc_SuppMinimize( p, pIsf ); + Bdc_Isf_t IsfL, * pIsfL = &IsfL; + Bdc_Isf_t IsfB, * pIsfR = &IsfB; + // check computed results if ( pFunc = Bdc_TableLookup( p, pIsf ) ) return pFunc; - pFunc = Bdc_ManNewNode( p ); - pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfA, pIsfB ); - pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfA ); - if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfA, pIsfB, pFunc->pFan0->puFunc ) ) + // decide on the decomposition type + pFunc = Bdc_FunNew( p ); + if ( pFunc == NULL ) + return NULL; + pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR ); + // decompose the left branch + pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL ); + if ( pFunc->pFan0 == NULL ) + return NULL; + // decompose the right branch + if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) ) { p->nNodes--; return pFunc->pFan0; } - pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfA ); - pFunc->puFunc = Vec_IntFetch( p->vMemory, p->nWords ); - pFunc->puFunc = + pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL ); + if ( pFunc->pFan1 == NULL ) + return NULL; + // compute the function of node + pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); + if ( pFunc->Type == BDC_TYPE_AND ) + Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars ); + else if ( pFunc->Type == BDC_TYPE_OR ) + Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars ); + else + assert( 0 ); + // verify correctness + assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) ); + // convert from OR to AND + if ( pFunc->Type == BDC_TYPE_OR ) + { + pFunc->Type = BDC_TYPE_AND; + pFunc->pFan0 = Bdc_Not(pFunc->pFan0); + pFunc->pFan1 = Bdc_Not(pFunc->pFan1); + Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars ); + pFunc = Bdc_Not(pFunc); + } + Bdc_TableAdd( p, Bdc_Regular(pFunc) ); + return pFunc; +} + +/**Function************************************************************* + + Synopsis [Updates the ISF of the right after the left was decompoosed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type ) +{ + if ( Type == BDC_TYPE_OR ) + { +// Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes ); +// Right.R = bdd_exist( R, setRightRes ); + +// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q ); +// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R ); +// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V ); Cudd_Ref( pR->Q ); +// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R ); + +// assert( pR->R != b0 ); +// return (int)( pR->Q == b0 ); + + Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars ); + Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); + Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); + assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) ); + return Kit_TruthIsConst0(pIsfR->puOn, p->nVars); + } + else if ( Type == BDC_TYPE_AND ) + { +// Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes ); +// Right.Q = bdd_exist( Q, setRightRes ); + +// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q ); +// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R ); +// pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V ); Cudd_Ref( pR->R ); +// pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V ); Cudd_Ref( pR->Q ); + +// assert( pR->Q != b0 ); +// return (int)( pR->R == b0 ); + + Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars ); + Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); + Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); + assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) ); + return Kit_TruthIsConst0(pIsfR->puOn, p->nVars); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Checks existence of OR-bidecomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars ) +{ + assert( nLeftVars > 0 ); + assert( nRightVars > 0 ); + // compute the decomposition coefficient + if ( nLeftVars >= nRightVars ) + return BDC_SCALE * (p->nVars * nRightVars + nLeftVars); + else // if ( nLeftVars < nRightVars ) + return BDC_SCALE * (p->nVars * nLeftVars + nRightVars); +} + +/**Function************************************************************* + + Synopsis [Checks existence of weak OR-bidecomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) +{ + char pVars[16]; + int v, nVars, Beg, End; + + assert( pIsfL->uSupp == 0 ); + assert( pIsfR->uSupp == 0 ); + + // fill in the variables + nVars = 0; + for ( v = 0; v < p->nVars; v++ ) + if ( pIsf->uSupp & (1 << v) ) + pVars[nVars++] = v; + + // try variable pairs + for ( Beg = 0; Beg < nVars; Beg++ ) + { + Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] ); + for ( End = nVars - 1; End > Beg; End-- ) + { + Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] ); + if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) ) + { + pIsfL->uSupp = (1 << Beg); + pIsfR->uSupp = (1 << End); + pIsfL->Var = Beg; + pIsfR->Var = End; + return 1; + } + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Checks existence of weak OR-bidecomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) +{ + int v, VarCost, VarBest, Cost, VarCostBest = 0; + + for ( v = 0; v < p->nVars; v++ ) + { + Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v ); +// if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse ) +// Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist ); +// if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 ) + if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) ) + { + // measure the cost of this variable +// VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube ); + +// Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ ); +// VarCost = Kit_TruthCountOnes( Univ, p->nVars ); +// Cudd_RecursiveDeref( dd, Univ ); + + Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v ); + VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars ); + if ( VarCost == 0 ) + VarCost = 1; + if ( VarCostBest < VarCost ) + { + VarCostBest = VarCost; + VarBest = v; + } + } + } + + // derive the components for weak-bi-decomposition if the variable is found + if ( VarCostBest ) + { +// funQLeftRes = Q & bdd_exist( R, setRightORweak ); + +// Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp ); +// pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q ); +// Cudd_RecursiveDeref( dd, Temp ); + + Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest ); + Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars ); + +// pL->R = pF->R; Cudd_Ref( pL->R ); +// pL->V = VarBest; Cudd_Ref( pL->V ); + Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars ); + pIsfL->Var = VarBest; + +// assert( pL->Q != b0 ); +// assert( pL->R != b0 ); +// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 ); + + // express cost in percents of the covered boolean space + Cost = VarCostBest * BDC_SCALE / (1<nVars); + if ( Cost == 0 ) + Cost = 1; + return Cost; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Checks existence of OR-bidecomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) +{ + unsigned uSuppRem; + int v, nLeftVars = 1, nRightVars = 1; + // clean the var sets + Bdc_IsfClean( pIsfL ); + Bdc_IsfClean( pIsfR ); + // find initial variable sets + if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) ) + return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR ); + // prequantify the variables in the offset + Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var ); + Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var ); + // go through the remaining variables + uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp; + assert( Kit_WordCountOnes(uSuppRem) > 0 ); + for ( v = 0; v < p->nVars; v++ ) + { + if ( (uSuppRem & (1 << v)) == 0 ) + continue; + // prequantify this variable + Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v ); + Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v ); + if ( nLeftVars < nRightVars ) + { +// if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse ) +// if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) ) + if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) ) + { +// pL->V &= VarNew; + pIsfL->uSupp |= (1 << v); + nLeftVars++; + } +// else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse ) + else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) ) + { +// pR->V &= VarNew; + pIsfR->uSupp |= (1 << v); + nRightVars++; + } + } + else + { +// if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse ) + if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) ) + { +// pR->V &= VarNew; + pIsfR->uSupp |= (1 << v); + nRightVars++; + } +// else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse ) + else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) ) + { +// pL->V &= VarNew; + pIsfL->uSupp |= (1 << v); + nLeftVars++; + } + } + } + + // derive the functions Q and R for the left branch +// pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V ); +// pL->R = bdd_exist( pF->R, pR->V ); +// Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( Temp ); +// pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q ); +// Cudd_RecursiveDeref( dd, Temp ); +// pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R ); + Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars ); + Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uSupp ); + Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars ); + // derive the functions Q and R for the right branch +// Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp ); +// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q ); +// Cudd_RecursiveDeref( dd, Temp ); +// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R ); +/* + Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars ); + Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); + Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars ); +*/ +// assert( pL->Q != b0 ); +// assert( pL->R != b0 ); +// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 ); + assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) ); + assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) ); + assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) ); + + return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars ); } +/**Function************************************************************* + + Synopsis [Performs one step of bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] +***********************************************************************/ +Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) +{ + int CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR; + + Bdc_IsfClean( p->pIsfOL ); + Bdc_IsfClean( p->pIsfOR ); + Bdc_IsfClean( p->pIsfAL ); + Bdc_IsfClean( p->pIsfAR ); + + // perform OR decomposition + CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR ); + + // perform AND decomposition + Bdc_IsfNot( pIsf ); + CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR ); + Bdc_IsfNot( pIsf ); + Bdc_IsfNot( p->pIsfAL ); + Bdc_IsfNot( p->pIsfAR ); + + // check the hash table + Bdc_SuppMinimize( p, p->pIsfOL ); + CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL); + Bdc_SuppMinimize( p, p->pIsfOR ); + CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL); + Bdc_SuppMinimize( p, p->pIsfAL ); + CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL); + Bdc_SuppMinimize( p, p->pIsfAR ); + CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL); + + // check if there is any reuse for the components + if ( CostOrL + CostOrR < CostAndL + CostAndR ) + { + Bdc_IsfCopy( pIsfL, p->pIsfOL ); + Bdc_IsfCopy( pIsfR, p->pIsfOR ); + return BDC_TYPE_OR; + } + if ( CostOrL + CostOrR > CostAndL + CostAndR ) + { + Bdc_IsfCopy( pIsfL, p->pIsfAL ); + Bdc_IsfCopy( pIsfR, p->pIsfAR ); + return BDC_TYPE_AND; + } + + // compare the two-component costs + if ( CostOr < CostAnd ) + { + Bdc_IsfCopy( pIsfL, p->pIsfOL ); + Bdc_IsfCopy( pIsfR, p->pIsfOR ); + return BDC_TYPE_OR; + } + return BDC_TYPE_AND; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/bdc/bdcInt.h b/src/opt/bdc/bdcInt.h index 39d50ae9..65ab9d27 100644 --- a/src/opt/bdc/bdcInt.h +++ b/src/opt/bdc/bdcInt.h @@ -29,13 +29,15 @@ extern "C" { /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#include "dec.h" +#include "kit.h" #include "bdc.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#define BDC_SCALE 100 // value used to compute the cost + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -46,18 +48,19 @@ typedef enum { BDC_TYPE_CONST1, // 1: constant 1 BDC_TYPE_PI, // 2: primary input BDC_TYPE_AND, // 4: AND-gate - BDC_TYPE_XOR, // 5: XOR-gate - BDC_TYPE_MUX, // 6: MUX-gate - BDC_TYPE_OTHER // 7: unused + BDC_TYPE_OR, // 5: OR-gate (temporary) + BDC_TYPE_XOR, // 6: XOR-gate + BDC_TYPE_MUX, // 7: MUX-gate + BDC_TYPE_OTHER // 8: unused } Bdc_Type_t; typedef struct Bdc_Fun_t_ Bdc_Fun_t; struct Bdc_Fun_t_ { int Type; // Const1, PI, AND, XOR, MUX - Bdc_Fun_t * pFan0; // next function with same support - Bdc_Fun_t * pFan1; // next function with same support - Bdc_Fun_t * pFan2; // next function with same support + Bdc_Fun_t * pFan0; // fanin of the given node + Bdc_Fun_t * pFan1; // fanin of the given node + Bdc_Fun_t * pFan2; // fanin of the given node unsigned uSupp; // bit mask of current support unsigned * puFunc; // the function of the node Bdc_Fun_t * pNext; // next function with same support @@ -67,11 +70,10 @@ struct Bdc_Fun_t_ typedef struct Bdc_Isf_t_ Bdc_Isf_t; struct Bdc_Isf_t_ { - unsigned uSupp; // bit mask of current support - unsigned uUnique; // bit mask of unique support + int Var; // the first variable assigned + unsigned uSupp; // the current support unsigned * puOn; // on-set unsigned * puOff; // off-set - int Cost; // cost of this component }; typedef struct Bdc_Man_t_ Bdc_Man_t; @@ -81,25 +83,44 @@ struct Bdc_Man_t_ Bdc_Par_t * pPars; // parameter set int nVars; // the number of variables int nWords; // the number of words - int nNodeLimit; // the limit on the number of new nodes + int nNodesLimit; // the limit on the number of new nodes + int nDivsLimit; // the limit on the number of divisors // internal nodes Bdc_Fun_t * pNodes; // storage for decomposition nodes int nNodes; // the number of nodes used + int nNodesNew; // the number of nodes used int nNodesAlloc; // the number of nodes allocated Bdc_Fun_t * pRoot; // the root node // resub candidates Bdc_Fun_t ** pTable; // hash table of candidates int nTableSize; // hash table size (1 << nVarsMax) + Vec_Int_t * vSpots; // the occupied spots in the table + // elementary truth tables + Vec_Ptr_t * vTruths; // for const 1 and elementary variables + unsigned * puTemp1; // temporary truth table + unsigned * puTemp2; // temporary truth table + unsigned * puTemp3; // temporary truth table + unsigned * puTemp4; // temporary truth table + // temporary ISFs + Bdc_Isf_t * pIsfOL, IsfOL; + Bdc_Isf_t * pIsfOR, IsfOR; + Bdc_Isf_t * pIsfAL, IsfAL; + Bdc_Isf_t * pIsfAR, IsfAR; // internal memory manager Vec_Int_t * vMemory; // memory for internal truth tables - int nMemStart; // the starting memory size }; // working with complemented attributes of objects -static inline bool Bdc_IsComplement( Bdc_Fun_t * p ) { return (bool)((unsigned long)p & (unsigned long)01); } -static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); } -static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); } -static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); } +static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((unsigned long)p & (unsigned long)01); } +static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); } +static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); } +static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); } + +static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; } +static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); } +static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->Var = 0; } +static inline void Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q ) { Bdc_Isf_t T = *p; *p = *q; *q = T; } +static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT; } //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// @@ -109,11 +130,14 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== bdcSupp.c ==========================================================*/ -extern int Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); +/*=== bdcDec.c ==========================================================*/ +extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); /*=== 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/opt/bdc/bdcTable.c b/src/opt/bdc/bdcTable.c new file mode 100644 index 00000000..d86a938d --- /dev/null +++ b/src/opt/bdc/bdcTable.c @@ -0,0 +1,140 @@ +/**CFile**************************************************************** + + FileName [bdcTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Truth-table-based bi-decomposition engine.] + + Synopsis [Hash table for intermediate nodes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 30, 2007.] + + Revision [$Id: bdcTable.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bdcInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// 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; + // 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.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth ) +{ + return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) && + Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars ); +} + +/**Function************************************************************* + + Synopsis [Adds the new entry to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) +{ + Bdc_Fun_t * pFunc; + for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext ) + if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) ) + return pFunc; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Adds the new entry to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc ) +{ + if ( p->pTable[pFunc->uSupp] == NULL ) + Vec_IntPush( p->vSpots, pFunc->uSupp ); + pFunc->pNext = p->pTable[pFunc->uSupp]; + p->pTable[pFunc->uSupp] = pFunc; +} + +/**Function************************************************************* + + Synopsis [Adds the new entry to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_TableClear( Bdc_Man_t * p ) +{ + int Spot, i; + Vec_IntForEachEntry( p->vSpots, Spot, i ) + p->pTable[Spot] = NULL; + Vec_IntClear( p->vSpots ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/bdc/bdc_.c b/src/opt/bdc/bdc_.c index 0fa51092..9d0a9462 100644 --- a/src/opt/bdc/bdc_.c +++ b/src/opt/bdc/bdc_.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "abc.h" #include "bdcInt.h" //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3