diff options
Diffstat (limited to 'src/aig/llb/llbFlow.c')
| -rw-r--r-- | src/aig/llb/llbFlow.c | 639 |
1 files changed, 639 insertions, 0 deletions
diff --git a/src/aig/llb/llbFlow.c b/src/aig/llb/llbFlow.c new file mode 100644 index 00000000..55405c09 --- /dev/null +++ b/src/aig/llb/llbFlow.c @@ -0,0 +1,639 @@ +/**CFile**************************************************************** + + FileName [llbFlow.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Flow computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Llb_Flw_t_ Llb_Flw_t; +struct Llb_Flw_t_ +{ + unsigned Source : 1; // source of the graph + unsigned Sink : 1; // sink of the graph + unsigned Flow : 1; // node has flow + unsigned Mark : 1; // visited node + unsigned Id : 14; // ID of the corresponding node + unsigned nFanins : 14; // number of fanins + Llb_Flw_t * Fanins[0]; // fanins +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Flw_t * Llb_FlwAlloc( Vec_Int_t * vMem, Vec_Ptr_t * vStore, int Id, int nFanins ) +{ + Llb_Flw_t * p; + int nWords = (sizeof(Llb_Flw_t) + nFanins * sizeof(void *)) / sizeof(int); + p = (Llb_Flw_t *)Vec_IntFetch( vMem, nWords ); + memset( p, 1, nWords * sizeof(int) ); + p->Id = Id; + p->nFanins = 0;//nFanins; + Vec_PtrWriteEntry( vStore, Id, p ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_FlwAddFanin( Llb_Flw_t * pFrom, Llb_Flw_t * pTo ) +{ + pFrom->Fanins[pFrom->nFanins++] = pTo; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigCreateFlw( Aig_Man_t * p, Vec_Int_t ** pvMem, Vec_Ptr_t ** pvTops, Vec_Ptr_t ** pvBots ) +{ + Llb_Flw_t * pFlwTop, * pFlwBot; + Vec_Ptr_t * vTops, * vBots; + Vec_Int_t * vMem; + Aig_Obj_t * pObj; + int i; + vMem = Vec_IntAlloc( Aig_ManObjNumMax(p) * (sizeof(Llb_Flw_t) + sizeof(void *) * 8) ); + vBots = Vec_PtrStart( Aig_ManObjNumMax(p) ); + vTops = Vec_PtrStart( Aig_ManObjNumMax(p) ); + Aig_ManForEachObj( p, pObj, i ) + { + pFlwBot = Llb_FlwAlloc( vMem, vBots, i, Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) ); + pFlwTop = Llb_FlwAlloc( vMem, vTops, i, Aig_ObjRefs(pObj) + 1 ); + Llb_FlwAddFanin( pFlwBot, pFlwTop ); + Llb_FlwAddFanin( pFlwTop, pFlwBot ); + Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)) ); + Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)) ); + Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)), pFlwBot ); + Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)), pFlwBot ); + } + Aig_ManForEachObj( p, pObj, i ) + { + pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i ); + pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i ); + assert( pFlwBot->nFanins == (unsigned)Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) ); + assert( pFlwTop->nFanins == (unsigned)Aig_ObjRefs(pObj) + 1 ); + } + *pvMem = vMem; + *pvTops = vTops; + *pvBots = vBots; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigCleanMarks( Vec_Ptr_t * vFlw ) +{ + Llb_Flw_t * pFlw; + int i; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i ) + pFlw->Mark = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigCleanFlow( Vec_Ptr_t * vFlw ) +{ + Llb_Flw_t * pFlw; + int i; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i ) + pFlw->Flow = 0; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_AigCollectCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vBots, Vec_Ptr_t * vTops ) +{ + Vec_Int_t * vCut; + Llb_Flw_t * pFlwBot, * pFlwTop; + Aig_Obj_t * pObj; + int i; + vCut = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + { + pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i ); + pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i ); + if ( pFlwBot->Mark && !pFlwTop->Mark ) + Vec_IntPush( vCut, i ); + } + return vCut; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_AigPushFlow_rec( Llb_Flw_t * pFlw, Llb_Flw_t * pFlwPrev, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed ) +{ + int i; + if ( pFlw->Mark ) + return 0; + pFlw->Mark = 1; + Vec_PtrPush( vMarked, pFlw ); + if ( pFlw->Source ) + return 0; + if ( pFlw->Sink ) + { + pFlw->Flow = 1; + Vec_PtrPush( vFlowed, pFlw ); + return 1; + } +// assert( Aig_ObjIsNode(pObj) ); + for ( i = 0; i < (int)pFlw->nFanins; i++ ) + { + if ( pFlw->Fanins[i] == pFlwPrev ) + continue; + if ( Llb_AigPushFlow_rec( pFlw->Fanins[i], pFlw, vMarked, vFlowed ) ) + break; + } + if ( i == (int)pFlw->nFanins ) + return 0; + if ( i == 0 ) + { + pFlw->Flow = 1; + Vec_PtrPush( vFlowed, pFlw ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_AigPushFlow( Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed ) +{ + Llb_Flw_t * pFlw; + int i, Counter = 0; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlwBots, pFlw, i ) + { + pFlw->Mark = 1; + if ( Llb_AigPushFlow_rec( pFlw->Fanins[0], pFlw, vMarked, vFlowed ) ) + { + Counter++; + pFlw->Flow = 1; + Vec_PtrPush( vFlowed, pFlw ); + } + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_AigFindMinCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vFlwTop, Vec_Ptr_t * vFlwBots2, Vec_Ptr_t * vFlwTop2 ) +{ + Vec_Int_t * vCut; + Vec_Ptr_t * vMarked, * vFlowed; + int Value; + vMarked = Vec_PtrAlloc( 100 ); + vFlowed = Vec_PtrAlloc( 100 ); + Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed ); + Llb_AigCleanMarks( vMarked ); + Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed ); + assert( Value == 0 ); + vCut = Llb_AigCollectCut( vNodes, vFlwBots, vFlwTop ); + Llb_AigCleanMarks( vMarked ); + Llb_AigCleanFlow( vFlowed ); + return vCut; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_AigCollectFlowTerminals( Aig_Man_t * p, Vec_Ptr_t * vFlws, Vec_Int_t * vCut ) +{ + Vec_Ptr_t * pFlwRes; + Aig_Obj_t * pObj; + int i; + pFlwRes = Vec_PtrAlloc( Vec_IntSize(vCut) ); + Aig_ManForEachNodeVec( p, vCut, pObj, i ) + Vec_PtrPush( pFlwRes, Vec_PtrEntry( vFlws, Aig_ObjId(pObj) ) ); + return pFlwRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigMarkFlowTerminals( Vec_Ptr_t * vFlws, int fSource, int fSink ) +{ + Llb_Flw_t * pFlw; + int i; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlws, pFlw, i ) + { + pFlw->Source = fSource; + pFlw->Sink = fSink; + } +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManCollectNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + assert( Aig_ObjIsNode(pObj) ); + Llb_ManCollectNodes_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Llb_ManCollectNodes_rec( p, Aig_ObjFanin1(pObj), vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_ManCollectNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + Aig_ManForEachNodeVec( p, vCut1, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) ); + Aig_ManForEachNodeVec( p, vCut2, pObj, i ) + Llb_ManCollectNodes_rec( p, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManCountNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Aig_ObjSetTravIdCurrent(p, pObj); + assert( Aig_ObjIsNode(pObj) ); + return 1 + Llb_ManCountNodes_rec( p, Aig_ObjFanin0(pObj) ) + + Llb_ManCountNodes_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManCountNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManIncrementTravId( p ); + Aig_ManForEachNodeVec( p, vCut1, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + Aig_ManForEachNodeVec( p, vCut2, pObj, i ) + Counter += Llb_ManCountNodes_rec( p, pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Computes starting cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManComputeCioCut( Aig_Man_t * pAig, int fCollectCos ) +{ + Vec_Int_t * vCut; + Aig_Obj_t * pObj; + int i; + vCut = Vec_IntAlloc( 500 ); + if ( fCollectCos ) + Aig_ManForEachPo( pAig, pObj, i ) + Vec_IntPush( vCut, Aig_ObjId(pObj) ); + else + Aig_ManForEachPi( pAig, pObj, i ) + Vec_IntPush( vCut, Aig_ObjId(pObj) ); + return vCut; +} + +/**Function************************************************************* + + Synopsis [Inserts the new cut into the array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManCutInsert( Aig_Man_t * p, Vec_Ptr_t * vCuts, Vec_Int_t * vVols, int iEntry, Vec_Int_t * vCutNew ) +{ + Vec_Int_t * vCut1, * vCut2; + int Vol1, Vol2; + Vec_PtrInsert( vCuts, iEntry, vCutNew ); + Vec_IntInsert( vVols, iEntry, -1 ); + vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry ); + vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 ); + Vol1 = Llb_ManCountNodes( p, vCut1, vCutNew ); + Vol2 = Llb_ManCountNodes( p, vCutNew, vCut2 ); + Vec_IntWriteEntry( vVols, iEntry-1, Vol1 ); + Vec_IntWriteEntry( vVols, iEntry, Vol2 ); +} + +/**Function************************************************************* + + Synopsis [Returns the set of cuts resulting from the flow computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_ManComputePartitioning( Aig_Man_t * p, int nVolumeMin, int nVolumeMax ) +{ + Vec_Ptr_t * vCuts, * vFlwTops, * vFlwBots; + Vec_Int_t * vVols, * vCut1, * vCut2, * vCut, * vMem; + int nMaxValue, iEntry; + vCuts = Vec_PtrAlloc( 1000 ); + vVols = Vec_IntAlloc( 1000 ); + // prepare flow computation + Llb_AigCreateFlw( p, &vMem, &vFlwTops, &vFlwBots ); + // start with regular cuts + Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 0) ); + Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 1) ); + Vec_IntPush( vVols, Aig_ManNodeNum(p) ); + // split cuts with the largest volume + while ( (nMaxValue = Vec_IntFindMax(vVols)) > nVolumeMax ) + { + Vec_Ptr_t * vNodes, * vFlwBots2, * vFlwTops2; + iEntry = Vec_IntFind( vVols, nMaxValue ); assert( iEntry >= 0 ); + vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry ); + vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 ); + // collect nodes + vNodes = Llb_ManCollectNodes( p, vCut1, vCut1 ); + assert( Vec_PtrSize(vNodes) == nMaxValue ); + assert( Llb_ManCountNodes(p, vCut1, vCut2) == nMaxValue ); + // collect sources and sinks + vFlwBots2 = Llb_AigCollectFlowTerminals( p, vFlwBots, vCut1 ); + vFlwTops2 = Llb_AigCollectFlowTerminals( p, vFlwTops, vCut2 ); + // mark sources and sinks + Llb_AigMarkFlowTerminals( vFlwBots2, 1, 0 ); + Llb_AigMarkFlowTerminals( vFlwTops2, 0, 1 ); + vCut = Llb_AigFindMinCut( vNodes, vFlwBots, vFlwTops, vFlwBots2, vFlwTops2 ); + Llb_AigMarkFlowTerminals( vFlwBots2, 0, 0 ); + Llb_AigMarkFlowTerminals( vFlwTops2, 0, 0 ); + // insert new cut + Llb_ManCutInsert( p, vCuts, vVols, iEntry+1, vCut ); + // deallocate + Vec_PtrFree( vNodes ); + Vec_PtrFree( vFlwBots2 ); + Vec_PtrFree( vFlwTops2 ); + } + Vec_IntFree( vMem ); + Vec_PtrFree( vFlwTops ); + Vec_PtrFree( vFlwBots ); + return vCuts; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManMarkPivotNodesFlow( Aig_Man_t * p, Vec_Ptr_t * vCuts ) +{ + Vec_Int_t * vVar2Obj, * vCut; + Aig_Obj_t * pObj; + int i, k; + // mark inputs/outputs + Aig_ManForEachPi( p, pObj, i ) + pObj->fMarkA = 1; + Saig_ManForEachLi( p, pObj, i ) + pObj->fMarkA = 1; + + // mark internal pivot nodes + Vec_PtrForEachEntry( Vec_Int_t *, vCuts, vCut, i ) + Aig_ManForEachNodeVec( p, vCut, pObj, k ) + pObj->fMarkA = 1; + + // assign variable numbers + Aig_ManConst1(p)->fMarkA = 0; + vVar2Obj = Vec_IntAlloc( 100 ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + Aig_ManForEachNode( p, pObj, i ) + if ( pObj->fMarkA ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + Saig_ManForEachLi( p, pObj, i ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + return vVar2Obj; +} + +/**Function************************************************************* + + Synopsis [Returns the set of cuts resulting from the flow computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPartitionUsingFlow( Llb_Man_t * p, Vec_Ptr_t * vCuts ) +{ + Vec_Int_t * vCut1, * vCut2; + int i; + vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, 0 ); + Vec_PtrForEachEntryStart( Vec_Int_t *, vCuts, vCut1, i, 1 ) + { + vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, i ); + Llb_ManGroupCreateFromCuts( p, vCut1, vCut2 ); + vCut1 = vCut2; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Vec_Ptr_t * vCuts; + Llb_Man_t * p; + vCuts = Llb_ManComputePartitioning( pAig, pPars->nVolumeMin, pPars->nVolumeMax ); + Aig_ManCleanMarkA( pAig ); + p = ABC_CALLOC( Llb_Man_t, 1 ); + p->pAigGlo = pAigGlo; + p->pPars = pPars; + p->pAig = pAig; + p->vVar2Obj = Llb_ManMarkPivotNodesFlow( p->pAig, vCuts ); + p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 ); + Llb_ManPrepareVarMap( p ); + Aig_ManCleanMarkA( pAig ); + Llb_ManPartitionUsingFlow( p, vCuts ); + Vec_VecFreeP( (Vec_Vec_t **)&vCuts ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |