From c7b331efcf42c94450d7590eeb0c71c525569c11 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 6 Jul 2008 08:01:00 -0700 Subject: Version abc80706 --- src/aig/nwk/module.make | 1 + src/aig/nwk/nwk.h | 14 + src/aig/nwk/nwkMerge.c | 763 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/nwk/nwkUtil_old.c | 615 ------------------------------------- src/base/abci/abc.c | 246 +++++++++++++++ src/base/abci/abcSense.c | 208 +++++++++++++ src/base/abci/module.make | 1 + 7 files changed, 1233 insertions(+), 615 deletions(-) create mode 100644 src/aig/nwk/nwkMerge.c delete mode 100644 src/aig/nwk/nwkUtil_old.c create mode 100644 src/base/abci/abcSense.c (limited to 'src') diff --git a/src/aig/nwk/module.make b/src/aig/nwk/module.make index c0447823..f4b19e1a 100644 --- a/src/aig/nwk/module.make +++ b/src/aig/nwk/module.make @@ -6,6 +6,7 @@ SRC += src/aig/nwk/nwkAig.c \ src/aig/nwk/nwkFlow.c \ src/aig/nwk/nwkMan.c \ src/aig/nwk/nwkMap.c \ + src/aig/nwk/nwkMerge.c \ src/aig/nwk/nwkObj.c \ src/aig/nwk/nwkSpeedup.c \ src/aig/nwk/nwkStrash.c \ diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index f74f44f3..0eb6cd81 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -109,6 +109,20 @@ struct Nwk_Obj_t_ }; +// the LUT merging parameters +typedef struct Nwk_LMPars_t_ Nwk_LMPars_t; +struct Nwk_LMPars_t_ +{ + int nMaxLutSize; // the max LUT size for merging (N=5) + int nMaxSuppSize; // the max total support size after merging (S=5) + int nMaxDistance; // the max number of nodes separating LUTs + int nMaxLevelDiff; // the max difference in levels + int nMaxFanout; // the max number of fanouts to traverse + int fUseTfiTfo; // enables the use of TFO/TFO nodes as candidates + int fVeryVerbose; // enables additional verbose output + int fVerbose; // enables verbose output +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/nwk/nwkMerge.c b/src/aig/nwk/nwkMerge.c new file mode 100644 index 00000000..57de7f04 --- /dev/null +++ b/src/aig/nwk/nwkMerge.c @@ -0,0 +1,763 @@ +/**CFile**************************************************************** + + FileName [nwkMerge.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [LUT merging algorithm.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Marks the fanins of the node with the current trav ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMarkFanins_rec( Nwk_Obj_t * pLut, int nLevMin ) +{ + Nwk_Obj_t * pNext; + int i; + if ( !Nwk_ObjIsNode(pLut) ) + return; + if ( Nwk_ObjIsTravIdCurrent( pLut ) ) + return; + Nwk_ObjSetTravIdCurrent( pLut ); + if ( Nwk_ObjLevel(pLut) < nLevMin ) + return; + Nwk_ObjForEachFanin( pLut, pNext, i ) + Nwk_ManMarkFanins_rec( pNext, nLevMin ); +} + +/**Function************************************************************* + + Synopsis [Marks the fanouts of the node with the current trav ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMarkFanouts_rec( Nwk_Obj_t * pLut, int nLevMax, int nFanMax ) +{ + Nwk_Obj_t * pNext; + int i; + if ( !Nwk_ObjIsNode(pLut) ) + return; + if ( Nwk_ObjIsTravIdCurrent( pLut ) ) + return; + Nwk_ObjSetTravIdCurrent( pLut ); + if ( Nwk_ObjLevel(pLut) > nLevMax ) + return; + if ( Nwk_ObjFanoutNum(pLut) > nFanMax ) + return; + Nwk_ObjForEachFanout( pLut, pNext, i ) + Nwk_ManMarkFanouts_rec( pNext, nLevMax, nFanMax ); +} + +/**Function************************************************************* + + Synopsis [Collects the circle of nodes around the given set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax ) +{ + Nwk_Obj_t * pObj, * pNext; + int i, k; + Vec_PtrClear( vNext ); + Vec_PtrForEachEntry( vStart, pObj, i ) + { + Nwk_ObjForEachFanin( pObj, pNext, k ) + { + if ( !Nwk_ObjIsNode(pNext) ) + continue; + if ( Nwk_ObjIsTravIdCurrent( pNext ) ) + continue; + Nwk_ObjSetTravIdCurrent( pNext ); + Vec_PtrPush( vNext, pNext ); + } + Nwk_ObjForEachFanout( pObj, pNext, k ) + { + if ( !Nwk_ObjIsNode(pNext) ) + continue; + if ( Nwk_ObjIsTravIdCurrent( pNext ) ) + continue; + Nwk_ObjSetTravIdCurrent( pNext ); + if ( Nwk_ObjFanoutNum(pNext) > nFanMax ) + continue; + Vec_PtrPush( vNext, pNext ); + } + } +} + +/**Function************************************************************* + + Synopsis [Collects the circle of nodes removes from the given one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManCollectNonOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars ) +{ + Vec_Ptr_t * vTemp; + Nwk_Obj_t * pObj; + int i, k; + Vec_PtrClear( vCands ); + if ( pPars->nMaxSuppSize - Nwk_ObjFaninNum(pLut) <= 1 ) + return; + + // collect nodes removed by this distance + assert( pPars->nMaxDistance > 0 ); + Vec_PtrClear( vStart ); + Vec_PtrPush( vStart, pLut ); + Nwk_ManIncrementTravId( pLut->pMan ); + Nwk_ObjSetTravIdCurrent( pLut ); + for ( i = 1; i < pPars->nMaxDistance; i++ ) + { + Nwk_ManCollectCircle( vStart, vNext, pPars->nMaxFanout ); + vTemp = vStart; + vStart = vNext; + vNext = vTemp; + // collect the nodes in vStart + Vec_PtrForEachEntry( vStart, pObj, k ) + Vec_PtrPush( vCands, pObj ); + } + + // mark the TFI/TFO nodes + Nwk_ManIncrementTravId( pLut->pMan ); + if ( pPars->fUseTfiTfo ) + Nwk_ObjSetTravIdCurrent( pLut ); + else + { + Nwk_ObjSetTravIdPrevious( pLut ); + Nwk_ManMarkFanins_rec( pLut, Nwk_ObjLevel(pLut) - pPars->nMaxDistance ); + Nwk_ObjSetTravIdPrevious( pLut ); + Nwk_ManMarkFanouts_rec( pLut, Nwk_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout ); + } + + // collect nodes satisfying the following conditions: + // - they are close enough in terms of distance + // - they are not in the TFI/TFO of the LUT + // - they have no more than the given number of fanins + // - they have no more than the given diff in delay + k = 0; + Vec_PtrForEachEntry( vCands, pObj, i ) + { + if ( Nwk_ObjIsTravIdCurrent(pObj) ) + continue; + if ( Nwk_ObjFaninNum(pLut) + Nwk_ObjFaninNum(pObj) > pPars->nMaxSuppSize ) + continue; + if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || + Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff ) + continue; + Vec_PtrWriteEntry( vCands, k++, pObj ); + } + Vec_PtrShrink( vCands, k ); +} + + +/**Function************************************************************* + + Synopsis [Count the total number of fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManCountTotalFanins( Nwk_Obj_t * pLut, Nwk_Obj_t * pCand ) +{ + Nwk_Obj_t * pFanin; + int i, nCounter = Nwk_ObjFaninNum(pLut); + Nwk_ObjForEachFanin( pCand, pFanin, i ) + nCounter += !pFanin->MarkC; + return nCounter; +} + +/**Function************************************************************* + + Synopsis [Collects overlapping candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwl_ManCollectOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars ) +{ + Nwk_Obj_t * pFanin, * pObj; + int i, k; + // mark fanins of pLut + Nwk_ObjForEachFanin( pLut, pFanin, i ) + pFanin->MarkC = 1; + // collect the matching fanouts of each fanin of the node + Vec_PtrClear( vCands ); + Nwk_ManIncrementTravId( pLut->pMan ); + Nwk_ObjSetTravIdCurrent( pLut ); + Nwk_ObjForEachFanin( pLut, pFanin, i ) + { + if ( !Nwk_ObjIsNode(pFanin) ) + continue; + if ( Nwk_ObjFanoutNum(pFanin) > pPars->nMaxFanout ) + continue; + Nwk_ObjForEachFanout( pFanin, pObj, k ) + { + if ( !Nwk_ObjIsNode(pObj) ) + continue; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + continue; + Nwk_ObjSetTravIdCurrent( pObj ); + // check the difference in delay + if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || + Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff ) + continue; + // check the total number of fanins of the node + if ( Nwk_ManCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize ) + continue; + Vec_PtrPush( vCands, pObj ); + } + } + // unmark fanins of pLut + Nwk_ObjForEachFanin( pLut, pFanin, i ) + pFanin->MarkC = 0; +} + + + +#define MAX_LIST 16 + +// edge of the graph +typedef struct Nwk_Edg_t_ Nwk_Edg_t; +struct Nwk_Edg_t_ +{ + int iNode1; // the first node + int iNode2; // the second node + Nwk_Edg_t * pNext; // the next edge +}; + +// vertex of the graph +typedef struct Nwk_Vrt_t_ Nwk_Vrt_t; +struct Nwk_Vrt_t_ +{ + int Id; // the vertex number + int iPrev; // the previous vertex in the list + int iNext; // the next vertex in the list + int nEdges; // the number of edges + int pEdges[0]; // the array of edges +}; + +// the connectivity graph +typedef struct Nwk_Grf_t_ Nwk_Grf_t; +struct Nwk_Grf_t_ +{ + // preliminary graph representation + int nObjs; // the number of objects + int nVertsPre; // the upper bound on the number of vertices + int nEdgeHash; // approximate number of edges + Nwk_Edg_t ** pEdgeHash; // hash table for edges + Aig_MmFixed_t * pMemEdges; // memory for edges + // graph representation + int nEdges; // the number of edges + int nVerts; // the number of vertices + Nwk_Vrt_t ** pVerts; // the array of vertices + Aig_MmFlex_t * pMemVerts; // memory for vertices + // intermediate data + int pLists1[MAX_LIST+1]; + int pLists2[MAX_LIST+1]; + // the results of matching + Vec_Int_t * vPairs; + // mappings graph into LUTs and back + int * pMapLut2Id; + int * pMapId2Lut; +}; + +/**Function************************************************************* + + Synopsis [Deallocates the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphFree( Nwk_Grf_t * p ) +{ + if ( p->vPairs ) Vec_IntFree( p->vPairs ); + if ( p->pMemEdges ) Aig_MmFixedStop( p->pMemEdges, 0 ); + if ( p->pMemVerts ) Aig_MmFlexStop( p->pMemVerts, 0 ); + FREE( p->pEdgeHash ); + FREE( p->pVerts ); + FREE( p->pMapLut2Id ); + FREE( p->pMapId2Lut ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Allocates the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Grf_t * Nwk_ManGraphAlloc( int nObjs, int nVertsPre ) +{ + Nwk_Grf_t * p; + p = ALLOC( Nwk_Grf_t, 1 ); + memset( p, 0, sizeof(Nwk_Grf_t) ); + p->nObjs = nObjs; + p->nVertsPre = nVertsPre; + p->nEdgeHash = Aig_PrimeCudd(10 * nVertsPre); + p->pEdgeHash = CALLOC( Nwk_Edg_t *, p->nEdgeHash ); + p->pMemEdges = Aig_MmFixedStart( sizeof(Nwk_Edg_t), p->nEdgeHash ); + p->pMapLut2Id = ALLOC( int, nObjs ); + p->pMapId2Lut = ALLOC( int, nVertsPre ); + p->vPairs = Vec_IntAlloc( 1000 ); + memset( p->pMapLut2Id, 0xff, sizeof(int) * nObjs ); + memset( p->pMapId2Lut, 0xff, sizeof(int) * nVertsPre ); + return p; +} + +/**Function************************************************************* + + Synopsis [Finds or adds the edge to the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphSetMapping( Nwk_Grf_t * p, int iLut ) +{ + p->nVerts++; + p->pMapId2Lut[p->nVerts] = iLut; + p->pMapLut2Id[iLut] = p->nVerts; +} + +/**Function************************************************************* + + Synopsis [Finds or adds the edge to the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 ) +{ + Nwk_Edg_t * pEntry; + int Key; + if ( iLut1 == iLut2 ) + return; + if ( iLut1 > iLut2 ) + { + Key = iLut1; + iLut1 = iLut2; + iLut2 = Key; + } + assert( iLut1 < iLut2 ); + Key = (741457 * iLut1 + 4256249 * iLut2) % p->nEdgeHash; + for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext ) + if ( pEntry->iNode1 == iLut1 && pEntry->iNode2 == iLut2 ) + return; + pEntry = (Nwk_Edg_t *)Aig_MmFixedEntryFetch( p->pMemEdges ); + pEntry->iNode1 = iLut1; + pEntry->iNode2 = iLut2; + pEntry->pNext = p->pEdgeHash[Key]; + p->pEdgeHash[Key] = pEntry; + p->nEdges++; +} + +/**Function************************************************************* + + Synopsis [Prepares the graph for solving the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListAdd( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t * pVertex ) +{ + if ( *pList ) + { + Nwk_Vrt_t * pHead; + pHead = p->pVerts[*pList]; + pVertex->iPrev = 0; + pVertex->iNext = pHead->Id; + pHead->iPrev = pVertex->Id; + } + *pList = pVertex->Id; +} + +/**Function************************************************************* + + Synopsis [Prepares the graph for solving the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListDelete( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t * pVertex ) +{ + assert( *pList ); + if ( pVertex->iPrev ) + p->pVerts[pVertex->iPrev]->iNext = pVertex->iNext; + if ( pVertex->iNext ) + p->pVerts[pVertex->iNext]->iNext = pVertex->iPrev; + if ( *pList == pVertex->Id ) + *pList = pVertex->iNext; + pVertex->iPrev = pVertex->iNext = 0; +} + +/**Function************************************************************* + + Synopsis [Inserts the edge into one of the linked lists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListInsert( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex ) +{ + Nwk_Vrt_t * pNext; + assert( pVertex->nEdges > 0 ); + if ( pVertex->nEdges == 1 ) + { + pNext = p->pVerts[ pVertex->pEdges[0] ]; + if ( pNext->nEdges >= MAX_LIST ) + Nwk_ManGraphListAdd( p, p->pLists1 + MAX_LIST, pVertex ); + else + Nwk_ManGraphListAdd( p, p->pLists1 + pNext->nEdges, pVertex ); + } + else + { + if ( pVertex->nEdges >= MAX_LIST ) + Nwk_ManGraphListAdd( p, p->pLists1 + MAX_LIST, pVertex ); + else + Nwk_ManGraphListAdd( p, p->pLists1 + pVertex->nEdges, pVertex ); + } +} + +/**Function************************************************************* + + Synopsis [Extracts the edge from one of the linked lists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListExtract( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex ) +{ + Nwk_Vrt_t * pNext; + assert( pVertex->nEdges > 0 ); + if ( pVertex->nEdges == 1 ) + { + pNext = p->pVerts[ pVertex->pEdges[0] ]; + if ( pNext->nEdges >= MAX_LIST ) + Nwk_ManGraphListDelete( p, p->pLists1 + MAX_LIST, pVertex ); + else + Nwk_ManGraphListDelete( p, p->pLists1 + pNext->nEdges, pVertex ); + } + else + { + if ( pVertex->nEdges >= MAX_LIST ) + Nwk_ManGraphListDelete( p, p->pLists1 + MAX_LIST, pVertex ); + else + Nwk_ManGraphListDelete( p, p->pLists1 + pVertex->nEdges, pVertex ); + } +} + +/**Function************************************************************* + + Synopsis [Prepares the graph for solving the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphPrepare( Nwk_Grf_t * p ) +{ + Nwk_Edg_t * pEntry; + Nwk_Vrt_t * pVertex; + int * pnEdges, Key, nBytes, i; + // count the edges + pnEdges = CALLOC( int, p->nVerts ); + for ( Key = 0; Key < p->nEdgeHash; Key++ ) + for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext ) + { + // translate into vertices + assert( pEntry->iNode1 < p->nObjs ); + assert( pEntry->iNode2 < p->nObjs ); + pEntry->iNode1 = p->pMapLut2Id[pEntry->iNode1]; + pEntry->iNode2 = p->pMapLut2Id[pEntry->iNode2]; + // count the edges + assert( pEntry->iNode1 < p->nVerts ); + assert( pEntry->iNode2 < p->nVerts ); + pnEdges[pEntry->iNode1]++; + pnEdges[pEntry->iNode2]++; + } + // allocate the real graph + p->pMemVerts = Aig_MmFlexStart(); + p->pVerts = ALLOC( Nwk_Vrt_t *, p->nVerts + 1 ); + p->pVerts[0] = NULL; + for ( i = 1; i <= p->nVerts; i++ ) + { + assert( pnEdges[i] > 0 ); + nBytes = sizeof(Nwk_Vrt_t) + sizeof(int) * pnEdges[i]; + p->pVerts[i] = (Nwk_Vrt_t *)Aig_MmFlexEntryFetch( p->pMemVerts, nBytes ); + memset( p->pVerts[i], 0, nBytes ); + p->pVerts[i]->Id = i; + } + // add edges to the real graph + for ( Key = 0; Key < p->nEdgeHash; Key++ ) + for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext ) + { + pVertex = p->pVerts[pEntry->iNode1]; + pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode2; + pVertex = p->pVerts[pEntry->iNode2]; + pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode1; + } + // put vertices into the data structure + for ( i = 1; i <= p->nVerts; i++ ) + { + assert( p->pVerts[i]->nEdges == pnEdges[i] ); + Nwk_ManGraphListInsert( p, p->pVerts[i] ); + } + // clean up + Aig_MmFixedStop( p->pMemEdges, 0 ); p->pMemEdges = NULL; + FREE( p->pEdgeHash ); + p->nEdgeHash = 0; + free( pnEdges ); +} + +/**Function************************************************************* + + Synopsis [Updates the problem after pulling out one edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphUpdate( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex, Nwk_Vrt_t * pNext ) +{ + Nwk_Vrt_t * pChanged; + int i, k; + // update neibors of pVertex + for ( i = 0; i < pVertex->nEdges; i++ ) + { + pChanged = p->pVerts[ pVertex->pEdges[i] ]; + Nwk_ManGraphListExtract( p, pChanged ); + for ( k = 0; k < pChanged->nEdges; k++ ) + if ( pChanged->pEdges[k] == pVertex->Id ) + break; + assert( k < pChanged->nEdges ); + pChanged->nEdges--; + for ( ; k < pChanged->nEdges; k++ ) + pChanged->pEdges[k] = pChanged->pEdges[k+1]; + if ( pChanged->nEdges > 0 ) + Nwk_ManGraphListInsert( p, pChanged ); + } + // update neibors of pNext + for ( i = 0; i < pNext->nEdges; i++ ) + { + pChanged = p->pVerts[ pNext->pEdges[i] ]; + Nwk_ManGraphListExtract( p, pChanged ); + for ( k = 0; k < pChanged->nEdges; k++ ) + if ( pChanged->pEdges[k] == pNext->Id ) + break; + assert( k < pChanged->nEdges ); + pChanged->nEdges--; + for ( ; k < pChanged->nEdges; k++ ) + pChanged->pEdges[k] = pChanged->pEdges[k+1]; + if ( pChanged->nEdges > 0 ) + Nwk_ManGraphListInsert( p, pChanged ); + } + // add to the result + if ( pVertex->Id < pNext->Id ) + { + Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); + Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); + } + else + { + Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); + Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); + } +} + +/**Function************************************************************* + + Synopsis [Solves the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphSolve( Nwk_Grf_t * p ) +{ + Nwk_Vrt_t * pVertex, * pNext; + int i, j; + while ( 1 ) + { + // find the next vertext to extract + for ( i = 1; i <= MAX_LIST; i++ ) + if ( p->pLists1[i] ) + { + pVertex = p->pVerts[ p->pLists1[i] ]; + assert( pVertex->nEdges == 1 ); + pNext = p->pVerts[ pVertex->pEdges[0] ]; + // update the data-structures + Nwk_ManGraphUpdate( p, pVertex, pNext ); + break; + } + // find the next vertext to extract + for ( j = 2; j <= MAX_LIST; j++ ) + if ( p->pLists2[j] ) + { + pVertex = p->pVerts[ p->pLists2[j] ]; + assert( pVertex->nEdges == j || j == MAX_LIST ); + // update the data-structures + Nwk_ManGraphUpdate( p, pVertex, pNext ); + break; + } + if ( i == MAX_LIST + 1 && j == MAX_LIST + 1 ) + break; + } +} + + +/**Function************************************************************* + + Synopsis [Performs LUT merging with parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars ) +{ + Nwk_Grf_t * p; + Vec_Int_t * vResult; + Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2; + Nwk_Obj_t * pLut, * pCand; + int i, k, nVertsPre; + // count the number of vertices + nVertsPre = 0; + Nwk_ManForEachNode( pNtk, pLut, i ) + nVertsPre += (int)(Nwk_ObjFaninNum(pLut) <= pPars->nMaxLutSize); + p = Nwk_ManGraphAlloc( Nwk_ManObjNumMax(pNtk), nVertsPre ); + // create graph + vStart = Vec_PtrAlloc( 1000 ); + vNext = Vec_PtrAlloc( 1000 ); + vCands1 = Vec_PtrAlloc( 1000 ); + vCands2 = Vec_PtrAlloc( 1000 ); + Nwk_ManForEachNode( pNtk, pLut, i ) + { + if ( Nwk_ObjFaninNum(pLut) > pPars->nMaxLutSize ) + continue; + Nwl_ManCollectOverlapCands( pLut, vCands1, pPars ); + Nwk_ManCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars ); + if ( Vec_PtrSize(vCands1) == 0 && Vec_PtrSize(vCands2) == 0 ) + continue; + // save candidates + Nwk_ManGraphSetMapping( p, Nwk_ObjId(pLut) ); + Vec_PtrForEachEntry( vCands1, pCand, k ) + Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) ); + Vec_PtrForEachEntry( vCands2, pCand, k ) + Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) ); + // print statistics about this node + printf( "Node %6d : Fanins = %d. Fanouts = %3d. Cand1 = %3d. Cand2 = %3d.\n", + Nwk_ObjId(pLut), Nwk_ObjFaninNum(pLut), Nwk_ObjFaninNum(pLut), + Vec_PtrSize(vCands1), Vec_PtrSize(vCands2) ); + } + Vec_PtrFree( vStart ); + Vec_PtrFree( vNext ); + Vec_PtrFree( vCands1 ); + Vec_PtrFree( vCands2 ); + // solve the graph problem + Nwk_ManGraphPrepare( p ); + Nwk_ManGraphSolve( p ); + vResult = p->vPairs; p->vPairs = NULL; + Nwk_ManGraphFree( p ); + return vResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk/nwkUtil_old.c b/src/aig/nwk/nwkUtil_old.c deleted file mode 100644 index c6f5c136..00000000 --- a/src/aig/nwk/nwkUtil_old.c +++ /dev/null @@ -1,615 +0,0 @@ -/**CFile**************************************************************** - - FileName [nwkUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Logic network representation.] - - Synopsis [Various utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: nwkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "nwk.h" -#include "kit.h" -#include - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Increments the current traversal ID of the network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk ) -{ - Nwk_Obj_t * pObj; - int i; - if ( pNtk->nTravIds >= (1<<26)-1 ) - { - pNtk->nTravIds = 0; - Nwk_ManForEachObj( pNtk, pObj, i ) - pObj->TravId = 0; - } - pNtk->nTravIds++; -} - -/**Function************************************************************* - - Synopsis [Reads the maximum number of fanins.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk ) -{ - Nwk_Obj_t * pNode; - int i, nFaninsMax = 0; - Nwk_ManForEachNode( pNtk, pNode, i ) - { - if ( nFaninsMax < Nwk_ObjFaninNum(pNode) ) - nFaninsMax = Nwk_ObjFaninNum(pNode); - } - return nFaninsMax; -} - -/**Function************************************************************* - - Synopsis [Reads the total number of all fanins.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk ) -{ - Nwk_Obj_t * pNode; - int i, nFanins = 0; - Nwk_ManForEachNode( pNtk, pNode, i ) - nFanins += Nwk_ObjFaninNum(pNode); - return nFanins; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_ManPiNum( Nwk_Man_t * pNtk ) -{ - Nwk_Obj_t * pNode; - int i, Counter = 0; - Nwk_ManForEachCi( pNtk, pNode, i ) - Counter += Nwk_ObjIsPi( pNode ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_ManPoNum( Nwk_Man_t * pNtk ) -{ - Nwk_Obj_t * pNode; - int i, Counter = 0; - Nwk_ManForEachCo( pNtk, pNode, i ) - Counter += Nwk_ObjIsPo( pNode ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Reads the number of BDD nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk ) -{ - Nwk_Obj_t * pNode; - int i, nNodes = 0; - Nwk_ManForEachNode( pNtk, pNode, i ) - { - if ( pNode->pFunc == NULL ) - { - printf( "Nwk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id ); - continue; - } - if ( Nwk_ObjFaninNum(pNode) < 2 ) - continue; - nNodes += Hop_DagSize( pNode->pFunc ); - } - return nNodes; -} - -/**Function************************************************************* - - Synopsis [Procedure used for sorting the nodes in increasing order of levels.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ) -{ - int Diff = (*pp1)->Level - (*pp2)->Level; - if ( Diff < 0 ) - return -1; - if ( Diff > 0 ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ) -{ - int Diff = (*pp1)->Level - (*pp2)->Level; - if ( Diff > 0 ) - return -1; - if ( Diff < 0 ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Deletes the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ObjPrint( Nwk_Obj_t * pObj ) -{ - Nwk_Obj_t * pNext; - int i; - printf( "ObjId = %5d. ", pObj->Id ); - if ( Nwk_ObjIsPi(pObj) ) - printf( "PI" ); - if ( Nwk_ObjIsPo(pObj) ) - printf( "PO" ); - if ( Nwk_ObjIsNode(pObj) ) - printf( "Node" ); - printf( " Fanins = " ); - Nwk_ObjForEachFanin( pObj, pNext, i ) - printf( "%d ", pNext->Id ); - printf( " Fanouts = " ); - Nwk_ObjForEachFanout( pObj, pNext, i ) - printf( "%d ", pNext->Id ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Deletes the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ) -{ - FILE * pFile; - Vec_Ptr_t * vNodes; - Vec_Int_t * vTruth; - Vec_Int_t * vCover; - Nwk_Obj_t * pObj, * pFanin; - Aig_MmFlex_t * pMem; - char * pSop = NULL; - unsigned * pTruth; - int i, k, nDigits, Counter = 0; - if ( Nwk_ManPoNum(pNtk) == 0 ) - { - printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" ); - return; - } - // collect nodes in the DFS order - nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) ); - // write the file - pFile = fopen( pFileName, "w" ); - fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" ); -// fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); - fprintf( pFile, ".model %s\n", pNtk->pName ); - // write PIs - fprintf( pFile, ".inputs" ); - Nwk_ManForEachCi( pNtk, pObj, i ) - if ( vPiNames ) - fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, i) ); - else - fprintf( pFile, " n%0*d", nDigits, pObj->Id ); - fprintf( pFile, "\n" ); - // write POs - fprintf( pFile, ".outputs" ); - Nwk_ManForEachCo( pNtk, pObj, i ) - if ( vPoNames ) - fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, i) ); - else - fprintf( pFile, " n%0*d", nDigits, pObj->Id ); - fprintf( pFile, "\n" ); - // write nodes - pMem = Aig_MmFlexStart(); - vTruth = Vec_IntAlloc( 1 << 16 ); - vCover = Vec_IntAlloc( 1 << 16 ); - vNodes = Nwk_ManDfs( pNtk ); - Vec_PtrForEachEntry( vNodes, pObj, i ) - { - if ( !Nwk_ObjIsNode(pObj) ) - continue; - // derive SOP for the AIG - pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); - if ( Hop_IsComplement(pObj->pFunc) ) - Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) ); - pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover ); - // write the node - fprintf( pFile, ".names" ); - if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) ) - { - Nwk_ObjForEachFanin( pObj, pFanin, k ) - if ( vPiNames && Nwk_ObjIsPi(pFanin) ) - fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) ); - else - fprintf( pFile, " n%0*d", nDigits, pFanin->Id ); - } - fprintf( pFile, " n%0*d\n", nDigits, pObj->Id ); - // write the function - fprintf( pFile, "%s", pSop ); - } - Vec_IntFree( vCover ); - Vec_IntFree( vTruth ); - Vec_PtrFree( vNodes ); - Aig_MmFlexStop( pMem, 0 ); - // write POs - Nwk_ManForEachCo( pNtk, pObj, i ) - { - fprintf( pFile, ".names" ); - if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) ) - fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) ); - else - fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id ); - if ( vPoNames ) - fprintf( pFile, " %s\n", Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) ); - else - fprintf( pFile, " n%0*d\n", nDigits, pObj->Id ); - fprintf( pFile, "%d 1\n", !pObj->fInvert ); - } - fprintf( pFile, ".end\n\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Prints the distribution of fanins/fanouts in the network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ) -{ - char Buffer[100]; - Nwk_Obj_t * pNode; - Vec_Int_t * vFanins, * vFanouts; - int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll; - int i, k, nSizeMax; - - // determine the largest fanin and fanout - nFaninsMax = nFanoutsMax = 0; - nFaninsAll = nFanoutsAll = 0; - Nwk_ManForEachNode( pNtk, pNode, i ) - { - nFanins = Nwk_ObjFaninNum(pNode); - nFanouts = Nwk_ObjFanoutNum(pNode); - nFaninsAll += nFanins; - nFanoutsAll += nFanouts; - nFaninsMax = AIG_MAX( nFaninsMax, nFanins ); - nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts ); - } - - // allocate storage for fanin/fanout numbers - nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); - vFanins = Vec_IntStart( nSizeMax ); - vFanouts = Vec_IntStart( nSizeMax ); - - // count the number of fanins and fanouts - Nwk_ManForEachNode( pNtk, pNode, i ) - { - nFanins = Nwk_ObjFaninNum(pNode); - nFanouts = Nwk_ObjFanoutNum(pNode); -// nFanouts = Nwk_NodeMffcSize(pNode); - - if ( nFanins < 10 ) - Vec_IntAddToEntry( vFanins, nFanins, 1 ); - else if ( nFanins < 100 ) - Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 ); - else if ( nFanins < 1000 ) - Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 ); - else if ( nFanins < 10000 ) - Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 ); - else if ( nFanins < 100000 ) - Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 ); - else if ( nFanins < 1000000 ) - Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 ); - else if ( nFanins < 10000000 ) - Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 ); - - if ( nFanouts < 10 ) - Vec_IntAddToEntry( vFanouts, nFanouts, 1 ); - else if ( nFanouts < 100 ) - Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 ); - else if ( nFanouts < 1000 ) - Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 ); - else if ( nFanouts < 10000 ) - Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 ); - else if ( nFanouts < 100000 ) - Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 ); - else if ( nFanouts < 1000000 ) - Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 ); - else if ( nFanouts < 10000000 ) - Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 ); - } - - printf( "The distribution of fanins and fanouts in the network:\n" ); - printf( " Number Nodes with fanin Nodes with fanout\n" ); - for ( k = 0; k < nSizeMax; k++ ) - { - if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 ) - continue; - if ( k < 10 ) - printf( "%15d : ", k ); - else - { - sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); - printf( "%15s : ", Buffer ); - } - if ( vFanins->pArray[k] == 0 ) - printf( " " ); - else - printf( "%12d ", vFanins->pArray[k] ); - printf( " " ); - if ( vFanouts->pArray[k] == 0 ) - printf( " " ); - else - printf( "%12d ", vFanouts->pArray[k] ); - printf( "\n" ); - } - Vec_IntFree( vFanins ); - Vec_IntFree( vFanouts ); - - printf( "Fanins: Max = %d. Ave = %.2f. Fanouts: Max = %d. Ave = %.2f.\n", - nFaninsMax, 1.0*nFaninsAll/Nwk_ManNodeNum(pNtk), - nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk) ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ManCleanMarks( Nwk_Man_t * pMan ) -{ - Nwk_Obj_t * pObj; - int i; - Nwk_ManForEachObj( pMan, pObj, i ) - pObj->MarkA = pObj->MarkB = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ManMarkCone_rec( Nwk_Obj_t * pObj ) -{ - Nwk_Obj_t * pNext; - int i; - if ( pObj->MarkA ) - return; - pObj->MarkA = 1; - Nwk_ObjForEachFanin( pObj, pNext, i ) - Nwk_ManMarkCone_rec( pNext ); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the flow can be pushed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Nwk_ManPushFlow_rec( Nwk_Obj_t * pObj ) -{ - Nwk_Obj_t * pNext; - int i; - if ( Nwk_ObjIsTravIdCurrent( pObj ) ) - return 0; - Nwk_ObjSetTravIdCurrent( pObj ); - // check the case when there is no flow - if ( !pObj->MarkB ) - { - if ( pObj->MarkA ) - return pObj->MarkB = 1; - Nwk_ObjForEachFanin( pObj, pNext, i ) - if ( Nwk_ManPushFlow_rec( pNext ) ) - return pObj->MarkB = 1; - } - // check the case when there is no flow or we could not push the flow - Nwk_ObjForEachFanout( pObj, pNext, i ) - if ( Nwk_ManPushFlow_rec( pNext ) ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Computes min-cut using max-flow.] - - Description [MarkA means the sink. MarkB means the flow is present.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nwk_ManComputeCut( Nwk_Man_t * pMan, int nLatches ) -{ - Vec_Ptr_t * vNodes; - Nwk_Obj_t * pObj, * pNext; - int i, k, RetValue, Counter = 0; - // set the sequential parameters - pMan->nLatches = nLatches; - pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches; - pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches; - // mark the CIs - Nwk_ManForEachCi( pMan, pObj, i ) - pObj->MarkA = 1; - // mark the TFI of the POs - Nwk_ManForEachPoSeq( pMan, pObj, i ) - Nwk_ManMarkCone_rec( pObj ); - // start flow computation from each LI -// Nwk_ManIncrementTravId( pMan ); - Nwk_ManForEachLiSeq( pMan, pObj, i ) - { - Nwk_ManIncrementTravId( pMan ); - if ( !Nwk_ManPushFlow_rec( pObj ) ) - continue; -// Nwk_ManIncrementTravId( pMan ); - Counter++; - } - // mark the nodes reachable from the LIs - Nwk_ManIncrementTravId( pMan ); - Nwk_ManForEachLiSeq( pMan, pObj, i ) - { - RetValue = Nwk_ManPushFlow_rec( pObj ); - assert( RetValue == 0 ); - } - // collect labeled nodes whose all fanins are labeled - vNodes = Vec_PtrAlloc( Counter ); - Nwk_ManForEachObj( pMan, pObj, i ) - { - // skip unlabeled - if ( !Nwk_ObjIsTravIdCurrent(pObj) ) - continue; - // visit the fanins - Nwk_ObjForEachFanin( pObj, pNext, k ) - if ( !Nwk_ObjIsTravIdCurrent(pNext) ) - break; - if ( k == Nwk_ObjFaninNum(pObj) ) - Vec_PtrPush( vNodes, pObj ); - } - // unlabel these nodes - Nwk_ManIncrementTravId( pMan ); - Vec_PtrForEachEntry( vNodes, pObj, i ) - Nwk_ObjSetTravIdCurrent( pObj ); - // collect labeled nodes having unlabeled fanouts - Vec_PtrClear( vNodes ); - Nwk_ManForEachObj( pMan, pObj, i ) - { - // skip unreachable nodes - if ( !Nwk_ObjIsTravIdPrevious(pObj) ) - continue; - if ( Nwk_ObjIsCo(pObj) ) - { - Vec_PtrPush( vNodes, pObj ); - continue; - } - Nwk_ObjForEachFanout( pObj, pNext, k ) - if ( Nwk_ObjIsTravIdCurrent(pNext) ) - break; - if ( k < Nwk_ObjFanoutNum(pObj) ) - Vec_PtrPush( vNodes, pObj ); - } - - // clean the marks - Nwk_ManCleanMarks( pMan ); - printf( "Flow = %5d. Cut = %5d. \n", Counter, Vec_PtrSize(vNodes) ); - Vec_PtrFree( vNodes ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2c34ed67..4fed39ab 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -123,6 +123,7 @@ static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSenseInput ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -228,6 +229,7 @@ static int Abc_CommandAbc8Mfs ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc8Lutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -380,6 +382,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "qvar", Abc_CommandQuaVar, 1 ); Cmd_CommandAdd( pAbc, "Various", "qrel", Abc_CommandQuaRel, 1 ); Cmd_CommandAdd( pAbc, "Various", "qreach", Abc_CommandQuaReach, 1 ); + Cmd_CommandAdd( pAbc, "Various", "senseinput", Abc_CommandSenseInput, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 ); @@ -480,6 +483,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC8", "*lp", Abc_CommandAbc8Lutpack, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*b", Abc_CommandAbc8Balance, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*speedup", Abc_CommandAbc8Speedup, 0 ); + Cmd_CommandAdd( pAbc, "ABC8", "*merge", Abc_CommandAbc8Merge, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*fraig", Abc_CommandAbc8Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 ); @@ -8096,6 +8100,98 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSenseInput( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Vec_Int_t * vResult; + int c, nConfLim, fVerbose; + + extern Vec_Int_t * Abc_NtkSensitivity( Abc_Ntk_t * pNtk, int nConfLim, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nConfLim = 1000; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLim < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum( pNtk ) ) + { + fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" ); + return 1; + } + if ( !Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "This command works only for combinational transition relations.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } + if ( Abc_NtkPoNum(pNtk) < 2 ) + { + fprintf( pErr, "The network should have at least two outputs.\n" ); + return 1; + } + + vResult = Abc_NtkSensitivity( pNtk, nConfLim, fVerbose ); + Vec_IntFree( vResult ); + return 0; + +usage: + fprintf( pErr, "usage: senseinput [-C num] [-vh]\n" ); + fprintf( pErr, "\t computes sensitivity of POs to PIs under constaint\n" ); + fprintf( pErr, "\t constraint should be represented as the last PO" ); + fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfLim ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -17224,6 +17320,156 @@ usage: return 1; } + +//#include "nwk.h" + +// the LUT merging parameters +typedef struct Nwk_LMPars_t_ Nwk_LMPars_t; +struct Nwk_LMPars_t_ +{ + int nMaxLutSize; // the max LUT size for merging (N=5) + int nMaxSuppSize; // the max total support size after merging (S=5) + int nMaxDistance; // the max number of nodes separating LUTs + int nMaxLevelDiff; // the max difference in levels + int nMaxFanout; // the max number of fanouts to traverse + int fUseTfiTfo; // enables the use of TFO/TFO nodes as candidates + int fVeryVerbose; // enables additional verbose output + int fVerbose; // enables verbose output +}; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Nwk_LMPars_t Pars, * pPars = &Pars; + Vec_Int_t * vResult; + int c; + int fUseLutLib = 0; + int Percentage = 100; + int Degree = 5; + int fVerbose = 0; + int fVeryVerbose = 0; + extern Vec_Int_t * Nwk_ManLutMerge( void * pNtk, Nwk_LMPars_t * pPars ); + + // set defaults + memset( pPars, 0, sizeof(Nwk_LMPars_t) ); + pPars->nMaxLutSize = 5; // the max LUT size for merging (N=5) + pPars->nMaxSuppSize = 5; // the max total support size after merging (S=5) + pPars->nMaxDistance = 3; // the max number of nodes separating LUTs + pPars->nMaxLevelDiff = 2; // the max difference in levels + pPars->nMaxFanout = 100; // the max number of fanouts to traverse + pPars->fUseTfiTfo = 0; // enables the use of TFO/TFO nodes as candidates + pPars->fVeryVerbose = 0; // enables additional verbose output + pPars->fVerbose = 1; // enables verbose output + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NSDLFcvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxLutSize < 2 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxSuppSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxSuppSize < 2 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxDistance = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxDistance < 2 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxLevelDiff = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxLevelDiff < 2 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxFanout = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxFanout < 2 ) + goto usage; + break; + case 'c': + pPars->fUseTfiTfo ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pAbc8Nwk == NULL ) + { + printf( "Abc_CommandAbc8Speedup(): There is no mapped network to merge LUTs.\n" ); + return 1; + } + + vResult = Nwk_ManLutMerge( pAbc->pAbc8Nwk, pPars ); + Vec_IntFree( vResult ); + return 0; + +usage: + fprintf( stdout, "usage: *merge [-NSDLF num] [-cwvh]\n" ); + fprintf( stdout, "\t creates pairs of topologically-related LUTs\n" ); + fprintf( stdout, "\t-N : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize ); + fprintf( stdout, "\t-S : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize ); + fprintf( stdout, "\t-D : the max distance in terms of LUTs (0 < num) [default = %d]\n", pPars->nMaxDistance ); + fprintf( stdout, "\t-L : the max difference in levels (0 <= num) [default = %d]\n", pPars->nMaxLevelDiff ); + fprintf( stdout, "\t-F : the max number of fanouts to stop traversal (0 < num) [default = %d]\n", pPars->nMaxFanout ); + fprintf( stdout, "\t-c : toggle the use of TFI/TFO nodes as candidates [default = %s]\n", pPars->fUseTfiTfo? "yes" : "no" ); + fprintf( stdout, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + fprintf( stdout, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcSense.c b/src/base/abci/abcSense.c new file mode 100644 index 00000000..f3d71a54 --- /dev/null +++ b/src/base/abci/abcSense.c @@ -0,0 +1,208 @@ +/**CFile**************************************************************** + + FileName [abcSense.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Copies the topmost levels of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkSensitivityMiter_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) +{ + assert( !Abc_ObjIsComplement(pNode) ); + if ( pNode->pCopy ) + return pNode->pCopy; + Abc_NtkSensitivityMiter_rec( pNtkNew, Abc_ObjFanin0(pNode) ); + Abc_NtkSensitivityMiter_rec( pNtkNew, Abc_ObjFanin1(pNode) ); + return pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Creates miter for the sensitivity analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSensitivityMiter( Abc_Ntk_t * pNtk, int iVar ) +{ + Abc_Ntk_t * pMiter; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pNext, * pFanin, * pOutput, * pObjNew; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + assert( iVar < Abc_NtkCiNum(pNtk) ); + + // duplicate the network + pMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + pMiter->pName = Extra_UtilStrsav(pNtk->pName); + pMiter->pSpec = Extra_UtilStrsav(pNtk->pSpec); + + // assign the PIs + Abc_NtkCleanCopy( pNtk ); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pMiter); + Abc_AigConst1(pNtk)->pData = Abc_AigConst1(pMiter); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = pObj->pData = Abc_NtkCreatePi( pMiter ); + Abc_NtkAddDummyPiNames( pMiter ); + + // assign the cofactors of the CI node to be constants + pObj = Abc_NtkCi( pNtk, iVar ); + pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pMiter) ); + pObj->pData = Abc_AigConst1(pMiter); + + // collect the internal nodes + vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj ) + { + pFanin = Abc_ObjFanin0(pObj); + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + pFanin->pData = Abc_NtkSensitivityMiter_rec( pMiter, pFanin ); + pFanin = Abc_ObjFanin1(pObj); + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + pFanin->pData = Abc_NtkSensitivityMiter_rec( pMiter, pFanin ); + pObj->pCopy = Abc_AigAnd( pMiter->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + pObj->pData = Abc_AigAnd( pMiter->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) ); + } + } + Vec_PtrFree( vNodes ); + + // update the affected COs + pOutput = Abc_ObjNot( Abc_AigConst1(pMiter) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + continue; + // get the result of quantification + if ( i == Abc_NtkCoNum(pNtk) - 1 ) + { + pOutput = Abc_AigAnd( pMiter->pManFunc, pOutput, Abc_ObjChild0Data(pObj) ); + pOutput = Abc_AigAnd( pMiter->pManFunc, pOutput, Abc_ObjChild0Copy(pObj) ); + } + else + { + pNext = Abc_AigXor( pMiter->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); + pOutput = Abc_AigOr( pMiter->pManFunc, pOutput, pNext ); + } + } + // add the PO node and name + pObjNew = Abc_NtkCreatePo(pMiter); + Abc_ObjAddFanin( pObjNew, pOutput ); + Abc_ObjAssignName( pObjNew, "miter", NULL ); + // make sure everything is okay + if ( !Abc_NtkCheck( pMiter ) ) + { + printf( "Abc_NtkSensitivityMiter: The network check has failed.\n" ); + Abc_NtkDelete( pMiter ); + return NULL; + } + return pMiter; +} + +/**Function************************************************************* + + Synopsis [Computing sensitivity of POs to POs under constaints.] + + Description [The input network is a combinatonal AIG. The last output + is a constraint. The procedure returns the list of number of PIs, + such that at least one PO depends on this PI, under the constraint.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkSensitivity( Abc_Ntk_t * pNtk, int nConfLim, int fVerbose ) +{ + ProgressBar * pProgress; + Prove_Params_t Params, * pParams = &Params; + Vec_Int_t * vResult = NULL; + Abc_Ntk_t * pMiter; + Abc_Obj_t * pObj; + int RetValue, i; + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + // set up solving parameters + Prove_ParamsSetDefault( pParams ); + pParams->nItersMax = 3; + pParams->nMiteringLimitLast = nConfLim; + // iterate through the PIs + vResult = Vec_IntAlloc( 100 ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // generate the sensitivity miter + pMiter = Abc_NtkSensitivityMiter( pNtk, i ); + // solve the miter using CEC engine + RetValue = Abc_NtkIvyProve( &pMiter, pParams ); + if ( RetValue == -1 ) // undecided + Vec_IntPush( vResult, i ); + else if ( RetValue == 0 ) + { + int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" ); +// else +// printf( "Networks are NOT EQUIVALENT.\n" ); + free( pSimInfo ); + Vec_IntPush( vResult, i ); + } + Abc_NtkDelete( pMiter ); + } + Extra_ProgressBarStop( pProgress ); + if ( fVerbose ) + { + printf( "The outputs are sensitive to %d (out of %d) inputs:\n", + Vec_IntSize(vResult), Abc_NtkCiNum(pNtk) ); + Vec_IntForEachEntry( vResult, RetValue, i ) + printf( "%d ", RetValue ); + printf( "\n" ); + } + return vResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index ca2f2501..777da95b 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -48,6 +48,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcRewrite.c \ src/base/abci/abcRr.c \ src/base/abci/abcSat.c \ + src/base/abci/abcSense.c \ src/base/abci/abcStrash.c \ src/base/abci/abcSweep.c \ src/base/abci/abcSymm.c \ -- cgit v1.2.3