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