| /**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; |
| abctime clk = 0; // Suppress "might be used uninitialized" |
| if ( p->pPars->fVerbose ) |
| clk = Abc_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 += Abc_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; |
| abctime clk = 0; // Suppress "might be used uninitialized" |
| if ( p->pPars->fVerbose ) |
| clk = Abc_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 += Abc_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; |
| abctime clk = 0; // Suppress "might be used uninitialized" |
| if ( p->pPars->fVerbose ) |
| clk = Abc_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 += Abc_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; |
| abctime 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 = Abc_Clock(); |
| pFunc = Bdc_TableLookup( p, pIsf ); |
| if ( p->pPars->fVerbose ) |
| p->timeCache += Abc_Clock() - clk; |
| if ( pFunc ) |
| return pFunc; |
| // decide on the decomposition type |
| if ( p->pPars->fVerbose ) |
| clk = Abc_Clock(); |
| Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR ); |
| if ( p->pPars->fVerbose ) |
| p->timeCheck += Abc_Clock() - clk; |
| if ( Type == BDC_TYPE_MUX ) |
| { |
| if ( p->pPars->fVerbose ) |
| clk = Abc_Clock(); |
| iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR ); |
| if ( p->pPars->fVerbose ) |
| p->timeMuxes += Abc_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 |
| |
