| /**CFile**************************************************************** |
| |
| FileName [llb2Cluster.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [BDD based reachability.] |
| |
| Synopsis [Non-linear quantification scheduling.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: llb2Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "llbInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find good static variable ordering.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter ) |
| { |
| Aig_Obj_t * pFanin0, * pFanin1; |
| if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) |
| return; |
| Aig_ObjSetTravIdCurrent( pAig, pObj ); |
| assert( Llb_ObjBddVar(vOrder, pObj) < 0 ); |
| if ( Aig_ObjIsCi(pObj) ) |
| { |
| Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); |
| return; |
| } |
| // try fanins with higher level first |
| pFanin0 = Aig_ObjFanin0(pObj); |
| pFanin1 = Aig_ObjFanin1(pObj); |
| // if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) ) |
| if ( pFanin0->Level > pFanin1->Level ) |
| { |
| Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter ); |
| Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter ); |
| } |
| else |
| { |
| Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter ); |
| Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter ); |
| } |
| if ( pObj->fMarkA ) |
| Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find good static variable ordering.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter ) |
| { |
| Vec_Int_t * vNodes = NULL; |
| Vec_Int_t * vOrder; |
| Aig_Obj_t * pObj; |
| int i, Counter = 0; |
| // mark nodes to exclude: AND with low level and CO drivers |
| Aig_ManCleanMarkA( pAig ); |
| Aig_ManForEachNode( pAig, pObj, i ) |
| if ( Aig_ObjLevel(pObj) > 3 ) |
| pObj->fMarkA = 1; |
| Aig_ManForEachCo( pAig, pObj, i ) |
| Aig_ObjFanin0(pObj)->fMarkA = 0; |
| |
| // collect nodes in the order |
| vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); |
| Aig_ManIncrementTravId( pAig ); |
| Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); |
| // Aig_ManForEachCo( pAig, pObj, i ) |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); |
| Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter ); |
| } |
| Aig_ManForEachCi( pAig, pObj, i ) |
| if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) |
| Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); |
| Aig_ManCleanMarkA( pAig ); |
| Vec_IntFreeP( &vNodes ); |
| // assert( Counter == Aig_ManObjNum(pAig) - 1 ); |
| |
| /* |
| Saig_ManForEachPi( pAig, pObj, i ) |
| printf( "pi%d ", Llb_ObjBddVar(vOrder, pObj) ); |
| printf( "\n" ); |
| Saig_ManForEachLo( pAig, pObj, i ) |
| printf( "lo%d ", Llb_ObjBddVar(vOrder, pObj) ); |
| printf( "\n" ); |
| Saig_ManForEachPo( pAig, pObj, i ) |
| printf( "po%d ", Llb_ObjBddVar(vOrder, pObj) ); |
| printf( "\n" ); |
| Saig_ManForEachLi( pAig, pObj, i ) |
| printf( "li%d ", Llb_ObjBddVar(vOrder, pObj) ); |
| printf( "\n" ); |
| Aig_ManForEachNode( pAig, pObj, i ) |
| printf( "n%d ", Llb_ObjBddVar(vOrder, pObj) ); |
| printf( "\n" ); |
| */ |
| if ( pCounter ) |
| *pCounter = Counter; |
| return vOrder; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives BDDs for the partitions.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots ) |
| { |
| DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar; |
| if ( Aig_ObjIsConst1(pObj) ) |
| return Cudd_ReadOne(dd); |
| if ( Aig_ObjIsCi(pObj) ) |
| return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); |
| if ( pObj->pData ) |
| return (DdNode *)pObj->pData; |
| if ( Aig_ObjIsCo(pObj) ) |
| { |
| bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) ); |
| bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart ); |
| Vec_PtrPush( vRoots, bPart ); |
| return NULL; |
| } |
| bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) ); |
| bBdd1 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) ); |
| bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd ); |
| if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) |
| { |
| vVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); |
| bPart = Cudd_bddXnor( dd, vVar, bBdd ); Cudd_Ref( bPart ); |
| Vec_PtrPush( vRoots, bPart ); |
| Cudd_RecursiveDeref( dd, bBdd ); |
| bBdd = vVar; Cudd_Ref( vVar ); |
| } |
| pObj->pData = bBdd; |
| return bBdd; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives BDDs for the partitions.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fOutputs ) |
| { |
| Vec_Ptr_t * vRoots; |
| Aig_Obj_t * pObj; |
| int i; |
| Aig_ManCleanData( pAig ); |
| vRoots = Vec_PtrAlloc( 100 ); |
| if ( fOutputs ) |
| { |
| Saig_ManForEachPo( pAig, pObj, i ) |
| Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots ); |
| } |
| else |
| { |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots ); |
| } |
| Aig_ManForEachNode( pAig, pObj, i ) |
| if ( pObj->pData ) |
| Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); |
| return vRoots; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates quantifiable variables for both types of traversal.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) |
| { |
| Vec_Int_t * vVars2Q; |
| Aig_Obj_t * pObj; |
| int i; |
| vVars2Q = Vec_IntAlloc( 0 ); |
| Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 ); |
| Saig_ManForEachLo( pAig, pObj, i ) |
| Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 ); |
| // Aig_ManForEachCo( pAig, pObj, i ) |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 ); |
| return vVars2Q; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates quantifiable variables for both types of traversal.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop ) |
| { |
| DdNode * bSupp; |
| Aig_Obj_t * pObj; |
| int i, Counter = 0; |
| bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); |
| if ( !fCo && !fFlop ) |
| { |
| Saig_ManForEachPi( pAig, pObj, i ) |
| if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) |
| Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) ); |
| } |
| else if ( fCo && !fFlop ) |
| { |
| Saig_ManForEachPo( pAig, pObj, i ) |
| if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) |
| Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) ); |
| } |
| else if ( !fCo && fFlop ) |
| { |
| Saig_ManForEachLo( pAig, pObj, i ) |
| if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) |
| Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) ); |
| } |
| else if ( fCo && fFlop ) |
| { |
| Saig_ManForEachLi( pAig, pObj, i ) |
| if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) |
| Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) ); |
| } |
| Cudd_RecursiveDeref( dd, bSupp ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates quantifiable variables for both types of traversal.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups ) |
| { |
| DdNode * bTemp; |
| int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd; |
| Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i ) |
| { |
| //Extra_bddPrintSupport(dd, bTemp); printf("\n" ); |
| nSuppAll = Cudd_SupportSize(dd,bTemp); |
| nSuppPi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0); |
| nSuppPo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0); |
| nSuppLi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1); |
| nSuppLo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1); |
| nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo); |
| |
| if ( Cudd_DagSize(bTemp) <= 10 ) |
| continue; |
| |
| printf( "%4d : bdd =%6d supp =%3d ", i, Cudd_DagSize(bTemp), nSuppAll ); |
| printf( "pi =%3d ", nSuppPi ); |
| printf( "po =%3d ", nSuppPo ); |
| printf( "lo =%3d ", nSuppLo ); |
| printf( "li =%3d ", nSuppLi ); |
| printf( "and =%3d", nSuppAnd ); |
| printf( "\n" ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates quantifiable variables for both types of traversal.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_Nonlin4PrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups ) |
| { |
| Aig_Obj_t * pObj; |
| int i, * pSupp; |
| int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0; |
| |
| pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) ); |
| Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp ); |
| |
| Aig_ManForEachObj( pAig, pObj, i ) |
| { |
| if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) |
| continue; |
| // remove variables that do not participate |
| if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 ) |
| { |
| if ( Aig_ObjIsNode(pObj) ) |
| Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 ); |
| continue; |
| } |
| nSuppAll++; |
| if ( Saig_ObjIsPi(pAig, pObj) ) |
| nSuppPi++; |
| else if ( Saig_ObjIsLo(pAig, pObj) ) |
| nSuppLo++; |
| else if ( Saig_ObjIsPo(pAig, pObj) ) |
| nSuppPo++; |
| else if ( Saig_ObjIsLi(pAig, pObj) ) |
| nSuppLi++; |
| else |
| nSuppAnd++; |
| } |
| ABC_FREE( pSupp ); |
| |
| printf( "Groups =%3d ", Vec_PtrSize(vGroups) ); |
| printf( "Variables: all =%4d ", nSuppAll ); |
| printf( "pi =%4d ", nSuppPi ); |
| printf( "po =%4d ", nSuppPo ); |
| printf( "lo =%4d ", nSuppLo ); |
| printf( "li =%4d ", nSuppLi ); |
| printf( "and =%4d", nSuppAnd ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose ) |
| { |
| DdManager * dd; |
| Vec_Int_t * vOrder, * vVars2Q; |
| Vec_Ptr_t * vParts, * vGroups; |
| DdNode * bTemp; |
| int i, nVarNum; |
| |
| // create the BDD manager |
| vOrder = Llb_Nonlin4FindOrder( pAig, &nVarNum ); |
| dd = Cudd_Init( nVarNum, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); |
| // Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); |
| |
| vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder ); |
| vParts = Llb_Nonlin4FindPartitions( dd, pAig, vOrder, 0 ); |
| |
| vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddMax ); |
| Vec_IntFree( vVars2Q ); |
| |
| Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i ) |
| Cudd_RecursiveDeref( dd, bTemp ); |
| Vec_PtrFree( vParts ); |
| |
| |
| // if ( fVerbose ) |
| Llb_Nonlin4PrintSuppProfile( dd, pAig, vOrder, vGroups ); |
| if ( fVerbose ) |
| printf( "Before reordering\n" ); |
| if ( fVerbose ) |
| Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups ); |
| |
| // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); |
| // printf( "After reordering\n" ); |
| // Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups ); |
| |
| if ( pvOrder ) |
| *pvOrder = vOrder; |
| else |
| Vec_IntFree( vOrder ); |
| |
| if ( pvGroups ) |
| *pvGroups = vGroups; |
| else |
| { |
| Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i ) |
| Cudd_RecursiveDeref( dd, bTemp ); |
| Vec_PtrFree( vGroups ); |
| } |
| |
| if ( pdd ) |
| *pdd = dd; |
| else |
| Extra_StopManager( dd ); |
| // Cudd_Quit( dd ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
