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