diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/bbr/bbr.h | 88 | ||||
-rw-r--r-- | src/aig/bbr/bbrImage.c | 1286 | ||||
-rw-r--r-- | src/aig/bbr/bbrNtbdd.c | 214 | ||||
-rw-r--r-- | src/aig/bbr/bbrReach.c | 414 | ||||
-rw-r--r-- | src/aig/bbr/bbr_.c | 47 | ||||
-rw-r--r-- | src/aig/bbr/module.make | 3 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 90 | ||||
-rw-r--r-- | src/aig/hop/hop.h | 3 | ||||
-rw-r--r-- | src/aig/hop/hopDfs.c | 68 | ||||
-rw-r--r-- | src/aig/hop/hopObj.c | 4 | ||||
-rw-r--r-- | src/aig/ntl/ntl.h | 2 | ||||
-rw-r--r-- | src/aig/ntl/ntlFraig.c | 4 | ||||
-rw-r--r-- | src/aig/ntl/ntlInsert.c | 9 | ||||
-rw-r--r-- | src/aig/ntl/ntlObj.c | 2 | ||||
-rw-r--r-- | src/aig/ntl/ntlReadBlif.c | 2 | ||||
-rw-r--r-- | src/aig/ntl/ntlWriteBlif.c | 2 | ||||
-rw-r--r-- | src/aig/nwk/nwk.h | 1 | ||||
-rw-r--r-- | src/aig/nwk/nwkMap.c | 5 | ||||
-rw-r--r-- | src/aig/nwk/nwkUtil.c | 56 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigPhase.c | 71 |
22 files changed, 2338 insertions, 37 deletions
diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h new file mode 100644 index 00000000..504fc463 --- /dev/null +++ b/src/aig/bbr/bbr.h @@ -0,0 +1,88 @@ +/**CFile**************************************************************** + + FileName [bbr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability analysis.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bbr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __BBR_H__ +#define __BBR_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include "cuddInt.h" +#include "aig.h" +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj ) { return pObj->pData; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== bbrImage.c ==========================================================*/ +typedef struct Bbr_ImageTree_t_ Bbr_ImageTree_t; +extern Bbr_ImageTree_t * Bbr_bddImageStart( + DdManager * dd, DdNode * bCare, + int nParts, DdNode ** pbParts, + int nVars, DdNode ** pbVars, int fVerbose ); +extern DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare ); +extern void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree ); +extern DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree ); +typedef struct Bbr_ImageTree2_t_ Bbr_ImageTree2_t; +extern Bbr_ImageTree2_t * Bbr_bddImageStart2( + DdManager * dd, DdNode * bCare, + int nParts, DdNode ** pbParts, + int nVars, DdNode ** pbVars, int fVerbose ); +extern DdNode * Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare ); +extern void Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree ); +extern DdNode * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree ); +/*=== bbrNtbdd.c ==========================================================*/ +extern void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ); +extern int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ); +extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose ); +/*=== bbrReach.c ==========================================================*/ +extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c new file mode 100644 index 00000000..cfe70d15 --- /dev/null +++ b/src/aig/bbr/bbrImage.c @@ -0,0 +1,1286 @@ +/**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 "mtr.h" + +/* + 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 +}; + +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 BDD_BLOW_UP 1000000 + +#define b0 Cudd_Not((dd)->one) +#define b1 (dd)->one + +#ifndef PRB +#define 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 ); +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 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 ) ); + + // consider the case of BDD node blowup + if ( fStop ) + { + for ( v = 0; v < dd->size; v++ ) + if ( pVars[v] ) + free( pVars[v] ); + free( pVars ); + for ( v = 0; v <= nParts; v++ ) + if ( pNodes[v] ) + { + Bbr_DeleteParts_rec( pNodes[v] ); + Bbr_bddImageTreeDelete_rec( pNodes[v] ); + } + free( pNodes ); + free( pParts ); + return NULL; + } + + // make sure the variables are gone + for ( v = 0; v < dd->size; v++ ) + assert( pVars[v] == NULL ); + FREE( pVars ); + + // create the tree + pTree = ALLOC( Bbr_ImageTree_t, 1 ); + memset( pTree, 0, sizeof(Bbr_ImageTree_t) ); + pTree->pCare = pCare; + 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 ); + 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 ); + 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: " ); +PRB( dd, pTree->bCareSupp ); +printf( "Current care set support: " ); +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 ); + 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 = ALLOC( Bbr_ImagePart_t *, nParts + 1 ); + // create structures for each variable + for ( i = 0; i < nParts; i++ ) + { + pParts[i] = 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] = 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 = ALLOC( DdNode *, nParts ); + for ( p = 0; p < nParts; p++ ) + pbFuncs[p] = pParts[p]->bSupp; + bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp ); + 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 = 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] = 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 = ALLOC( Bbr_ImageNode_t *, nParts ); + // create structures for each leaf nodes + for ( i = 0; i < nParts; i++ ) + { + pNodes[i] = 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 ); + 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]; +PRB( dd, pNode->bCube ); +PRB( dd, pNode->pPart->bFunc ); +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 ); + 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 ); + 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 > BDD_BLOW_UP ) + 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 ) +{ + 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; + + pVar = pVars[iVarBest]; + + // this var cannot appear in one partition only + nSupp = Cudd_SupportSize( 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 ); + FREE( pVars[v] ); + } + // clean the best var + Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts ); + 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]; + + // 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; + + // 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 > BDD_BLOW_UP ) + { + *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 = 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; +/* +PRB( dd, pNode1->pPart->bSupp ); +PRB( dd, pNode2->pPart->bSupp ); +PRB( dd, pPart->bSupp ); +*/ + // create a new node + pNode = 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; + 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 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 ) + { + PRB( pNode->dd, Cube ); + } + else + printf( "\n" ); + return; + } + + printf( "<*> " ); + if ( Cube != NULL ) + { + 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 = 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 ); + 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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/bbr/bbrNtbdd.c b/src/aig/bbr/bbrNtbdd.c new file mode 100644 index 00000000..5e51a157 --- /dev/null +++ b/src/aig/bbr/bbrNtbdd.c @@ -0,0 +1,214 @@ +/**CFile**************************************************************** + + FileName [bbrNtbdd.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability analysis.] + + Synopsis [Procedures to construct global BDDs for the network.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bbrNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bbr.h" +//#include "bar.h" + +typedef char ProgressBar; + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline void Aig_ObjSetGlobalBdd( Aig_Obj_t * pObj, DdNode * bFunc ) { pObj->pData = bFunc; } +static inline void Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, pObj->pData ); pObj->pData = NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the global BDD for one AIG node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Bbr_NodeGlobalBdds_rec( DdManager * dd, Aig_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose ) +{ + DdNode * bFunc, * bFunc0, * bFunc1; + int fDetectMuxes = 1; + assert( !Aig_IsComplement(pNode) ); + if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax ) + { +// Extra_ProgressBarStop( pProgress ); + if ( fVerbose ) + printf( "The number of live nodes reached %d.\n", nBddSizeMax ); + fflush( stdout ); + return NULL; + } + // if the result is available return + if ( Aig_ObjGlobalBdd(pNode) == NULL ) + { + // compute the result for both branches + bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); + if ( bFunc0 == NULL ) + return NULL; + Cudd_Ref( bFunc0 ); + bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); + if ( bFunc1 == NULL ) + return NULL; + Cudd_Ref( bFunc1 ); + bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) ); + bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) ); + // get the final result + bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bFunc0 ); + Cudd_RecursiveDeref( dd, bFunc1 ); + // add the number of used nodes + (*pCounter)++; + // set the result + assert( Aig_ObjGlobalBdd(pNode) == NULL ); + Aig_ObjSetGlobalBdd( pNode, bFunc ); + // increment the progress bar +// if ( pProgress ) +// Extra_ProgressBarUpdate( pProgress, *pCounter, NULL ); + } + // prepare the return value + bFunc = Aig_ObjGlobalBdd(pNode); + // dereference BDD at the node + if ( --pNode->nRefs == 0 && fDropInternal ) + { + Cudd_Deref( bFunc ); + Aig_ObjSetGlobalBdd( pNode, NULL ); + } + return bFunc; +} + +/**Function************************************************************* + + Synopsis [Frees the global BDDs of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjGlobalBdd(pObj) ) + Aig_ObjCleanGlobalBdd( dd, pObj ); +} + +/**Function************************************************************* + + Synopsis [Returns the shared size of global BDDs of the COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ) +{ + Vec_Ptr_t * vFuncsGlob; + Aig_Obj_t * pObj; + int RetValue, i; + // complement the global functions + vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) ); + RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) ); + Vec_PtrFree( vFuncsGlob ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Recursively computes global BDDs for the AIG in the manager.] + + Description [On exit, BDDs are stored in the pNode->pData fields.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose ) +{ + ProgressBar * pProgress = NULL; + Aig_Obj_t * pObj; + DdManager * dd; + DdNode * bFunc; + int i, Counter; + // start the manager + dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + // set reordering + if ( fReorder ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + // prepare to construct global BDDs + Aig_ManCleanData( p ); + // assign the constant node BDD + Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one ); Cudd_Ref( dd->one ); + // set the elementary variables + Aig_ManForEachPi( p, pObj, i ) + { + Aig_ObjSetGlobalBdd( pObj, dd->vars[i] ); Cudd_Ref( dd->vars[i] ); + } + + // collect the global functions of the COs + Counter = 0; + // construct the BDDs +// pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose ); + if ( bFunc == NULL ) + { + if ( fVerbose ) + printf( "Constructing global BDDs is aborted.\n" ); + Aig_ManFreeGlobalBdds( p, dd ); + Cudd_Quit( dd ); + // reset references + Aig_ManResetRefs( p ); + return NULL; + } + bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) ); Cudd_Ref( bFunc ); + Aig_ObjSetGlobalBdd( pObj, bFunc ); + } +// Extra_ProgressBarStop( pProgress ); + // reset references + Aig_ManResetRefs( p ); + // reorder one more time + if ( fReorder ) + { + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); + Cudd_AutodynDisable( dd ); + } +// Cudd_PrintInfo( dd, stdout ); + return dd; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c new file mode 100644 index 00000000..95bfe1ba --- /dev/null +++ b/src/aig/bbr/bbrReach.c @@ -0,0 +1,414 @@ +/**CFile**************************************************************** + + FileName [bbrReach.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability analysis.] + + Synopsis [Procedures to perform reachability analysis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bbr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) +{ + DdNode * bTemp, * bProd; + int i; + assert( iStart <= iStop ); + assert( iStart >= 0 && iStart <= dd->size ); + assert( iStop >= 0 && iStop <= dd->size ); + bProd = (dd)->one; Cudd_Ref( bProd ); + for ( i = iStart; i < iStop; i++ ) + { + bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bProd ); + return bProd; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bbr_StopManager( DdManager * dd ) +{ + int RetValue; + // check for remaining references in the package + RetValue = Cudd_CheckZeroRef( dd ); + if ( RetValue > 0 ) + printf( "\nThe number of referenced nodes = %d\n\n", RetValue ); +// Cudd_PrintInfo( dd, stdout ); + Cudd_Quit( dd ); +} + +/**Function************************************************************* + + Synopsis [Computes the initial state and sets up the variable map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose ) +{ + DdNode ** pbVarsX, ** pbVarsY; + DdNode * bTemp, * bProd; + Aig_Obj_t * pLatch; + int i; + + // set the variable mapping for Cudd_bddVarMap() + pbVarsX = ALLOC( DdNode *, dd->size ); + pbVarsY = ALLOC( DdNode *, dd->size ); + bProd = (dd)->one; Cudd_Ref( bProd ); + Saig_ManForEachLo( p, pLatch, i ) + { + pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ]; + pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ]; + // get the initial value of the latch + bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) ); + FREE( pbVarsX ); + FREE( pbVarsY ); + + Cudd_Deref( bProd ); + return bProd; +} + +/**Function************************************************************* + + Synopsis [Collects the array of output BDDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p ) +{ + DdNode ** pbOutputs; + Aig_Obj_t * pNode; + int i; + // compute the transition relation + pbOutputs = ALLOC( DdNode *, Saig_ManPoNum(p) ); + Saig_ManForEachPo( p, pNode, i ) + { + pbOutputs[i] = Aig_ObjGlobalBdd(pNode); Cudd_Ref( pbOutputs[i] ); + } + return pbOutputs; +} + +/**Function************************************************************* + + Synopsis [Collects the array of partition BDDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose ) +{ + DdNode ** pbParts; + DdNode * bVar; + Aig_Obj_t * pNode; + int i; + + // extand the BDD manager to represent NS variables + assert( dd->size == Saig_ManCiNum(p) ); + Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 ); + + // enable reordering + if ( fReorder ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + else + Cudd_AutodynDisable( dd ); + + // compute the transition relation + pbParts = ALLOC( DdNode *, Saig_ManRegNum(p) ); + Saig_ManForEachLi( p, pNode, i ) + { + bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i ); + pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] ); + } + // free global BDDs + Aig_ManFreeGlobalBdds( p, dd ); + + // reorder and disable reordering + if ( fReorder ) + { + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + Cudd_AutodynDisable( dd ); + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) ); + } + return pbParts; +} + +/**Function************************************************************* + + Synopsis [Computes the set of unreachable states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +{ + int fInternalReorder = 0; + Bbr_ImageTree_t * pTree; + Bbr_ImageTree2_t * pTree2; + DdNode * bReached, * bCubeCs; + DdNode * bCurrent, * bNext, * bTemp; + DdNode ** pbVarsY; + Aig_Obj_t * pLatch; + int i, nIters, nBddSize; + int nThreshold = 10000; + + // collect the NS variables + // set the variable mapping for Cudd_bddVarMap() + pbVarsY = ALLOC( DdNode *, dd->size ); + Saig_ManForEachLo( p, pLatch, i ) + pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ]; + + // start the image computation + bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs ); + if ( fPartition ) + pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose ); + else + pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose ); + Cudd_RecursiveDeref( dd, bCubeCs ); + free( pbVarsY ); + if ( pTree == NULL ) + { + printf( "BDDs blew up during qualitification scheduling. " ); + return -1; + } + + // perform reachability analisys + bCurrent = bInitial; Cudd_Ref( bCurrent ); + bReached = bInitial; Cudd_Ref( bReached ); + for ( nIters = 1; nIters <= nIterMax; nIters++ ) + { + // compute the next states + if ( fPartition ) + bNext = Bbr_bddImageCompute( pTree, bCurrent ); + else + bNext = Bbr_bddImageCompute2( pTree2, bCurrent ); + if ( bNext == NULL ) + { + printf( "BDDs blew up during image computation. " ); + if ( fPartition ) + Bbr_bddImageTreeDelete( pTree ); + else + Bbr_bddImageTreeDelete2( pTree2 ); + return -1; + } + Cudd_Ref( bNext ); + Cudd_RecursiveDeref( dd, bCurrent ); + // remap these states into the current state vars + bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext ); + Cudd_RecursiveDeref( dd, bTemp ); + // check if there are any new states + if ( Cudd_bddLeq( dd, bNext, bReached ) ) + break; + // check the BDD size + nBddSize = Cudd_DagSize(bNext); + if ( nBddSize > nBddMax ) + break; + // check the result + for ( i = 0; i < Saig_ManPoNum(p); i++ ) + { + if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) ) + { + printf( "Output %d was asserted in frame %d. ", i, nIters ); + Cudd_RecursiveDeref( dd, bReached ); + bReached = NULL; + break; + } + } + if ( i < Saig_ManPoNum(p) ) + break; + // get the new states + bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + // minimize the new states with the reached states +// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); +// Cudd_RecursiveDeref( dd, bTemp ); + // add to the reached states + bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bNext ); + if ( fVerbose ) + fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize ); + if ( fInternalReorder && fReorder && nBddSize > nThreshold ) + { + if ( fVerbose ) + fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + Cudd_AutodynDisable( dd ); + if ( fVerbose ) + fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) ); + nThreshold *= 2; + } + if ( fVerbose ) + fprintf( stdout, "\r" ); + } + Cudd_RecursiveDeref( dd, bNext ); + // undo the image tree + if ( fPartition ) + Bbr_bddImageTreeDelete( pTree ); + else + Bbr_bddImageTreeDelete2( pTree2 ); + if ( bReached == NULL ) + return 0; // proved reachable + // report the stats + if ( fVerbose ) + { + double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) ); + if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) + fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters ); + else + fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters ); + fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) ); + fflush( stdout ); + } +//PRB( dd, bReached ); + Cudd_RecursiveDeref( dd, bReached ); + if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) + { + printf( "Verified only for states reachable in %d frames. ", nIters ); + return -1; // undecided + } + printf( "The miter is proved unreachable after %d iterations. ", nIters ); + return 1; // unreachable +} + +/**Function************************************************************* + + Synopsis [Performs reachability to see if any .] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +{ + DdManager * dd; + DdNode ** pbParts, ** pbOutputs; + DdNode * bInitial; + int RetValue, i, clk = clock(); + + assert( Saig_ManRegNum(p) > 0 ); + + // compute the global BDDs of the latches + dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose ); + if ( dd == NULL ) + { + printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax ); + return -1; + } + if ( fVerbose ) + printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + + // save outputs + pbOutputs = Aig_ManCreateOutputs( dd, p ); + + // create partitions + pbParts = Aig_ManCreatePartitions( dd, p, fReorder, fVerbose ); + + // create the initial state and the variable map + bInitial = Aig_ManInitStateVarMap( dd, p, fVerbose ); Cudd_Ref( bInitial ); + + // check the result + RetValue = -1; + for ( i = 0; i < Saig_ManPoNum(p); i++ ) + { + if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) ) + { + printf( "The miter output %d is proved REACHABLE in the initial state. ", i ); + RetValue = 0; + break; + } + } + // explore reachable states + if ( RetValue == -1 ) + RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); + + // cleanup + Cudd_RecursiveDeref( dd, bInitial ); + for ( i = 0; i < Saig_ManRegNum(p); i++ ) + Cudd_RecursiveDeref( dd, pbParts[i] ); + free( pbParts ); + for ( i = 0; i < Saig_ManPoNum(p); i++ ) + Cudd_RecursiveDeref( dd, pbOutputs[i] ); + free( pbOutputs ); + if ( RetValue == -1 ) + Cudd_Quit( dd ); + else + Bbr_StopManager( dd ); + + // report the runtime + PRT( "Time", clock() - clk ); + fflush( stdout ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/bbr/bbr_.c b/src/aig/bbr/bbr_.c new file mode 100644 index 00000000..f94c50e6 --- /dev/null +++ b/src/aig/bbr/bbr_.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: .c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "__Int.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make new file mode 100644 index 00000000..52a824b9 --- /dev/null +++ b/src/aig/bbr/module.make @@ -0,0 +1,3 @@ +SRC += src/aig/bbr/bbrImage.c \ + src/aig/bbr/bbrNtbdd.c \ + src/aig/bdr/bbrReach.c diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7c2b95db..44cfe847 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -328,7 +328,7 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ -extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ); +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 99d4bc89..64222a47 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ) +int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; @@ -79,6 +79,23 @@ clk = clock(); PRT( "Time", clock() - clk ); } + // perform phase abstraction +clk = clock(); + if ( fPhaseAbstract ) + { + extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ); + pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); + pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + } + // perform forward retiming if ( fRetimeFirst && pNew->nRegs ) { @@ -133,6 +150,26 @@ PRT( "Time", clock() - clk ); } } + // perform min-area retiming + if ( fRetimeRegs && pNew->nRegs ) + { + extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); +clk = clock(); + pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); +// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 ); + Aig_ManStop( pTemp ); + pNew = Aig_ManDupOrdered( pTemp = pNew ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + } + // perform seq sweeping while increasing the number of frames RetValue = Fra_FraigMiterStatus( pNew ); if ( RetValue == -1 ) @@ -152,31 +189,22 @@ PRT( "Time", clock() - clk ); if ( RetValue != -1 ) break; - // perform rewriting -clk = clock(); - pNew = Aig_ManDupOrdered( pTemp = pNew ); - Aig_ManStop( pTemp ); - pNew = Dar_ManRewriteDefault( pTemp = pNew ); - Aig_ManStop( pTemp ); - if ( fVerbose ) - { - printf( "Rewriting: Latches = %5d. Nodes = %6d. ", - Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); -PRT( "Time", clock() - clk ); - } - // perform retiming - if ( fRetimeFirst && pNew->nRegs ) -// if ( pNew->nRegs ) +// if ( fRetimeFirst && pNew->nRegs ) + if ( pNew->nRegs ) { + extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); clk = clock(); - pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); +// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 ); Aig_ManStop( pTemp ); pNew = Aig_ManDupOrdered( pTemp = pNew ); Aig_ManStop( pTemp ); if ( fVerbose ) { - printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", + printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } @@ -185,6 +213,20 @@ PRT( "Time", clock() - clk ); if ( pNew->nRegs ) pNew = Aig_ManConstReduce( pNew, 0 ); + // perform rewriting +clk = clock(); + pNew = Aig_ManDupOrdered( pTemp = pNew ); + Aig_ManStop( pTemp ); +// pNew = Dar_ManRewriteDefault( pTemp = pNew ); + pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Rewriting: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + // perform sequential simulation if ( pNew->nRegs ) { @@ -213,6 +255,18 @@ PRT( "Time", clock() - clkTotal ); // get the miter status RetValue = Fra_FraigMiterStatus( pNew ); + // try reachability analysis + if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 ) + { + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); + assert( Aig_ManRegNum(pNew) > 0 ); + pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); +clk = clock(); + RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); +PRT( "Time", clock() - clk ); + } + finish: // report the miter if ( RetValue == 1 ) diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index 12374a49..05e6471e 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -188,7 +188,7 @@ static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_ static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; } static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; } static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); } -static inline int Hop_ObjFaninPhase( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; } +static inline int Hop_ObjPhaseCompl( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; } static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); } static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin ) { @@ -284,6 +284,7 @@ extern int Hop_DagSize( Hop_Obj_t * pObj ); extern void Hop_ConeUnmark_rec( Hop_Obj_t * pObj ); extern Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars ); extern Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar ); +extern Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars ); /*=== hopMan.c ==========================================================*/ extern Hop_Man_t * Hop_ManStart(); extern Hop_Man_t * Hop_ManDup( Hop_Man_t * p ); diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c index 49e5f221..d798bc35 100644 --- a/src/aig/hop/hopDfs.c +++ b/src/aig/hop/hopDfs.c @@ -392,6 +392,74 @@ Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, in return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); } +/**Function************************************************************* + + Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_Remap_rec( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Hop_Remap_rec( p, Hop_ObjFanin0(pObj) ); + Hop_Remap_rec( p, Hop_ObjFanin1(pObj) ); + pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars ) +{ + Hop_Obj_t * pObj; + int i, k; + // quit if the PI variable is not defined + if ( nVars > Hop_ManPiNum(p) ) + { + printf( "Hop_Remap(): The number of variables (%d) is more than the manager size (%d).\n", nVars, Hop_ManPiNum(p) ); + return NULL; + } + // return if constant + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + return pRoot; + if ( uSupp == 0 ) + return Hop_NotCond( Hop_ManConst0(p), Hop_ObjPhaseCompl(pRoot) ); + // set the PI mapping + k = 0; + Hop_ManForEachPi( p, pObj, i ) + { + if ( i == nVars ) + break; + if ( uSupp & (1 << i) ) + pObj->pData = Hop_IthVar(p, k++); + else + pObj->pData = Hop_ManConst0(p); + } + assert( k > 0 && k < nVars ); + // recursively perform composition + Hop_Remap_rec( p, Hop_Regular(pRoot) ); + // clear the markings + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); + return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c index c8e70dd3..69f63ee6 100644 --- a/src/aig/hop/hopObj.c +++ b/src/aig/hop/hopObj.c @@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver ) else pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) ); // set the phase - pObj->fPhase = Hop_ObjFaninPhase(pDriver); + pObj->fPhase = Hop_ObjPhaseCompl(pDriver); // update node counters of the manager p->nObjs[AIG_PO]++; return pObj; @@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj else pObj->nRefs = Hop_ObjLevelNew( pObj ); // set the phase - pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1); + pObj->fPhase = Hop_ObjPhaseCompl(pFan0) & Hop_ObjPhaseCompl(pFan1); // add the node to the structural hash table Hop_TableInsert( p, pObj ); } diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 659f6c60..55581026 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -52,7 +52,7 @@ typedef enum { NTL_OBJ_NONE, // 0: non-existent object NTL_OBJ_PI, // 1: primary input NTL_OBJ_PO, // 2: primary output - NTL_OBJ_LATCH, // 3: latch node + NTL_OBJ_LATCH, // 3: latch NTL_OBJ_NODE, // 4: logic node NTL_OBJ_LUT1, // 5: inverter/buffer NTL_OBJ_BOX, // 6: white box or black box diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 767ea6e4..a723c981 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -76,6 +76,8 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_ if ( Aig_ObjIsPo(pObj) ) continue; pObjCol = pObj->pData; + if ( pObjCol == NULL ) + continue; if ( pMapBack[pObjCol->Id] == NULL ) pMapBack[pObjCol->Id] = pObj; } @@ -89,6 +91,8 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_ continue; // get the collapsed node pObjCol = pObj->pData; + if ( pObjCol == NULL ) + continue; // get the representative of the collapsed node pObjColRepr = pAigCol->pReprs[pObjCol->Id]; if ( pObjColRepr == NULL ) diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 3e9f82d6..3cd9470b 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -82,6 +82,8 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t Ntl_ObjSetFanin( pNode, pNet, k ); } } + else + pNode->nFanins = 0; sprintf( Buffer, "lut%0*d", nDigits, i ); if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) ) { @@ -302,6 +304,8 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) Ntl_ObjSetFanin( pNode, pNet, k ); } } + else + pNode->nFanins = 0; sprintf( Buffer, "lut%0*d", nDigits, i ); if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) ) { @@ -341,13 +345,16 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) ) { printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" ); - return 0; + return NULL; } } // clean CI/CO marks Ntl_ManUnmarkCiCoNets( p ); if ( !Ntl_ManCheck( p ) ) + { printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName ); + return NULL; + } return p; } diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c index c86ab47b..10bfbbb7 100644 --- a/src/aig/ntl/ntlObj.c +++ b/src/aig/ntl/ntlObj.c @@ -103,7 +103,7 @@ Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel ) Vec_PtrPush( pModel->vObjs, p ); p->pModel = pModel; p->Type = NTL_OBJ_LATCH; - p->nFanins = 2; + p->nFanins = 1; p->nFanouts = 1; pModel->nObjs[NTL_OBJ_LATCH]++; return p; diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index cac53058..3574b61e 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -825,7 +825,7 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ) { pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2); pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); - pObj->pFanio[1] = pNetLi; +// pObj->pFanio[1] = pNetLi; } return 1; } diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 9814ed5d..51d41c26 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -28,7 +28,7 @@ //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - + /**Function************************************************************* Synopsis [Writes one model into the BLIF file.] diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index c36f3498..b0edd243 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -285,6 +285,7 @@ extern void Nwk_ObjPrint( Nwk_Obj_t * pObj ); extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames ); extern void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ); extern void Nwk_ManCleanMarks( Nwk_Man_t * pNtk ); +extern void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c index 45d56eb5..88e08413 100644 --- a/src/aig/nwk/nwkMap.c +++ b/src/aig/nwk/nwkMap.c @@ -146,7 +146,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf ) /**Function************************************************************* - Synopsis [Recursively derives the truth table for the cut.] + Synopsis [Recursively derives the local AIG for the cut.] Description [] @@ -193,7 +193,7 @@ Hop_Obj_t * Nwk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj /**Function************************************************************* - Synopsis [Derives the truth table for one cut.] + Synopsis [Derives the local AIG for the cut.] Description [] @@ -309,6 +309,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI } Vec_PtrFree( vIfToAig ); pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 ); + Nwk_ManMinimumBase( pNtk, 0 ); assert( Nwk_ManCheck( pNtk ) ); return pNtk; } diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index 1ef0af67..14f7632f 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -56,7 +56,7 @@ void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk ) /**Function************************************************************* - Synopsis [Reads the maximum number of fanins.] + Synopsis [Reads the maximum number of fanins of a node.] Description [] @@ -100,7 +100,7 @@ int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk ) /**Function************************************************************* - Synopsis [] + Synopsis [Returns the number of true PIs.] Description [] @@ -120,7 +120,7 @@ int Nwk_ManPiNum( Nwk_Man_t * pNtk ) /**Function************************************************************* - Synopsis [] + Synopsis [Returns the number of true POs.] Description [] @@ -140,7 +140,7 @@ int Nwk_ManPoNum( Nwk_Man_t * pNtk ) /**Function************************************************************* - Synopsis [Reads the number of BDD nodes.] + Synopsis [Reads the number of AIG nodes.] Description [] @@ -211,7 +211,7 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ) /**Function************************************************************* - Synopsis [Deletes the node.] + Synopsis [Prints the objects.] Description [] @@ -242,7 +242,7 @@ void Nwk_ObjPrint( Nwk_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Deletes the node.] + Synopsis [Dumps the BLIF file for the network.] Description [] @@ -449,7 +449,7 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ) /**Function************************************************************* - Synopsis [] + Synopsis [Cleans the temporary marks of the nodes.] Description [] @@ -466,6 +466,48 @@ void Nwk_ManCleanMarks( Nwk_Man_t * pMan ) pObj->MarkA = pObj->MarkB = 0; } +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) +{ + unsigned * pTruth; + Vec_Int_t * vTruth; + Nwk_Obj_t * pObj, * pFanin, * pObjNew; + int uSupp, nSuppSize, i, k, Counter = 0; + vTruth = Vec_IntAlloc( 1 << 16 ); + Nwk_ManForEachNode( pNtk, pObj, i ) + { + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); + nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj)); + if ( nSuppSize == Nwk_ObjFaninNum(pObj) ) + continue; + Counter++; + uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) ); + // create new node with the given support + pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) ); + Nwk_ObjForEachFanin( pObj, pFanin, k ) + if ( uSupp & (1 << k) ) + Nwk_ObjAddFanin( pObjNew, pFanin ); + pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) ); + if ( fVerbose ) + printf( "Reducing node %d fanins from %d to %d.\n", + pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) ); + Nwk_ObjReplace( pObj, pObjNew ); + } + if ( fVerbose && Counter ) + printf( "Support minimization reduced support of %d nodes.\n", Counter ); + Vec_IntFree( vTruth ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index e399b8bb..f9677cb0 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -45,6 +45,8 @@ extern "C" { static inline int Saig_ManPiNum( Aig_Man_t * p ) { return p->nTruePis; } static inline int Saig_ManPoNum( Aig_Man_t * p ) { return p->nTruePos; } +static inline int Saig_ManCiNum( Aig_Man_t * p ) { return p->nTruePis + p->nRegs; } +static inline int Saig_ManCoNum( Aig_Man_t * p ) { return p->nTruePos + p->nRegs; } static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; } static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i); } static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i); } diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index fc00ce3c..f98bb49b 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -800,7 +800,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame printf( "Print-out finished. Phase assignment is not performed.\n" ); else if ( nFrames < 2 ) printf( "The number of frames is less than 2. Phase assignment is not performed.\n" ); - else if ( pTsi->nCycle == 0 ) + else if ( pTsi->nCycle == 1 ) printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" ); else if ( pTsi->nCycle % nFrames != 0 ) printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames ); @@ -814,6 +814,75 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame return pNew; } +/**Function************************************************************* + + Synopsis [Performs automated phase abstraction.] + + Description [Takes the AIG manager and the array of initial states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) +{ + Aig_Man_t * pNew = NULL; + Saig_Tsim_t * pTsi; + int fPrint = 0; + int nFrames; + assert( Saig_ManRegNum(p) ); + assert( Saig_ManPiNum(p) ); + assert( Saig_ManPoNum(p) ); + // perform terminary simulation + pTsi = Saig_ManReachableTernary( p, NULL ); + if ( pTsi == NULL ) + return NULL; + // derive information + pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); + pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix; + pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords); + // print statistics + if ( fVerbose ) + { + printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n", + pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); + if ( pTsi->nNonXRegs < 100 ) + Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix ); + } + nFrames = pTsi->nCycle; + if ( fPrint ) + { + printf( "Print-out finished. Phase assignment is not performed.\n" ); + } + else if ( nFrames < 2 ) + { +// printf( "The number of frames is less than 2. Phase assignment is not performed.\n" ); + } + else if ( pTsi->nCycle == 1 ) + { +// printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" ); + } + else if ( pTsi->nCycle % nFrames != 0 ) + { +// printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames ); + } + else if ( pTsi->nNonXRegs == 0 ) + { +// printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" ); + } + else if ( !Saig_ManFindRegisters( pTsi, nFrames, 0, fVerbose ) ) + { +// printf( "There is no registers to abstract with %d frames.\n", nFrames ); + } + else + pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose ); + Saig_TsiStop( pTsi ); + if ( pNew == NULL ) + pNew = Aig_ManDup( p ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |