diff options
Diffstat (limited to 'src/aig/bdc')
-rw-r--r-- | src/aig/bdc/bdc.h | 92 | ||||
-rw-r--r-- | src/aig/bdc/bdcCore.c | 314 | ||||
-rw-r--r-- | src/aig/bdc/bdcDec.c | 751 | ||||
-rw-r--r-- | src/aig/bdc/bdcInt.h | 165 | ||||
-rw-r--r-- | src/aig/bdc/bdcSpfd.c | 1176 | ||||
-rw-r--r-- | src/aig/bdc/bdcTable.c | 134 | ||||
-rw-r--r-- | src/aig/bdc/bdc_.c | 54 | ||||
-rw-r--r-- | src/aig/bdc/module.make | 5 |
8 files changed, 0 insertions, 2691 deletions
diff --git a/src/aig/bdc/bdc.h b/src/aig/bdc/bdc.h deleted file mode 100644 index 8a240b0c..00000000 --- a/src/aig/bdc/bdc.h +++ /dev/null @@ -1,92 +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__ - - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - - - -ABC_NAMESPACE_HEADER_START - - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Bdc_Fun_t_ Bdc_Fun_t; -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 -}; - -// working with complemented attributes of objects -static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((ABC_PTRUINT_T)p & (ABC_PTRUINT_T)01); } -static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((ABC_PTRUINT_T)p & ~(ABC_PTRUINT_T)01); } -static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((ABC_PTRUINT_T)p ^ (ABC_PTRUINT_T)01); } -static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((ABC_PTRUINT_T)p ^ (ABC_PTRUINT_T)(c!=0)); } - -//////////////////////////////////////////////////////////////////////// -/// 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 nNodesMax ); -extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ); -extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ); -extern int Bdc_ManNodeNum( Bdc_Man_t * p ); -extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ); -extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ); -extern void * Bdc_FuncCopy( Bdc_Fun_t * p ); -extern int Bdc_FuncCopyInt( Bdc_Fun_t * p ); -extern void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy ); -extern void Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy ); - - - -ABC_NAMESPACE_HEADER_END - - - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c deleted file mode 100644 index 58324f81..00000000 --- a/src/aig/bdc/bdcCore.c +++ /dev/null @@ -1,314 +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" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Accessing contents of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ) { return Bdc_FunWithId(p, i); } -Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ) { return p->pRoot; } -int Bdc_ManNodeNum( Bdc_Man_t * p ) { return p->nNodes; } -Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ) { return p->pFan0; } -Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ) { return p->pFan1; } -void * Bdc_FuncCopy( Bdc_Fun_t * p ) { return p->pCopy; } -int Bdc_FuncCopyInt( Bdc_Fun_t * p ) { return p->iCopy; } -void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy ) { p->pCopy = pCopy; } -void Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy ) { p->iCopy = iCopy; } - -/**Function************************************************************* - - Synopsis [Allocate resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) -{ - Bdc_Man_t * p; - p = ABC_ALLOC( Bdc_Man_t, 1 ); - memset( p, 0, sizeof(Bdc_Man_t) ); - assert( pPars->nVarsMax > 1 && pPars->nVarsMax < 16 ); - p->pPars = pPars; - p->nWords = Kit_TruthWordNum( pPars->nVarsMax ); - p->nDivsLimit = 200; - // internal nodes - p->nNodesAlloc = 512; - p->pNodes = ABC_ALLOC( Bdc_Fun_t, p->nNodesAlloc ); - // memory - p->vMemory = Vec_IntStart( 8 * p->nWords * p->nNodesAlloc ); - Vec_IntClear(p->vMemory); - // set up hash table - p->nTableSize = (1 << p->pPars->nVarsMax); - p->pTable = ABC_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_PtrAllocTruthTables( p->pPars->nVarsMax ); - p->puTemp1 = ABC_ALLOC( unsigned, 4 * p->nWords ); - p->puTemp2 = p->puTemp1 + p->nWords; - p->puTemp3 = p->puTemp2 + p->nWords; - p->puTemp4 = p->puTemp3 + p->nWords; - // 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 ) -{ - 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) ); - ABC_PRT( "Cache", p->timeCache ); - ABC_PRT( "Check", p->timeCheck ); - ABC_PRT( "Muxes", p->timeMuxes ); - ABC_PRT( "Supps", p->timeSupps ); - ABC_PRT( "TOTAL", p->timeTotal ); - } - Vec_IntFree( p->vMemory ); - Vec_IntFree( p->vSpots ); - Vec_PtrFree( p->vTruths ); - ABC_FREE( p->puTemp1 ); - ABC_FREE( p->pNodes ); - ABC_FREE( p->pTable ); - ABC_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 = 0; - p->nNodesNew = - 1 - p->nVars - (vDivs? Vec_PtrSize(vDivs) : 0); - // add constant 1 - pNode = Bdc_FunNew( p ); - pNode->Type = BDC_TYPE_CONST1; - pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); - Kit_TruthFill( pNode->puFunc, p->nVars ); - pNode->uSupp = 0; - Bdc_TableAdd( p, pNode ); - // add variables - for ( i = 0; i < p->nVars; i++ ) - { - pNode = Bdc_FunNew( p ); - pNode->Type = BDC_TYPE_PI; - pNode->puFunc = (unsigned *)Vec_PtrEntry( p->vTruths, i ); - pNode->uSupp = (1 << i); - Bdc_TableAdd( p, pNode ); - } - // add the divisors - if ( vDivs ) - Vec_PtrForEachEntry( unsigned *, 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; - } - assert( p->nNodesNew == 0 ); -} - -/**Function************************************************************* - - Synopsis [Clears the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_ManDecPrint( Bdc_Man_t * p ) -{ - Bdc_Fun_t * pNode; - int i; - printf( " 0 : Const 1\n" ); - for ( i = 1; i < p->nNodes; i++ ) - { - printf( " %d : ", i ); - pNode = p->pNodes + i; - if ( pNode->Type == BDC_TYPE_PI ) - printf( "PI " ); - else - { - printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) ); - printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) ); - } - Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) ); - printf( "\n" ); - } - printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) ); -} - -/**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; - int clk = clock(); - assert( nVars <= p->pPars->nVarsMax ); - // set current manager parameters - p->nVars = nVars; - p->nWords = Kit_TruthWordNum( nVars ); - p->nNodesMax = nNodesMax; - Bdc_ManPrepare( p, vDivs ); - if ( puCare && Kit_TruthIsConst0( puCare, nVars ) ) - { - p->pRoot = Bdc_Not(p->pNodes); - return 0; - } - // copy the function - Bdc_IsfStart( p, pIsf ); - if ( puCare ) - { - Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars ); - Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars ); - } - else - { - Kit_TruthCopy( pIsf->puOn, puFunc, p->nVars ); - Kit_TruthNot( pIsf->puOff, puFunc, p->nVars ); - } - 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; -} - -/**Function************************************************************* - - Synopsis [Performs decomposition of one function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_ManDecomposeTest( unsigned uTruth, int nVars ) -{ - static int Counter = 0; - static int Total = 0; - Bdc_Par_t Pars = {0}, * pPars = &Pars; - Bdc_Man_t * p; - int RetValue; -// unsigned uCare = ~0x888f888f; - unsigned uCare = ~0; -// unsigned uFunc = 0x88888888; -// unsigned uFunc = 0xf888f888; -// unsigned uFunc = 0x117e117e; -// unsigned uFunc = 0x018b018b; - unsigned uFunc = uTruth; - - pPars->nVarsMax = 8; - p = Bdc_ManAlloc( pPars ); - RetValue = Bdc_ManDecompose( p, &uFunc, &uCare, nVars, NULL, 1000 ); - Total += RetValue; - printf( "%5d : Nodes = %5d. Total = %8d.\n", ++Counter, RetValue, Total ); -// Bdc_ManDecPrint( p ); - Bdc_ManFree( p ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c deleted file mode 100644 index 61f46f17..00000000 --- a/src/aig/bdc/bdcDec.c +++ /dev/null @@ -1,751 +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" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// 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; - int clk = 0; // Suppress "might be used uninitialized" - 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; - int clk = 0; // Suppress "might be used uninitialized" - 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.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type ) -{ - unsigned * puTruth = p->puTemp1; - // get the truth table of the left branch - if ( Bdc_IsComplement(pFunc0) ) - Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars ); - else - Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars ); - // split into parts - 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->uUniq ); - Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq ); -// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) ); - 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_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars ); - Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq ); - Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq ); -// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) ); - assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) ); - return Kit_TruthIsConst0(pIsfR->puOff, 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->uUniq = (1 << pVars[Beg]); - pIsfR->uUniq = (1 << pVars[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; - int VarBest = -1; // Suppress "might be used uninitialized" - int Cost, VarCostBest = 0; - - for ( v = 0; v < p->nVars; v++ ) - { - if ( (pIsf->uSupp & (1 << v)) == 0 ) - continue; -// 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 ) - - Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v ); - 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->uUniq = (1 << VarBest); - pIsfR->uUniq = 0; - -// assert( pL->Q != b0 ); -// assert( pL->R != b0 ); -// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 ); -// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) ); - - // 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 uSupportRem; - int v, nLeftVars = 1, nRightVars = 1; - // clean the var sets - Bdc_IsfStart( p, pIsfL ); - Bdc_IsfStart( p, pIsfR ); - // check that the support is correct - assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) ); - assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) ); - // 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_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq ); - Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq ); - // go through the remaining variables - uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq; - for ( v = 0; v < p->nVars; v++ ) - { - if ( (uSupportRem & (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->uUniq |= (1 << v); - nLeftVars++; - Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars ); - } -// 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->uUniq |= (1 << v); - nRightVars++; - Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars ); - } - } - 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->uUniq |= (1 << v); - nRightVars++; - Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars ); - } -// 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->uUniq |= (1 << v); - nLeftVars++; - Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars ); - } - } - } - - // 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->uUniq ); - Kit_TruthCopy( pIsfL->puOff, p->puTemp2, 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) ); - - // 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->uUniq ); - Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars ); - - assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) ); - assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) ); -// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) ); - - assert( pIsfL->uUniq ); - assert( pIsfR->uUniq ); - 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 WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR; - - Bdc_IsfClean( p->pIsfOL ); - Bdc_IsfClean( p->pIsfOR ); - Bdc_IsfClean( p->pIsfAL ); - Bdc_IsfClean( p->pIsfAR ); - - // perform OR decomposition - WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR ); - - // perform AND decomposition - Bdc_IsfNot( pIsf ); - WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR ); - Bdc_IsfNot( pIsf ); - Bdc_IsfNot( p->pIsfAL ); - Bdc_IsfNot( p->pIsfAR ); - - // check the case when decomposition does not exist - if ( WeightOr == 0 && WeightAnd == 0 ) - { - Bdc_IsfCopy( pIsfL, p->pIsfOL ); - Bdc_IsfCopy( pIsfR, p->pIsfOR ); - return BDC_TYPE_MUX; - } - // check the hash table - assert( WeightOr || WeightAnd ); - WeightOrL = WeightOrR = 0; - if ( WeightOr ) - { - if ( p->pIsfOL->uUniq ) - { - Bdc_SuppMinimize( p, p->pIsfOL ); - WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL); - } - if ( p->pIsfOR->uUniq ) - { - Bdc_SuppMinimize( p, p->pIsfOR ); - WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL); - } - } - WeightAndL = WeightAndR = 0; - if ( WeightAnd ) - { - if ( p->pIsfAL->uUniq ) - { - Bdc_SuppMinimize( p, p->pIsfAL ); - WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL); - } - if ( p->pIsfAR->uUniq ) - { - Bdc_SuppMinimize( p, p->pIsfAR ); - WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL); - } - } - - // 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; - } - - // 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; -} - -/**Function************************************************************* - - Synopsis [Find variable that leads to minimum sum of support sizes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) -{ - int Var, VarMin, nSuppMin, nSuppCur; - unsigned uSupp0, uSupp1; - int clk = 0; // Suppress "might be used uninitialized" - if ( p->pPars->fVerbose ) - clk = clock(); - VarMin = -1; - nSuppMin = 1000; - for ( Var = 0; Var < p->nVars; Var++ ) - { - if ( (pIsf->uSupp & (1 << Var)) == 0 ) - continue; - Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, Var ); - Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var ); - Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, Var ); - Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var ); - uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars ); - uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars ); - nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1); - if ( nSuppMin > nSuppCur ) - { - nSuppMin = nSuppCur; - VarMin = Var; - break; - } - } - if ( VarMin >= 0 ) - { - Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, VarMin ); - Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin ); - Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, VarMin ); - Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin ); - Bdc_SuppMinimize( p, pIsfL ); - Bdc_SuppMinimize( p, pIsfR ); - } - if ( p->pPars->fVerbose ) - p->timeMuxes += clock() - clk; - return VarMin; -} - -/**Function************************************************************* - - Synopsis [Creates gates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc ) -{ - unsigned * puTruth = p->puTemp1; - if ( Bdc_IsComplement(pFunc) ) - Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars ); - else - Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars ); - return Bdc_TableCheckContainment( p, pIsf, puTruth ); -} - -/**Function************************************************************* - - Synopsis [Creates gates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type ) -{ - Bdc_Fun_t * pFunc; - pFunc = Bdc_FunNew( p ); - if ( pFunc == NULL ) - return NULL; - pFunc->Type = Type; - pFunc->pFan0 = pFunc0; - pFunc->pFan1 = pFunc1; - pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); - // get the truth table of the left branch - if ( Bdc_IsComplement(pFunc0) ) - Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars ); - else - Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars ); - // get the truth table of the right branch - if ( Bdc_IsComplement(pFunc1) ) - Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars ); - else - Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars ); - // compute the function of node - if ( pFunc->Type == BDC_TYPE_AND ) - { - Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars ); - } - else if ( pFunc->Type == BDC_TYPE_OR ) - { - Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars ); - // transform to AND gate - 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); - } - else - assert( 0 ); - // add to table - Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars ); - Bdc_TableAdd( p, Bdc_Regular(pFunc) ); - return pFunc; -} - -/**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 ) -{ -// int static Counter = 0; -// int LocalCounter = Counter++; - Bdc_Type_t Type; - Bdc_Fun_t * pFunc, * pFunc0, * pFunc1; - Bdc_Isf_t IsfL, * pIsfL = &IsfL; - Bdc_Isf_t IsfB, * pIsfR = &IsfB; - int iVar; - int clk = 0; // Suppress "might be used uninitialized" -/* -printf( "Init function (%d):\n", LocalCounter ); -Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n"); -Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n"); -*/ - // check computed results - assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) ); - 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 ) - { - 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 ) - return NULL; - pFunc = Bdc_FunWithId( p, iVar + 1 ); - pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND ); - pFunc1 = Bdc_ManCreateGate( p, pFunc, pFunc1, BDC_TYPE_AND ); - if ( pFunc0 == NULL || pFunc1 == NULL ) - return NULL; - pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR ); - } - else - { - pFunc0 = Bdc_ManDecompose_rec( p, pIsfL ); - if ( pFunc0 == NULL ) - return NULL; - // decompose the right branch - if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) ) - { - p->nNodesNew--; - return pFunc0; - } - Bdc_SuppMinimize( p, pIsfR ); - pFunc1 = Bdc_ManDecompose_rec( p, pIsfR ); - if ( pFunc1 == NULL ) - return NULL; - // create new gate - pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type ); - } - return pFunc; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h deleted file mode 100644 index 74630664..00000000 --- a/src/aig/bdc/bdcInt.h +++ /dev/null @@ -1,165 +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__ - - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "kit.h" -#include "bdc.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - - - -ABC_NAMESPACE_HEADER_START - - -#define BDC_SCALE 1000 // 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, // 3: AND-gate - BDC_TYPE_OR, // 4: OR-gate (temporary) - BDC_TYPE_XOR, // 5: XOR-gate - BDC_TYPE_MUX, // 6: MUX-gate - BDC_TYPE_OTHER // 7: unused -} Bdc_Type_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 - unsigned uSupp; // bit mask of current support - unsigned * puFunc; // the function of the node - Bdc_Fun_t * pNext; // next function with same support - union { int iCopy; // the literal of the node (AIG) - void * pCopy; }; // the function of the node (BDD or AIG) - -}; - -typedef struct Bdc_Isf_t_ Bdc_Isf_t; -struct Bdc_Isf_t_ -{ - unsigned uSupp; // the complete support of this component - unsigned uUniq; // the unique variables of this component - unsigned * puOn; // on-set - unsigned * puOff; // off-set -}; - -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 nNodesMax; // 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 nNodesAlloc; // the number of nodes allocated - int nNodes; // the number of all nodes created so far - int nNodesNew; // the number of new AND nodes created so far - 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 - // 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; -}; - -static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; } -static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id ) { assert( Id < p->nNodes ); return p->pNodes + Id; } -static inline int Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun ) { return pFun - p->pNodes; } -static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->uSupp = 0; pF->uUniq = 0; pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); assert( pF->puOff && pF->puOn ); } -static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->uUniq = 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 ); -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 int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth ); - - - -ABC_NAMESPACE_HEADER_END - - - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/aig/bdc/bdcSpfd.c b/src/aig/bdc/bdcSpfd.c deleted file mode 100644 index 2f05419d..00000000 --- a/src/aig/bdc/bdcSpfd.c +++ /dev/null @@ -1,1176 +0,0 @@ -/**CFile**************************************************************** - - FileName [bdcSpfd.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: bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "bdcInt.h" -#include "aig.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Bdc_Nod_t_ Bdc_Nod_t; -struct Bdc_Nod_t_ -{ - unsigned iFan0g : 8; - unsigned iFan0n : 12; - unsigned Type : 12; // 0-3 = AND; 4 = XOR - - unsigned iFan1g : 8; - unsigned iFan1n : 12; - unsigned Weight : 12; - - word Truth; -}; - -static word Truths[6] = { - 0xAAAAAAAAAAAAAAAA, - 0xCCCCCCCCCCCCCCCC, - 0xF0F0F0F0F0F0F0F0, - 0xFF00FF00FF00FF00, - 0xFFFF0000FFFF0000, - 0xFFFFFFFF00000000 -}; - -static inline int Bdc_CountOnes( word t ) -{ - t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555); - t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333); - t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F); - t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF); - t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF); - return (t & 0x00000000FFFFFFFF) + (t>>32); -} - -static inline int Bdc_CountSpfd( word t, word f ) -{ - int n00 = Bdc_CountOnes( ~t & ~f ); - int n01 = Bdc_CountOnes( t & ~f ); - int n10 = Bdc_CountOnes( ~t & f ); - int n11 = Bdc_CountOnes( t & f ); - return n00 * n11 + n10 * n01; -} - -static inline word Bdc_Cof6( word t, int iVar, int fCof1 ) -{ - assert( iVar >= 0 && iVar < 6 ); - if ( fCof1 ) - return (t & Truths[iVar]) | ((t & Truths[iVar]) >> (1<<iVar)); - else - return (t &~Truths[iVar]) | ((t &~Truths[iVar]) << (1<<iVar)); -} - -int Bdc_SpfdAdjCost( word t ) -{ - word c0, c1; - int v, Cost = 0; - for ( v = 0; v < 6; v++ ) - { - c0 = Bdc_Cof6( t, v, 0 ); - c1 = Bdc_Cof6( t, v, 1 ); - Cost += Bdc_CountOnes( c0 ^ c1 ); - } - return Cost; -} - - -extern void Abc_Show6VarFunc( word F0, word F1 ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdPrint_rec( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels ) -{ - assert( Level > 0 ); - printf( "(" ); - - if ( pNode->Type & 1 ) - printf( "!" ); - if ( pNode->iFan0g == 0 ) - printf( "%c", 'a' + pNode->iFan0n ); - else - { - Bdc_Nod_t * pNode0 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan0g); - Bdc_SpfdPrint_rec( pNode0 + pNode->iFan0n, pNode->iFan0g, vLevels ); - } - - if ( pNode->Type & 4 ) - printf( "+" ); - else - printf( "*" ); - - if ( pNode->Type & 2 ) - printf( "!" ); - if ( pNode->iFan1g == 0 ) - printf( "%c", 'a' + pNode->iFan1n ); - else - { - Bdc_Nod_t * pNode1 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan1g); - Bdc_SpfdPrint_rec( pNode1 + pNode->iFan1n, pNode->iFan1g, vLevels ); - } - - printf( ")" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels, word Truth ) -{ - word Diff = Truth ^ pNode->Truth; - Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( " " ); - Extra_PrintHex( stdout, (unsigned *)&Diff, 6 ); printf( " " ); - Bdc_SpfdPrint_rec( pNode, Level, vLevels ); - printf( " %d\n", pNode->Weight ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax ) -{ - int nSize = nCands * nCands * (nGatesMax + 1) * 5; - Vec_Ptr_t * vLevels; - Vec_Int_t * vBegs, * vWeight; - Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2; - int Count0, Count1, * pPerm; - int i, j, k, c, n, clk; - assert( nGatesMax < (1<<8) ); - assert( nCands < (1<<12) ); - assert( (1<<(nVars-1))*(1<<(nVars-1)) < (1<<12) ); // max SPFD - - printf( "Storage size = %d (%d * %d * %d * %d).\n", nSize, nCands, nCands, nGatesMax + 1, 5 ); - - printf( "SPFD = %d.\n", Bdc_CountOnes(Truth) * Bdc_CountOnes(~Truth) ); - - // consider elementary functions - if ( Truth == 0 || Truth == ~0 ) - { - printf( "Function is a constant.\n" ); - return; - } - for ( i = 0; i < nVars; i++ ) - if ( Truth == Truths[i] || Truth == ~Truths[i] ) - { - printf( "Function is an elementary variable.\n" ); - return; - } - - // allocate - vLevels = Vec_PtrAlloc( 100 ); - vBegs = Vec_IntAlloc( 100 ); - vWeight = Vec_IntAlloc( 100 ); - - // initialize elementary variables - pNode = ABC_CALLOC( Bdc_Nod_t, nVars ); - for ( i = 0; i < nVars; i++ ) - pNode[i].Truth = Truths[i]; - for ( i = 0; i < nVars; i++ ) - pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth ); - Vec_PtrPush( vLevels, pNode ); - Vec_IntPush( vBegs, nVars ); - - // the next level -clk = clock(); - pNode0 = pNode; - pNode = ABC_CALLOC( Bdc_Nod_t, 5 * nVars * (nVars - 1) / 2 ); - for ( c = i = 0; i < nVars; i++ ) - for ( j = i+1; j < nVars; j++ ) - { - pNode[c].Truth = pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0; - pNode[c].Truth = ~pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1; - pNode[c].Truth = pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2; - pNode[c].Truth = ~pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3; - pNode[c].Truth = pNode0[i].Truth ^ pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4; - } - assert( c == 5 * nVars * (nVars - 1) / 2 ); - Vec_PtrPush( vLevels, pNode ); - Vec_IntPush( vBegs, c ); - for ( i = 0; i < c; i++ ) - { - pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth ); -//Bdc_SpfdPrint( pNode + i, 1, vLevels ); - if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth ) - { - printf( "Function can be implemented using 1 gate.\n" ); - pNode = NULL; - goto cleanup; - } - } -printf( "Selected %6d gates on level %2d. ", c, 1 ); -Abc_PrintTime( 1, "Time", clock() - clk ); - - - // iterate through levels - pNode = ABC_CALLOC( Bdc_Nod_t, nSize ); - for ( n = 2; n <= nGatesMax; n++ ) - { -clk = clock(); - c = 0; - pNode1 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, n-1 ); - Count1 = Vec_IntEntry( vBegs, n-1 ); - // go through previous levels - for ( k = 0; k < n-1; k++ ) - { - pNode0 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, k ); - Count0 = Vec_IntEntry( vBegs, k ); - for ( i = 0; i < Count0; i++ ) - for ( j = 0; j < Count1; j++ ) - { - pNode[c].Truth = pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0; - pNode[c].Truth = ~pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1; - pNode[c].Truth = pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2; - pNode[c].Truth = ~pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3; - pNode[c].Truth = pNode0[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4; - } - assert( c < nSize ); - } - // go through current level - for ( i = 0; i < Count1; i++ ) - for ( j = i+1; j < Count1; j++ ) - { - pNode[c].Truth = pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0; - pNode[c].Truth = ~pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1; - pNode[c].Truth = pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2; - pNode[c].Truth = ~pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3; - pNode[c].Truth = pNode1[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4; - } - assert( c < nSize ); - // sort - Vec_IntClear( vWeight ); - for ( i = 0; i < c; i++ ) - { - pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth ); -if ( pNode[i].Weight > 300 ) -Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth ); - Vec_IntPush( vWeight, pNode[i].Weight ); - - if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth ) - { - printf( "Function can be implemented using %d gates.\n", n ); - Bdc_SpfdPrint( pNode + i, n, vLevels, Truth ); - goto cleanup; - } - } - pPerm = Abc_SortCost( Vec_IntArray(vWeight), c ); - assert( Vec_IntEntry(vWeight, pPerm[0]) <= Vec_IntEntry(vWeight, pPerm[c-1]) ); - - printf( "Best SPFD = %d.\n", Vec_IntEntry(vWeight, pPerm[c-1]) ); -// for ( i = 0; i < c; i++ ) -//printf( "%d ", Vec_IntEntry(vWeight, pPerm[i]) ); - - // choose the best ones - pNode2 = ABC_CALLOC( Bdc_Nod_t, nCands ); - for ( j = 0, i = c-1; i >= 0; i-- ) - { - pNode2[j++] = pNode[pPerm[i]]; - if ( j == nCands ) - break; - } - ABC_FREE( pPerm ); - Vec_PtrPush( vLevels, pNode2 ); - Vec_IntPush( vBegs, j ); - -printf( "Selected %6d gates (out of %6d) on level %2d. ", j, c, n ); -Abc_PrintTime( 1, "Time", clock() - clk ); - - for ( i = 0; i < 10; i++ ) - Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth ); - } - -cleanup: - ABC_FREE( pNode ); - Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i ) - ABC_FREE( pNode ); - Vec_PtrFree( vLevels ); - Vec_IntFree( vBegs ); - Vec_IntFree( vWeight ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdDecomposeTest_() -{ - int fTry = 0; -// word T[17]; -// int i; - -// word Truth = Truths[0] & ~Truths[3]; -// word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]); -// word Truth = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5])); -// word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]); -// word Truth = 0x9ef7a8d9c7193a0f; // AAFFAAFF0A0F0A0F -// word Truth = 0x34080226CD163000; - word Truth = 0x5052585a0002080a; - int nVars = 6; - int nCands = 200;// 75; - int nGatesMax = 20; - - if ( fTry ) - Bdc_SpfdDecompose( Truth, nVars, nCands, nGatesMax ); -/* - for ( i = 0; i < 6; i++ ) - T[i] = Truths[i]; - T[7] = 0; - T[8] = ~T[1] & T[3]; - T[9] = ~T[8] & T[0]; - T[10] = T[1] & T[4]; - T[11] = T[10] & T[2]; - T[12] = T[11] & T[9]; - T[13] = ~T[0] & T[5]; - T[14] = T[2] & T[13]; - T[15] = ~T[12] & ~T[14]; - T[16] = ~T[15]; -// if ( T[16] != Truth ) -// printf( "Failed\n" ); - - for ( i = 0; i < 17; i++ ) - { -// printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], Truth) ); - printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], T[16]) ); - Extra_PrintBinary( stdout, (unsigned *)&T[i], 64 ); printf( "\n" ); - } -// Extra_PrintBinary( stdout, (unsigned *)&Truth, 64 ); printf( "\n" ); -*/ -} - - - - -typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes -struct Bdc_Ent_t_ -{ - unsigned iFan0 : 29; - unsigned fCompl0 : 1; - unsigned fCompl : 1; - unsigned fMark0 : 1; - unsigned iFan1 : 29; - unsigned fCompl1 : 1; - unsigned fExor : 1; - unsigned fMark1 : 1; - int iNext; - int iList; - word Truth; -}; - -#define BDC_TERM 0x1FFFFFFF - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_SpfdMark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt ) -{ - if ( pEnt->iFan0 == BDC_TERM ) - return 0; - if ( pEnt->fMark0 ) - return 0; - pEnt->fMark0 = 1; - return pEnt->fMark1 + - Bdc_SpfdMark0(p, p + pEnt->iFan0) + - Bdc_SpfdMark0(p, p + pEnt->iFan1); -} -int Bdc_SpfdMark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt ) -{ - if ( pEnt->iFan0 == BDC_TERM ) - return 0; - if ( pEnt->fMark1 ) - return 0; - pEnt->fMark1 = 1; - return pEnt->fMark0 + - Bdc_SpfdMark1(p, p + pEnt->iFan0) + - Bdc_SpfdMark1(p, p + pEnt->iFan1); -} -void Bdc_SpfdUnmark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt ) -{ - if ( pEnt->iFan0 == BDC_TERM ) - return; - pEnt->fMark0 = 0; - Bdc_SpfdUnmark0( p, p + pEnt->iFan0 ); - Bdc_SpfdUnmark0( p, p + pEnt->iFan1 ); -} -void Bdc_SpfdUnmark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt ) -{ - if ( pEnt->iFan0 == BDC_TERM ) - return; - pEnt->fMark1 = 0; - Bdc_SpfdUnmark1( p, p + pEnt->iFan0 ); - Bdc_SpfdUnmark1( p, p + pEnt->iFan1 ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_SpfdCheckOverlap( Bdc_Ent_t * p, Bdc_Ent_t * pEnt0, Bdc_Ent_t * pEnt1 ) -{ - int RetValue; - RetValue = Bdc_SpfdMark0( p, pEnt0 ); - assert( RetValue == 0 ); - RetValue = Bdc_SpfdMark1( p, pEnt1 ); - Bdc_SpfdUnmark0( p, pEnt0 ); - Bdc_SpfdUnmark1( p, pEnt1 ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_SpfdHashValue( word t, int Size ) -{ - // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html - // 53, - // 97, - // 193, - // 389, - // 769, - // 1543, - // 3079, - // 6151, - // 12289, - // 24593, - // 49157, - // 98317, - // 196613, - // 393241, - // 786433, - // 1572869, - // 3145739, - // 6291469, - // 12582917, - // 25165843, - // 50331653, - // 100663319, - // 201326611, - // 402653189, - // 805306457, - // 1610612741, - static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741}; - unsigned char * s = (unsigned char *)&t; - unsigned i, Value = 0; - for ( i = 0; i < 8; i++ ) - Value ^= BigPrimes[i] * s[i]; - return Value % Size; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t ) -{ - Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size ); - if ( pBin->iList == 0 ) - return &pBin->iList; - for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext ) - { - if ( pBin->Truth == t ) - return NULL; - if ( pBin->iNext == 0 ) - return &pBin->iNext; - } - assert( 0 ); - return NULL; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights ) -{ -// int nFuncs = 8000000; // the number of functions to compute -// int nSize = 2777111; // the hash table size to use -// int Limit = 6; - -// int nFuncs = 51000000; // the number of functions to compute -// int nSize = 50331653; // the hash table size to use -// int Limit = 6; - - int nFuncs = 250000000; // the number of functions to compute - int nSize = 201326611; // the hash table size to use - int Limit = 6; - - int * pPlace, i, n, m, k, s, fCompl, clk = clock(), clk2; - Vec_Int_t * vStops; - Vec_Wrd_t * vTruths; - Vec_Int_t * vWeights; - Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1; - word t0, t1, t; - assert( nSize <= nFuncs ); - - printf( "Allocating %.2f Mb of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) ); - - p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) ); - memset( p, 255, sizeof(Bdc_Ent_t) ); - p->iList = 0; - for ( q = p; q < p+nFuncs; q++ ) - q->iList = 0; - q = p + 1; - printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p ); - - vTruths = Vec_WrdStart( nFuncs ); - vWeights = Vec_IntStart( nFuncs ); - Vec_WrdClear( vTruths ); - Vec_IntClear( vWeights ); - - // create elementary vars - vStops = Vec_IntAlloc( 10 ); - Vec_IntPush( vStops, 1 ); - for ( i = 0; i < 6; i++ ) - { - q->iFan0 = BDC_TERM; - q->iFan1 = i; - q->Truth = Truths[i]; - pPlace = Bdc_SpfdHashLookup( p, nSize, q->Truth ); - *pPlace = q-p; - q++; - Vec_WrdPush( vTruths, Truths[i] ); - Vec_IntPush( vWeights, 0 ); - } - Vec_IntPush( vStops, 7 ); - printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p ); - - // create gates - for ( n = 0; n < Limit; n++ ) - { - // try previous - for ( k = 0; k < Limit; k++ ) - for ( m = 0; m < Limit; m++ ) - { - if ( k + m != n || k > m ) - continue; - // set the start and stop - pBeg0 = p + Vec_IntEntry( vStops, k ); - pEnd0 = p + Vec_IntEntry( vStops, k+1 ); - // set the start and stop - pBeg1 = p + Vec_IntEntry( vStops, m ); - pEnd1 = p + Vec_IntEntry( vStops, m+1 ); - - clk2 = clock(); - printf( "Trying %7d x %7d. ", pEnd0-pBeg0, pEnd1-pBeg1 ); - for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ ) - for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ ) - if ( k < m || pThis1 > pThis0 ) -// if ( n < 5 || Bdc_SpfdCheckOverlap(p, pThis0, pThis1) ) - for ( s = 0; s < 5; s++ ) - { - t0 = (s&1) ? ~pThis0->Truth : pThis0->Truth; - t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth; - t = ((s>>2)&1) ? t0 ^ t1 : t0 & t1; - fCompl = t & 1; - if ( fCompl ) - t = ~t; - if ( t == 0 ) - continue; - pPlace = Bdc_SpfdHashLookup( p, nSize, t ); - if ( pPlace == NULL ) - continue; - q->iFan0 = pThis0-p; - q->fCompl0 = s&1; - q->iFan1 = pThis1-p; - q->fCompl1 = (s>>1)&1; - q->fExor = (s>>2)&1; - q->Truth = t; - q->fCompl = fCompl; - *pPlace = q-p; - q++; - Vec_WrdPush( vTruths, t ); -// Vec_IntPush( vWeights, n == 5 ? n : n+1 ); - Vec_IntPush( vWeights, n+1 ); - if ( q-p == nFuncs ) - { - printf( "Reached limit of %d functions.\n", nFuncs ); - goto finish; - } - } - printf( "Added %d + %d + 1 = %d. Total = %8d. ", k, m, n+1, q-p ); - Abc_PrintTime( 1, "Time", clock() - clk2 ); - } - Vec_IntPush( vStops, q-p ); - } - Abc_PrintTime( 1, "Time", clock() - clk ); - - - { - FILE * pFile = fopen( "func6v6n_bin.txt", "wb" ); - fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile ); - fclose( pFile ); - } - { - FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" ); - fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile ); - fclose( pFile ); - } - - -finish: - Vec_IntFree( vStops ); - free( p ); - - *pvWeights = vWeights; -// Vec_WrdFree( vTruths ); - return vTruths; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Wrd_t * Bdc_SpfdReadFiles5( Vec_Int_t ** pvWeights ) -{ - Vec_Int_t * vWeights; - Vec_Wrd_t * vDivs; - FILE * pFile; - - vDivs = Vec_WrdStart( 3863759 ); - pFile = fopen( "func6v5n_bin.txt", "rb" ); - fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile ); - fclose( pFile ); - - vWeights = Vec_IntStart( 3863759 ); - pFile = fopen( "func6v5nW_bin.txt", "rb" ); - fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile ); - fclose( pFile ); - - *pvWeights = vWeights; - return vDivs; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Wrd_t * Bdc_SpfdReadFiles6( Vec_Int_t ** pvWeights ) -{ - Vec_Int_t * vWeights; - Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 ); - FILE * pFile = fopen( "func6v6n_bin.txt", "rb" ); - fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile ); - fclose( pFile ); - - vWeights = Vec_IntStart( 12776759 ); - pFile = fopen( "func6v6nW_bin.txt", "rb" ); - fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile ); - fclose( pFile ); - - *pvWeights = vWeights; - return vDivs; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights ) -{ - int Ones = Bdc_CountOnes(f); - if ( Ones == 0 ) - return -1; - return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i)); -// return Bdc_CountOnes(f); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost ) -{ - word Func, FuncBest; - int i, Cost, CostBest = -1, NumBest; - Vec_WrdForEachEntry( vDivs, Func, i ) - { - if ( (Func & F0) == 0 ) - { - Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights); - if ( CostBest < Cost ) - { - CostBest = Cost; - FuncBest = Func; - NumBest = i; - } - } - if ( (Func & F1) == 0 ) - { - Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights); - if ( CostBest < Cost ) - { - CostBest = Cost; - FuncBest = Func; - NumBest = i; - } - } - if ( (~Func & F0) == 0 ) - { - Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights); - if ( CostBest < Cost ) - { - CostBest = Cost; - FuncBest = ~Func; - NumBest = i; - } - } - if ( (~Func & F1) == 0 ) - { - Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights); - if ( CostBest < Cost ) - { - CostBest = Cost; - FuncBest = ~Func; - NumBest = i; - } - } - } - (*pCost) += Vec_IntEntry(vWeights, NumBest); - assert( CostBest > 0 ); - printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) ); - Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" ); - return FuncBest; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights ) -{ - word F1 = t; - word F0 = ~F1; - word Func; - int i, Cost = 0; - printf( "Trying: " ); - Extra_PrintHex( stdout, (unsigned *)&t, 6 ); printf( "\n" ); -// Abc_Show6VarFunc( F0, F1 ); - for ( i = 0; F0 && F1; i++ ) - { - printf( "*** ITER %2d ", i ); - Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost ); - F0 &= ~Func; - F1 &= ~Func; -// Abc_Show6VarFunc( F0, F1 ); - } - Cost += (i-1); - printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) ); - return Cost; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdDecomposeTest44() -{ -// word t = 0x5052585a0002080a; - - word t = 0x9ef7a8d9c7193a0f; -// word t = 0x6BFDA276C7193A0F; -// word t = 0xA3756AFE0B1DF60B; - -// word t = 0xFEF7AEBFCE80AA0F; -// word t = 0x9EF7FDBFC77F6F0F; -// word t = 0xDEF7FDFF377F6FFF; - -// word t = 0x345D02736DB390A5; // xor with var 0 - -// word t = 0x3EFDA2736D139A0F; // best solution after changes - - Vec_Int_t * vWeights; - Vec_Wrd_t * vDivs; - word c0, c1, s, tt, tbest; - int i, j, Cost, CostBest = 100000; - int clk = clock(); - - return; - -// printf( "%d\n", RAND_MAX ); - - vDivs = Bdc_SpfdDecomposeTest__( &vWeights ); -// vDivs = Bdc_SpfdReadFiles5( &vWeights ); - -// Abc_Show6VarFunc( ~t, t ); - - // try function - tt = t; - Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights ); - if ( CostBest > Cost ) - { - CostBest = Cost; - tbest = tt; - } - printf( "\n" ); - - // try complemented output - for ( i = 0; i < 6; i++ ) - { - tt = t ^ Truths[i]; - Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights ); - if ( CostBest > Cost ) - { - CostBest = Cost; - tbest = tt; - } - } - printf( "\n" ); - - // try complemented input - for ( i = 0; i < 6; i++ ) - for ( j = 0; j < 6; j++ ) - { - if ( i == j ) - continue; - c0 = Bdc_Cof6( t, i, 0 ); - c1 = Bdc_Cof6( t, i, 1 ); - s = Truths[i] ^ Truths[j]; - tt = (~s & c0) | (s & c1); - - Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights ); - if ( CostBest > Cost ) - { - CostBest = Cost; - tbest = tt; - } - } - -/* - for ( i = 0; i < 6; i++ ) - for ( j = 0; j < 6; j++ ) - { - if ( i == j ) - continue; - c0 = Bdc_Cof6( t, i, 0 ); - c1 = Bdc_Cof6( t, i, 1 ); - s = Truths[i] ^ Truths[j]; - tt = (~s & c0) | (s & c1); - - for ( k = 0; k < 6; k++ ) - for ( n = 0; n < 6; n++ ) - { - if ( k == n ) - continue; - c0 = Bdc_Cof6( tt, k, 0 ); - c1 = Bdc_Cof6( tt, k, 1 ); - s = Truths[k] ^ Truths[n]; - ttt= (~s & c0) | (s & c1); - - Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights ); - if ( CostBest > Cost ) - { - CostBest = Cost; - tbest = ttt; - } - } - } -*/ - - printf( "Best solution found with cost %d. ", CostBest ); - Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" ); - Abc_PrintTime( 1, " Time", clock() - clk ); - - Vec_WrdFree( vDivs ); - Vec_IntFree( vWeights ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdDecomposeTest3() -{ - int nSizeM = (1 << 26); - int nSizeK = (1 << 3); - Vec_Wrd_t * v1M; - Vec_Wrd_t * v1K; - int i, k, Counter, clk; -// int EntryM, EntryK; - Aig_ManRandom64( 1 ); - - v1M = Vec_WrdAlloc( nSizeM ); - for ( i = 0; i < nSizeM; i++ ) - Vec_WrdPush( v1M, Aig_ManRandom64(0) ); - - v1K = Vec_WrdAlloc( nSizeK ); - for ( i = 0; i < nSizeK; i++ ) - Vec_WrdPush( v1K, Aig_ManRandom64(0) ); - - clk = clock(); - Counter = 0; - for ( i = 0; i < nSizeM; i++ ) - for ( k = 0; k < nSizeK; k++ ) - Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]); -// Vec_WrdForEachEntry( v1M, EntryM, i ) -// Vec_WrdForEachEntry( v1K, EntryK, k ) -// Counter += ((EntryM & EntryK) == EntryK); - - printf( "Total = %8d. ", Counter ); - Abc_PrintTime( 1, "Time", clock() - clk ); - - clk = clock(); - Counter = 0; - for ( k = 0; k < nSizeK; k++ ) - for ( i = 0; i < nSizeM; i++ ) - Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]); - printf( "Total = %8d. ", Counter ); - Abc_PrintTime( 1, "Time", clock() - clk ); - -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdDecomposeTest8() -{ -// word t = 0x9ef7a8d9c7193a0f; -// word t = 0x9EF7FDBFC77F6F0F; - word t = 0x513B57150819050F; - - Vec_Int_t * vWeights; - Vec_Wrd_t * vDivs; - word Func, FuncBest; - int Cost, CostBest = ABC_INFINITY; - int i, clk = clock(); - -// return; - - vDivs = Bdc_SpfdReadFiles5( &vWeights ); - - printf( "Best init = %4d. ", Bdc_SpfdAdjCost(t) ); - Extra_PrintHex( stdout, (unsigned *)&t, 6 ); //printf( "\n" ); - Abc_PrintTime( 1, " Time", clock() - clk ); - - Vec_WrdForEachEntry( vDivs, Func, i ) - { - Cost = Bdc_SpfdAdjCost( t ^ Func ); - if ( CostBest > Cost ) - { - CostBest = Cost; - FuncBest = Func; - } - } - - printf( "Best cost = %4d. ", CostBest ); - Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); //printf( "\n" ); - Abc_PrintTime( 1, " Time", clock() - clk ); - -Abc_Show6VarFunc( 0, t ); -Abc_Show6VarFunc( 0, FuncBest ); -Abc_Show6VarFunc( 0, (FuncBest ^ t) ); - - FuncBest ^= t; - Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" ); - -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bdc_SpfdDecomposeTest() -{ - int nSizeM = (1 << 26); // big array size - int nSizeK = (1 << 3); // small array size - Vec_Wrd_t * v1M, * v1K; - int EntryM, EntryK; - int i, k, Counter, clk; - - Aig_ManRandom64( 1 ); - - v1M = Vec_WrdAlloc( nSizeM ); - for ( i = 0; i < nSizeM; i++ ) - Vec_WrdPush( v1M, Aig_ManRandom64(0) ); - - v1K = Vec_WrdAlloc( nSizeK ); - for ( i = 0; i < nSizeK; i++ ) - Vec_WrdPush( v1K, Aig_ManRandom64(0) ); - - clk = clock(); - Counter = 0; -// for ( i = 0; i < nSizeM; i++ ) -// for ( k = 0; k < nSizeK; k++ ) -// Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]); - Vec_WrdForEachEntry( v1M, EntryM, i ) - Vec_WrdForEachEntry( v1K, EntryK, k ) - Counter += ((EntryM & EntryK) == EntryK); - printf( "Total = %8d. ", Counter ); - Abc_PrintTime( 1, "Time", clock() - clk ); - - clk = clock(); - Counter = 0; -// for ( k = 0; k < nSizeK; k++ ) -// for ( i = 0; i < nSizeM; i++ ) -// Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]); - Vec_WrdForEachEntry( v1K, EntryK, k ) - Vec_WrdForEachEntry( v1M, EntryM, i ) - Counter += ((EntryM & EntryK) == EntryK); - printf( "Total = %8d. ", Counter ); - Abc_PrintTime( 1, "Time", clock() - clk ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c deleted file mode 100644 index 69f35d88..00000000 --- a/src/aig/bdc/bdcTable.c +++ /dev/null @@ -1,134 +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" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**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( puTruth, pIsf->puOff, 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 ) -{ - int fDisableCache = 0; - Bdc_Fun_t * pFunc; - if ( fDisableCache && Kit_WordCountOnes(pIsf->uSupp) > 1 ) - return NULL; - if ( pIsf->uSupp == 0 ) - { - assert( p->pTable[pIsf->uSupp] == p->pNodes ); - if ( Kit_TruthIsConst1( pIsf->puOn, p->nVars ) ) - return p->pNodes; - assert( Kit_TruthIsConst1( pIsf->puOff, p->nVars ) ); - return Bdc_Not(p->pNodes); - } - for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext ) - if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) ) - return pFunc; - Bdc_IsfNot( pIsf ); - for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext ) - if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) ) - { - Bdc_IsfNot( pIsf ); - return Bdc_Not(pFunc); - } - Bdc_IsfNot( pIsf ); - 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 /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/bdc/bdc_.c b/src/aig/bdc/bdc_.c deleted file mode 100644 index b29d4f5e..00000000 --- a/src/aig/bdc/bdc_.c +++ /dev/null @@ -1,54 +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" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/bdc/module.make b/src/aig/bdc/module.make deleted file mode 100644 index 97f5b33b..00000000 --- a/src/aig/bdc/module.make +++ /dev/null @@ -1,5 +0,0 @@ -SRC += src/aig/bdc/bdcCore.c \ - src/aig/bdc/bdcDec.c \ - src/aig/bdc/bdcSpfd.c \ - src/aig/bdc/bdcTable.c - |