diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-16 17:04:01 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-16 17:04:01 -0800 |
commit | d671adbb86b241a71e15bcd67831b267d0de6abf (patch) | |
tree | bab3c4ab785fcbef40e27ddeb90ec5b1b679b8ca /src/opt | |
parent | a0052e22b43ff9d0125ca8e71f96589226e44e42 (diff) | |
download | abc-d671adbb86b241a71e15bcd67831b267d0de6abf.tar.gz abc-d671adbb86b241a71e15bcd67831b267d0de6abf.tar.bz2 abc-d671adbb86b241a71e15bcd67831b267d0de6abf.zip |
DSD manager.
Diffstat (limited to 'src/opt')
-rw-r--r-- | src/opt/dau/dauTree.c | 239 |
1 files changed, 194 insertions, 45 deletions
diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index 1c11b6e2..2a817f04 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -93,18 +93,20 @@ static inline Dss_Obj_t * Dss_Lit2Obj( Dss_Man_t * p, int iLit ) static inline Dss_Obj_t * Dss_ObjFanin( Dss_Man_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_ManObj(p, Abc_Lit2Var(pObj->pFans[i])); } static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]); } -#define Dss_NtkForEachNode( p, pObj, i ) \ +#define Dss_NtkForEachNode( p, pObj, i ) \ Vec_PtrForEachEntryStart( Dss_Obj_t *, p->vObjs, pObj, i, p->nVars + 1 ) -#define Dss_ObjForEachFaninNtk( p, pObj, pFanin, i ) \ +#define Dss_ObjForEachFaninNtk( p, pObj, pFanin, i ) \ for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFaninNtk(p, pObj, i)); i++ ) -#define Dss_ObjForEachChildNtk( p, pObj, pFanin, i ) \ +#define Dss_ObjForEachChildNtk( p, pObj, pFanin, i ) \ for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChildNtk(p, pObj, i)); i++ ) -#define Dss_ManForEachObjVec( vLits, p, pObj, i ) \ +#define Dss_ManForEachObj( p, pObj, i ) \ + Vec_PtrForEachEntry( Dss_Obj_t *, p->vObjs, pObj, i ) +#define Dss_ManForEachObjVec( vLits, p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(p, Vec_IntEntry(vLits,i))); i++ ) -#define Dss_ObjForEachFanin( p, pObj, pFanin, i ) \ +#define Dss_ObjForEachFanin( p, pObj, pFanin, i ) \ for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFanin(p, pObj, i)); i++ ) -#define Dss_ObjForEachChild( p, pObj, pFanin, i ) \ +#define Dss_ObjForEachChild( p, pObj, pFanin, i ) \ for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(p, pObj, i)); i++ ) @@ -490,14 +492,22 @@ Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits ) { Dss_Obj_t * pObj, * pFanin, * pPrev = NULL; int i, Entry; + // check structural canonicity + assert( Type != DAU_DSD_MUX || Vec_IntSize(vFaninLits) == 3 ); + assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 0)) ); + assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 1)) || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 2)) ); // check that leaves are in good order + if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR ) Dss_ManForEachObjVec( vFaninLits, p, pFanin, i ) { + assert( Type != DAU_DSD_AND || Abc_LitIsCompl(Vec_IntEntry(vFaninLits, i)) || Dss_ObjType(pFanin) != DAU_DSD_AND ); + assert( Type != DAU_DSD_XOR || Dss_ObjType(pFanin) != DAU_DSD_XOR ); assert( pPrev == NULL || Dss_ObjCompare(p, pPrev, pFanin) <= 0 ); pPrev = pFanin; } // create new node pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), 0 ); + assert( pObj->nSupp == 0 ); Vec_IntForEachEntry( vFaninLits, Entry, i ) { pObj->pFans[i] = Entry; @@ -591,6 +601,46 @@ void Dss_ManFree( Dss_Man_t * p ) ABC_FREE( p->pBins ); ABC_FREE( p ); } +void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) +{ + char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'}; + char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'}; + Dss_Obj_t * pFanin; + int i; + assert( !Dss_IsComplement(pObj) ); + if ( pObj->Type == DAU_DSD_CONST0 ) + { printf( "0" ); return; } + if ( pObj->Type == DAU_DSD_VAR ) + { printf( "%c", 'a' + pObj->iVar ); return; } + printf( "%c", OpenType[pObj->Type] ); + Dss_ObjForEachFanin( p, pObj, pFanin, i ) + { + printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" ); + Dss_ManPrint_rec( p, pFanin ); + } + printf( "%c", CloseType[pObj->Type] ); +} +void Dss_ManPrintOne( Dss_Man_t * p, Dss_Obj_t * pObj ) +{ + printf( "%6d : ", Dss_ObjId(pObj) ); + printf( "%2d ", pObj->nSupp ); + Dss_ManPrint_rec( p, pObj ); + printf( "\n" ); +} +void Dss_ManPrintAll( Dss_Man_t * p ) +{ + Dss_Obj_t * pObj; + int i, nSuppMax = 0; + printf( "DSD manager contains %d objects:\n", Vec_PtrSize(p->vObjs) ); + Dss_ManForEachObj( p, pObj, i ) + { + if ( (int)pObj->nSupp < nSuppMax ) + continue; + Dss_ManPrintOne( p, pObj ); + nSuppMax = Abc_MaxInt( nSuppMax, pObj->nSupp ); + } + printf( "\n" ); +} /**Function************************************************************* @@ -604,13 +654,15 @@ void Dss_ManFree( Dss_Man_t * p ) SeeAlso [] ***********************************************************************/ -Dss_Obj_t * Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) +Dss_Obj_t * Dss_ManShiftTree_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) { Vec_Int_t * vFaninLits; - Dss_Obj_t * pFanin, * pObjNew; - int i; + Dss_Obj_t * pMirror, * pFanin, * pObjNew; + int i, nSupp = Shift; assert( !Dss_IsComplement(pObj) ); assert( pObj->Mirror == pObj->Id ); + if ( Shift == 0 ) + return pObj; if ( pObj->Type == DAU_DSD_VAR ) { assert( (int)pObj->iVar + Shift < p->nVars ); @@ -620,8 +672,11 @@ Dss_Obj_t * Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) vFaninLits = Vec_IntAlloc( 10 ); Dss_ObjForEachFanin( p, pObj, pFanin, i ) { - pFanin = Dss_ManShiftTree( p, pFanin, Shift ); + pMirror = Dss_ManObj( p, pFanin->Mirror ); + pFanin = Dss_ManShiftTree_rec( p, pMirror, nSupp ); Vec_IntPush( vFaninLits, Abc_Var2Lit(pFanin->Id, Dss_ObjFaninC(pObj, i)) ); + assert( pFanin->nSupp > 0 ); + nSupp += pFanin->nSupp; } // create new graph pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, vFaninLits ); @@ -629,6 +684,20 @@ Dss_Obj_t * Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) Vec_IntFree( vFaninLits ); return pObjNew; } +void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec_Int_t * vLeaves ) +{ + int i, nSupp = 0; + Vec_IntClear( vLeaves ); + for ( i = 0; i < nChildren; i++ ) + { + Dss_Obj_t * pMirror = Dss_ManObj( p, Dss_Regular(pChildren[i])->Mirror ); + Dss_Obj_t * pFanin = Dss_ManShiftTree_rec( p, pMirror, nSupp ); + assert( !Dss_IsComplement(pFanin) ); + Vec_IntPush( vLeaves, Abc_Var2Lit(pFanin->Id, Dss_IsComplement(pChildren[i])) ); + assert( pFanin->nSupp > 0 ); + nSupp += pFanin->nSupp; + } +} /**Function************************************************************* @@ -644,7 +713,7 @@ Dss_Obj_t * Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPerm ) { Dss_Obj_t * pChildren[DAU_MAX_VAR]; - Dss_Obj_t * pObj, * pFanin, * pChild, * pMirror; + Dss_Obj_t * pObj, * pChild; int i, k, nChildren = 0, fCompl = 0, nSupp = 0; if ( Type == DAU_DSD_AND ) @@ -701,17 +770,7 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPe else assert( 0 ); // shift subgraphs - nSupp = 0; - Vec_IntClear( p->vLeaves ); - for ( i = 0; i < nChildren; i++ ) - { - pMirror = Dss_ManObj( p, Dss_Regular(pChildren[i])->Mirror ); - pFanin = Dss_ManShiftTree( p, pMirror, nSupp ); - assert( !Dss_IsComplement(pFanin) ); - assert( pFanin->nSupp > 0 ); - nSupp += pFanin->nSupp; - Vec_IntPush( p->vLeaves, Abc_Var2Lit(pFanin->Id, Dss_IsComplement(pChildren[i])) ); - } + Dss_ManShiftTree( p, pChildren, nChildren, p->vLeaves ); // create new graph pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves ); pObj->Mirror = pObj->Id; @@ -729,6 +788,46 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPe SeeAlso [] ***********************************************************************/ +int Dss_ObjCheckTransparent( Dss_Man_t * p, Dss_Obj_t * pObj ) +{ + Dss_Obj_t * pFanin; + int i; + if ( pObj->Type == DAU_DSD_VAR ) + return 1; + if ( pObj->Type == DAU_DSD_AND ) + return 0; + if ( pObj->Type == DAU_DSD_XOR ) + { + Dss_ObjForEachFanin( p, pObj, pFanin, i ) + if ( Dss_ObjCheckTransparent( p, pFanin ) ) + return 1; + return 0; + } + if ( pObj->Type == DAU_DSD_MUX ) + { + pFanin = Dss_ObjFanin( p, pObj, 1 ); + if ( !Dss_ObjCheckTransparent(p, pFanin) ) + return 0; + pFanin = Dss_ObjFanin( p, pObj, 2 ); + if ( !Dss_ObjCheckTransparent(p, pFanin) ) + return 0; + return 1; + } + assert( pObj->Type == DAU_DSD_PRIME ); + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Dau_DsdTest() { int nVars = 8; @@ -756,9 +855,9 @@ void Dau_DsdTest() ***********************************************************************/ void Dau_DsdTest_() { - int nVars = 8; + int nVars = 6; Vec_Vec_t * vFuncs = Vec_VecStart( nVars+1 ); - Vec_Int_t * vOne, * vTwo, * vThree; + Vec_Int_t * vOne, * vTwo, * vThree, * vRes; Dss_Man_t * p; int pEntries[3]; int e0, e1, e2, iLit; @@ -774,6 +873,7 @@ void Dau_DsdTest_() // enumerate for ( s = 2; s <= nVars; s++ ) { + vRes = Vec_VecEntryInt( vFuncs, s ); for ( i = 1; i < s; i++ ) for ( k = i; k < s; k++ ) if ( i + k == s ) @@ -783,44 +883,93 @@ void Dau_DsdTest_() Vec_IntForEachEntry( vOne, pEntries[0], e0 ) Vec_IntForEachEntry( vTwo, pEntries[1], e1 ) { - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); - Vec_VecPushInt( vFuncs, s, iLit ); + int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[0])) ); + int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[1])) ); - pEntries[0] = Abc_LitNot( pEntries[0] ); iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); - Vec_VecPushInt( vFuncs, s, iLit ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); - pEntries[1] = Abc_LitNot( pEntries[1] ); - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); - Vec_VecPushInt( vFuncs, s, iLit ); + if ( fAddInv0 ) + { + pEntries[0] = Abc_LitNot( pEntries[0] ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + pEntries[0] = Abc_LitNot( pEntries[0] ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); + } - pEntries[0] = Abc_LitNot( pEntries[0] ); - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); - Vec_VecPushInt( vFuncs, s, iLit ); + if ( fAddInv1 ) + { + pEntries[1] = Abc_LitNot( pEntries[1] ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + pEntries[1] = Abc_LitNot( pEntries[1] ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); + } + + if ( fAddInv0 && fAddInv1 ) + { + pEntries[0] = Abc_LitNot( pEntries[0] ); + pEntries[1] = Abc_LitNot( pEntries[1] ); + iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL ); + pEntries[0] = Abc_LitNot( pEntries[0] ); + pEntries[1] = Abc_LitNot( pEntries[1] ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); + } - pEntries[1] = Abc_LitNot( pEntries[1] ); iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL ); - Vec_VecPushInt( vFuncs, s, iLit ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); } } for ( i = 1; i < s; i++ ) - for ( k = i; k < s; k++ ) - for ( j = i; j < s; j++ ) + for ( k = 1; k < s; k++ ) + for ( j = 1; j < s; j++ ) if ( i + k + j == s ) { - vOne = Vec_VecEntryInt( vFuncs, i ); - vTwo = Vec_VecEntryInt( vFuncs, k ); + vOne = Vec_VecEntryInt( vFuncs, i ); + vTwo = Vec_VecEntryInt( vFuncs, k ); vThree = Vec_VecEntryInt( vFuncs, j ); - Vec_IntForEachEntry( vOne, pEntries[0], e0 ) - Vec_IntForEachEntry( vTwo, pEntries[1], e1 ) - Vec_IntForEachEntry( vTwo, pEntries[2], e2 ) + Vec_IntForEachEntry( vOne, pEntries[0], e0 ) + Vec_IntForEachEntry( vTwo, pEntries[1], e1 ) + Vec_IntForEachEntry( vThree, pEntries[2], e2 ) { - iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 3, NULL ); - Vec_VecPushInt( vFuncs, s, iLit ); + int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[0])) ); + int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[1])) ); + int fAddInv2 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[2])) ); + + if ( !fAddInv0 && k > j ) + continue; + + iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); + + if ( fAddInv1 ) + { + pEntries[1] = Abc_LitNot( pEntries[1] ); + iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL ); + pEntries[1] = Abc_LitNot( pEntries[1] ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); + } + + if ( fAddInv2 ) + { + pEntries[2] = Abc_LitNot( pEntries[2] ); + iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL ); + pEntries[2] = Abc_LitNot( pEntries[2] ); + assert( !Abc_LitIsCompl(iLit) ); + Vec_IntPush( vRes, iLit ); + } } } + Vec_IntUniqify( vRes ); } + Dss_ManPrintAll( p ); Dss_ManFree( p ); Vec_VecFree( vFuncs ); |