diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 6fddcac96b..fe8ce9dea9 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -30,6 +30,7 @@ #include #include #include +#include #include "misc/vec/vec.h" #include "misc/vec/vecWec.h" @@ -45,6 +46,35 @@ ABC_NAMESPACE_HEADER_START #define GIA_NONE 0x1FFFFFFF #define GIA_VOID 0x0FFFFFFF +// Multi-origin tracking: small-buffer optimization with overflow +#ifndef GIA_ORIGINS_INLINE +#define GIA_ORIGINS_INLINE 4 // number of inline origin slots (configurable at compile time) +#endif + +typedef union { + struct { + int origins[GIA_ORIGINS_INLINE]; // -1 = unused slot + } inl; + struct { + int sentinel; // INT_MIN marks overflow mode + int count; // number of origins in overflow array + int * overflow; // heap-allocated origin array + } ovf; +} Gia_OriginsEntry_t; + +#define GIA_ORIGINS_STRIDE ((int)(sizeof(Gia_OriginsEntry_t) / sizeof(int))) +#define GIA_ORIGINS_SENTINEL INT_MIN + +// Compile-time checks: inline slots must cover the overflow header +// (sentinel + count + pointer; minimum 4 ints on 64-bit), and must +// not exceed the hardcoded initial overflow capacity of 8. +#if GIA_ORIGINS_INLINE < 4 +# error "GIA_ORIGINS_INLINE must be >= 4 (overflow header needs sentinel+count+ptr, min 4 ints on 64-bit)" +#endif +#if GIA_ORIGINS_INLINE > 7 +# error "GIA_ORIGINS_INLINE must be <= 7 (initial overflow capacity is 8)" +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -190,6 +220,8 @@ struct Gia_Man_t_ Vec_Int_t * vIdsOrig; // original object IDs Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent Vec_Int_t * vEquLitIds; // original object IDs proved equivalent + Vec_Int_t * vOrigins; // per-object origin mapping (from "y" extension) + int nOriginsMax; // max origins per object (0 = unlimited) Vec_Int_t * vCofVars; // cofactoring variables Vec_Vec_t * vClockDoms; // clock domains Vec_Flt_t * vTiming; // arrival/required/slack @@ -462,6 +494,78 @@ static inline int Gia_ManIsConst0Lit( int iLit ) { return (iLit == static inline int Gia_ManIsConst1Lit( int iLit ) { return (iLit == 1); } static inline int Gia_ManIsConstLit( int iLit ) { return (iLit <= 1); } +// Multi-origin accessors +static inline Gia_OriginsEntry_t * Gia_ObjOriginsEntry( Gia_Man_t * p, int iObj ) +{ + return (Gia_OriginsEntry_t *)(Vec_IntArray(p->vOrigins) + iObj * GIA_ORIGINS_STRIDE); +} +static inline int Gia_ObjOriginsIsOverflow( Gia_OriginsEntry_t * e ) +{ + return e->inl.origins[0] == GIA_ORIGINS_SENTINEL; +} +static inline int Gia_ObjOriginsNum( Gia_Man_t * p, int iObj ) +{ + Gia_OriginsEntry_t * e; + int k; + if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) ) + return 0; + e = Gia_ObjOriginsEntry( p, iObj ); + if ( Gia_ObjOriginsIsOverflow(e) ) + return e->ovf.count; + for ( k = 0; k < GIA_ORIGINS_INLINE; k++ ) + if ( e->inl.origins[k] == -1 ) break; + return k; +} +static inline int Gia_ObjOriginsGet( Gia_Man_t * p, int iObj, int idx ) +{ + Gia_OriginsEntry_t * e; + if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) ) + return -1; + e = Gia_ObjOriginsEntry( p, iObj ); + if ( Gia_ObjOriginsIsOverflow(e) ) + return (idx < e->ovf.count) ? e->ovf.overflow[idx] : -1; + return (idx < GIA_ORIGINS_INLINE) ? e->inl.origins[idx] : -1; +} +// Backward compatible: get first/primary origin +static inline int Gia_ObjOrigin( Gia_Man_t * p, int iObj ) +{ + Gia_OriginsEntry_t * e; + if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) ) + return -1; + e = Gia_ObjOriginsEntry( p, iObj ); + if ( Gia_ObjOriginsIsOverflow(e) ) + return e->ovf.count > 0 ? e->ovf.overflow[0] : -1; + return e->inl.origins[0]; +} +// Set single origin (clears any existing, for initialization) +static inline void Gia_ObjSetOrigin( Gia_Man_t * p, int iObj, int iOrig ) +{ + Gia_OriginsEntry_t * e; + int k; + if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) ) + return; + e = Gia_ObjOriginsEntry( p, iObj ); + if ( Gia_ObjOriginsIsOverflow(e) && e->ovf.overflow ) + ABC_FREE( e->ovf.overflow ); + e->inl.origins[0] = iOrig; + for ( k = 1; k < GIA_ORIGINS_INLINE; k++ ) + e->inl.origins[k] = -1; +} +// Grow vOrigins to accommodate object iObj +static inline void Gia_ManOriginsGrow( Gia_Man_t * p, int iObj ) +{ + Vec_IntFillExtra( p->vOrigins, (iObj + 1) * GIA_ORIGINS_STRIDE, -1 ); +} +// Allocate vOrigins for nObjs objects (all entries initialized to -1) +static inline Vec_Int_t * Gia_ManOriginsAlloc( int nObjs ) +{ + return Vec_IntStartFull( nObjs * GIA_ORIGINS_STRIDE ); +} +// Iteration macro (caller must declare int _nOrig before use, or use nOrig variant) +#define Gia_ObjForEachOrigin( p, iObj, orig, idx ) \ + for ( idx = 0, _nOrig = Gia_ObjOriginsNum(p, iObj); \ + (idx < _nOrig) && ((orig = Gia_ObjOriginsGet(p, iObj, idx)), 1); idx++ ) + static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); } static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); } static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } @@ -1348,6 +1452,14 @@ extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p, int fRevFan extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ); extern Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres ); extern Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft ); +extern void Gia_ObjAddOrigin( Gia_Man_t * p, int iObj, int iOrig ); +extern void Gia_ObjUnionOrigins( Gia_Man_t * p, int iDst, Gia_Man_t * pSrc, int iSrc ); +extern void Gia_ManOriginsFreeOverflows( Gia_Man_t * p ); +extern void Gia_ManOriginsReset( Gia_Man_t * p ); +extern void Gia_ManOriginsDup( Gia_Man_t * pNew, Gia_Man_t * pOld ); +extern void Gia_ManOriginsDupVec( Gia_Man_t * pNew, Gia_Man_t * pOld, Vec_Int_t * vCopies ); +extern void Gia_ManOriginsAfterRoundTrip( Gia_Man_t * pNew, Gia_Man_t * pOld ); +extern void Gia_ManOriginsDupIf( Gia_Man_t * pNew, Gia_Man_t * p, void * pIfMan ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 07bab5fec2..70d19e351a 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -600,6 +600,7 @@ Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ) Aig_ManStop( pTemp ); pGia = Gia_ManFromAig( pNew ); Aig_ManStop( pNew ); + Gia_ManOriginsAfterRoundTrip( pGia, p ); Gia_ManTransferTiming( pGia, p ); return pGia; } @@ -658,6 +659,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars ) Gia_ManStop( pGia ); pGia = Gia_ManDup( p ); } + else + Gia_ManOriginsAfterRoundTrip( pGia, p ); Gia_ManTransferTiming( pGia, p ); return pGia; } diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index c37c3ea9e4..d3050beeca 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -947,7 +947,44 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi else if ( fVerbose ) printf( "Finished reading extension \"y\".\n" ); } else { - if ( fVerbose ) printf( "Cannot read extension \"y\" because AIG is rehashed. Use \"&r -s \".\n" ); + if ( fVerbose ) printf( "Skipped extension \"y\" for vEquLitIds (AIG is rehashed).\n" ); + } + // populate vOrigins using vNodes to map AIG→GIA object indices + // sentinel -2 at pData[0] distinguishes new format from old + if ( vNodes && nInts >= 1 && ((int *)pCur)[0] == -2 ) { + // new multi-origin format: sentinel, then [count, lit0, lit1, ...] per AIG object + int k, nAigObjs = Vec_IntSize(vNodes); + int * pData = (int *)pCur; + int pos = 1; // skip sentinel + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + for ( k = 0; k < nAigObjs && pos < nInts; k++ ) + { + int giaLit = Vec_IntEntry( vNodes, k ); + int giaObj = Abc_Lit2Var( giaLit ); + int nOrig = pData[pos++]; + int j; + for ( j = 0; j < nOrig && pos < nInts; j++, pos++ ) + { + int rawLit = pData[pos]; + if ( rawLit >= 0 && giaObj < Gia_ManObjNum(pNew) ) + Gia_ObjAddOrigin( pNew, giaObj, Abc_Lit2Var(rawLit) ); + } + } + if ( fVerbose ) printf( "Finished reading extension \"y\" (multi-origin).\n" ); + } + else if ( vNodes && nInts == Vec_IntSize(vNodes) ) { + // old single-origin format: one literal per AIG object + int k; + int * pData = (int *)pCur; + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + for ( k = 0; k < nInts; k++ ) + { + int giaLit = Vec_IntEntry( vNodes, k ); + int giaObj = Abc_Lit2Var( giaLit ); + int rawLit = pData[k]; + if ( rawLit >= 0 && giaObj < Gia_ManObjNum(pNew) ) + Gia_ObjSetOrigin( pNew, giaObj, Abc_Lit2Var(rawLit) ); + } } pCur += 4*nInts; } @@ -1836,8 +1873,30 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) ); fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile ); } - // write object classes - if ( p->vEquLitIds ) + // write object origins (vOrigins takes priority over vEquLitIds) + // New variable-length format: sentinel -2, then for each object [count, lit0, lit1, ...] + if ( p->vOrigins ) + { + int k, nObjs = Gia_ManObjNum(p); + Vec_Int_t * vData = Vec_IntAlloc( 1 + nObjs * 2 ); + assert( Vec_IntSize(p->vOrigins) >= nObjs * GIA_ORIGINS_STRIDE ); + Vec_IntPush( vData, -2 ); // sentinel distinguishes new format from old + for ( k = 0; k < nObjs; k++ ) + { + int nOrig = Gia_ObjOriginsNum( p, k ); + int idx, orig, _nOrig; + Vec_IntPush( vData, nOrig ); + Gia_ObjForEachOrigin( p, k, orig, idx ) + Vec_IntPush( vData, orig >= 0 ? 2 * orig : -1 ); + } + fprintf( pFile, "y" ); + Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(vData) ); + fwrite( Vec_IntArray(vData), 1, (size_t)4*Vec_IntSize(vData), pFile ); + if ( fVerbose ) printf( "Finished writing extension \"y\" (multi-origin, %d ints for %d objs).\n", + Vec_IntSize(vData), nObjs ); + Vec_IntFree( vData ); + } + else if ( p->vEquLitIds ) { fprintf( pFile, "y" ); Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) ); diff --git a/src/aig/gia/giaBalAig.c b/src/aig/gia/giaBalAig.c index 5603b4108b..9a132f8432 100644 --- a/src/aig/gia/giaBalAig.c +++ b/src/aig/gia/giaBalAig.c @@ -420,6 +420,7 @@ Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p, int fStrict ) } assert( !fStrict || Gia_ManObjNum(pNew) <= Gia_ManObjNum(p) ); Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); // perform cleanup pNew = Gia_ManCleanup( pTemp = pNew ); @@ -819,6 +820,7 @@ Gia_Man_t * Dam_ManMultiAig( Dam_Man_t * pMan ) } // assert( Gia_ManObjNum(pNew) <= Gia_ManObjNum(p) ); Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); // perform cleanup pNew = Gia_ManCleanup( pTemp = pNew ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index d1187cb241..d6fa79173a 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "gia.h" +#include "map/if/if.h" #include "misc/tim/tim.h" #include "misc/vec/vecWec.h" #include "proof/cec/cec.h" @@ -193,12 +194,294 @@ int Gia_ManDupOrderDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } +/**Function************************************************************* + + Synopsis [Adds an origin to an object with deduplication.] + + Description [May promote inline storage to heap-allocated overflow.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ObjAddOrigin( Gia_Man_t * p, int iObj, int iOrig ) +{ + Gia_OriginsEntry_t * e; + int k; + if ( iOrig < 0 || !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) ) + return; + e = Gia_ObjOriginsEntry( p, iObj ); + if ( Gia_ObjOriginsIsOverflow(e) ) + { + // cap check: skip if at user-specified limit + if ( p->nOriginsMax > 0 && e->ovf.count >= p->nOriginsMax ) + return; + // overflow mode: check for duplicate + for ( k = 0; k < e->ovf.count; k++ ) + if ( e->ovf.overflow[k] == iOrig ) return; + // geometric growth: double capacity when count is a power of 2 + if ( e->ovf.count >= 8 && (e->ovf.count & (e->ovf.count - 1)) == 0 ) + e->ovf.overflow = ABC_REALLOC( int, e->ovf.overflow, e->ovf.count * 2 ); + e->ovf.overflow[e->ovf.count++] = iOrig; + } + else + { + // inline mode: check for duplicate and find empty slot + for ( k = 0; k < GIA_ORIGINS_INLINE; k++ ) + { + if ( e->inl.origins[k] == iOrig ) return; + if ( e->inl.origins[k] == -1 ) + { + e->inl.origins[k] = iOrig; + return; + } + } + // inline buffer full: promote to overflow with 8-slot initial capacity + { + int * pOverflow = ABC_ALLOC( int, 8 ); + for ( k = 0; k < GIA_ORIGINS_INLINE; k++ ) + pOverflow[k] = e->inl.origins[k]; + pOverflow[GIA_ORIGINS_INLINE] = iOrig; + e->ovf.sentinel = GIA_ORIGINS_SENTINEL; + e->ovf.count = GIA_ORIGINS_INLINE + 1; + e->ovf.overflow = pOverflow; + } + } +} + +/**Function************************************************************* + + Synopsis [Unions all origins from src object into dst object.] + + Description [Iterates over all origins of iSrc in pSrc and adds each + to iDst in p, with deduplication. pSrc and p may be the same manager.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ObjUnionOrigins( Gia_Man_t * p, int iDst, Gia_Man_t * pSrc, int iSrc ) +{ + int idx, orig, _nOrig; + Gia_ObjForEachOrigin( pSrc, iSrc, orig, idx ) + Gia_ObjAddOrigin( p, iDst, orig ); +} + +/**Function************************************************************* + + Synopsis [Frees all overflow arrays in vOrigins.] + + Description [Walks every object's origins entry and frees the heap + array for entries in overflow mode. Must be called before freeing + the vOrigins Vec_Int_t itself.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManOriginsFreeOverflows( Gia_Man_t * p ) +{ + int i, nObjs; + Gia_OriginsEntry_t * e; + if ( !p->vOrigins ) + return; + nObjs = Vec_IntSize(p->vOrigins) / GIA_ORIGINS_STRIDE; + for ( i = 0; i < nObjs; i++ ) + { + e = Gia_ObjOriginsEntry( p, i ); + if ( Gia_ObjOriginsIsOverflow(e) && e->ovf.overflow ) + ABC_FREE( e->ovf.overflow ); + } +} + +/**Function************************************************************* + + Synopsis [Frees existing vOrigins (overflows + vec).] + + Description [Used before reallocation to prevent leaks.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManOriginsReset( Gia_Man_t * p ) +{ + if ( !p->vOrigins ) + return; + Gia_ManOriginsFreeOverflows( p ); + Vec_IntFreeP( &p->vOrigins ); +} + +/**Function************************************************************* + + Synopsis [Propagates origin mapping from old to new manager.] + + Description [Uses Value field of old objects to find corresponding + new objects. Copies full multi-origin entries.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManOriginsDup( Gia_Man_t * pNew, Gia_Man_t * pOld ) +{ + Gia_Obj_t * pObj; + int i; + if ( !pOld->vOrigins ) + return; + Gia_ManOriginsReset( pNew ); + pNew->nOriginsMax = pOld->nOriginsMax; + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + Gia_ManForEachObj( pOld, pObj, i ) + { + if ( i * GIA_ORIGINS_STRIDE >= Vec_IntSize(pOld->vOrigins) ) + break; + if ( (int)Gia_ObjValue(pObj) != -1 ) + { + int iNew = Abc_Lit2Var( Gia_ObjValue(pObj) ); + if ( iNew < Gia_ManObjNum(pNew) ) + Gia_ObjUnionOrigins( pNew, iNew, pOld, i ); + } + } +} + +/**Function************************************************************* + + Synopsis [Propagates origins using a copies vector.] + + Description [Like Gia_ManOriginsDup but uses an explicit vCopies + vector instead of the Value field. Entry i of vCopies is the literal + in pNew corresponding to old object i.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManOriginsDupVec( Gia_Man_t * pNew, Gia_Man_t * pOld, Vec_Int_t * vCopies ) +{ + int i, iLit; + if ( !pOld->vOrigins ) + return; + Gia_ManOriginsReset( pNew ); + pNew->nOriginsMax = pOld->nOriginsMax; + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + Vec_IntForEachEntry( vCopies, iLit, i ) + { + if ( iLit != -1 ) + { + int iNew = Abc_Lit2Var( iLit ); + if ( iNew < Gia_ManObjNum(pNew) && i * GIA_ORIGINS_STRIDE < Vec_IntSize(pOld->vOrigins) ) + Gia_ObjUnionOrigins( pNew, iNew, pOld, i ); + } + } +} + +/**Function************************************************************* + + Synopsis [Restores origins after GIA->AIG->GIA round-trip.] + + Description [CIs map 1:1 in order. CO drivers map 1:1 (output + correspondence preserved through optimization). Remaining AND nodes + get origins via top-down propagation from CO drivers through fanin + cones.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManOriginsAfterRoundTrip( Gia_Man_t * pNew, Gia_Man_t * pOld ) +{ + Gia_Obj_t * pObj; + int i; + if ( !pOld->vOrigins ) + return; + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pOld) ); + assert( Gia_ManCoNum(pNew) == Gia_ManCoNum(pOld) ); + Gia_ManOriginsReset( pNew ); + pNew->nOriginsMax = pOld->nOriginsMax; + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + // const0 + Gia_ObjUnionOrigins( pNew, 0, pOld, 0 ); + // CIs map 1:1 in order + Gia_ManForEachCi( pNew, pObj, i ) + { + int iNewObj = Gia_ObjId( pNew, pObj ); + int iOldCi = Gia_ObjId( pOld, Gia_ManCi(pOld, i) ); + Gia_ObjUnionOrigins( pNew, iNewObj, pOld, iOldCi ); + } + // CO drivers map 1:1 (output correspondence preserved through optimization) + Gia_ManForEachCo( pNew, pObj, i ) + { + int iNewDriver = Gia_ObjFaninId0p( pNew, pObj ); + Gia_Obj_t * pOldCo = Gia_ManCo( pOld, i ); + int iOldDriver = Gia_ObjFaninId0p( pOld, pOldCo ); + if ( iNewDriver > 0 ) + Gia_ObjUnionOrigins( pNew, iNewDriver, pOld, iOldDriver ); + } + // Top-down propagation: spread CO driver origins backward through fanin cones + for ( i = Gia_ManObjNum(pNew) - 1; i > 0; i-- ) + { + int f0, f1; + pObj = Gia_ManObj( pNew, i ); + if ( !Gia_ObjIsAnd(pObj) ) + continue; + if ( Gia_ObjOriginsNum(pNew, i) == 0 ) + continue; + f0 = Gia_ObjFaninId0(pObj, i); + f1 = Gia_ObjFaninId1(pObj, i); + if ( f0 > 0 ) + Gia_ObjUnionOrigins( pNew, f0, pNew, i ); + if ( f1 > 0 ) + Gia_ObjUnionOrigins( pNew, f1, pNew, i ); + } +} + +/**Function************************************************************* + + Synopsis [Propagates origins through IF mapper correspondence.] + + Description [IF objects 0..Gia_ManObjNum(p)-1 correspond 1:1 to + input GIA objects; iCopy gives the literal in the output GIA.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManOriginsDupIf( Gia_Man_t * pNew, Gia_Man_t * p, void * pIfManVoid ) +{ + If_Man_t * pIfMan = (If_Man_t *)pIfManVoid; + If_Obj_t * pIfObj = NULL; + int i; + if ( !p->vOrigins ) + return; + Gia_ManOriginsReset( pNew ); + pNew->nOriginsMax = p->nOriginsMax; + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + If_ManForEachObj( pIfMan, pIfObj, i ) + { + if ( i * GIA_ORIGINS_STRIDE < Vec_IntSize(p->vOrigins) && pIfObj->iCopy >= 0 ) + { + int iNewObj = Abc_Lit2Var( pIfObj->iCopy ); + if ( iNewObj < Gia_ManObjNum(pNew) ) + Gia_ObjUnionOrigins( pNew, iNewObj, p, i ); + } + } +} + /**Function************************************************************* Synopsis [Duplicates AIG while putting objects in the DFS order.] Description [] - + SideEffects [] SeeAlso [] @@ -221,6 +504,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ) pObj->Value = Gia_ManAppendCi(pNew); assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); Gia_ManDupRemapCis( pNew, p ); + Gia_ManOriginsDup( pNew, p ); Gia_ManDupRemapEquiv( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); return pNew; @@ -545,6 +829,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManOriginsDup( pNew, p ); Gia_ManDupRemapEquiv( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); assert( Gia_ManIsNormalized(pNew) ); @@ -778,6 +1063,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) else if ( Gia_ObjIsCo(pObj) ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); if ( p->pCexSeq ) pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); @@ -829,11 +1115,31 @@ Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p ) pNew->vConfigs2 = Vec_StrDup( p->vConfigs2 ); if ( p->pCellStr ) pNew->pCellStr = Abc_UtilStrsav( p->pCellStr ); + // copy origins if present (deep-copy overflow arrays) + pNew->nOriginsMax = p->nOriginsMax; + if ( p->vOrigins ) + { + int iObj, nObjs; + Gia_OriginsEntry_t * eSrc, * eDst; + Gia_ManOriginsReset( pNew ); + pNew->vOrigins = Vec_IntDup( p->vOrigins ); + nObjs = Vec_IntSize(p->vOrigins) / GIA_ORIGINS_STRIDE; + for ( iObj = 0; iObj < nObjs; iObj++ ) + { + eSrc = Gia_ObjOriginsEntry( p, iObj ); + if ( Gia_ObjOriginsIsOverflow(eSrc) && eSrc->ovf.overflow ) + { + eDst = Gia_ObjOriginsEntry( pNew, iObj ); + eDst->ovf.overflow = ABC_ALLOC( int, eSrc->ovf.count ); + memcpy( eDst->ovf.overflow, eSrc->ovf.overflow, sizeof(int) * eSrc->ovf.count ); + } + } + } // copy names if present if ( p->vNamesIn ) pNew->vNamesIn = Vec_PtrDupStr( p->vNamesIn ); if ( p->vNamesOut ) - pNew->vNamesOut = Vec_PtrDupStr( p->vNamesOut ); + pNew->vNamesOut = Vec_PtrDupStr( p->vNamesOut ); return pNew; } Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis ) @@ -1575,6 +1881,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(pSibl->Value); } } + Gia_ManOriginsDup( pNew, p ); return pNew; } @@ -1806,6 +2113,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew->nConstrs = p->nConstrs; if ( p->pCexSeq ) @@ -1874,6 +2182,7 @@ Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p ) Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManOriginsDup( pNew, p ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); @@ -3890,6 +4199,8 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ) Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) ); } Gia_ManHashStop( pNew ); + // propagate origins from the first (primary) AIG + Gia_ManOriginsDup( pNew, pGia0 ); // check the presence of dangling nodes nNodes = Gia_ManHasDangling( pNew ); //assert( nNodes == 0 ); @@ -3931,6 +4242,7 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ) Gia_ManForEachRi( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); // Gia_ManDupRemapEquiv( pNew, p ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew->nConstrs = nConstr; assert( Gia_ManIsNormalized(pNew) ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index e8ddc99131..96013df928 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -744,6 +744,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); return pNew; } @@ -2071,6 +2072,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); Gia_ManRemoveBadChoices( pNew ); //Gia_ManEquivPrintClasses( pNew, 0, 0 ); + Gia_ManOriginsDup( pNew, p ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); //Gia_ManEquivPrintClasses( pNew, 0, 0 ); diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 063cfd31ab..fc581149a1 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -491,6 +491,12 @@ int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 ) if ( *pPlace ) { p->nHashHit++; + // on hash hit, union input origins into existing node + if ( p->vOrigins && *pPlace * GIA_ORIGINS_STRIDE < Vec_IntSize(p->vOrigins) ) + { + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLit0) ); + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLit1) ); + } return Abc_Var2Lit( *pPlace, fCompl ); } p->nHashMiss++; @@ -503,6 +509,14 @@ int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 ) assert( *pPlace == 0 ); *pPlace = Abc_Lit2Var( iNode ); } + // propagate origins from both inputs into new node + if ( p->vOrigins ) + { + int iNew = *pPlace; + Gia_ManOriginsGrow( p, iNew ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLit0) ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLit1) ); + } return Abc_Var2Lit( *pPlace, fCompl ); } } @@ -546,6 +560,13 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 ) if ( *pPlace ) { p->nHashHit++; + // on hash hit, union input origins into existing node + if ( p->vOrigins && *pPlace * GIA_ORIGINS_STRIDE < Vec_IntSize(p->vOrigins) ) + { + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLit0) ); + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLit1) ); + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLitC) ); + } return Abc_Var2Lit( *pPlace, fCompl ); } p->nHashMiss++; @@ -558,6 +579,15 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 ) assert( *pPlace == 0 ); *pPlace = Abc_Lit2Var( iNode ); } + // propagate origins from all three inputs into new node + if ( p->vOrigins ) + { + int iNew = *pPlace; + Gia_ManOriginsGrow( p, iNew ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLit0) ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLit1) ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLitC) ); + } return Abc_Var2Lit( *pPlace, fCompl ); } } @@ -603,6 +633,12 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) if ( *pPlace ) { p->nHashHit++; + // on hash hit, union input origins into existing node + if ( p->vOrigins && *pPlace * GIA_ORIGINS_STRIDE < Vec_IntSize(p->vOrigins) ) + { + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLit0) ); + Gia_ObjUnionOrigins( p, *pPlace, p, Abc_Lit2Var(iLit1) ); + } return Abc_Var2Lit( *pPlace, 0 ); } p->nHashMiss++; @@ -615,6 +651,14 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) assert( *pPlace == 0 ); *pPlace = Abc_Lit2Var( iNode ); } + // propagate origins from both inputs into new node + if ( p->vOrigins ) + { + int iNew = *pPlace; + Gia_ManOriginsGrow( p, iNew ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLit0) ); + Gia_ObjUnionOrigins( p, iNew, p, Abc_Lit2Var(iLit1) ); + } return Abc_Var2Lit( *pPlace, 0 ); } } @@ -761,6 +805,7 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ) } Gia_ManHashStop( pNew ); pNew->fAddStrash = 0; + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); // printf( "Top gate is %s\n", Gia_ObjFaninC0(Gia_ManCo(pNew, 0))? "OR" : "AND" ); pNew = Gia_ManCleanup( pTemp = pNew ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index c2d8886c0a..77ceeb25ee 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -3065,6 +3065,8 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars ) pNew = Gia_ManFromIfAig( pIfMan ); else pNew = Gia_ManFromIfLogic( pIfMan ); + // propagate origin mapping from input GIA through IF mapper to output GIA + Gia_ManOriginsDupIf( pNew, p, pIfMan ); if ( p->vCiArrs || p->vCoReqs ) { If_Obj_t * pIfObj = NULL; @@ -3160,6 +3162,7 @@ Gia_Man_t * Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRati pIfMan = Gia_ManToIf( p, pPars ); If_ManPerformMapping( pIfMan ); pNew = Gia_ManFromIfAig( pIfMan ); + Gia_ManOriginsDupIf( pNew, p, pIfMan ); If_ManStop( pIfMan ); Gia_ManTransferTiming( pNew, p ); // transfer name @@ -3193,6 +3196,7 @@ Gia_Man_t * Gia_ManPerformDsdBalance( Gia_Man_t * p, int nLutSize, int nCutNum, If_DsdManAllocIsops( pIfMan->pIfDsdMan, pPars->nLutSize ); If_ManPerformMapping( pIfMan ); pNew = Gia_ManFromIfAig( pIfMan ); + Gia_ManOriginsDupIf( pNew, p, pIfMan ); If_ManStop( pIfMan ); Gia_ManTransferTiming( pNew, p ); // transfer name @@ -3298,6 +3302,7 @@ Gia_Man_t * Gia_ManDupHashMapping( Gia_Man_t * p ) Vec_IntPush( vMapping, Abc_Lit2Var(pObj->Value) ); } pNew->vMapping = vMapping; + Gia_ManOriginsDup( pNew, p ); return pNew; } @@ -3377,6 +3382,7 @@ Gia_Man_t * Gia_ManDupUnhashMapping( Gia_Man_t * p ) } Vec_IntFree( vMap ); pNew->vMapping = vMapping; + Gia_ManOriginsDup( pNew, p ); return pNew; } diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 205ab40801..e0711a288a 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -1511,10 +1511,11 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) if ( p->pPars->fGenCnf ) Jf_ManGenCnf( ABC_CONST(0xAAAAAAAAAAAAAAAA), iLit, vLeaves, vLits, vClas, vCover ); } + Gia_ManOriginsDupVec( pNew, p->pGia, vCopies ); Vec_IntFree( vCopies ); Vec_IntFree( vCover ); Vec_IntFree( vLeaves ); - // finish mapping + // finish mapping if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) ) Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) ); else @@ -1653,6 +1654,7 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p ) } if ( !p->pPars->fCutMin ) Gia_ObjComputeTruthTableStop( p->pGia ); + Gia_ManOriginsDupVec( pNew, p->pGia, vCopies ); Vec_IntFree( vCopies ); Vec_IntFree( vLeaves ); Vec_IntFree( vCover ); diff --git a/src/aig/gia/giaLf.c b/src/aig/gia/giaLf.c index 4f3e49f424..7d15a45d3d 100644 --- a/src/aig/gia/giaLf.c +++ b/src/aig/gia/giaLf.c @@ -1771,6 +1771,7 @@ Gia_Man_t * Lf_ManDeriveMappingCoarse( Lf_Man_t * p ) Vec_IntPush( pNew->vMapping, pCut->fMux7 ? -Abc_Lit2Var(pObj->Value) : Abc_Lit2Var(pObj->Value) ); } Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + Gia_ManOriginsDup( pNew, pGia ); assert( Vec_IntCap(pNew->vMapping) == 16 || Vec_IntSize(pNew->vMapping) == Vec_IntCap(pNew->vMapping) ); return pNew; } @@ -1909,10 +1910,11 @@ Gia_Man_t * Lf_ManDeriveMappingGia( Lf_Man_t * p ) iLit = Lf_ManDerivePart( p, pNew, vMapping, vMapping2, vCopies, pCut, vLeaves, vCover, pObj ); Vec_IntWriteEntry( vCopies, i, Abc_LitNotCond(iLit, Abc_LitIsCompl(pCut->iFunc)) ); } + Gia_ManOriginsDupVec( pNew, p->pGia, vCopies ); Vec_IntFree( vCopies ); Vec_IntFree( vCover ); Vec_IntFree( vLeaves ); - // finish mapping + // finish mapping if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) ) Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) ); else diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 889a49c0e2..6ee993fa02 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -107,6 +107,8 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vIdsOrig ); Vec_IntFreeP( &p->vIdsEquiv ); Vec_IntFreeP( &p->vEquLitIds ); + Gia_ManOriginsFreeOverflows( p ); + Vec_IntFreeP( &p->vOrigins ); Vec_IntFreeP( &p->vLutConfigs ); Vec_IntFreeP( &p->vEdgeDelay ); Vec_IntFreeP( &p->vEdgeDelayR ); diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index 6ad6b0039c..5330eac918 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -531,6 +531,25 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) if ( p->vRegInits ) pNew->vRegInits = Vec_IntDup( p->vRegInits ); pNew->nAnd2Delay = p->nAnd2Delay; + // propagate origins via MFS ID correspondence + if ( p->vOrigins ) + { + int iOldObj; + pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) ); + Vec_IntForEachEntry( vMfs2Old, iOldObj, i ) + { + if ( iOldObj >= 0 ) + { + int iNewLit = Vec_IntEntry( vMfs2Gia, i ); + if ( iNewLit >= 0 ) + { + int iNewObj = Abc_Lit2Var( iNewLit ); + if ( iNewObj < Gia_ManObjNum(pNew) && iOldObj * GIA_ORIGINS_STRIDE < Vec_IntSize(p->vOrigins) ) + Gia_ObjUnionOrigins( pNew, iNewObj, p, iOldObj ); + } + } + } + } // cleanup Vec_WecFree( vGroups ); diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c index ff542c3053..8eb2e761b9 100644 --- a/src/aig/gia/giaMuxes.c +++ b/src/aig/gia/giaMuxes.c @@ -140,6 +140,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit ) pNew->pSibls[Gia_ObjId(pNew, pObjNew)] = Gia_ObjId(pNew, pSiblNew); } Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); // perform cleanup pNew = Gia_ManCleanup( pTemp = pNew ); @@ -253,6 +254,7 @@ Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p, int fSkipBufs ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); // perform cleanup pNew = Gia_ManCleanup( pTemp = pNew ); diff --git a/src/aig/gia/giaScript.c b/src/aig/gia/giaScript.c index b52288a946..59d8791517 100644 --- a/src/aig/gia/giaScript.c +++ b/src/aig/gia/giaScript.c @@ -315,6 +315,7 @@ Gia_Man_t * Gia_ManDupFromBarBufs( Gia_Man_t * p ) Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Gia_ManOriginsDup( pNew, p ); return pNew; } Gia_Man_t * Gia_ManDupToBarBufs( Gia_Man_t * p, int nBarBufs ) @@ -357,6 +358,7 @@ Gia_Man_t * Gia_ManDupToBarBufs( Gia_Man_t * p, int nBarBufs ) assert( Gia_ManBufNum(pNew) == nBarBufs ); assert( Gia_ManCiNum(pNew) == nPiReal ); assert( Gia_ManCoNum(pNew) == nPoReal ); + Gia_ManOriginsDup( pNew, p ); return pNew; } @@ -396,6 +398,8 @@ Gia_Man_t * Gia_ManAigSynch2Choices( Gia_Man_t * pGia1, Gia_Man_t * pGia2, Gia_M // convert to GIA pGia = Gia_ManFromAigChoices( pMan ); Aig_ManStop( pMan ); + // recover origins from base variant (pGia1) via CI/CO correspondence + Gia_ManOriginsAfterRoundTrip( pGia, pGia1 ); return pGia; } Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * pInit, void * pPars0, int nLutSize, int nRelaxRatio ) diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c index d93ff2a605..d3e8a1407d 100644 --- a/src/aig/gia/giaSweep.c +++ b/src/aig/gia/giaSweep.c @@ -204,6 +204,7 @@ Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, int fSeq ) assert( Gia_ManCiNum(pNew) == Tim_ManPiNum((Tim_Man_t*)pNew->pManTime) + Gia_ManCoNum(pNew->pAigExtra) ); Vec_IntFree( vBoxesLeft ); pNew->nAnd2Delay = p->nAnd2Delay; + Gia_ManOriginsDup( pNew, p ); return pNew; } @@ -368,6 +369,7 @@ Gia_Man_t * Gia_ManFraigReduceGia( Gia_Man_t * p, int * pReprs ) else assert( 0 ); } Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); return pNew; } diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 5f13dcfa70..0ad60aac6a 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -186,6 +186,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p, int fHashMapping ) Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew->nConstrs = p->nConstrs; assert( Gia_ManIsNormalized(pNew) ); + Gia_ManOriginsDup( pNew, p ); Gia_ManDupRemapEquiv( pNew, p ); return pNew; } @@ -240,6 +241,7 @@ Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p ) Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew->nConstrs = p->nConstrs; assert( Gia_ManIsNormalized(pNew) ); + Gia_ManOriginsDup( pNew, p ); Gia_ManDupRemapEquiv( pNew, p ); return pNew; } @@ -420,6 +422,7 @@ Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p ) pObj->Value = 0; else assert( 0 ); } + Gia_ManOriginsDup( pNew, p ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); Vec_IntFree( vNodes ); return pNew; @@ -777,6 +780,7 @@ Gia_Man_t * Gia_ManDupMoveLast( Gia_Man_t * p, int iInsert, int nItems ) else assert( 0 ); } Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Gia_ManOriginsDup( pNew, p ); return pNew; } @@ -903,6 +907,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v assert( curCo == Gia_ManCoNum(p) ); Gia_ManSetRegNum( pNew, (fSeq && p->vRegClasses) ? Vec_IntSize(p->vRegClasses) : Gia_ManRegNum(p) ); Gia_ManHashStop( pNew ); + Gia_ManOriginsDup( pNew, p ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManCleanupRemap( p, pTemp ); Gia_ManStop( pTemp ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6cc8df18fc..47b464ff98 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -426,6 +426,8 @@ static int Abc_CommandAbc9WriteVer ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Write ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9WriteLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Origins ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9OriginsId ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Pms ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1269,6 +1271,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&write", Abc_CommandAbc9Write, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&wlut", Abc_CommandAbc9WriteLut, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&ps", Abc_CommandAbc9Ps, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&origins", Abc_CommandAbc9Origins, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&origins_id", Abc_CommandAbc9OriginsId, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&pfan", Abc_CommandAbc9PFan, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&pms", Abc_CommandAbc9Pms, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&psig", Abc_CommandAbc9PSig, 0 ); @@ -35540,6 +35544,186 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } +/**Function************************************************************* + + Synopsis [Prints multi-origin statistics.] + + Description [Shows how many objects have origins, total origin count, + average/max per node, overflow count, and a histogram. Origins are + populated either by reading an XAIGER file with a "y" extension + (normal abc9 flow) or by the &origins_id command (testing).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Origins( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pGia = pAbc->pGia; + int c, fSetCap = 0, nOriginsMax = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Mh" ) ) != EOF ) + { + switch ( c ) + { + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nOriginsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nOriginsMax < 0 ) + { + Abc_Print( -1, "The max origins value should be non-negative.\n" ); + goto usage; + } + fSetCap = 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Origins(): There is no AIG.\n" ); + return 0; + } + if ( fSetCap ) + { + pGia->nOriginsMax = nOriginsMax; + Abc_Print( 1, "Origins cap set to %d%s.\n", nOriginsMax, nOriginsMax ? "" : " (unlimited)" ); + return 0; + } + if ( pGia->vOrigins == NULL ) + { + Abc_Print( 1, "No origin tracking data.\n" ); + return 0; + } + { + int i, nObjs = Gia_ManObjNum(pGia); + int nEntries = 0, nOrigins = 0, nMaxOrigins = 0; + int nOverflow = 0; + int histogram[16]; + memset( histogram, 0, sizeof(histogram) ); + for ( i = 0; i < nObjs; i++ ) + { + int nOrig = Gia_ObjOriginsNum( pGia, i ); + if ( nOrig > 0 ) + { + nEntries++; + nOrigins += nOrig; + if ( nOrig > nMaxOrigins ) + nMaxOrigins = nOrig; + if ( nOrig < 16 ) + histogram[nOrig]++; + else + histogram[15]++; + if ( nOrig > GIA_ORIGINS_INLINE ) + nOverflow++; + } + } + Abc_Print( 1, "Origins: %d entries, %d total origins (%.2fx avg), max %d, overflow %d\n", + nEntries, nOrigins, + nEntries > 0 ? (double)nOrigins / nEntries : 0.0, + nMaxOrigins, nOverflow ); + Abc_Print( 1, " Histogram: " ); + for ( i = 1; i < 16; i++ ) + if ( histogram[i] > 0 ) + Abc_Print( 1, "%s%d=%d", i > 1 ? " " : "", i, histogram[i] ); + Abc_Print( 1, "\n" ); + } + return 0; + +usage: + Abc_Print( -2, "usage: &origins [-M num] [-h]\n" ); + Abc_Print( -2, "\t prints multi-origin tracking statistics\n" ); + Abc_Print( -2, "\t-M num : set max origins per object (0 = unlimited) [default = %d]\n", pGia ? pGia->nOriginsMax : 0 ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [Initialize identity origins for testing/debugging.] + + Description [Sets each AND node's origin to itself. This is a testing + convenience for exercising origin propagation in standalone ABC sessions. + In the normal abc9 flow, origins are supplied by Yosys via the XAIGER + "y" extension and this command is not needed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9OriginsId( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pGia = pAbc->pGia; + int c, nOriginsMax = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Mh" ) ) != EOF ) + { + switch ( c ) + { + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nOriginsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nOriginsMax < 0 ) + { + Abc_Print( -1, "The max origins value should be non-negative.\n" ); + goto usage; + } + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9OriginsId(): There is no AIG.\n" ); + return 0; + } + if ( pGia->vOrigins != NULL ) + { + Abc_Print( 1, "Origins already present (%d entries). Use without existing origins.\n", + Vec_IntSize(pGia->vOrigins) / GIA_ORIGINS_STRIDE ); + return 0; + } + { + int i, nObjs = Gia_ManObjNum(pGia); + Gia_Obj_t * pObj; + pGia->nOriginsMax = nOriginsMax; + pGia->vOrigins = Gia_ManOriginsAlloc( nObjs ); + Gia_ManForEachAnd( pGia, pObj, i ) + Gia_ObjSetOrigin( pGia, i, i ); + Abc_Print( 1, "Initialized identity origins for %d AND nodes", Gia_ManAndNum(pGia) ); + if ( nOriginsMax > 0 ) + Abc_Print( 1, " (max %d per node)", nOriginsMax ); + Abc_Print( 1, ".\n" ); + } + return 0; + +usage: + Abc_Print( -2, "usage: &origins_id [-M num] [-h]\n" ); + Abc_Print( -2, "\t sets identity origins for testing (each AND node -> itself)\n" ); + Abc_Print( -2, "\t in normal abc9 flow, origins come from XAIGER \"y\" extension\n" ); + Abc_Print( -2, "\t-M num : max origins per object, 0 = unlimited [default = %d]\n", nOriginsMax ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c index a49a253cd9..5bf81bdd96 100644 --- a/src/opt/dau/dauGia.c +++ b/src/opt/dau/dauGia.c @@ -562,6 +562,8 @@ void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes ) assert( iLev == 1 + Abc_MaxInt(iLev0, iLev1) ); } */ + // propagate origins + Gia_ManOriginsDup( pNew, p ); // perform cleanup pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 0496b2e49b..a8a8f563ae 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -714,6 +714,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Gia_ManOriginsDup( pNew, p ); return pNew; }