diff options
Diffstat (limited to 'src/bdd/dsd/dsdProc.c')
| -rw-r--r-- | src/bdd/dsd/dsdProc.c | 1617 |
1 files changed, 1617 insertions, 0 deletions
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c new file mode 100644 index 00000000..543ad387 --- /dev/null +++ b/src/bdd/dsd/dsdProc.c @@ -0,0 +1,1617 @@ +/**CFile**************************************************************** + + FileName [dsdProc.c] + + PackageName [DSD: Disjoint-support decomposition package.] + + Synopsis [The core procedures of the package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 8.0. Started - September 22, 2003.] + + Revision [$Id: dsdProc.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dsdInt.h" + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the most important procedures +void dsdKernelDecompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs ); +static Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * F ); + +// additional procedures +static Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity ); +static int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH ); +static void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor ); +static int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall ); + +// list copying +static void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize ); +static void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int Skipped ); + +// debugging procedures +static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ); + +//////////////////////////////////////////////////////////////////////// +/// STATIC VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// the counter of marks +static int s_Mark; + +// debugging flag +static int s_Show = 0; +// temporary var used for debugging +static int Depth = 0; + +static int s_Loops1; +static int s_Loops2; +static int s_Loops3; +static int s_Pivot; +static int s_PivotNo; +static int s_Common; +static int s_CommonNo; + +static int s_Case4Calls; +static int s_Case4CallsSpecial; + +static int s_Case5; +static int s_Loops2Useless; + + +static int s_DecNodesTotal; +static int s_DecNodesUsed; + +// statistical variables +static int s_nDecBlocks; +static int s_nLiterals; +static int s_nExorGates; +static int s_nReusedBlocks; +static int s_nCascades; +static float s_nArea; +static float s_MaxDelay; +static long s_Time; +static int s_nInvertors; +static int s_nPrimeBlocks; + +static int HashSuccess = 0; +static int HashFailure = 0; + +static int s_CacheEntries; + + +//////////////////////////////////////////////////////////////////////// +/// DECOMPOSITION FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs DSD for the array of functions represented by BDDs.] + + Description [This function takes the DSD manager, which should be + previously allocated by the call to Dsd_ManagerStart(). The resulting + DSD tree is stored in the DSD manager (pDsdMan->pRoots, pDsdMan->nRoots). + Access to the tree is through the APIs of the manager. The resulting + tree is a shared DSD DAG for the functions given in the array. For one + function the resulting DAG is always a tree. The root node pointers can + be complemented, as discussed in the literature referred to in "dsd.h". + This procedure can be called repeatedly for different functions. There is + no need to remove the decomposition tree after it is returned, because + the next call to the DSD manager will "recycle" the tree. The user should + not modify or dereference any data associated with the nodes of the + DSD trees (the user can only change the contents of a temporary + mark associated with each node by the calling to Dsd_NodeSetMark()). + All the decomposition trees and intermediate nodes will be removed when + the DSD manager is deallocated at the end by calling Dsd_ManagerStop().] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs ) +{ + DdManager * dd = pDsdMan->dd; + int i; + long clk; + Dsd_Node_t * pTemp; + int SumMaxGateSize = 0; + int nDecOutputs = 0; + int nCBFOutputs = 0; +/* +s_Loops1 = 0; +s_Loops2 = 0; +s_Loops3 = 0; +s_Case4Calls = 0; +s_Case4CallsSpecial = 0; +s_Case5 = 0; +s_Loops2Useless = 0; +*/ + // resize the number of roots in the manager + if ( pDsdMan->nRootsAlloc < nFuncs ) + { + if ( pDsdMan->nRootsAlloc > 0 ) + free( pDsdMan->pRoots ); + pDsdMan->nRootsAlloc = nFuncs; + pDsdMan->pRoots = (Dsd_Node_t **) malloc( pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) ); + } + + if ( pDsdMan->fVerbose ) + printf( "\nDecomposability statistics for individual outputs:\n" ); + + // set the counter of decomposition nodes + s_nDecBlocks = 0; + + // perform decomposition for all outputs + clk = clock(); + pDsdMan->nRoots = 0; + s_nCascades = 0; + for ( i = 0; i < nFuncs; i++ ) + { + int nLiteralsPrev; + int nDecBlocksPrev; + int nExorGatesPrev; + int nReusedBlocksPres; + int nCascades; + int MaxBlock; + int nPrimeBlocks; + long clk; + + clk = clock(); + nLiteralsPrev = s_nLiterals; + nDecBlocksPrev = s_nDecBlocks; + nExorGatesPrev = s_nExorGates; + nReusedBlocksPres = s_nReusedBlocks; + nPrimeBlocks = s_nPrimeBlocks; + + pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] ); + + Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock ); + s_nCascades = ddMax( s_nCascades, nCascades ); + pTemp = Dsd_Regular(pDsdMan->pRoots[i]); + if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) ) + nDecOutputs++; + if ( MaxBlock < 3 ) + nCBFOutputs++; + SumMaxGateSize += MaxBlock; + + if ( pDsdMan->fVerbose ) + { + printf("#%02d: ", i ); + printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) ); + printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) ); + printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) ); + printf("Max=%3d. ", MaxBlock ); + printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres ); + printf("Csc=%2d. ", nCascades ); + printf("T= %.2f s. ", (float)(clock()-clk)/(float)(CLOCKS_PER_SEC) ) ; + printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) ); + printf("\n"); + fflush( stdout ); + } + } + assert( pDsdMan->nRoots == nFuncs ); + + if ( pDsdMan->fVerbose ) + { + printf( "\n" ); + printf( "The cumulative decomposability statistics:\n" ); + printf( " Total outputs = %5d\n", nFuncs ); + printf( " Decomposable outputs = %5d\n", nDecOutputs ); + printf( " Completely decomposable outputs = %5d\n", nCBFOutputs ); + printf( " The sum of max gate sizes = %5d\n", SumMaxGateSize ); + printf( " Shared BDD size = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) ); + printf( " Decomposition entries = %5d\n", st_count( pDsdMan->Table ) ); + printf( " Pure decomposition time = %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) ); + } +/* + printf( "s_Loops1 = %d.\n", s_Loops1 ); + printf( "s_Loops2 = %d.\n", s_Loops2 ); + printf( "s_Loops3 = %d.\n", s_Loops3 ); + printf( "s_Case4Calls = %d.\n", s_Case4Calls ); + printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial ); + printf( "s_Case5 = %d.\n", s_Case5 ); + printf( "s_Loops2Useless = %d.\n", s_Loops2Useless ); +*/ +} + +/**Function************************************************************* + + Synopsis [Performs decomposition for one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ) +{ + return dsdKernelDecompose_rec( pDsdMan, bFunc ); +} + +/**Function************************************************************* + + Synopsis [The main function of this module. Recursive implementation of DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 ) +{ + DdManager * dd = pDsdMan->dd; + DdNode * bLow; + DdNode * bLowR; + DdNode * bHigh; + + int VarInt; + DdNode * bVarCur; + Dsd_Node_t * pVarCurDE; + // works only if var indices start from 0!!! + DdNode * bSuppNew = NULL, * bTemp; + + int fContained; + int nSuppLH; + int nSuppL; + int nSuppH; + + + + // various decomposition nodes + Dsd_Node_t * pThis, * pL, * pH, * pLR, * pHR; + + Dsd_Node_t * pSmallR, * pLargeR; + Dsd_Node_t * pTableEntry; + + + // treat the complemented case + DdNode * bF = Cudd_Regular(bFunc0); + int fCompF = (int)(bF != bFunc0); + + // check cache + if ( st_lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) ) + { // the entry is present + HashSuccess++; + return Dsd_NotCond( pTableEntry, fCompF ); + } + HashFailure++; + Depth++; + + // proceed to consider "four cases" + ////////////////////////////////////////////////////////////////////// + // TERMINAL CASES - CASES 1 and 2 + ////////////////////////////////////////////////////////////////////// + bLow = cuddE(bF); + bLowR = Cudd_Regular(bLow); + bHigh = cuddT(bF); + VarInt = bF->index; + bVarCur = dd->vars[VarInt]; + pVarCurDE = pDsdMan->pInputs[VarInt]; + // works only if var indices start from 0!!! + bSuppNew = NULL; + + if ( bLowR->index == CUDD_CONST_INDEX || bHigh->index == CUDD_CONST_INDEX ) + { // one of the cofactors in the constant + if ( bHigh == b1 ) // bHigh cannot be equal to b0, because then it will be complemented + if ( bLow == b0 ) // bLow cannot be equal to b1, because then the node will have bLow == bHigh + ///////////////////////////////////////////////////////////////// + // bLow == 0, bHigh == 1, F = x'&0 + x&1 = x + ///////////////////////////////////////////////////////////////// + { // create the elementary variable node + assert(0); // should be already in the hash table + pThis = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, s_nDecBlocks++ ); + pThis->pDecs[0] = NULL; + } + else // if ( bLow != constant ) + ///////////////////////////////////////////////////////////////// + // bLow != const, bHigh == 1, F = x'&bLow + x&1 = bLow + x --- DSD_NODE_OR(x,bLow) + ///////////////////////////////////////////////////////////////// + { + pL = dsdKernelDecompose_rec( pDsdMan, bLow ); + pLR = Dsd_Regular( pL ); + bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew); + if ( pLR->Type == DSD_NODE_OR && pL == pLR ) // OR and no complement + { // add to the components + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pL->nDecs+1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, pVarCurDE, pL->pDecs, pL->nDecs ); + } + else // all other cases + { // create a new 2-input OR-gate + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 ); + } + } + else // if ( bHigh != const ) // meaning that bLow should be a constant + { + pH = dsdKernelDecompose_rec( pDsdMan, bHigh ); + pHR = Dsd_Regular( pH ); + bSuppNew = Cudd_bddAnd( dd, bVarCur, pHR->S ); Cudd_Ref(bSuppNew); + if ( bLow == b0 ) + ///////////////////////////////////////////////////////////////// + // Low == 0, High != 1, F = x'&0+x&High = (x'+High')'--- NOR(x',High') + ///////////////////////////////////////////////////////////////// + if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement + { // add to the components + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs ); + pThis = Dsd_Not(pThis); + } + else // all other cases + { // create a new 2-input NOR gate + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); + pH = Dsd_Not(pH); + dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 ); + pThis = Dsd_Not(pThis); + } + else // if ( bLow == b1 ) + ///////////////////////////////////////////////////////////////// + // Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High) + ///////////////////////////////////////////////////////////////// + if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement + { // add to the components + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pH->nDecs+1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pH->pDecs, pH->nDecs ); + } + else // all other cases + { // create a new 2-input OR-gate + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 ); + } + } + goto EXIT; + } + // else if ( bLow != const && bHigh != const ) + + // the case of equal cofactors (up to complementation) + if ( bLowR == bHigh ) + ///////////////////////////////////////////////////////////////// + // Low == G, High == G', F = x'&G + x&G' = (x(+)G) --- EXOR(x,Low) + ///////////////////////////////////////////////////////////////// + { + pL = dsdKernelDecompose_rec( pDsdMan, bLow ); + pLR = Dsd_Regular( pL ); + bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew); + if ( pLR->Type == DSD_NODE_EXOR ) // complemented or not - does not matter! + { // add to the components + pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, pLR->nDecs+1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, pVarCurDE, pLR->pDecs, pLR->nDecs ); + if ( pL != pLR ) + pThis = Dsd_Not( pThis ); + } + else // all other cases + { // create a new 2-input EXOR-gate + pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ ); + if ( pL != pLR ) // complemented + { + dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pLR, 1 ); + pThis = Dsd_Not( pThis ); + } + else // non-complemented + dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 ); + } + goto EXIT; + } + + ////////////////////////////////////////////////////////////////////// + // solve subproblems + ////////////////////////////////////////////////////////////////////// + pL = dsdKernelDecompose_rec( pDsdMan, bLow ); + pH = dsdKernelDecompose_rec( pDsdMan, bHigh ); + pLR = Dsd_Regular( pL ); + pHR = Dsd_Regular( pH ); + + assert( pLR->Type == DSD_NODE_BUF || pLR->Type == DSD_NODE_OR || pLR->Type == DSD_NODE_EXOR || pLR->Type == DSD_NODE_PRIME ); + assert( pHR->Type == DSD_NODE_BUF || pHR->Type == DSD_NODE_OR || pHR->Type == DSD_NODE_EXOR || pHR->Type == DSD_NODE_PRIME ); + +/* +if ( Depth == 1 ) +{ +// PRK(bLow,pDecTreeTotal->nInputs); +// PRK(bHigh,pDecTreeTotal->nInputs); +if ( s_Show ) +{ + PRD( pL ); + PRD( pH ); +} +} +*/ + // compute the new support + bTemp = Cudd_bddAnd( dd, pLR->S, pHR->S ); Cudd_Ref( bTemp ); + nSuppL = Extra_bddSuppSize( dd, pLR->S ); + nSuppH = Extra_bddSuppSize( dd, pHR->S ); + nSuppLH = Extra_bddSuppSize( dd, bTemp ); + bSuppNew = Cudd_bddAnd( dd, bTemp, bVarCur ); Cudd_Ref( bSuppNew ); + Cudd_RecursiveDeref( dd, bTemp ); + + + // several possibilities are possible + // (1) support of one component contains another + // (2) none of the supports is contained in another + fContained = dsdKernelCheckContainment( pDsdMan, pLR, pHR, &pLargeR, &pSmallR ); + + ////////////////////////////////////////////////////////////////////// + // CASE 3.b One of the cofactors in a constant (OR and EXOR) + ////////////////////////////////////////////////////////////////////// + // the support of the larger component should contain the support of the smaller + // it is possible to have PRIME function in this role + // for example: F = ITE( a+b, c(+)d, e+f ), F0 = ITE( b, c(+)d, e+f ), F1 = c(+)d + if ( fContained ) + { + Dsd_Node_t * pSmall, * pLarge; + int c, iCompLarge; // the number of the component is Large is equal to the whole of Small + int fLowIsLarge; + + DdNode * bFTemp; // the changed input function + Dsd_Node_t * pDETemp, * pDENew; + + Dsd_Node_t * pComp = NULL; + int nComp; + + if ( pSmallR == pLR ) + { // Low is Small => High is Large + pSmall = pL; + pLarge = pH; + fLowIsLarge = 0; + } + else + { // vice versa + pSmall = pH; + pLarge = pL; + fLowIsLarge = 1; + } + + // treat the situation when the larger is PRIME + if ( pLargeR->Type == DSD_NODE_PRIME ) //&& pLargeR->nDecs != pSmallR->nDecs ) + { + // QUESTION: Is it possible for pLargeR->nDecs > 3 + // and pSmall contained as one of input in pLarge? + // Yes, for example F = a'c + a & MUX(b,c',d) = a'c + abc' + ab'd is non-decomposable + // Consider the function H(a->xy) = F( xy, b, c, d ) + // H0 = H(x=0) = F(0,b,c,d) = c + // H1 = F(x=1) = F(y,b,c,d) - non-decomposable + // + // QUESTION: Is it possible that pLarge is PRIME(3) and pSmall is OR(2), + // which is not contained in PRIME as one input? + // Yes, for example F = abcd + b'c'd' + a'c'd' = PRIME(ab, c, d) + // F(a=0) = c'd' = NOT(OR(a,d)) F(a=1) = bcd + b'c'd' = PRIME(b,c,d) + // To find decomposition, we have to prove that F(a=1)|b=0 = F(a=0) + + // Is it possible that (pLargeR->nDecs == pSmallR->nDecs) and yet this case holds? + // Yes, consider the function such that F(a=0) = PRIME(a,b+c,d,e) and F(a=1) = OR(b,c,d,e) + // They have the same number of inputs and it is possible that they will be the cofactors + // as discribed in the previous example. + + // find the component, which when substituted for 0 or 1, produces the desired result + int g, fFoundComp; // {0,1} depending on whether setting cofactor to 0 or 1 worked out + + DdNode * bLarge, * bSmall; + if ( fLowIsLarge ) + { + bLarge = bLow; + bSmall = bHigh; + } + else + { + bLarge = bHigh; + bSmall = bLow; + } + + for ( g = 0; g < pLargeR->nDecs; g++ ) +// if ( g != c ) + { + pDETemp = pLargeR->pDecs[g]; // cannot be complemented + if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) ) + { + fFoundComp = 1; + break; + } + + s_Loops1++; + + if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, Cudd_Not(pDETemp->G), b1 ) ) + { + fFoundComp = 0; + break; + } + + s_Loops1++; + } + + if ( g != pLargeR->nDecs ) + { // decomposition is found + if ( fFoundComp ) + if ( fLowIsLarge ) + bFTemp = Cudd_bddOr( dd, bVarCur, pLargeR->pDecs[g]->G ); + else + bFTemp = Cudd_bddOr( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G ); + else + if ( fLowIsLarge ) + bFTemp = Cudd_bddAnd( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G ); + else + bFTemp = Cudd_bddAnd( dd, bVarCur, pLargeR->pDecs[g]->G ); + Cudd_Ref( bFTemp ); + + pDENew = dsdKernelDecompose_rec( pDsdMan, bFTemp ); + pDENew = Dsd_Regular( pDENew ); + Cudd_RecursiveDeref( dd, bFTemp ); + + // get the new gate + pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLargeR->nDecs, s_nDecBlocks++ ); + dsdKernelCopyListPlusOneMinusOne( pThis, pDENew, pLargeR->pDecs, pLargeR->nDecs, g ); + goto EXIT; + } + } + + // try to find one component in the pLarger that is equal to the whole of pSmaller + for ( c = 0; c < pLargeR->nDecs; c++ ) + if ( pLargeR->pDecs[c] == pSmall || pLargeR->pDecs[c] == Dsd_Not(pSmall) ) + { + iCompLarge = c; + break; + } + + // assign the equal component + if ( c != pLargeR->nDecs ) // the decomposition is possible! + { + pComp = pLargeR->pDecs[iCompLarge]; + nComp = 1; + } + else // the decomposition is still possible + { // for example F = OR(ab,c,d), F(a=0) = OR(c,d), F(a=1) = OR(b,c,d) + // supp(F0) is contained in supp(F1), Polarity(F(a=0)) == Polarity(F(a=1)) + + // try to find a group of common components + if ( pLargeR->Type == pSmallR->Type && + (pLargeR->Type == DSD_NODE_EXOR || pSmallR->Type == DSD_NODE_OR&& ((pLarge==pLargeR) == (pSmall==pSmallR))) ) + { + Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; + int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH ); + // if all the components of pSmall are contained in pLarge, + // then the decomposition exists + if ( nCommon == pSmallR->nDecs ) + { + pComp = pSmallR; + nComp = pSmallR->nDecs; + } + } + } + + if ( pComp ) // the decomposition is possible! + { +// Dsd_Node_t * pComp = pLargeR->pDecs[iCompLarge]; + Dsd_Node_t * pCompR = Dsd_Regular( pComp ); + int fComp1 = (int)( pLarge != pLargeR ); + int fComp2 = (int)( pComp != pCompR ); + int fComp3 = (int)( pSmall != pSmallR ); + + DdNode * bFuncComp; // the function of the given component + DdNode * bFuncNew; // the function of the input component + + if ( pLargeR->Type == DSD_NODE_OR ) // Figure 4 of Matsunaga's paper + { + // the decomposition exists only if the polarity assignment + // along the paths is the same + if ( (fComp1 ^ fComp2) == fComp3 ) + { // decomposition exists = consider 4 cases + // consideration of cases leads to the following conclusion + // fComp1 gives the polarity of the resulting DSD_NODE_OR gate + // fComp2 gives the polarity of the common component feeding into the DSD_NODE_OR gate + // + // | fComp1 pL/ |pS + // <> .........<=>....... <> | + // | / | + // [OR] [OR] | fComp3 + // / \ fComp2 / | \ | + // <> <> .......<=>... /..|..<> | + // / \ / | \| + // [OR] [C] S1 S2 C + // / \ + // <> \ + // / \ + // [OR] [x] + // / \ + // S1 S2 + // + + + // at this point we have the function F (bFTemp) and the common component C (bFuncComp) + // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0 + // we compute the following R = Exist( F - C, supp(C) ) + bFTemp = (fComp1)? Cudd_Not( bF ): bF; + bFuncComp = (fComp2)? Cudd_Not( pCompR->G ): pCompR->G; + bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bFuncComp), pCompR->S ); Cudd_Ref( bFuncNew ); + + // there is no need to copy the dec entry list first, because pComp is a component + // which will not be destroyed by the recursive call to decomposition + pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); + assert( Dsd_IsComplement(pDENew) ); // follows from the consideration of cases + Cudd_RecursiveDeref( dd, bFuncNew ); + + // get the new gate + if ( nComp == 1 ) + { + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); + pThis->pDecs[0] = pDENew; + pThis->pDecs[1] = pComp; // takes the complement + } + else + { // pComp is not complemented + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nComp+1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp ); + } + + if ( fComp1 ) + pThis = Dsd_Not( pThis ); + goto EXIT; + } + } + else if ( pLargeR->Type == DSD_NODE_EXOR ) // Figure 5 of Matsunaga's paper (with correction) + { // decomposition always exists = consider 4 cases + + // consideration of cases leads to the following conclusion + // fComp3 gives the COMPLEMENT of the polarity of the resulting EXOR gate + // (if fComp3 is 0, the EXOR gate is complemented, and vice versa) + // + // | fComp1 pL/ |pS + // <> .........<=>....... /....| fComp3 + // | / | + // [XOR] [XOR] | + // / \ fComp2==0 / | \ | + // / \ / | \ | + // / \ / | \| + // [OR] [C] S1 S2 C + // / \ + // <> \ + // / \ + // [XOR] [x] + // / \ + // S1 S2 + // + + assert( fComp2 == 0 ); + // find the functionality of the lower gates + bFTemp = (fComp3)? bF: Cudd_Not( bF ); + bFuncNew = Cudd_bddXor( dd, bFTemp, pComp->G ); Cudd_Ref( bFuncNew ); + + pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); + assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases + Cudd_RecursiveDeref( dd, bFuncNew ); + + // get the new gate + if ( nComp == 1 ) + { + pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ ); + pThis->pDecs[0] = pDENew; + pThis->pDecs[1] = pComp; + } + else + { // pComp is not complemented + pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nComp+1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp ); + } + + if ( !fComp3 ) + pThis = Dsd_Not( pThis ); + goto EXIT; + } + } + } + + // this case was added to fix the trivial bug found November 4, 2002 in Japan + // by running the example provided by T. Sasao + if ( nSuppLH == nSuppL + nSuppH ) // the supports of the components are disjoint + { + // create a new component of the type ITE( a, pH, pL ) + pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, 3, s_nDecBlocks++ ); + if ( dd->perm[pLR->S->index] < dd->perm[pHR->S->index] ) // pLR is higher in the varible order + { + pThis->pDecs[1] = pLR; + pThis->pDecs[2] = pHR; + } + else // pHR is higher in the varible order + { + pThis->pDecs[1] = pHR; + pThis->pDecs[2] = pLR; + } + // add the first component + pThis->pDecs[0] = pVarCurDE; + goto EXIT; + } + + + ////////////////////////////////////////////////////////////////////// + // CASE 3.a Neither of the cofactors is a constant (OR, EXOR, PRIME) + ////////////////////////////////////////////////////////////////////// + // the component types are identical + // and if they are OR, they are either both complemented or both not complemented + // and if they are PRIME, their dec numbers should be the same + if ( pLR->Type == pHR->Type && + pLR->Type != DSD_NODE_BUF && + (pLR->Type != DSD_NODE_OR || ( pL == pLR && pH == pHR || pL != pLR && pH != pHR ) ) && + (pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs) ) + { + // array to store common comps in pL and pH + Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; + int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLR, pHR, &pCommon, &pLastDiffL, &pLastDiffH ); + if ( nCommon ) + { + if ( pLR->Type == DSD_NODE_OR ) // Figure 2 of Matsunaga's paper + { // at this point we have the function F and the group of common components C + // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0 + // we compute the following R = Exist( F - C, supp(C) ) + + // compute the sum total of the common components and the union of their supports + DdNode * bCommF, * bCommS, * bFTemp, * bFuncNew; + Dsd_Node_t * pDENew; + + dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 ); + Cudd_Ref( bCommF ); + Cudd_Ref( bCommS ); + bFTemp = ( pL != pLR )? Cudd_Not(bF): bF; + + bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew ); + Cudd_RecursiveDeref( dd, bCommF ); + Cudd_RecursiveDeref( dd, bCommS ); + + // get the new gate + + // copy the components first, then call the decomposition + // because decomposition will distroy the list used for copying + pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nCommon + 1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon ); + + // call the decomposition recursively + pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); +// assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases + Cudd_RecursiveDeref( dd, bFuncNew ); + + // add the first component + pThis->pDecs[0] = pDENew; + + if ( pL != pLR ) + pThis = Dsd_Not( pThis ); + goto EXIT; + } + else + if ( pLR->Type == DSD_NODE_EXOR ) // Figure 3 of Matsunaga's paper + { + // compute the sum total of the common components and the union of their supports + DdNode * bCommF, * bFuncNew; + Dsd_Node_t * pDENew; + int fCompExor; + + dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, 1 ); + Cudd_Ref( bCommF ); + + bFuncNew = Cudd_bddXor( dd, bF, bCommF ); Cudd_Ref( bFuncNew ); + Cudd_RecursiveDeref( dd, bCommF ); + + // get the new gate + + // copy the components first, then call the decomposition + // because decomposition will distroy the list used for copying + pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nCommon + 1, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon ); + + // call the decomposition recursively + pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); + Cudd_RecursiveDeref( dd, bFuncNew ); + + // remember the fact that it was complemented + fCompExor = Dsd_IsComplement(pDENew); + pDENew = Dsd_Regular(pDENew); + + // add the first component + pThis->pDecs[0] = pDENew; + + + if ( fCompExor ) + pThis = Dsd_Not( pThis ); + goto EXIT; + } + else + if ( pLR->Type == DSD_NODE_PRIME && (nCommon == pLR->nDecs-1 || nCommon == pLR->nDecs) ) + { + // for example the function F(a,b,c,d) = ITE(b,c,a(+)d) produces + // two cofactors F(a=0) = PRIME(b,c,d) and F(a=1) = PRIME(b,c,d) + // with exactly the same list of common components + + Dsd_Node_t * pDENew; + DdNode * bFuncNew; + int fCompComp = 0; // this flag can be {0,1,2} + // if it is 0 there is no identity + // if it is 1/2, the cofactored functions are equal in the direct/complemented polarity + + if ( nCommon == pLR->nDecs ) + { // all the components are the same + // find the formal input, in which pLow and pHigh differ (if such input exists) + int m; + Dsd_Node_t * pTempL, * pTempH; + + s_Common++; + for ( m = 0; m < pLR->nDecs; m++ ) + { + pTempL = pLR->pDecs[m]; // cannot be complemented + pTempH = pHR->pDecs[m]; // cannot be complemented + + if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pTempL->G, Cudd_Not(pTempH->G) ) && + Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pTempL->G), pTempH->G ) ) + { + pLastDiffL = pTempL; + pLastDiffH = pTempH; + assert( pLastDiffL == pLastDiffH ); + fCompComp = 2; + break; + } + + s_Loops2++; + s_Loops2++; +/* + if ( s_Loops2 % 10000 == 0 ) + { + int i; + for ( i = 0; i < pLR->nDecs; i++ ) + printf( " %d(s=%d)", pLR->pDecs[i]->Type, + Extra_bddSuppSize(dd, pLR->pDecs[i]->S) ); + printf( "\n" ); + } +*/ + + } +// if ( pLR->nDecs == Extra_bddSuppSize(dd, pLR->S) ) +// s_Loops2Useless += pLR->nDecs * 2; + + if ( fCompComp ) + { // put the equal components into pCommon, so that they could be copied into the new dec entry + nCommon = 0; + for ( m = 0; m < pLR->nDecs; m++ ) + if ( pLR->pDecs[m] != pLastDiffL ) + pCommon[nCommon++] = pLR->pDecs[m]; + assert( nCommon = pLR->nDecs-1 ); + } + } + else + { // the differing components are known - check that they have compatible PRIME function + + s_CommonNo++; + + // find the numbers of different components + assert( pLastDiffL ); + assert( pLastDiffH ); + // also, they cannot be complemented, because the decomposition type is PRIME + + if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), Cudd_Not(pLastDiffH->G) ) && + Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, pLastDiffH->G ) ) + fCompComp = 1; + else if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, Cudd_Not(pLastDiffH->G) ) && + Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), pLastDiffH->G ) ) + fCompComp = 2; + + s_Loops3 += 4; + } + + if ( fCompComp ) + { + if ( fCompComp == 1 ) // it is true that bLow(G=0) == bHigh(H=0) && bLow(G=1) == bHigh(H=1) + bFuncNew = Cudd_bddIte( dd, bVarCur, pLastDiffH->G, pLastDiffL->G ); + else // it is true that bLow(G=0) == bHigh(H=1) && bLow(G=1) == bHigh(H=0) + bFuncNew = Cudd_bddIte( dd, bVarCur, Cudd_Not(pLastDiffH->G), pLastDiffL->G ); + Cudd_Ref( bFuncNew ); + + // get the new gate + + // copy the components first, then call the decomposition + // because decomposition will distroy the list used for copying + pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLR->nDecs, s_nDecBlocks++ ); + dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon ); + + // create a new component + pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); + Cudd_RecursiveDeref( dd, bFuncNew ); + // the BDD of the argument function in PRIME decomposition, should be regular + pDENew = Dsd_Regular(pDENew); + + // add the first component + pThis->pDecs[0] = pDENew; + goto EXIT; + } + } // end of PRIME type + } // end of existing common components + } // end of CASE 3.a + +// if ( Depth != 1) +// { + +//CASE4: + ////////////////////////////////////////////////////////////////////// + // CASE 4 + ////////////////////////////////////////////////////////////////////// + { + // estimate the number of entries in the list + int nEntriesMax = pDsdMan->nInputs - dd->perm[VarInt]; + + // create the new decomposition entry + int nEntries = 0; + + DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init; + Dsd_Node_t *pHigher, *pLower, * pTemp, * pDENew; + + + int levTopSuppL; + int levTopSuppH; + int levTop; + + pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, nEntriesMax, s_nDecBlocks++ ); + pThis->pDecs[ nEntries++ ] = pVarCurDE; + // other entries will be added to this list one-by-one during analysis + + // count how many times does it happen that the decomposition entries are + s_Case4Calls++; + + // consider the simplest case: when the supports are equal + // and at least one of the components + // is the PRIME without decompositions, or + // when both of them are without decomposition + if ( (((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) || (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) && pLR->S == pHR->S) || + ((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) && (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) ) + { + + s_Case4CallsSpecial++; + // walk through both supports and create the decomposition list composed of simple entries + SuppL = pLR->S; + SuppH = pHR->S; + do + { + // determine levels + levTopSuppL = cuddI(dd,SuppL->index); + levTopSuppH = cuddI(dd,SuppH->index); + + // skip the topmost variable in both supports + if ( levTopSuppL <= levTopSuppH ) + { + levTop = levTopSuppL; + SuppL = cuddT(SuppL); + } + else + levTop = levTopSuppH; + + if ( levTopSuppH <= levTopSuppL ) + SuppH = cuddT(SuppH); + + // set the new decomposition entry + pThis->pDecs[ nEntries++ ] = pDsdMan->pInputs[ dd->invperm[levTop] ]; + } + while ( SuppL != b1 || SuppH != b1 ); + } + else + { + + // compare two different decomposition lists + SuppL_init = pLR->S; + SuppH_init = pHR->S; + // start references (because these supports will change) + SuppL = pLR->S; Cudd_Ref( SuppL ); + SuppH = pHR->S; Cudd_Ref( SuppH ); + while ( SuppL != b1 || SuppH != b1 ) + { + // determine the top level in cofactors and + // whether they have the same top level + int TopLevL = cuddI(dd,SuppL->index); + int TopLevH = cuddI(dd,SuppH->index); + int TopLevel = TopLevH; + int fEqualLevel = 0; + + DdNode * bVarTop; + DdNode * bSuppSubract; + + + if ( TopLevL < TopLevH ) + { + pHigher = pLR; + pLower = pHR; + TopLevel = TopLevL; + } + else if ( TopLevL > TopLevH ) + { + pHigher = pHR; + pLower = pLR; + } + else + fEqualLevel = 1; + assert( TopLevel != CUDD_CONST_INDEX ); + + + // find the currently top variable in the decomposition lists + bVarTop = dd->vars[dd->invperm[TopLevel]]; + + if ( !fEqualLevel ) + { + // find the lower support + DdNode * bSuppLower = (TopLevL < TopLevH)? SuppH_init: SuppL_init; + + // find the first component in pHigher + // whose support does not overlap with supp(Lower) + // and remember the previous component + int fPolarity; + Dsd_Node_t * pPrev = NULL; // the pointer to the component proceeding pCur + Dsd_Node_t * pCur = pHigher; // the first component not contained in supp(Lower) + while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) ) + { // get the next component + pPrev = pCur; + pCur = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity ); + }; + + // look for the possibility to subtract more than one component + if ( pPrev == NULL || pPrev->Type == DSD_NODE_PRIME ) + { // if there is no previous component, or if the previous component is PRIME + // there is no way to subtract more than one component + + // add the new decomposition entry (it is already regular) + pThis->pDecs[ nEntries++ ] = pCur; + // assign the support to be subtracted from both components + bSuppSubract = pCur->S; + } + else // all other types + { + // go through the decomposition list of pPrev and find components + // whose support does not overlap with supp(Lower) + + static Dsd_Node_t * pNonOverlap[MAXINPUTS]; + int i, nNonOverlap = 0; + for ( i = 0; i < pPrev->nDecs; i++ ) + { + pTemp = Dsd_Regular( pPrev->pDecs[i] ); + if ( !Extra_bddSuppOverlapping( dd, pTemp->S, bSuppLower ) ) + pNonOverlap[ nNonOverlap++ ] = pPrev->pDecs[i]; + } + assert( nNonOverlap > 0 ); + + if ( nNonOverlap == 1 ) + { // one one component was found, which is the original one + assert( Dsd_Regular(pNonOverlap[0]) == pCur); + // add the new decomposition entry + pThis->pDecs[ nEntries++ ] = pCur; + // assign the support to be subtracted from both components + bSuppSubract = pCur->S; + } + else // more than one components was found + { + // find the OR (EXOR) of the non-overlapping components + DdNode * bCommF; + dsdKernelComputeSumOfComponents( pDsdMan, pNonOverlap, nNonOverlap, &bCommF, NULL, (int)(pPrev->Type==DSD_NODE_EXOR) ); + Cudd_Ref( bCommF ); + + // create a new gated + pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF ); + Cudd_RecursiveDeref(dd, bCommF); + // make it regular... it must be regular already + assert( !Dsd_IsComplement(pDENew) ); + + // add the new decomposition entry + pThis->pDecs[ nEntries++ ] = pDENew; + // assign the support to be subtracted from both components + bSuppSubract = pDENew->S; + } + } + + // subtract its support from the support of upper component + if ( TopLevL < TopLevH ) + { + SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ); Cudd_Ref( SuppL ); + Cudd_RecursiveDeref(dd, bTemp); + } + else + { + SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ); Cudd_Ref( SuppH ); + Cudd_RecursiveDeref(dd, bTemp); + } + } // end of if ( !fEqualLevel ) + else // if ( fEqualLevel ) -- they have the same top level var + { + static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks + static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks + int nMarkedLeft = 0; + + int fPolarity = 0; + Dsd_Node_t * pTempL = pLR; + + int fPolarityCurH = 0; + Dsd_Node_t * pPrevH = NULL, * pCurH = pHR; + + int fPolarityCurL = 0; + Dsd_Node_t * pPrevL = NULL, * pCurL = pLR; // = pMarkedLeft[0]; + int index = 1; + + // set the new mark + s_Mark++; + + // go over the dec list of pL, mark all components that contain the given variable + assert( Extra_bddSuppContainVar( dd, pLR->S, bVarTop ) ); + assert( Extra_bddSuppContainVar( dd, pHR->S, bVarTop ) ); + do { + pTempL->Mark = s_Mark; + pMarkedLeft[ nMarkedLeft ] = pTempL; + pMarkedPols[ nMarkedLeft ] = fPolarity; + nMarkedLeft++; + } while ( pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity ) ); + + // go over the dec list of pH, and find the component that is marked and the previos one + // (such component always exists, because they have common variables) + while ( pCurH->Mark != s_Mark ) + { + pPrevH = pCurH; + pCurH = dsdKernelFindContainingComponent( pDsdMan, pCurH, bVarTop, &fPolarityCurH ); + assert( pCurH ); + } + + // go through the first list once again and find + // the component proceeding the one marked found in the second list + while ( pCurL != pCurH ) + { + pPrevL = pCurL; + pCurL = pMarkedLeft[index]; + fPolarityCurL = pMarkedPols[index]; + index++; + } + + // look for the possibility to subtract more than one component + if ( !pPrevL || !pPrevH || pPrevL->Type != pPrevH->Type || pPrevL->Type == DSD_NODE_PRIME || fPolarityCurL != fPolarityCurH ) + { // there is no way to extract more than one + pThis->pDecs[ nEntries++ ] = pCurH; + // assign the support to be subtracted from both components + bSuppSubract = pCurH->S; + } + else + { + // find the equal components in two decomposition lists + Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; + int nCommon = dsdKernelFindCommonComponents( pDsdMan, pPrevL, pPrevH, &pCommon, &pLastDiffL, &pLastDiffH ); + + if ( nCommon == 0 || nCommon == 1 ) + { // one one component was found, which is the original one + // assert( Dsd_Regular(pCommon[0]) == pCurL); + // add the new decomposition entry + pThis->pDecs[ nEntries++ ] = pCurL; + // assign the support to be subtracted from both components + bSuppSubract = pCurL->S; + } + else // more than one components was found + { + // find the OR (EXOR) of the non-overlapping components + DdNode * bCommF; + dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, (int)(pPrevL->Type==DSD_NODE_EXOR) ); + Cudd_Ref( bCommF ); + + pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF ); + assert( !Dsd_IsComplement(pDENew) ); // cannot be complemented because of construction + Cudd_RecursiveDeref( dd, bCommF ); + + // add the new decomposition entry + pThis->pDecs[ nEntries++ ] = pDENew; + + // assign the support to be subtracted from both components + bSuppSubract = pDENew->S; + } + } + + SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ), Cudd_Ref( SuppL ); + Cudd_RecursiveDeref(dd, bTemp); + + SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH ); + Cudd_RecursiveDeref(dd, bTemp); + + } // end of if ( fEqualLevel ) + + } // end of decomposition list comparison + Cudd_RecursiveDeref( dd, SuppL ); + Cudd_RecursiveDeref( dd, SuppH ); + + } + + // check that the estimation of the number of entries was okay + assert( nEntries <= nEntriesMax ); + +// if ( nEntries != Extra_bddSuppSize(dd, bSuppNew) ) +// s_Case5++; + + // update the number of entries in the new decomposition list + pThis->nDecs = nEntries; + } +//} +EXIT: + + { + // if the component created is complemented, it represents a function without complement + // therefore, as it is, without complement, it should recieve the complemented function + Dsd_Node_t * pThisR = Dsd_Regular( pThis ); + assert( pThisR->G == NULL ); + assert( pThisR->S == NULL ); + + if ( pThisR == pThis ) // set regular function + pThisR->G = bF; + else // set complemented function + pThisR->G = Cudd_Not(bF); + Cudd_Ref(bF); // reference the function in the component + + assert( bSuppNew ); + pThisR->S = bSuppNew; // takes the reference from the new support + if ( st_insert( pDsdMan->Table, (char*)bF, (char*)pThis ) ) + { + assert( 0 ); + } + s_CacheEntries++; + + +/* + if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 ) + { + // write the function, for which verification does not work + cout << endl << "Internal verification failed!"" ); + + // create the variable mask + static int s_pVarMask[MAXINPUTS]; + int nInputCounter = 0; + + Cudd_SupportArray( dd, bF, s_pVarMask ); + int k; + for ( k = 0; k < dd->size; k++ ) + if ( s_pVarMask[k] ) + nInputCounter++; + + cout << endl << "The problem function is "" ); + + DdNode * zNewFunc = Cudd_zddIsopCover( dd, bF, bF ); Cudd_Ref( zNewFunc ); + cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask ); + Cudd_RecursiveDerefZdd( dd, zNewFunc ); + } +*/ + + } + + Depth--; + return Dsd_NotCond( pThis, fCompF ); +} + + +//////////////////////////////////////////////////////////////////////// +/// OTHER FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Finds the corresponding decomposition entry.] + + Description [This function returns the non-complemented pointer to the + DecEntry of that component which contains the given variable in its + support, or NULL if no such component exists] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity ) + +{ + Dsd_Node_t * pTemp; + int i; + +// assert( !Dsd_IsComplement( pWhere ) ); +// assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) ); + + if ( pWhere->nDecs == 1 ) + return NULL; + + for( i = 0; i < pWhere->nDecs; i++ ) + { + pTemp = Dsd_Regular( pWhere->pDecs[i] ); + if ( Extra_bddSuppContainVar( pDsdMan->dd, pTemp->S, Var ) ) + { + *fPolarity = (int)( pTemp != pWhere->pDecs[i] ); + return pTemp; + } + } + assert( 0 ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Find the common decomposition components.] + + Description [This function determines the common components. It counts + the number of common components in the decomposition lists of pL and pH + and returns their number and the lists of common components. It assumes + that pL and pH are regular pointers. It retuns also the pointers to the + last different components encountered in pL and pH.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH ) +{ + static Dsd_Node_t * Common[MAXINPUTS]; + int nCommon = 0; + + // pointers to the current decomposition entries + Dsd_Node_t * pLcur; + Dsd_Node_t * pHcur; + + // the pointers to their supports + DdNode * bSLcur; + DdNode * bSHcur; + + // the top variable in the supports + int TopVar; + + // the indices running through the components + int iCurL = 0; + int iCurH = 0; + while ( iCurL < pL->nDecs && iCurH < pH->nDecs ) + { // both did not run out + + pLcur = Dsd_Regular(pL->pDecs[iCurL]); + pHcur = Dsd_Regular(pH->pDecs[iCurH]); + + bSLcur = pLcur->S; + bSHcur = pHcur->S; + + // find out what component is higher in the BDD + if ( pDsdMan->dd->perm[bSLcur->index] < pDsdMan->dd->perm[bSHcur->index] ) + TopVar = bSLcur->index; + else + TopVar = bSHcur->index; + + if ( TopVar == bSLcur->index && TopVar == bSHcur->index ) + { + // the components may be equal - should match exactly! + if ( pL->pDecs[iCurL] == pH->pDecs[iCurH] ) + Common[nCommon++] = pL->pDecs[iCurL]; + else + { + *pLastDiffL = pL->pDecs[iCurL]; + *pLastDiffH = pH->pDecs[iCurH]; + } + + // skip both + iCurL++; + iCurH++; + } + else if ( TopVar == bSLcur->index ) + { // the components cannot be equal + // skip the top-most one + *pLastDiffL = pL->pDecs[iCurL++]; + } + else // if ( TopVar == bSHcur->index ) + { // the components cannot be equal + // skip the top-most one + *pLastDiffH = pH->pDecs[iCurH++]; + } + } + + // if one of the lists still has components, write the first one down + if ( iCurL < pL->nDecs ) + *pLastDiffL = pL->pDecs[iCurL]; + + if ( iCurH < pH->nDecs ) + *pLastDiffH = pH->pDecs[iCurH]; + + // return the pointer to the array + *pCommon = Common; + // return the number of common components + return nCommon; +} + +/**Function************************************************************* + + Synopsis [Computes the sum (OR or EXOR) of the functions of the components.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor ) +{ + DdManager * dd = pDsdMan->dd; + DdNode * bF, * bS, * bFadd, * bTemp; + Dsd_Node_t * pDE, * pDER; + int i; + + // start the function + bF = b0; Cudd_Ref( bF ); + // start the support + if ( pCompS ) + bS = b1, Cudd_Ref( bS ); + + assert( nCommon > 0 ); + for ( i = 0; i < nCommon; i++ ) + { + pDE = pCommon[i]; + pDER = Dsd_Regular( pDE ); + bFadd = (pDE != pDER)? Cudd_Not(pDER->G): pDER->G; + // add to the function + if ( fExor ) + bF = Cudd_bddXor( dd, bTemp = bF, bFadd ); + else + bF = Cudd_bddOr( dd, bTemp = bF, bFadd ); + Cudd_Ref( bF ); + Cudd_RecursiveDeref( dd, bTemp ); + if ( pCompS ) + { + // add to the support + bS = Cudd_bddAnd( dd, bTemp = bS, pDER->S ); Cudd_Ref( bS ); + Cudd_RecursiveDeref( dd, bTemp ); + } + } + // return the function + Cudd_Deref( bF ); + *pCompF = bF; + + // return the support + if ( pCompS ) + Cudd_Deref( bS ), *pCompS = bS; +} + +/**Function************************************************************* + + Synopsis [Checks support containment of the decomposition components.] + + Description [This function returns 1 if support of one component is contained + in that of another. In this case, pLarge (pSmall) is assigned to point to the + larger (smaller) support. If the supports are identical return 0, and does not + assign the components.] +] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall ) +{ + DdManager * dd = pDsdMan->dd; + DdNode * bSuppLarge, * bSuppSmall; + int RetValue; + + RetValue = Extra_bddSuppCheckContainment( dd, pL->S, pH->S, &bSuppLarge, &bSuppSmall ); + + if ( RetValue == 0 ) + return 0; + + if ( pH->S == bSuppLarge ) + { + *pLarge = pH; + *pSmall = pL; + } + else // if ( pL->S == bSuppLarge ) + { + *pLarge = pL; + *pSmall = pH; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Copies the list of components plus one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize ) +{ + int i; + assert( nListSize+1 == p->nDecs ); + p->pDecs[0] = First; + for( i = 0; i < nListSize; i++ ) + p->pDecs[i+1] = ppList[i]; +} + +/**Function************************************************************* + + Synopsis [Copies the list of components plus one, and skips one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int iSkipped ) +{ + int i, Counter; + assert( nListSize == p->nDecs ); + p->pDecs[0] = First; + for( i = 0, Counter = 1; i < nListSize; i++ ) + if ( i != iSkipped ) + p->pDecs[Counter++] = ppList[i]; +} + +/**Function************************************************************* + + Synopsis [Debugging procedure to compute the functionality of the decomposed structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ) +{ + DdManager * dd = pDsdMan->dd; + Dsd_Node_t * pR = Dsd_Regular(pDE); + int fCompP = (int)( pDE != pR ); + int RetValue; + + DdNode * bRes; + if ( pR->Type == DSD_NODE_CONST1 ) + bRes = b1; + else if ( pR->Type == DSD_NODE_BUF ) + bRes = pR->G; + else if ( pR->Type == DSD_NODE_OR || pR->Type == DSD_NODE_EXOR ) + dsdKernelComputeSumOfComponents( pDsdMan, pR->pDecs, pR->nDecs, &bRes, NULL, (int)(pR->Type == DSD_NODE_EXOR) ); + else if ( pR->Type == DSD_NODE_PRIME ) + { + int i; + static DdNode * bGVars[MAXINPUTS]; + // transform the function of this block, so that it depended on inputs + // corresponding to the formal inputs + DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 ); Cudd_Ref( bNewFunc ); + + // compose this function with the inputs + // create the elementary permutation + for ( i = 0; i < dd->size; i++ ) + bGVars[i] = dd->vars[i]; + + // assign functions to be composed + for ( i = 0; i < pR->nDecs; i++ ) + bGVars[dd->invperm[i]] = pR->pDecs[i]->G; + + // perform the composition + bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bNewFunc ); + + ///////////////////////////////////////////////////////// + RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) ); + ///////////////////////////////////////////////////////// + Cudd_Deref( bRes ); + } + else + { + assert(0); + } + + Cudd_Ref( bRes ); + RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) ); + Cudd_RecursiveDeref( dd, bRes ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// |