summaryrefslogtreecommitdiffstats
path: root/src/proof/bbr/bbrImage.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/bbr/bbrImage.c')
-rw-r--r--src/proof/bbr/bbrImage.c1327
1 files changed, 1327 insertions, 0 deletions
diff --git a/src/proof/bbr/bbrImage.c b/src/proof/bbr/bbrImage.c
new file mode 100644
index 00000000..23b43169
--- /dev/null
+++ b/src/proof/bbr/bbrImage.c
@@ -0,0 +1,1327 @@
+/**CFile****************************************************************
+
+ FileName [bbrImage.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [BDD-based reachability analysis.]
+
+ Synopsis [Performs image computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: bbrImage.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bbr.h"
+#include "src/bdd/mtr/mtr.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 Bbr_ImageNode_t_ Bbr_ImageNode_t;
+typedef struct Bbr_ImagePart_t_ Bbr_ImagePart_t;
+typedef struct Bbr_ImageVar_t_ Bbr_ImageVar_t;
+
+struct Bbr_ImageTree_t_
+{
+ Bbr_ImageNode_t * pRoot; // the root of quantification tree
+ Bbr_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
+ int nBddMax; // the number of node to stop
+};
+
+struct Bbr_ImageNode_t_
+{
+ DdManager * dd; // the manager
+ DdNode * bCube; // the cube to quantify
+ DdNode * bImage; // the partial image
+ Bbr_ImageNode_t * pNode1; // the first branch
+ Bbr_ImageNode_t * pNode2; // the second branch
+ Bbr_ImagePart_t * pPart; // the partition (temporary)
+};
+
+struct Bbr_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 Bbr_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 */
+/*---------------------------------------------------------------------------*/
+
+#define b0 Cudd_Not((dd)->one)
+#define b1 (dd)->one
+
+#ifndef ABC_PRB
+#define ABC_PRB(dd,f) printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")
+#endif
+
+/**AutomaticStart*************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+static Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
+ int nParts, DdNode ** pbParts, DdNode * bCare );
+static Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
+ int nParts, Bbr_ImagePart_t ** pParts,
+ int nVars, DdNode ** pbVarsNs );
+static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
+ int nParts, Bbr_ImagePart_t ** pParts,
+ int nVars, Bbr_ImageVar_t ** pVars );
+static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
+static int Bbr_BuildTreeNode( DdManager * dd,
+ int nNodes, Bbr_ImageNode_t ** pNodes,
+ int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax );
+static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd,
+ int nNodes, Bbr_ImageNode_t ** pNodes );
+static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
+static int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode );
+static int Bbr_FindBestVariable( DdManager * dd,
+ int nNodes, Bbr_ImageNode_t ** pNodes,
+ int nVars, Bbr_ImageVar_t ** pVars );
+static void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts,
+ int nNodes, Bbr_ImageNode_t ** pNodes,
+ int * piNode1, int * piNode2 );
+static Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+ Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 );
+
+static void Bbr_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
+ int nParts, DdNode ** pbParts,
+ int nVars, DdNode ** pbVars );
+static void Bbr_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc,
+ DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
+
+static void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree );
+static void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int nOffset );
+
+static void Bbr_bddPrint( DdManager * dd, DdNode * F );
+
+/**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, Bbr_bddImageCompute() should be called.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Bbr_ImageTree_t * Bbr_bddImageStart(
+ DdManager * dd, DdNode * bCare, // the care set
+ int nParts, DdNode ** pbParts, // the partitions for image computation
+ int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ) // the NS and parameter variables (not quantified!)
+{
+ Bbr_ImageTree_t * pTree;
+ Bbr_ImagePart_t ** pParts;
+ Bbr_ImageVar_t ** pVars;
+ Bbr_ImageNode_t ** pNodes, * pCare;
+ int fStop, v;
+
+ if ( fVerbose && dd->size <= 80 )
+ Bbr_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
+
+ // create variables, partitions and leaf nodes
+ pParts = Bbr_CreateParts( dd, nParts, pbParts, bCare );
+ pVars = Bbr_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
+ pNodes = Bbr_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
+ pCare = pNodes[nParts];
+
+ // process the nodes
+ while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );
+
+ // consider the case of BDD node blowup
+ if ( fStop )
+ {
+ for ( v = 0; v < dd->size; v++ )
+ if ( pVars[v] )
+ ABC_FREE( pVars[v] );
+ ABC_FREE( pVars );
+ for ( v = 0; v <= nParts; v++ )
+ if ( pNodes[v] )
+ {
+ Bbr_DeleteParts_rec( pNodes[v] );
+ Bbr_bddImageTreeDelete_rec( pNodes[v] );
+ }
+ ABC_FREE( pNodes );
+ ABC_FREE( pParts );
+ return NULL;
+ }
+
+ // make sure the variables are gone
+ for ( v = 0; v < dd->size; v++ )
+ assert( pVars[v] == NULL );
+ ABC_FREE( pVars );
+
+ // create the tree
+ pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
+ memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
+ pTree->pCare = pCare;
+ pTree->nBddMax = nBddMax;
+ pTree->fVerbose = fVerbose;
+
+ // merge the topmost nodes
+ while ( (pTree->pRoot = Bbr_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 )
+// Bbr_bddImagePrintTree( pTree );
+
+ // set the support of the care set
+ pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp );
+
+ // clean the partitions
+ Bbr_DeleteParts_rec( pTree->pRoot );
+ ABC_FREE( pParts );
+
+ return pTree;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute the image.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Bbr_bddImageCompute( Bbr_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;
+ if ( !Bbr_bddImageCompute_rec( pTree, pTree->pRoot ) )
+ return NULL;
+ 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 Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree )
+{
+ if ( pTree->bCareSupp )
+ Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
+ Bbr_bddImageTreeDelete_rec( pTree->pRoot );
+ ABC_FREE( pTree );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the image from the tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree )
+{
+ return pTree->pRoot->bImage;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+ Synopsis [Outputs the BDD in a readable format.]
+
+ Description []
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+void Bbr_bddPrint( DdManager * dd, DdNode * F )
+{
+ DdGen * Gen;
+ int * Cube;
+ CUDD_VALUE_TYPE Value;
+ int nVars = dd->size;
+ int fFirstCube = 1;
+ int i;
+
+ if ( F == NULL )
+ {
+ printf("NULL");
+ return;
+ }
+ if ( F == b0 )
+ {
+ printf("Constant 0");
+ return;
+ }
+ if ( F == b1 )
+ {
+ printf("Constant 1");
+ return;
+ }
+
+ Cudd_ForeachCube( dd, F, Gen, Cube, Value )
+ {
+ if ( fFirstCube )
+ fFirstCube = 0;
+ else
+// Output << " + ";
+ printf( " + " );
+
+ for ( i = 0; i < nVars; i++ )
+ if ( Cube[i] == 0 )
+ printf( "[%d]'", i );
+// printf( "%c'", (char)('a'+i) );
+ else if ( Cube[i] == 1 )
+ printf( "[%d]", i );
+// printf( "%c", (char)('a'+i) );
+ }
+
+// printf("\n");
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+ Synopsis [Creates partitions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
+ int nParts, DdNode ** pbParts, DdNode * bCare )
+{
+ Bbr_ImagePart_t ** pParts;
+ int i;
+
+ // start the partitions
+ pParts = ABC_ALLOC( Bbr_ImagePart_t *, nParts + 1 );
+ // create structures for each variable
+ for ( i = 0; i < nParts; i++ )
+ {
+ pParts[i] = ABC_ALLOC( Bbr_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 = Cudd_SupportSize( 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( Bbr_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 = Cudd_SupportSize( 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 []
+
+***********************************************************************/
+Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
+ int nParts, Bbr_ImagePart_t ** pParts,
+ int nVars, DdNode ** pbVars )
+{
+ Bbr_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 = Cudd_SupportSize( dd, bSupp );
+
+ // start the variables
+ pVars = ABC_ALLOC( Bbr_ImageVar_t *, dd->size );
+ memset( pVars, 0, sizeof(Bbr_ImageVar_t *) * dd->size );
+ // create structures for each variable
+ for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+ {
+ iVar = bSuppTemp->index;
+ pVars[iVar] = ABC_ALLOC( Bbr_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 []
+
+***********************************************************************/
+Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
+ int nParts, Bbr_ImagePart_t ** pParts,
+ int nVars, Bbr_ImageVar_t ** pVars )
+{
+ Bbr_ImageNode_t ** pNodes;
+ Bbr_ImageNode_t * pNode;
+ DdNode * bTemp;
+ int i, v, iPart;
+/*
+ DdManager * dd; // the manager
+ DdNode * bCube; // the cube to quantify
+ DdNode * bImage; // the partial image
+ Bbr_ImageNode_t * pNode1; // the first branch
+ Bbr_ImageNode_t * pNode2; // the second branch
+ Bbr_ImagePart_t * pPart; // the partition (temporary)
+*/
+ // start the partitions
+ pNodes = ABC_ALLOC( Bbr_ImageNode_t *, nParts );
+ // create structures for each leaf nodes
+ for ( i = 0; i < nParts; i++ )
+ {
+ pNodes[i] = ABC_ALLOC( Bbr_ImageNode_t, 1 );
+ memset( pNodes[i], 0, sizeof(Bbr_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 = Cudd_SupportSize( 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 Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode )
+{
+ Bbr_ImagePart_t * pPart;
+ if ( pNode->pNode1 )
+ Bbr_DeleteParts_rec( pNode->pNode1 );
+ if ( pNode->pNode2 )
+ Bbr_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 Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode )
+{
+ if ( pNode->pNode1 )
+ Bbr_bddImageTreeDelete_rec( pNode->pNode1 );
+ if ( pNode->pNode2 )
+ Bbr_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 []
+
+***********************************************************************/
+int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_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 1;
+ }
+
+ // compute the children
+ if ( pNode->pNode1 )
+ if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode1 ) )
+ return 0;
+ if ( pNode->pNode2 )
+ if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode2 ) )
+ return 0;
+
+ // 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;
+ }
+ if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Builds the tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bbr_BuildTreeNode( DdManager * dd,
+ int nNodes, Bbr_ImageNode_t ** pNodes,
+ int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax )
+{
+ Bbr_ImageNode_t * pNode1, * pNode2;
+ Bbr_ImageVar_t * pVar;
+ Bbr_ImageNode_t * pNode;
+ DdNode * bCube, * bTemp, * bSuppTemp;//, * bParts;
+ int iNode1, iNode2;
+ int iVarBest, nSupp, v;
+
+ // find the best variable
+ iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
+ if ( iVarBest == -1 )
+ return 0;
+/*
+for ( v = 0; v < nVars; v++ )
+{
+ DdNode * bSupp;
+ if ( pVars[v] == NULL )
+ continue;
+ printf( "%3d :", v );
+ printf( "%3d ", pVars[v]->nParts );
+ bSupp = Cudd_Support( dd, pVars[v]->bParts ); Cudd_Ref( bSupp );
+ Bbr_bddPrint( dd, bSupp ); printf( "\n" );
+ Cudd_RecursiveDeref( dd, bSupp );
+}
+*/
+ pVar = pVars[iVarBest];
+
+ // this var cannot appear in one partition only
+ nSupp = Cudd_SupportSize( dd, pVar->bParts );
+ assert( nSupp == pVar->nParts );
+ assert( nSupp != 1 );
+//printf( "var = %d supp = %d\n\n", iVarBest, nSupp );
+
+ // 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 = Bbr_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
+ Cudd_RecursiveDeref( dd, bCube );
+ }
+ else // if ( pVar->nParts > 2 )
+ {
+ // find two smallest BDDs that have this var
+ Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
+ pNode1 = pNodes[iNode1];
+ pNode2 = pNodes[iNode2];
+//printf( "smallest bdds with this var: %d %d\n", iNode1, 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 = Bbr_CombineTwoNodes( dd, b1, pNode1, pNode2 );
+ }
+
+ // clean the old nodes
+ pNodes[iNode1] = pNode;
+ pNodes[iNode2] = NULL;
+//printf( "Removing node %d (leaving node %d)\n", iNode2, iNode1 );
+
+ // 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 = Cudd_SupportSize( dd, pVar->bParts );
+ }
+
+ *pfStop = 0;
+ if ( dd->keys-dd->dead > (unsigned)nBddMax )
+ {
+ *pfStop = 1;
+ return 0;
+ }
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Merges the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Bbr_ImageNode_t * Bbr_MergeTopNodes(
+ DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes )
+{
+ Bbr_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 = Bbr_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 []
+
+***********************************************************************/
+Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+ Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 )
+{
+ Bbr_ImageNode_t * pNode;
+ Bbr_ImagePart_t * pPart;
+
+ // create a new partition
+ pPart = ABC_ALLOC( Bbr_ImagePart_t, 1 );
+ memset( pPart, 0, sizeof(Bbr_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 = Cudd_SupportSize( 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( Bbr_ImageNode_t, 1 );
+ memset( pNode, 0, sizeof(Bbr_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 Bbr_FindBestVariable( DdManager * dd,
+ int nNodes, Bbr_ImageNode_t ** pNodes,
+ int nVars, Bbr_ImageVar_t ** pVars )
+{
+ DdNode * bTemp;
+ int iVarBest, v;
+ double CostBest, CostCur;
+
+ CostBest = 100000000000000.0;
+ iVarBest = -1;
+
+ // check if there are two-variable partitions
+ for ( v = 0; v < nVars; v++ )
+ if ( pVars[v] && pVars[v]->nParts == 2 )
+ {
+ 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;
+ }
+ }
+ if ( iVarBest >= 0 )
+ return iVarBest;
+
+ // find other partition
+ for ( v = 0; v < nVars; v++ )
+ if ( pVars[v] )
+ {
+ assert( pVars[v]->nParts > 1 );
+ 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 Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts,
+ int nNodes, Bbr_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 Bbr_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++ )
+ Bbr_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
+ Bbr_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 Bbr_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 Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree )
+{
+ printf( "The quantification scheduling tree:\n" );
+ Bbr_bddImagePrintTree_rec( pTree->pRoot, 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the tree for quenstification scheduling.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bbr_bddImagePrintTree_rec( Bbr_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( " " );
+ Bbr_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
+
+ for ( i = 0; i < Offset; i++ )
+ printf( " " );
+ Bbr_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
+}
+
+/**Function********************************************************************
+
+ Synopsis [Computes the positive polarty cube composed of the first vars in the array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * Bbr_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
+{
+ DdNode * bRes;
+ DdNode * bTemp;
+ int i;
+
+ bRes = b1; Cudd_Ref( bRes );
+ for ( i = 0; i < nVars; i++ )
+ {
+ bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
+
+ Cudd_Deref( bRes );
+ return bRes;
+}
+
+
+
+
+
+struct Bbr_ImageTree2_t_
+{
+ DdManager * dd;
+ DdNode * bRel;
+ DdNode * bCube;
+ DdNode * bImage;
+};
+
+/**Function*************************************************************
+
+ Synopsis [Starts the monolithic image computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Bbr_ImageTree2_t * Bbr_bddImageStart2(
+ DdManager * dd, DdNode * bCare,
+ int nParts, DdNode ** pbParts,
+ int nVars, DdNode ** pbVars, int fVerbose )
+{
+ Bbr_ImageTree2_t * pTree;
+ DdNode * bCubeAll, * bCubeNot, * bTemp;
+ int i;
+
+ pTree = ABC_ALLOC( Bbr_ImageTree2_t, 1 );
+ pTree->dd = dd;
+ pTree->bImage = NULL;
+
+ bCubeAll = Bbr_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll );
+ bCubeNot = Bbr_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 );
+ }
+ Bbr_bddImageCompute2( pTree, bCare );
+ return pTree;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Bbr_bddImageCompute2( Bbr_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 Bbr_bddImageTreeDelete2( Bbr_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 * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree )
+{
+ return pTree->bImage;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:49:06 +0000