diff options
Diffstat (limited to 'src/aig/cec2/cecClass.c')
| -rw-r--r-- | src/aig/cec2/cecClass.c | 571 |
1 files changed, 0 insertions, 571 deletions
diff --git a/src/aig/cec2/cecClass.c b/src/aig/cec2/cecClass.c deleted file mode 100644 index 24e40281..00000000 --- a/src/aig/cec2/cecClass.c +++ /dev/null @@ -1,571 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecClass.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [Equivalence class representation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p, int nLevels ) -{ - Aig_Man_t * pAig; - Aig_Obj_t ** pCopy; - Aig_Obj_t * pRes0, * pRes1, * pRepr, * pNode; - Aig_Obj_t * pMiter; - int i; - pAig = Aig_ManStart( p->nNodes ); - pCopy = ABC_ALLOC( Aig_Obj_t *, p->nObjs ); - pCopy[0] = Aig_ManConst1(pAig); - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] == -1 ) // pi always has zero first fanin - { - pCopy[i] = Aig_ObjCreatePi( pAig ); - continue; - } - if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - pRes0 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans0[i])], Cec_LitIsCompl(p->pFans0[i]) ); - pRes1 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans1[i])], Cec_LitIsCompl(p->pFans1[i]) ); - pNode = pCopy[i] = Aig_And( pAig, pRes0, pRes1 ); - if ( p->pReprs[i] < 0 ) - continue; - assert( p->pReprs[i] < i ); - pRepr = pCopy[p->pReprs[i]]; - if ( Aig_Regular(pNode) == Aig_Regular(pRepr) ) - continue; - pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) ); - if ( nLevels && ((int)Aig_Regular(pRepr)->Level > nLevels || (int)Aig_Regular(pNode)->Level > nLevels) ) - continue; - pMiter = Aig_Exor( pAig, pNode, pRepr ); - Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); -// Aig_ObjCreatePo( pAig, Aig_Regular(pRepr) ); -// Aig_ObjCreatePo( pAig, Aig_Regular(pCopy[i]) ); - } - ABC_FREE( pCopy ); - Aig_ManSetRegNum( pAig, 0 ); - Aig_ManCleanup( pAig ); - return pAig; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCountOne( Caig_Man_t * p, int i ) -{ - int Ent, nLits = 0; - assert( p->pReprs[i] < 0 && p->pNexts[i] > 0 ); - for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] ) - { - assert( p->pReprs[Ent] == i ); - nLits++; - } - return 1 + nLits; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCountLiterals( Caig_Man_t * p ) -{ - int i, nLits = 0; - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - nLits += Caig_ManCountOne(p, i) - 1; - return nLits; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter ) -{ - int Ent; - printf( "Class %4d : Num = %2d {", Counter, Caig_ManCountOne(p, i) ); - for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) - printf(" %d", Ent ); - printf( " }\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose ) -{ - int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits; - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - Counter++; - if ( p->pReprs[i] == 0 ) - Counter1++; - if ( p->pReprs[i] < 0 && p->pNexts[i] == 0 ) - CounterX++; - } - nLits = Caig_ManCountLiterals( p ); - printf( "Class = %6d. Const = %6d. Unsed = %6d. Lits = %7d. All = %7d. Mem = %5.2f Mb\n", - Counter, Counter1, CounterX, nLits, nLits+Counter1, 1.0*p->nMemsMax/(1<<20) ); - if ( fVerbose ) - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - Caig_ManPrintOne( p, i, ++Counter ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i ) -{ - int Ent; - Vec_PtrClear( p->vSims ); - for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) - Vec_PtrPush( p->vSims, p->pSims + Ent ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i ) -{ - unsigned * pSim; - int Ent; - Vec_PtrClear( p->vSims ); - for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) - { - pSim = Caig_ManSimDeref( p, Ent ); - Vec_PtrPush( p->vSims, pSim + 1 ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords ) -{ - int w; - if ( (p0[0] & 1) == (p1[0] & 1) ) - { - for ( w = 0; w < nWords; w++ ) - if ( p0[w] != p1[w] ) - return 0; - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( p0[w] != ~p1[w] ) - return 0; - return 1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCompareConst( unsigned * p, int nWords ) -{ - int w; - if ( p[0] & 1 ) - { - for ( w = 0; w < nWords; w++ ) - if ( p[w] != ~0 ) - return 0; - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( p[w] != 0 ) - return 0; - return 1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass ) -{ - int * pNext, Repr, Ent, i; - assert( Vec_IntSize(vClass) > 0 ); - Vec_IntForEachEntry( vClass, Ent, i ) - { - if ( i == 0 ) - { - Repr = Ent; - p->pReprs[Ent] = -1; - pNext = p->pNexts + Ent; - } - else - { - p->pReprs[Ent] = Repr; - *pNext = Ent; - pNext = p->pNexts + Ent; - } - } - *pNext = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims ) -{ - unsigned * pSim0, * pSim1; - int Ent, c = 0, d = 0; - Vec_IntClear( p->vClassOld ); - Vec_IntClear( p->vClassNew ); - pSim0 = Vec_PtrEntry( vSims, c++ ); - Vec_IntPush( p->vClassOld, i ); - for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] ) - { - pSim1 = Vec_PtrEntry( vSims, c++ ); - if ( Caig_ManCompareEqual( pSim0, pSim1, p->nWords ) ) - Vec_IntPush( p->vClassOld, Ent ); - else - { - Vec_IntPush( p->vClassNew, Ent ); - Vec_PtrWriteEntry( vSims, d++, pSim1 ); - } - } -//if ( Vec_PtrSize(vSims) > 100 ) -//printf( "%d -> %d %d \n", Vec_PtrSize(vSims), Vec_IntSize(p->vClassOld), Vec_IntSize(p->vClassNew) ); - Vec_PtrShrink( vSims, d ); - if ( Vec_IntSize(p->vClassNew) == 0 ) - return 0; - Caig_ManClassCreate( p, p->vClassOld ); - Caig_ManClassCreate( p, p->vClassNew ); - if ( Vec_IntSize(p->vClassNew) > 1 ) - return 1 + Caig_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), vSims ); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize ) -{ - static int s_Primes[16] = { - 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, - 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; - unsigned uHash = 0; - int i; - if ( pSim[0] & 1 ) - for ( i = 0; i < nWords; i++ ) - uHash ^= ~pSim[i] * s_Primes[i & 0xf]; - else - for ( i = 0; i < nWords; i++ ) - uHash ^= pSim[i] * s_Primes[i & 0xf]; - return (int)(uHash % nTableSize); - -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManClassesCreate( Caig_Man_t * p ) -{ - int * pTable, nTableSize, i, Key; - nTableSize = Aig_PrimeCudd( 100 + p->nObjs / 10 ); - pTable = ABC_CALLOC( int, nTableSize ); - p->pReprs = ABC_ALLOC( int, p->nObjs ); - p->pNexts = ABC_CALLOC( int, p->nObjs ); - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] > 0 && p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - if ( Caig_ManCompareConst( p->pSims + i, 1 ) ) - { - p->pReprs[i] = 0; - continue; - } - Key = Caig_ManHashKey( p->pSims + i, 1, nTableSize ); - if ( pTable[Key] == 0 ) - p->pReprs[i] = -1; - else - { - p->pNexts[ pTable[Key] ] = i; - p->pReprs[i] = p->pReprs[ pTable[Key] ]; - if ( p->pReprs[i] == -1 ) - p->pReprs[i] = pTable[Key]; - } - pTable[Key] = i; - } - ABC_FREE( pTable ); -Caig_ManPrintClasses( p, 0 ); - // refine classes - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - { - Caig_ManCollectSimsSimple( p, i ); - Caig_ManClassRefineOne( p, i, p->vSims ); - } - // clean memory - memset( p->pSims, 0, sizeof(unsigned) * p->nObjs ); -Caig_ManPrintClasses( p, 0 ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManSimulateSimple( Caig_Man_t * p ) -{ - unsigned Res0, Res1; - int i; - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] == -1 ) // pi - { - p->pSims[i] = Aig_ManRandom( 0 ); - continue; - } - if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - Res0 = p->pSims[Cec_Lit2Var(p->pFans0[i])]; - Res1 = p->pSims[Cec_Lit2Var(p->pFans1[i])]; - p->pSims[i] = (Cec_LitIsCompl(p->pFans0[i]) ? ~Res0: Res0) & - (Cec_LitIsCompl(p->pFans1[i]) ? ~Res1: Res1); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined ) -{ - Vec_Int_t * vClasses; - int * pTable, nTableSize, i, Key, iNode; - unsigned * pSim; - if ( Vec_IntSize(vRefined) == 0 ) - return; - nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); - pTable = ABC_CALLOC( int, nTableSize ); - vClasses = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vRefined, iNode, i ) - { - pSim = Caig_ManSimRead( p, iNode ); - assert( !Caig_ManCompareConst( pSim + 1, p->nWords ) ); - Key = Caig_ManHashKey( pSim + 1, p->nWords, nTableSize ); - if ( pTable[Key] == 0 ) - { - assert( p->pReprs[iNode] == 0 ); - assert( p->pNexts[iNode] == 0 ); - p->pReprs[iNode] = -1; - Vec_IntPush( vClasses, iNode ); - } - else - { - p->pNexts[ pTable[Key] ] = iNode; - p->pReprs[iNode] = p->pReprs[ pTable[Key] ]; - if ( p->pReprs[iNode] == -1 ) - p->pReprs[iNode] = pTable[Key]; - assert( p->pReprs[iNode] > 0 ); - } - pTable[Key] = iNode; - } - ABC_FREE( pTable ); - // refine classes - Vec_IntForEachEntry( vClasses, iNode, i ) - { - if ( p->pNexts[iNode] == 0 ) - { - Caig_ManSimDeref( p, iNode ); - continue; - } - Caig_ManCollectSimsNormal( p, iNode ); - Caig_ManClassRefineOne( p, iNode, p->vSims ); - } - Vec_IntFree( vClasses ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters ) -{ - Vec_Ptr_t * vInfo; - Caig_Man_t * p; - int i; - Aig_ManRandom( 1 ); - p = Caig_ManCreate( pAig ); - p->nWords = 1; - Caig_ManSimulateSimple( p ); - Caig_ManClassesCreate( p ); - p->nWords = nWords; - for ( i = 0; i < nIters; i++ ) - { - p->nWords = i + 1; - Caig_ManSimMemRelink( p ); - p->nMemsMax = 0; - - vInfo = Vec_PtrAllocSimInfo( p->nPis, p->nWords ); - Aig_ManRandomInfo( vInfo, 0, p->nWords ); - Caig_ManSimulateRound( p, vInfo, NULL ); - Vec_PtrFree( vInfo ); -Caig_ManPrintClasses( p, 0 ); - } - - p->nWords = nWords; - Caig_ManSimMemRelink( p ); - p->nMemsMax = 0; - return p; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |