Skip to content

Add per-object origin tracking (vOrigins) to Gia_Man_t #487

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
robtaylor wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Add per-object origin tracking (vOrigins) to Gia_Man_t #487

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e261ac1
Add per-object origin tracking (vOrigins) to Gia_Man_t
robtaylor Feb 28, 2026
ace3e2f
Propagate vOrigins through all ABC9 engines
robtaylor Mar 5, 2026
a213928
Fix vOrigins bounds checks for grown GIA objects
robtaylor Mar 6, 2026
8ccd01a
Add defensive bounds check to Gia_ObjSetOrigin, propagate vOrigins in…
robtaylor Mar 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions src/aig/gia/gia.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,6 +190,7 @@ 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)
Vec_Int_t * vCofVars; // cofactoring variables
Vec_Vec_t * vClockDoms; // clock domains
Vec_Flt_t * vTiming; // arrival/required/slack
Expand Down Expand Up @@ -462,6 +463,9 @@ 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); }

static inline int Gia_ObjOrigin( Gia_Man_t * p, int iObj ) { return (p->vOrigins && iObj < Vec_IntSize(p->vOrigins)) ? Vec_IntEntry(p->vOrigins, iObj) : -1; }
static inline void Gia_ObjSetOrigin( Gia_Man_t * p, int iObj, int iOrig ) { if (p->vOrigins && iObj < Vec_IntSize(p->vOrigins)) Vec_IntWriteEntry(p->vOrigins, iObj, iOrig); }

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)); }
Expand Down Expand Up @@ -1348,6 +1352,9 @@ 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_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 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 );
Expand Down
3 changes: 3 additions & 0 deletions src/aig/gia/giaAig.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down Expand Up @@ -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;
}
Expand Down
36 changes: 33 additions & 3 deletions src/aig/gia/giaAiger.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -947,7 +947,21 @@ 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 <file.aig>\".\n" );
if ( fVerbose ) printf( "Skipped extension \"y\" for vEquLitIds (AIG is rehashed).\n" );
}
// populate vOrigins using vNodes to map AIG→GIA object indices
if ( nInts == Vec_IntSize(vNodes) ) {
int k;
int * pData = (int *)pCur;
pNew->vOrigins = Vec_IntStartFull( 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) )
Vec_IntWriteEntry( pNew->vOrigins, giaObj, Abc_Lit2Var(rawLit) );
}
}
pCur += 4*nInts;
}
Expand Down Expand Up @@ -1836,8 +1850,24 @@ 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)
if ( p->vOrigins )
{
int k, nObjs = Gia_ManObjNum(p);
Vec_Int_t * vLits = Vec_IntStart( nObjs );
assert( Vec_IntSize(p->vOrigins) == nObjs );
for ( k = 0; k < nObjs; k++ )
{
int orig = Vec_IntEntry(p->vOrigins, k);
Vec_IntWriteEntry( vLits, k, orig >= 0 ? 2 * orig : -1 );
}
fprintf( pFile, "y" );
Gia_FileWriteBufferSize( pFile, 4*nObjs );
fwrite( Vec_IntArray(vLits), 1, (size_t)4*nObjs, pFile );
Vec_IntFree( vLits );
if ( fVerbose ) printf( "Finished writing extension \"y\" (from origins).\n" );
}
else if ( p->vEquLitIds )
{
fprintf( pFile, "y" );
Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
Expand Down
2 changes: 2 additions & 0 deletions src/aig/gia/giaBalAig.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
Expand Down Expand Up @@ -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 );
Expand Down
133 changes: 131 additions & 2 deletions src/aig/gia/giaDup.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,12 +193,130 @@ 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 [Propagates origin mapping from old to new manager.]

Description [Uses Value field of old objects to find corresponding new objects.]

SideEffects []

SeeAlso []

***********************************************************************/
void Gia_ManOriginsDup( Gia_Man_t * pNew, Gia_Man_t * pOld )
{
Gia_Obj_t * pObj;
int i;
if ( !pOld->vOrigins )
return;
pNew->vOrigins = Vec_IntStartFull( Gia_ManObjNum(pNew) );
Gia_ManForEachObj( pOld, pObj, i )
{
if ( i >= Vec_IntSize(pOld->vOrigins) )
break;
if ( (int)Gia_ObjValue(pObj) != -1 )
{
int iNew = Abc_Lit2Var( Gia_ObjValue(pObj) );
if ( iNew < Gia_ManObjNum(pNew) )
Vec_IntWriteEntry( pNew->vOrigins, iNew,
Vec_IntEntry(pOld->vOrigins, 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. Note: shared nodes between multiple CO cones get the origin
of whichever CO driver is visited first (non-deterministic but
acceptable for best-effort source attribution).]

SideEffects []

SeeAlso []

***********************************************************************/
void Gia_ManOriginsDupVec( Gia_Man_t * pNew, Gia_Man_t * pOld, Vec_Int_t * vCopies )
{
int i, iLit;
if ( !pOld->vOrigins )
return;
pNew->vOrigins = Vec_IntStartFull( Gia_ManObjNum(pNew) );
Vec_IntForEachEntry( vCopies, iLit, i )
{
if ( iLit != -1 )
{
int iNew = Abc_Lit2Var( iLit );
if ( iNew < Gia_ManObjNum(pNew) && i < Vec_IntSize(pOld->vOrigins) )
Vec_IntWriteEntry( pNew->vOrigins, iNew,
Vec_IntEntry(pOld->vOrigins, i) );
}
}
}

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) );
pNew->vOrigins = Vec_IntStartFull( Gia_ManObjNum(pNew) );
// const0
if ( Vec_IntSize(pOld->vOrigins) > 0 )
Vec_IntWriteEntry( pNew->vOrigins, 0, Vec_IntEntry(pOld->vOrigins, 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) );
if ( iOldCi < Vec_IntSize(pOld->vOrigins) )
Vec_IntWriteEntry( pNew->vOrigins, iNewObj,
Vec_IntEntry(pOld->vOrigins, 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 && iOldDriver < Vec_IntSize(pOld->vOrigins) &&
Vec_IntEntry(pNew->vOrigins, iNewDriver) == -1 )
Vec_IntWriteEntry( pNew->vOrigins, iNewDriver,
Vec_IntEntry(pOld->vOrigins, iOldDriver) );
}
// Top-down propagation: spread CO driver origins backward through fanin cones
// Walk AND nodes in reverse topological order (high to low ID)
for ( i = Gia_ManObjNum(pNew) - 1; i > 0; i-- )
{
int f0, f1, orig;
pObj = Gia_ManObj( pNew, i );
if ( !Gia_ObjIsAnd(pObj) )
continue;
orig = Vec_IntEntry( pNew->vOrigins, i );
if ( orig < 0 )
continue;
f0 = Gia_ObjFaninId0(pObj, i);
f1 = Gia_ObjFaninId1(pObj, i);
if ( f0 > 0 && Vec_IntEntry(pNew->vOrigins, f0) == -1 )
Vec_IntWriteEntry( pNew->vOrigins, f0, orig );
if ( f1 > 0 && Vec_IntEntry(pNew->vOrigins, f1) == -1 )
Vec_IntWriteEntry( pNew->vOrigins, f1, orig );
}
}

/**Function*************************************************************

Synopsis [Duplicates AIG while putting objects in the DFS order.]

Description []

SideEffects []

SeeAlso []
Expand All @@ -221,6 +339,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;
Expand Down Expand Up @@ -545,6 +664,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) );
Expand Down Expand Up @@ -778,6 +898,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) );
Expand Down Expand Up @@ -829,11 +950,14 @@ 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
if ( p->vOrigins )
pNew->vOrigins = Vec_IntDup( p->vOrigins );
// 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 )
Expand Down Expand Up @@ -1575,6 +1699,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;
}

Expand Down Expand Up @@ -1806,6 +1931,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 )
Expand Down Expand Up @@ -1874,6 +2000,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) );
Expand Down Expand Up @@ -3890,6 +4017,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 );
Expand Down
2 changes: 2 additions & 0 deletions src/aig/gia/giaEquiv.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down Expand Up @@ -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 );
Expand Down
37 changes: 37 additions & 0 deletions src/aig/gia/giaHash.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -503,6 +503,17 @@ int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
assert( *pPlace == 0 );
*pPlace = Abc_Lit2Var( iNode );
}
// propagate origin from parent with lower valid origin ID
if ( p->vOrigins )
{
int iNew = *pPlace;
int o0 = Gia_ObjOrigin(p, Abc_Lit2Var(iLit0));
int o1 = Gia_ObjOrigin(p, Abc_Lit2Var(iLit1));
int orig = (o0 >= 0 && (o1 < 0 || o0 <= o1)) ? o0 : o1;
while ( Vec_IntSize(p->vOrigins) <= iNew )
Vec_IntPush( p->vOrigins, -1 );
Vec_IntWriteEntry( p->vOrigins, iNew, orig );
}
return Abc_Var2Lit( *pPlace, fCompl );
}
}
Expand Down Expand Up @@ -558,6 +569,19 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
assert( *pPlace == 0 );
*pPlace = Abc_Lit2Var( iNode );
}
// propagate origin from parent with lower valid origin ID
if ( p->vOrigins )
{
int iNew = *pPlace;
int o0 = Gia_ObjOrigin(p, Abc_Lit2Var(iLit0));
int o1 = Gia_ObjOrigin(p, Abc_Lit2Var(iLit1));
int oC = Gia_ObjOrigin(p, Abc_Lit2Var(iLitC));
int orig = (o0 >= 0 && (o1 < 0 || o0 <= o1)) ? o0 : o1;
if ( oC >= 0 && (orig < 0 || oC <= orig) ) orig = oC;
while ( Vec_IntSize(p->vOrigins) <= iNew )
Vec_IntPush( p->vOrigins, -1 );
Vec_IntWriteEntry( p->vOrigins, iNew, orig );
}
return Abc_Var2Lit( *pPlace, fCompl );
}
}
Expand Down Expand Up @@ -615,6 +639,18 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
assert( *pPlace == 0 );
*pPlace = Abc_Lit2Var( iNode );
}
// propagate origin from parent with lower valid origin ID
if ( p->vOrigins )
{
int iNew = *pPlace;
int o0 = Gia_ObjOrigin(p, Abc_Lit2Var(iLit0));
int o1 = Gia_ObjOrigin(p, Abc_Lit2Var(iLit1));
int orig = (o0 >= 0 && (o1 < 0 || o0 <= o1)) ? o0 : o1;
// grow vOrigins if needed
while ( Vec_IntSize(p->vOrigins) <= iNew )
Vec_IntPush( p->vOrigins, -1 );
Vec_IntWriteEntry( p->vOrigins, iNew, orig );
}
return Abc_Var2Lit( *pPlace, 0 );
}
}
Expand Down Expand Up @@ -761,6 +797,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 );
Expand Down
Loading
Loading