/**CFile****************************************************************
FileName [llbPart.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Initial partition computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbPart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan )
{
Llb_Grp_t * p;
p = ABC_CALLOC( Llb_Grp_t, 1 );
p->pMan = pMan;
p->vIns = Vec_PtrAlloc( 8 );
p->vOuts = Vec_PtrAlloc( 8 );
p->Id = Vec_PtrSize( pMan->vGroups );
Vec_PtrPush( pMan->vGroups, p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManGroupStop( Llb_Grp_t * p )
{
if ( p == NULL )
return;
Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL );
Vec_PtrFreeP( &p->vIns );
Vec_PtrFreeP( &p->vOuts );
Vec_PtrFreeP( &p->vNodes );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsConst1(pObj) )
return;
if ( Aig_ObjIsPo(pObj) )
{
Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
return;
}
assert( Aig_ObjIsAnd(pObj) );
Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin1(pObj), vNodes );
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis [Collects the support of MFFC.]
Description [Returns the number of internal nodes in the MFFC.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_ManGroupCollect( Llb_Grp_t * pGroup )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
vNodes = Vec_PtrAlloc( 100 );
Aig_ManIncrementTravId( pGroup->pMan->pAig );
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
Aig_ObjSetTravIdCurrent( pGroup->pMan->pAig, pObj );
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
Aig_ObjSetTravIdPrevious( pGroup->pMan->pAig, pObj );
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
Llb_ManGroupCollect_rec( pGroup->pMan->pAig, pObj, vNodes );
return vNodes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManGroupCreate_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsConst1(pObj) )
return;
if ( pObj->fMarkA )
{
Vec_PtrPush( vSupp, pObj );
return;
}
assert( Aig_ObjIsAnd(pObj) );
Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin0(pObj), vSupp );
Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin1(pObj), vSupp );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj )
{
Llb_Grp_t * p;
assert( pObj->fMarkA == 1 );
// derive group
p = Llb_ManGroupAlloc( pMan );
Vec_PtrPush( p->vOuts, pObj );
Aig_ManIncrementTravId( pMan->pAig );
if ( Aig_ObjIsPo(pObj) )
Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
else
{
Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin1(pObj), p->vIns );
}
// derive internal objects
assert( p->vNodes == NULL );
p->vNodes = Llb_ManGroupCollect( p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreateFirst( Llb_Man_t * pMan )
{
Llb_Grp_t * p;
Aig_Obj_t * pObj;
int i;
p = Llb_ManGroupAlloc( pMan );
Saig_ManForEachLo( pMan->pAig, pObj, i )
Vec_PtrPush( p->vOuts, pObj );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreateLast( Llb_Man_t * pMan )
{
Llb_Grp_t * p;
Aig_Obj_t * pObj;
int i;
p = Llb_ManGroupAlloc( pMan );
Saig_ManForEachLi( pMan->pAig, pObj, i )
Vec_PtrPush( p->vIns, pObj );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 )
{
Llb_Grp_t * p;
Aig_Obj_t * pObj;
int i;
p = Llb_ManGroupAlloc( p1->pMan );
// create inputs
Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i )
Vec_PtrPush( p->vIns, pObj );
Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i )
Vec_PtrPushUnique( p->vIns, pObj );
// create outputs
Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i )
Vec_PtrPush( p->vOuts, pObj );
Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i )
Vec_PtrPushUnique( p->vOuts, pObj );
// derive internal objects
assert( p->vNodes == NULL );
p->vNodes = Llb_ManGroupCollect( p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManGroupMarkNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
if ( Aig_ObjIsTravIdPrevious(p, pObj) )
{
Aig_ObjSetTravIdCurrent(p, pObj);
return;
}
Aig_ObjSetTravIdCurrent(p, pObj);
assert( Aig_ObjIsNode(pObj) );
Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin0(pObj) );
Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin1(pObj) );
}
/**Function*************************************************************
Synopsis [Creates group from two cuts derived by the flow computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
{
Llb_Grp_t * p;
Aig_Obj_t * pObj;
int i;
p = Llb_ManGroupAlloc( pMan );
// mark Cut1
Aig_ManIncrementTravId( pMan->pAig );
Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
// collect unmarked Cut2
Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
Vec_PtrPush( p->vOuts, pObj );
// mark nodes reachable from Cut2
Aig_ManIncrementTravId( pMan->pAig );
Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
// collect marked Cut1
Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
Vec_PtrPush( p->vIns, pObj );
// derive internal objects
assert( p->vNodes == NULL );
p->vNodes = Llb_ManGroupCollect( p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManPrepareGroups( Llb_Man_t * pMan )
{
Aig_Obj_t * pObj;
int i;
assert( pMan->vGroups == NULL );
pMan->vGroups = Vec_PtrAlloc( 1000 );
Llb_ManGroupCreateFirst( pMan );
Aig_ManForEachNode( pMan->pAig, pObj, i )
{
if ( pObj->fMarkA )
Llb_ManGroupCreate( pMan, pObj );
}
Saig_ManForEachLi( pMan->pAig, pObj, i )
{
if ( pObj->fMarkA )
Llb_ManGroupCreate( pMan, pObj );
}
Llb_ManGroupCreateLast( pMan );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManPrintSpan( Llb_Man_t * p )
{
Llb_Grp_t * pGroup;
Aig_Obj_t * pVar;
int i, k, Span = 0, SpanMax = 0;
Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
{
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
Span++;
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
Span++;
SpanMax = ABC_MAX( SpanMax, Span );
printf( "%d ", Span );
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
Span--;
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
Span--;
}
printf( "\n" );
printf( "Max = %d\n", SpanMax );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_ManGroupHasVar( Llb_Man_t * p, int iGroup, int iVar )
{
Llb_Grp_t * pGroup = (Llb_Grp_t *)Vec_PtrEntry( p->vGroups, iGroup );
Aig_Obj_t * pObj;
int i;
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
if ( pObj->Id == iVar )
return 1;
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
if ( pObj->Id == iVar )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManPrintHisto( Llb_Man_t * p )
{
Aig_Obj_t * pObj;
int i, k;
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( Vec_IntEntry(p->vObj2Var, i) < 0 )
continue;
printf( "%3d :", i );
for ( k = 0; k < Vec_IntEntry(p->vVarBegs, i); k++ )
printf( " " );
for ( ; k <= Vec_IntEntry(p->vVarEnds, i); k++ )
printf( "%c", Llb_ManGroupHasVar(p, k, i)? '*':'-' );
printf( "\n" );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END