diff options
Diffstat (limited to 'src/aig/llb/llbFlow.c')
| -rw-r--r-- | src/aig/llb/llbFlow.c | 639 |
1 files changed, 0 insertions, 639 deletions
diff --git a/src/aig/llb/llbFlow.c b/src/aig/llb/llbFlow.c deleted file mode 100644 index 55405c09..00000000 --- a/src/aig/llb/llbFlow.c +++ /dev/null @@ -1,639 +0,0 @@ -/**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 - |