diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-12 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-12 08:01:00 -0700 |
commit | c5277d3334e3dbca556fbf82bbe1c0cacdc85cb1 (patch) | |
tree | c6ea67f6b0a823cc097de6b61c9195ffafdb08b1 /src/opt/bdc | |
parent | 066726076deedaf6d5b38ee4ed27eeb4a2b0061a (diff) | |
download | abc-c5277d3334e3dbca556fbf82bbe1c0cacdc85cb1.tar.gz abc-c5277d3334e3dbca556fbf82bbe1c0cacdc85cb1.tar.bz2 abc-c5277d3334e3dbca556fbf82bbe1c0cacdc85cb1.zip |
Version abc70712
Diffstat (limited to 'src/opt/bdc')
-rw-r--r-- | src/opt/bdc/bdc.h | 73 | ||||
-rw-r--r-- | src/opt/bdc/bdcCore.c | 189 | ||||
-rw-r--r-- | src/opt/bdc/bdcDec.c | 461 | ||||
-rw-r--r-- | src/opt/bdc/bdcInt.h | 151 | ||||
-rw-r--r-- | src/opt/bdc/bdcTable.c | 140 | ||||
-rw-r--r-- | src/opt/bdc/bdc_.c | 49 | ||||
-rw-r--r-- | src/opt/bdc/module.make | 8 |
7 files changed, 0 insertions, 1071 deletions
diff --git a/src/opt/bdc/bdc.h b/src/opt/bdc/bdc.h deleted file mode 100644 index 71875edb..00000000 --- a/src/opt/bdc/bdc.h +++ /dev/null @@ -1,73 +0,0 @@ -/**CFile**************************************************************** - - FileName [bdc.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Truth-table-based bi-decomposition engine.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 30, 2007.] - - Revision [$Id: bdc.h,v 1.00 2007/01/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __BDC_H__ -#define __BDC_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Bdc_Man_t_ Bdc_Man_t; -typedef struct Bdc_Par_t_ Bdc_Par_t; -struct Bdc_Par_t_ -{ - // general parameters - int nVarsMax; // the maximum support - int fVerbose; // enable basic stats - int fVeryVerbose; // enable detailed stats -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== bdcCore.c ==========================================================*/ -extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); -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 -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/opt/bdc/bdcCore.c b/src/opt/bdc/bdcCore.c deleted file mode 100644 index 157927b1..00000000 --- a/src/opt/bdc/bdcCore.c +++ /dev/null @@ -1,189 +0,0 @@ -/**CFile**************************************************************** - - FileName [bdcCore.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Truth-table-based bi-decomposition engine.] - - Synopsis [The gateway to bi-decomposition.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 30, 2007.] - - Revision [$Id: bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "bdcInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocate resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) -{ - Bdc_Man_t * p; - 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 = 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 ); - // 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->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.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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 [Clears the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) -{ - unsigned * puTruth; - Bdc_Fun_t * pNode; - int i; - 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 ) - { - 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; - } -} - -/**Function************************************************************* - - Synopsis [Performs decomposition of one function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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 ); - 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 ); - 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->nNodesNew; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/bdc/bdcDec.c b/src/opt/bdc/bdcDec.c deleted file mode 100644 index 747fcb14..00000000 --- a/src/opt/bdc/bdcDec.c +++ /dev/null @@ -1,461 +0,0 @@ -/**CFile**************************************************************** - - FileName [bdcDec.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Truth-table-based bi-decomposition engine.] - - Synopsis [Decomposition procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 30, 2007.] - - Revision [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#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 /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs one step of bi-decomposition.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) -{ - Bdc_Fun_t * pFunc; - Bdc_Isf_t IsfL, * pIsfL = &IsfL; - Bdc_Isf_t IsfB, * pIsfR = &IsfB; - // check computed results - if ( pFunc = Bdc_TableLookup( p, pIsf ) ) - return pFunc; - // 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, 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<<p->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 deleted file mode 100644 index 65ab9d27..00000000 --- a/src/opt/bdc/bdcInt.h +++ /dev/null @@ -1,151 +0,0 @@ -/**CFile**************************************************************** - - FileName [bdcInt.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Truth-table-based bi-decomposition engine.] - - Synopsis [Internal declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __BDC_INT_H__ -#define __BDC_INT_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "kit.h" -#include "bdc.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -#define BDC_SCALE 100 // value used to compute the cost - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -// network types -typedef enum { - BDC_TYPE_NONE = 0, // 0: unknown - BDC_TYPE_CONST1, // 1: constant 1 - BDC_TYPE_PI, // 2: primary input - BDC_TYPE_AND, // 4: AND-gate - 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; // 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 - void * pCopy; // the copy field -}; - -typedef struct Bdc_Isf_t_ Bdc_Isf_t; -struct Bdc_Isf_t_ -{ - int Var; // the first variable assigned - unsigned uSupp; // the current support - unsigned * puOn; // on-set - unsigned * puOff; // off-set -}; - -typedef struct Bdc_Man_t_ Bdc_Man_t; -struct Bdc_Man_t_ -{ - // external parameters - Bdc_Par_t * pPars; // parameter set - int nVars; // the number of variables - int nWords; // the number of words - 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 -}; - -// working with complemented attributes of objects -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 /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== 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 -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/opt/bdc/bdcTable.c b/src/opt/bdc/bdcTable.c deleted file mode 100644 index d86a938d..00000000 --- a/src/opt/bdc/bdcTable.c +++ /dev/null @@ -1,140 +0,0 @@ -/**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 deleted file mode 100644 index 9d0a9462..00000000 --- a/src/opt/bdc/bdc_.c +++ /dev/null @@ -1,49 +0,0 @@ -/**CFile**************************************************************** - - FileName [bdc_.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Truth-table-based bi-decomposition engine.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 30, 2007.] - - Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "bdcInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/bdc/module.make b/src/opt/bdc/module.make deleted file mode 100644 index 85936f5b..00000000 --- a/src/opt/bdc/module.make +++ /dev/null @@ -1,8 +0,0 @@ -SRC += src/opt/res/resCore.c \ - src/opt/res/resDivs.c \ - src/opt/res/resFilter.c \ - src/opt/res/resSat.c \ - src/opt/res/resSim.c \ - src/opt/res/resStrash.c \ - src/opt/res/resUpdate.c \ - src/opt/res/resWin.c |