| /**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 | |