/**CFile**************************************************************** FileName [extraBddImage.c] PackageName [extra] Synopsis [Various reusable software utilities.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - September 1, 2003.] Revision [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] ***********************************************************************/ #include "extraBdd.h" ABC_NAMESPACE_IMPL_START /* The ideas implemented in this file are inspired by the paper: Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple, Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in Image Computation. ICCAD, 2001. */ /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ typedef struct Extra_ImageNode_t_ Extra_ImageNode_t; typedef struct Extra_ImagePart_t_ Extra_ImagePart_t; typedef struct Extra_ImageVar_t_ Extra_ImageVar_t; struct Extra_ImageTree_t_ { Extra_ImageNode_t * pRoot; // the root of quantification tree Extra_ImageNode_t * pCare; // the leaf node with the care set DdNode * bCareSupp; // the cube to quantify from the care int fVerbose; // the verbosity flag int nNodesMax; // the max number of nodes in one iter int nNodesMaxT; // the overall max number of nodes int nIter; // the number of iterations with this tree }; struct Extra_ImageNode_t_ { DdManager * dd; // the manager DdNode * bCube; // the cube to quantify DdNode * bImage; // the partial image Extra_ImageNode_t * pNode1; // the first branch Extra_ImageNode_t * pNode2; // the second branch Extra_ImagePart_t * pPart; // the partition (temporary) }; struct Extra_ImagePart_t_ { DdNode * bFunc; // the partition DdNode * bSupp; // the support of this partition int nNodes; // the number of BDD nodes short nSupp; // the number of support variables short iPart; // the number of this partition }; struct Extra_ImageVar_t_ { int iNum; // the BDD index of this variable DdNode * bParts; // the partition numbers int nParts; // the number of partitions }; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd, int nParts, DdNode ** pbParts, DdNode * bCare ); static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd, int nParts, Extra_ImagePart_t ** pParts, int nVars, DdNode ** pbVarsNs ); static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, int nParts, Extra_ImagePart_t ** pParts, int nVars, Extra_ImageVar_t ** pVars ); static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode ); static int Extra_BuildTreeNode( DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes, int nVars, Extra_ImageVar_t ** pVars ); static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes ); static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode ); static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode ); static int Extra_FindBestVariable( DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes, int nVars, Extra_ImageVar_t ** pVars ); static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, int nNodes, Extra_ImageNode_t ** pNodes, int * piNode1, int * piNode2 ); static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube, Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 ); static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, int nVars, DdNode ** pbVars ); static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, DdNode * bVarsCs, DdNode * bVarsNs, int iPart ); static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree ); static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset ); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function************************************************************* Synopsis [Starts the image computation using tree-based scheduling.] Description [This procedure starts the image computation. It uses the given care set to test-run the image computation and creates the quantification tree by scheduling variable quantifications. The tree can be used to compute images for other care sets without rescheduling. In this case, Extra_bddImageCompute() should be called.] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImageTree_t * Extra_bddImageStart( DdManager * dd, DdNode * bCare, // the care set int nParts, DdNode ** pbParts, // the partitions for image computation int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!) { Extra_ImageTree_t * pTree; Extra_ImagePart_t ** pParts; Extra_ImageVar_t ** pVars; Extra_ImageNode_t ** pNodes; int v; if ( fVerbose && dd->size <= 80 ) Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars ); // create variables, partitions and leaf nodes pParts = Extra_CreateParts( dd, nParts, pbParts, bCare ); pVars = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars ); pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars ); // create the tree pTree = ABC_ALLOC( Extra_ImageTree_t, 1 ); memset( pTree, 0, sizeof(Extra_ImageTree_t) ); pTree->pCare = pNodes[nParts]; pTree->fVerbose = fVerbose; // process the nodes while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) ); // make sure the variables are gone for ( v = 0; v < dd->size; v++ ) assert( pVars[v] == NULL ); ABC_FREE( pVars ); // merge the topmost nodes while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL ); // make sure the nodes are gone for ( v = 0; v < nParts + 1; v++ ) assert( pNodes[v] == NULL ); ABC_FREE( pNodes ); // if ( fVerbose ) // Extra_bddImagePrintTree( pTree ); // set the support of the care set pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp ); // clean the partitions Extra_DeleteParts_rec( pTree->pRoot ); ABC_FREE( pParts ); return pTree; } /**Function************************************************************* Synopsis [Compute the image.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare ) { DdManager * dd = pTree->pCare->dd; DdNode * bSupp, * bRem; pTree->nIter++; // make sure the supports are okay bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp ); if ( bSupp != pTree->bCareSupp ) { bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem ); if ( bRem != b1 ) { printf( "Original care set support: " ); ABC_PRB( dd, pTree->bCareSupp ); printf( "Current care set support: " ); ABC_PRB( dd, bSupp ); Cudd_RecursiveDeref( dd, bSupp ); Cudd_RecursiveDeref( dd, bRem ); printf( "The care set depends on some vars that were not in the care set during scheduling.\n" ); return NULL; } Cudd_RecursiveDeref( dd, bRem ); } Cudd_RecursiveDeref( dd, bSupp ); // remove the previous image Cudd_RecursiveDeref( dd, pTree->pCare->bImage ); pTree->pCare->bImage = bCare; Cudd_Ref( bCare ); // compute the image pTree->nNodesMax = 0; Extra_bddImageCompute_rec( pTree, pTree->pRoot ); if ( pTree->nNodesMaxT < pTree->nNodesMax ) pTree->nNodesMaxT = pTree->nNodesMax; // if ( pTree->fVerbose ) // printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax ); return pTree->pRoot->bImage; } /**Function************************************************************* Synopsis [Delete the tree.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree ) { if ( pTree->bCareSupp ) Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp ); Extra_bddImageTreeDelete_rec( pTree->pRoot ); ABC_FREE( pTree ); } /**Function************************************************************* Synopsis [Reads the image from the tree.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree ) { return pTree->pRoot->bImage; } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static Functions */ /*---------------------------------------------------------------------------*/ /**Function************************************************************* Synopsis [Creates partitions.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd, int nParts, DdNode ** pbParts, DdNode * bCare ) { Extra_ImagePart_t ** pParts; int i; // start the partitions pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 ); // create structures for each variable for ( i = 0; i < nParts; i++ ) { pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 ); pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc ); pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp ); pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp ); pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc ); pParts[i]->iPart = i; } // add the care set as the last partition pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 ); pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc ); pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp ); pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp ); pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc ); pParts[nParts]->iPart = nParts; return pParts; } /**Function************************************************************* Synopsis [Creates variables.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd, int nParts, Extra_ImagePart_t ** pParts, int nVars, DdNode ** pbVars ) { Extra_ImageVar_t ** pVars; DdNode ** pbFuncs; DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp; int nVarsTotal, iVar, p, Counter; // put all the functions into one array pbFuncs = ABC_ALLOC( DdNode *, nParts ); for ( p = 0; p < nParts; p++ ) pbFuncs[p] = pParts[p]->bSupp; bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp ); ABC_FREE( pbFuncs ); // remove the NS vars bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs ); bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bCubeNs ); // get the number of I and CS variables to be quantified nVarsTotal = Extra_bddSuppSize( dd, bSupp ); // start the variables pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size ); memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size ); // create structures for each variable for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) ) { iVar = bSuppTemp->index; pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 ); pVars[iVar]->iNum = iVar; // collect all the parts this var belongs to Counter = 0; bParts = b1; Cudd_Ref( bParts ); for ( p = 0; p < nParts; p++ ) if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) ) { bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts ); Cudd_RecursiveDeref( dd, bTemp ); Counter++; } pVars[iVar]->bParts = bParts; // takes ref pVars[iVar]->nParts = Counter; } Cudd_RecursiveDeref( dd, bSupp ); return pVars; } /**Function************************************************************* Synopsis [Creates variables.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, int nParts, Extra_ImagePart_t ** pParts, int nVars, Extra_ImageVar_t ** pVars ) { Extra_ImageNode_t ** pNodes; Extra_ImageNode_t * pNode; DdNode * bTemp; int i, v, iPart; /* DdManager * dd; // the manager DdNode * bCube; // the cube to quantify DdNode * bImage; // the partial image Extra_ImageNode_t * pNode1; // the first branch Extra_ImageNode_t * pNode2; // the second branch Extra_ImagePart_t * pPart; // the partition (temporary) */ // start the partitions pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts ); // create structures for each leaf nodes for ( i = 0; i < nParts; i++ ) { pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 ); memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) ); pNodes[i]->dd = dd; pNodes[i]->pPart = pParts[i]; } // find the quantification cubes for each leaf node for ( v = 0; v < nVars; v++ ) { if ( pVars[v] == NULL ) continue; assert( pVars[v]->nParts > 0 ); if ( pVars[v]->nParts > 1 ) continue; iPart = pVars[v]->bParts->index; if ( pNodes[iPart]->bCube == NULL ) { pNodes[iPart]->bCube = dd->vars[v]; Cudd_Ref( dd->vars[v] ); } else { pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] ); Cudd_Ref( pNodes[iPart]->bCube ); Cudd_RecursiveDeref( dd, bTemp ); } // remove these variables Cudd_RecursiveDeref( dd, pVars[v]->bParts ); ABC_FREE( pVars[v] ); } // assign the leaf node images for ( i = 0; i < nParts; i++ ) { pNode = pNodes[i]; if ( pNode->bCube ) { // update the partition pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube ); Cudd_Ref( pParts[i]->bFunc ); Cudd_RecursiveDeref( dd, bTemp ); // update the support the partition pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube ); Cudd_Ref( pParts[i]->bSupp ); Cudd_RecursiveDeref( dd, bTemp ); // update the numbers pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp ); pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc ); // get rid of the cube // save the last (care set) quantification cube if ( i < nParts - 1 ) { Cudd_RecursiveDeref( dd, pNode->bCube ); pNode->bCube = NULL; } } // copy the function pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage ); } /* for ( i = 0; i < nParts; i++ ) { pNode = pNodes[i]; ABC_PRB( dd, pNode->bCube ); ABC_PRB( dd, pNode->pPart->bFunc ); ABC_PRB( dd, pNode->pPart->bSupp ); printf( "\n" ); } */ return pNodes; } /**Function************************************************************* Synopsis [Delete the partitions from the nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode ) { Extra_ImagePart_t * pPart; if ( pNode->pNode1 ) Extra_DeleteParts_rec( pNode->pNode1 ); if ( pNode->pNode2 ) Extra_DeleteParts_rec( pNode->pNode2 ); pPart = pNode->pPart; Cudd_RecursiveDeref( pNode->dd, pPart->bFunc ); Cudd_RecursiveDeref( pNode->dd, pPart->bSupp ); ABC_FREE( pNode->pPart ); } /**Function************************************************************* Synopsis [Delete the partitions from the nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode ) { if ( pNode->pNode1 ) Extra_bddImageTreeDelete_rec( pNode->pNode1 ); if ( pNode->pNode2 ) Extra_bddImageTreeDelete_rec( pNode->pNode2 ); if ( pNode->bCube ) Cudd_RecursiveDeref( pNode->dd, pNode->bCube ); if ( pNode->bImage ) Cudd_RecursiveDeref( pNode->dd, pNode->bImage ); assert( pNode->pPart == NULL ); ABC_FREE( pNode ); } /**Function************************************************************* Synopsis [Recompute the image.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode ) { DdManager * dd = pNode->dd; DdNode * bTemp; int nNodes; // trivial case if ( pNode->pNode1 == NULL ) { if ( pNode->bCube ) { pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube ); Cudd_Ref( pNode->bImage ); Cudd_RecursiveDeref( dd, bTemp ); } return; } // compute the children if ( pNode->pNode1 ) Extra_bddImageCompute_rec( pTree, pNode->pNode1 ); if ( pNode->pNode2 ) Extra_bddImageCompute_rec( pTree, pNode->pNode2 ); // clean the old image if ( pNode->bImage ) Cudd_RecursiveDeref( dd, pNode->bImage ); pNode->bImage = NULL; // compute the new image if ( pNode->bCube ) pNode->bImage = Cudd_bddAndAbstract( dd, pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube ); else pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage ); Cudd_Ref( pNode->bImage ); if ( pTree->fVerbose ) { nNodes = Cudd_DagSize( pNode->bImage ); if ( pTree->nNodesMax < nNodes ) pTree->nNodesMax = nNodes; } } /**Function************************************************************* Synopsis [Builds the tree.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Extra_BuildTreeNode( DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes, int nVars, Extra_ImageVar_t ** pVars ) { Extra_ImageNode_t * pNode1, * pNode2; Extra_ImageVar_t * pVar; Extra_ImageNode_t * pNode; DdNode * bCube, * bTemp, * bSuppTemp, * bParts; int iNode1, iNode2; int iVarBest, nSupp, v; // find the best variable iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars ); if ( iVarBest == -1 ) return 0; pVar = pVars[iVarBest]; // this var cannot appear in one partition only nSupp = Extra_bddSuppSize( dd, pVar->bParts ); assert( nSupp == pVar->nParts ); assert( nSupp != 1 ); // if it appears in only two partitions, quantify it if ( pVar->nParts == 2 ) { // get the nodes iNode1 = pVar->bParts->index; iNode2 = cuddT(pVar->bParts)->index; pNode1 = pNodes[iNode1]; pNode2 = pNodes[iNode2]; // get the quantification cube bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube ); // add the variables that appear only in these partitions for ( v = 0; v < nVars; v++ ) if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts ) { // add this var bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube ); Cudd_RecursiveDeref( dd, bTemp ); // clean this var Cudd_RecursiveDeref( dd, pVars[v]->bParts ); ABC_FREE( pVars[v] ); } // clean the best var Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts ); ABC_FREE( pVars[iVarBest] ); // combines two nodes pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 ); Cudd_RecursiveDeref( dd, bCube ); } else // if ( pVar->nParts > 2 ) { // find two smallest BDDs that have this var Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 ); pNode1 = pNodes[iNode1]; pNode2 = pNodes[iNode2]; // it is not possible that a var appears only in these two // otherwise, it would have a different cost bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts ); for ( v = 0; v < nVars; v++ ) if ( pVars[v] && pVars[v]->bParts == bParts ) assert( 0 ); Cudd_RecursiveDeref( dd, bParts ); // combines two nodes pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 ); } // clean the old nodes pNodes[iNode1] = pNode; pNodes[iNode2] = NULL; // update the variables that appear in pNode[iNode2] for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) ) { pVar = pVars[bSuppTemp->index]; if ( pVar == NULL ) // this variable is not be quantified continue; // quantify this var assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) ); pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts ); Cudd_RecursiveDeref( dd, bTemp ); // add the new var pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts ); Cudd_RecursiveDeref( dd, bTemp ); // update the score pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts ); } return 1; } /**Function************************************************************* Synopsis [Merges the nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes ) { Extra_ImageNode_t * pNode; int n1 = -1, n2 = -1, n; // find the first and the second non-empty spots for ( n = 0; n < nNodes; n++ ) if ( pNodes[n] ) { if ( n1 == -1 ) n1 = n; else if ( n2 == -1 ) { n2 = n; break; } } assert( n1 != -1 ); // check the situation when only one such node is detected if ( n2 == -1 ) { // save the node pNode = pNodes[n1]; // clean the node pNodes[n1] = NULL; return pNode; } // combines two nodes pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] ); // clean the old nodes pNodes[n1] = pNode; pNodes[n2] = NULL; return NULL; } /**Function************************************************************* Synopsis [Merges two nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube, Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 ) { Extra_ImageNode_t * pNode; Extra_ImagePart_t * pPart; // create a new partition pPart = ABC_ALLOC( Extra_ImagePart_t, 1 ); memset( pPart, 0, sizeof(Extra_ImagePart_t) ); // create the function pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc ); // update the support the partition pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube ); Cudd_Ref( pPart->bSupp ); // update the numbers pPart->nSupp = Extra_bddSuppSize( dd, pPart->bSupp ); pPart->nNodes = Cudd_DagSize( pPart->bFunc ); pPart->iPart = -1; /* ABC_PRB( dd, pNode1->pPart->bSupp ); ABC_PRB( dd, pNode2->pPart->bSupp ); ABC_PRB( dd, pPart->bSupp ); */ // create a new node pNode = ABC_ALLOC( Extra_ImageNode_t, 1 ); memset( pNode, 0, sizeof(Extra_ImageNode_t) ); pNode->dd = dd; pNode->pPart = pPart; pNode->pNode1 = pNode1; pNode->pNode2 = pNode2; // compute the image pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube ); Cudd_Ref( pNode->bImage ); // save the cube if ( bCube != b1 ) { pNode->bCube = bCube; Cudd_Ref( bCube ); } return pNode; } /**Function************************************************************* Synopsis [Computes the best variable.] Description [The variables is the best if the sum of squares of the BDD sizes of the partitions, in which it participates, is the minimum.] SideEffects [] SeeAlso [] ***********************************************************************/ int Extra_FindBestVariable( DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes, int nVars, Extra_ImageVar_t ** pVars ) { DdNode * bTemp; int iVarBest, v; double CostBest, CostCur; CostBest = 100000000000000.0; iVarBest = -1; for ( v = 0; v < nVars; v++ ) if ( pVars[v] ) { CostCur = 0; for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) ) CostCur += pNodes[bTemp->index]->pPart->nNodes * pNodes[bTemp->index]->pPart->nNodes; if ( CostBest > CostCur ) { CostBest = CostCur; iVarBest = v; } } return iVarBest; } /**Function************************************************************* Synopsis [Computes two smallest partions that have this var.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, int nNodes, Extra_ImageNode_t ** pNodes, int * piNode1, int * piNode2 ) { DdNode * bTemp; int iPart1, iPart2; int CostMin1, CostMin2, Cost; // go through the partitions iPart1 = iPart2 = -1; CostMin1 = CostMin2 = 1000000; for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) ) { Cost = pNodes[bTemp->index]->pPart->nNodes; if ( CostMin1 > Cost ) { CostMin2 = CostMin1; iPart2 = iPart1; CostMin1 = Cost; iPart1 = bTemp->index; } else if ( CostMin2 > Cost ) { CostMin2 = Cost; iPart2 = bTemp->index; } } *piNode1 = iPart1; *piNode2 = iPart2; } /**Function************************************************************* Synopsis [Prints the latch dependency matrix.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare, // the care set int nParts, DdNode ** pbParts, // the partitions for image computation int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!) { int i; DdNode * bVarsCs, * bVarsNs; bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs ); bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs ); printf( "The latch dependency matrix:\n" ); printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n", nParts, dd->size, nVars ); printf( " : " ); for ( i = 0; i < dd->size; i++ ) printf( "%d", i % 10 ); printf( "\n" ); for ( i = 0; i < nParts; i++ ) Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i ); Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts ); Cudd_RecursiveDeref( dd, bVarsCs ); Cudd_RecursiveDeref( dd, bVarsNs ); } /**Function************************************************************* Synopsis [Prints one row of the latch dependency matrix.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, // the function DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars int iPart ) { DdNode * bSupport; int v; bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport ); printf( " %3d : ", iPart ); for ( v = 0; v < dd->size; v++ ) { if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) ) { if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) ) printf( "c" ); else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) ) printf( "n" ); else printf( "i" ); } else printf( "." ); } printf( "\n" ); Cudd_RecursiveDeref( dd, bSupport ); } /**Function************************************************************* Synopsis [Prints the tree for quenstification scheduling.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree ) { printf( "The quantification scheduling tree:\n" ); Extra_bddImagePrintTree_rec( pTree->pRoot, 1 ); } /**Function************************************************************* Synopsis [Prints the tree for quenstification scheduling.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset ) { DdNode * Cube; int i; Cube = pNode->bCube; if ( pNode->pNode1 == NULL ) { printf( "<%d> ", pNode->pPart->iPart ); if ( Cube != NULL ) { ABC_PRB( pNode->dd, Cube ); } else printf( "\n" ); return; } printf( "<*> " ); if ( Cube != NULL ) { ABC_PRB( pNode->dd, Cube ); } else printf( "\n" ); for ( i = 0; i < Offset; i++ ) printf( " " ); Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 ); for ( i = 0; i < Offset; i++ ) printf( " " ); Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 ); } struct Extra_ImageTree2_t_ { DdManager * dd; DdNode * bRel; DdNode * bCube; DdNode * bImage; }; /**Function************************************************************* Synopsis [Starts the monolithic image computation.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Extra_ImageTree2_t * Extra_bddImageStart2( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, int nVars, DdNode ** pbVars, int fVerbose ) { Extra_ImageTree2_t * pTree; DdNode * bCubeAll, * bCubeNot, * bTemp; int i; pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 ); pTree->dd = dd; pTree->bImage = NULL; bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll ); bCubeNot = Extra_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot ); pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube ); Cudd_RecursiveDeref( dd, bCubeAll ); Cudd_RecursiveDeref( dd, bCubeNot ); // derive the monolithic relation pTree->bRel = b1; Cudd_Ref( pTree->bRel ); for ( i = 0; i < nParts; i++ ) { pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel ); Cudd_RecursiveDeref( dd, bTemp ); } Extra_bddImageCompute2( pTree, bCare ); return pTree; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare ) { if ( pTree->bImage ) Cudd_RecursiveDeref( pTree->dd, pTree->bImage ); pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); Cudd_Ref( pTree->bImage ); return pTree->bImage; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree ) { if ( pTree->bRel ) Cudd_RecursiveDeref( pTree->dd, pTree->bRel ); if ( pTree->bCube ) Cudd_RecursiveDeref( pTree->dd, pTree->bCube ); if ( pTree->bImage ) Cudd_RecursiveDeref( pTree->dd, pTree->bImage ); ABC_FREE( pTree ); } /**Function************************************************************* Synopsis [Returns the previously computed image.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree ) { return pTree->bImage; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END