Skip to content

A
abc
Commit fec988f6 by Alan Mishchenko
Options

Renamed Aig_ObjPioNum to be Aig_ObjCioId.

parent c46c957a
Showing with 146 additions and 146 deletions
src/aig/aig/aig.h
...@@ -71,7 +71,7 @@ struct Aig_Obj_t_ // 9 words ...@@ -71,7 +71,7 @@ struct Aig_Obj_t_ // 9 words
{ {
union { union {
Aig_Obj_t * pNext; // strashing table Aig_Obj_t * pNext; // strashing table
int PioNum; // the number of PI/PO int CioId; // 0-based number of CI/CO
}; };
Aig_Obj_t * pFanin0; // fanin Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin Aig_Obj_t * pFanin1; // fanin
...@@ -268,7 +268,6 @@ static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_ ...@@ -268,7 +268,6 @@ static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_
static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; } static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; }
static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; }
static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; } static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; }
static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; } static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; }
static inline int Aig_ObjIsCi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI; } static inline int Aig_ObjIsCi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI; }
...@@ -281,6 +280,8 @@ static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj- ...@@ -281,6 +280,8 @@ static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj-
static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; } static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; } static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; }
static inline int Aig_ObjIsCand( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI || pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; } static inline int Aig_ObjIsCand( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI || pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjCioId( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return pObj->CioId; }
static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; }
static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; } static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; }
static inline void Aig_ObjSetMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; } static inline void Aig_ObjSetMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; }
...@@ -327,7 +328,6 @@ static inline void Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig ...@@ -327,7 +328,6 @@ static inline void Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig
static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; } static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; }
static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; } static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; }
static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); }
static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(ABC_PTRINT_T)pObj->pNext; }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{ {
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
...@@ -658,8 +658,8 @@ extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ); ...@@ -658,8 +658,8 @@ extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
extern void Aig_ManDump( Aig_Man_t * p ); extern void Aig_ManDump( Aig_Man_t * p );
extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ); extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ); extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
extern void Aig_ManSetPioNumbers( Aig_Man_t * p ); extern void Aig_ManSetCioIds( Aig_Man_t * p );
extern void Aig_ManCleanPioNumbers( Aig_Man_t * p ); extern void Aig_ManCleanCioIds( Aig_Man_t * p );
extern int Aig_ManChoiceNum( Aig_Man_t * p ); extern int Aig_ManChoiceNum( Aig_Man_t * p );
extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix ); extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
extern unsigned Aig_ManRandom( int fReset ); extern unsigned Aig_ManRandom( int fReset );
......
src/aig/aig/aigDfs.c
...@@ -47,7 +47,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) ...@@ -47,7 +47,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
{ {
Aig_Obj_t * pObj, * pNext; Aig_Obj_t * pObj, * pNext;
int i, k, iBox, iTerm1, nTerms; int i, k, iBox, iTerm1, nTerms;
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
Aig_ManIncrementTravId( p ); Aig_ManIncrementTravId( p );
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
{ {
...@@ -79,7 +79,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) ...@@ -79,7 +79,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
{ {
if ( p->pManTime ) if ( p->pManTime )
{ {
iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
if ( iBox >= 0 ) // this is not a true PI if ( iBox >= 0 ) // this is not a true PI
{ {
iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox ); iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
...@@ -87,7 +87,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) ...@@ -87,7 +87,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
for ( k = 0; k < nTerms; k++ ) for ( k = 0; k < nTerms; k++ )
{ {
pNext = Aig_ManCo( p, iTerm1 + k ); pNext = Aig_ManCo( p, iTerm1 + k );
assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pNext) ) == iBox );
if ( !Aig_ObjIsTravIdCurrent(p,pNext) ) if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
{ {
printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id ); printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
...@@ -101,7 +101,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) ...@@ -101,7 +101,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
assert( 0 ); assert( 0 );
Aig_ObjSetTravIdCurrent( p, pObj ); Aig_ObjSetTravIdCurrent( p, pObj );
} }
Aig_ManCleanPioNumbers( p ); Aig_ManCleanCioIds( p );
return 1; return 1;
} }
...@@ -505,7 +505,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -505,7 +505,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{ {
if ( p->pManTime ) if ( p->pManTime )
{ {
iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
if ( iBox >= 0 ) // this is not a true PI if ( iBox >= 0 ) // this is not a true PI
{ {
iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox ); iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
...@@ -572,7 +572,7 @@ int Aig_ManChoiceLevel( Aig_Man_t * p ) ...@@ -572,7 +572,7 @@ int Aig_ManChoiceLevel( Aig_Man_t * p )
int i, LevelMax = 0; int i, LevelMax = 0;
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
Aig_ObjSetLevel( pObj, 0 ); Aig_ObjSetLevel( pObj, 0 );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
Aig_ManIncrementTravId( p ); Aig_ManIncrementTravId( p );
Aig_ManForEachCo( p, pObj, i ) Aig_ManForEachCo( p, pObj, i )
{ {
...@@ -587,7 +587,7 @@ int Aig_ManChoiceLevel( Aig_Man_t * p ) ...@@ -587,7 +587,7 @@ int Aig_ManChoiceLevel( Aig_Man_t * p )
if ( LevelMax < Aig_ObjLevel(pObj) ) if ( LevelMax < Aig_ObjLevel(pObj) )
LevelMax = Aig_ObjLevel(pObj); LevelMax = Aig_ObjLevel(pObj);
} }
Aig_ManCleanPioNumbers( p ); Aig_ManCleanCioIds( p );
// Aig_ManForEachNode( p, pObj, i ) // Aig_ManForEachNode( p, pObj, i )
// assert( Aig_ObjLevel(pObj) > 0 ); // assert( Aig_ObjLevel(pObj) > 0 );
return LevelMax; return LevelMax;
......
src/aig/aig/aigDup.c
...@@ -679,16 +679,16 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder ) ...@@ -679,16 +679,16 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder )
int i; int i;
assert( Aig_ManCiNum(p) == Aig_ManCiNum(pOrder) ); assert( Aig_ManCiNum(p) == Aig_ManCiNum(pOrder) );
assert( Aig_ManCoNum(p) == Aig_ManCoNum(pOrder) ); assert( Aig_ManCoNum(p) == Aig_ManCoNum(pOrder) );
Aig_ManSetPioNumbers( pOrder ); Aig_ManSetCioIds( pOrder );
vPios = Vec_PtrAlloc( Aig_ManCiNum(p) + Aig_ManCoNum(p) ); vPios = Vec_PtrAlloc( Aig_ManCiNum(p) + Aig_ManCoNum(p) );
Aig_ManForEachObj( pOrder, pObj, i ) Aig_ManForEachObj( pOrder, pObj, i )
{ {
if ( Aig_ObjIsCi(pObj) ) if ( Aig_ObjIsCi(pObj) )
Vec_PtrPush( vPios, Aig_ManCi(p, Aig_ObjPioNum(pObj)) ); Vec_PtrPush( vPios, Aig_ManCi(p, Aig_ObjCioId(pObj)) );
else if ( Aig_ObjIsCo(pObj) ) else if ( Aig_ObjIsCo(pObj) )
Vec_PtrPush( vPios, Aig_ManCo(p, Aig_ObjPioNum(pObj)) ); Vec_PtrPush( vPios, Aig_ManCo(p, Aig_ObjCioId(pObj)) );
} }
Aig_ManCleanPioNumbers( pOrder ); Aig_ManCleanCioIds( pOrder );
return vPios; return vPios;
} }
......
src/aig/aig/aigJust.c
...@@ -114,7 +114,7 @@ int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Ve ...@@ -114,7 +114,7 @@ int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Ve
// if ( Aig_ObjId(pNode) % 1000 == 0 ) // if ( Aig_ObjId(pNode) % 1000 == 0 )
// Value ^= 1; // Value ^= 1;
if ( vSuppLits ) if ( vSuppLits )
Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
return 1; return 1;
} }
assert( Aig_ObjIsNode(pNode) ); assert( Aig_ObjIsNode(pNode) );
......
src/aig/aig/aigMan.c
...@@ -455,7 +455,7 @@ void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs ) ...@@ -455,7 +455,7 @@ void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs )
p->nRegs = nRegs; p->nRegs = nRegs;
p->nTruePis = Aig_ManCiNum(p) - nRegs; p->nTruePis = Aig_ManCiNum(p) - nRegs;
p->nTruePos = Aig_ManCoNum(p) - nRegs; p->nTruePos = Aig_ManCoNum(p) - nRegs;
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/aig/aig/aigPart.c
...@@ -1133,7 +1133,7 @@ void Aig_ManSupportNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vSupp ...@@ -1133,7 +1133,7 @@ void Aig_ManSupportNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vSupp
Aig_ObjSetTravIdCurrent(p, pObj); Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsCi(pObj) ) if ( Aig_ObjIsCi(pObj) )
{ {
Vec_IntPush( vSupport, Aig_ObjPioNum(pObj) ); Vec_IntPush( vSupport, Aig_ObjCioId(pObj) );
return; return;
} }
Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(pObj), vSupport ); Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(pObj), vSupport );
...@@ -1156,7 +1156,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts ) ...@@ -1156,7 +1156,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts )
Vec_Ptr_t * vPartSupps; Vec_Ptr_t * vPartSupps;
Vec_Int_t * vPart, * vSupport; Vec_Int_t * vPart, * vSupport;
int i, k, iOut; int i, k, iOut;
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) ); vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) );
Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
{ {
...@@ -1168,7 +1168,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts ) ...@@ -1168,7 +1168,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts )
// Vec_IntSort( vSupport, 0 ); // Vec_IntSort( vSupport, 0 );
Vec_PtrPush( vPartSupps, vSupport ); Vec_PtrPush( vPartSupps, vSupport );
} }
Aig_ManCleanPioNumbers( p ); Aig_ManCleanCioIds( p );
return vPartSupps; return vPartSupps;
} }
...@@ -1392,7 +1392,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM ...@@ -1392,7 +1392,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
// set the PI numbers // set the PI numbers
Aig_ManSetPioNumbers( pAig ); Aig_ManSetCioIds( pAig );
// create the total fraiged AIG // create the total fraiged AIG
Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
...@@ -1425,7 +1425,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM ...@@ -1425,7 +1425,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
Vec_VecFree( (Vec_Vec_t *)vParts ); Vec_VecFree( (Vec_Vec_t *)vParts );
// clear the PI numbers // clear the PI numbers
Aig_ManCleanPioNumbers( pAig ); Aig_ManCleanCioIds( pAig );
// derive the result of choicing // derive the result of choicing
return Aig_ManDupRepr( pAig, 0 ); return Aig_ManDupRepr( pAig, 0 );
......
src/aig/aig/aigScl.c
...@@ -77,15 +77,15 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) ...@@ -77,15 +77,15 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
pObj->pData = Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) ); pObj->pData = Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped ) if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped )
{ {
Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObj) ); Vec_IntPush( pNew->vFlopReprs, Aig_ObjCioId(pObj) );
if ( Aig_ObjIsConst1( Aig_Regular(pObjMapped) ) ) if ( Aig_ObjIsConst1( Aig_Regular(pObjMapped) ) )
Vec_IntPush( pNew->vFlopReprs, -1 ); Vec_IntPush( pNew->vFlopReprs, -1 );
else else
{ {
assert( !Aig_IsComplement(pObjMapped) ); assert( !Aig_IsComplement(pObjMapped) );
assert( Aig_ObjIsCi(pObjMapped) ); assert( Aig_ObjIsCi(pObjMapped) );
assert( Aig_ObjPioNum(pObj) != Aig_ObjPioNum(pObjMapped) ); assert( Aig_ObjCioId(pObj) != Aig_ObjCioId(pObjMapped) );
Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObjMapped) ); Vec_IntPush( pNew->vFlopReprs, Aig_ObjCioId(pObjMapped) );
} }
} }
} }
...@@ -236,7 +236,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) ...@@ -236,7 +236,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
Vec_PtrFree( vNodes ); Vec_PtrFree( vNodes );
p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p); p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p); p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
// remove dangling nodes // remove dangling nodes
return Aig_ManCleanup( p ); return Aig_ManCleanup( p );
} }
......
src/aig/aig/aigUtil.c
...@@ -799,16 +799,16 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec ...@@ -799,16 +799,16 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec
// write nodes // write nodes
if ( pConst1 ) if ( pConst1 )
fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData ); fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{ {
fprintf( pFile, ".names" ); fprintf( pFile, ".names" );
if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) ) if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin0(pObj))) ); fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
else else
fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData ); fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) ) if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) )
fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin1(pObj))) ); fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) );
else else
fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData ); fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
fprintf( pFile, " n%0*d\n", nDigits, pObj->iData ); fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
...@@ -819,16 +819,16 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec ...@@ -819,16 +819,16 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec
{ {
fprintf( pFile, ".names" ); fprintf( pFile, ".names" );
if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) ) if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin0(pObj))) ); fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
else else
fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData ); fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
if ( vPoNames ) if ( vPoNames )
fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjPioNum(pObj)) ); fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) );
else else
fprintf( pFile, " n%0*d\n", nDigits, pObj->iData ); fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) ); fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
} }
Aig_ManCleanPioNumbers( p ); Aig_ManCleanCioIds( p );
fprintf( pFile, ".end\n\n" ); fprintf( pFile, ".end\n\n" );
fclose( pFile ); fclose( pFile );
Vec_PtrFree( vNodes ); Vec_PtrFree( vNodes );
...@@ -962,14 +962,14 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ) ...@@ -962,14 +962,14 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Aig_ManSetPioNumbers( Aig_Man_t * p ) void Aig_ManSetCioIds( Aig_Man_t * p )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
Aig_ManForEachCi( p, pObj, i ) Aig_ManForEachCi( p, pObj, i )
pObj->PioNum = i; pObj->CioId = i;
Aig_ManForEachCo( p, pObj, i ) Aig_ManForEachCo( p, pObj, i )
pObj->PioNum = i; pObj->CioId = i;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -983,7 +983,7 @@ void Aig_ManSetPioNumbers( Aig_Man_t * p ) ...@@ -983,7 +983,7 @@ void Aig_ManSetPioNumbers( Aig_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Aig_ManCleanPioNumbers( Aig_Man_t * p ) void Aig_ManCleanCioIds( Aig_Man_t * p )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
......
src/aig/saig/saig.h
...@@ -104,13 +104,13 @@ static inline int Saig_ManConstrNum( Aig_Man_t * p ) { ...@@ -104,13 +104,13 @@ static inline int Saig_ManConstrNum( Aig_Man_t * p ) {
static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+i); } static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+i); }
static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+i); } static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+i); }
static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPiNum(p); } static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) < Saig_ManPiNum(p); }
static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); } static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) < Saig_ManPoNum(p); }
static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); } static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPiNum(p); }
static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); } static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPoNum(p); }
static inline Aig_Obj_t * Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPiNum(p)); } static inline Aig_Obj_t * Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+Aig_ObjCioId(pObj)-Saig_ManPiNum(p)); }
static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPoNum(p)); } static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+Aig_ObjCioId(pObj)-Saig_ManPoNum(p)); }
static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjPioNum(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p); else assert(0); return -1; } static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPoNum(p); else assert(0); return -1; }
// iterator over the primary inputs/outputs // iterator over the primary inputs/outputs
#define Saig_ManForEachPi( p, pObj, i ) \ #define Saig_ManForEachPi( p, pObj, i ) \
......
src/aig/saig/saigAbsCba.c
...@@ -268,7 +268,7 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr ...@@ -268,7 +268,7 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr
return; return;
if ( Aig_ObjIsCi(pObj) ) if ( Aig_ObjIsCi(pObj) )
{ {
Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
return; return;
} }
assert( Aig_ObjIsNode(pObj) ); assert( Aig_ObjIsNode(pObj) );
...@@ -460,15 +460,15 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI ...@@ -460,15 +460,15 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
pObj->pData = Aig_ManConst1(pFrames); pObj->pData = Aig_ManConst1(pFrames);
else if ( Saig_ObjIsPi(pAig, pObj) ) else if ( Saig_ObjIsPi(pAig, pObj) )
{ {
if ( Aig_ObjPioNum(pObj) < nInputs ) if ( Aig_ObjCioId(pObj) < nInputs )
{ {
int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
} }
else else
{ {
pObj->pData = Aig_ObjCreateCi( pFrames ); pObj->pData = Aig_ObjCreateCi( pFrames );
Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) ); Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
Vec_IntPush( *pvMapPiF2A, f ); Vec_IntPush( *pvMapPiF2A, f );
} }
} }
...@@ -569,7 +569,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p ) ...@@ -569,7 +569,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p )
continue; continue;
pObjLi = Aig_ManObj( p->pAig, ObjId ); pObjLi = Aig_ManObj( p->pAig, ObjId );
assert( Saig_ObjIsLi(p->pAig, pObjLi) ); assert( Saig_ObjIsLi(p->pAig, pObjLi) );
Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjPioNum(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) ); Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjCioId(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) );
} }
} }
// print statistics // print statistics
......
src/aig/saig/saigAbsPba.c
...@@ -122,7 +122,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec ...@@ -122,7 +122,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec
pObj->pData = Aig_ObjChild0Copy(pObj); pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Saig_ObjIsPi(pAig, pObj) ) else if ( Saig_ObjIsPi(pAig, pObj) )
{ {
Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManCiNum(pFrames) ); Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjCioId(pObj), Aig_ManCiNum(pFrames) );
pObj->pData = Aig_ObjCreateCi( pFrames ); pObj->pData = Aig_ObjCreateCi( pFrames );
} }
else if ( Aig_ObjIsConst1(pObj) ) else if ( Aig_ObjIsConst1(pObj) )
...@@ -144,7 +144,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec ...@@ -144,7 +144,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec
{ {
if ( Saig_ObjIsLi(pAig, pObj) ) if ( Saig_ObjIsLi(pAig, pObj) )
{ {
int iFlopNum = Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig); int iFlopNum = Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig);
assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) ); assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) );
Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData ); Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData );
} }
......
src/aig/saig/saigAbsStart.c
...@@ -250,7 +250,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) ...@@ -250,7 +250,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
assert( Aig_ManRegNum(p) > 0 ); assert( Aig_ManRegNum(p) > 0 );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
printf( "Performing counter-example-based refinement.\n" ); printf( "Performing counter-example-based refinement.\n" );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
vFlops = Vec_IntStartNatural( 1 ); vFlops = Vec_IntStartNatural( 1 );
/* /*
iFlop = Saig_ManFindFirstFlop( p ); iFlop = Saig_ManFindFirstFlop( p );
......
src/aig/saig/saigBmc3.c
...@@ -697,7 +697,7 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int ...@@ -697,7 +697,7 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int
Vec_IntPush( p->vVisited, iFrame ); Vec_IntPush( p->vVisited, iFrame );
} }
else if ( iLit != ~0 && Saig_ObjIsPi(p->pAig, pObj) ) // save PI SAT var num else if ( iLit != ~0 && Saig_ObjIsPi(p->pAig, pObj) ) // save PI SAT var num
Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjPioNum(pObj), lit_var(iLit) ); Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjCioId(pObj), lit_var(iLit) );
return iLit; return iLit;
} }
...@@ -1051,7 +1051,7 @@ void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract ) ...@@ -1051,7 +1051,7 @@ void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract )
if ( i < nPisAbstract ) if ( i < nPisAbstract )
{ {
pObj->fMarkA = 1; pObj->fMarkA = 1;
// printf( "%d=%d ", Aig_ObjPioNum(pObj), Aig_ObjRefs(pObj) ); // printf( "%d=%d ", Aig_ObjCioId(pObj), Aig_ObjRefs(pObj) );
} }
} }
// printf( "\n" ); // printf( "\n" );
......
src/aig/saig/saigCexMin.c
...@@ -279,7 +279,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p ...@@ -279,7 +279,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p
{ {
assert( Aig_ObjIsCi(pObj) ); assert( Aig_ObjIsCi(pObj) );
if ( Saig_ObjIsPi(pAig, pObj) ) if ( Saig_ObjIsPi(pAig, pObj) )
Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) ); Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
else if ( f == 0 ) else if ( f == 0 )
Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) ); Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
else else
...@@ -333,7 +333,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC ...@@ -333,7 +333,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
{ {
assert( Aig_ObjIsCi(pObj) ); assert( Aig_ObjIsCi(pObj) );
if ( Saig_ObjIsPi(pAig, pObj) ) if ( Saig_ObjIsPi(pAig, pObj) )
Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) ); Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
else if ( f == 0 ) else if ( f == 0 )
Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) ); Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
else else
...@@ -369,7 +369,7 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t ...@@ -369,7 +369,7 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t
if ( Aig_ObjIsCi(pObj) ) if ( Aig_ObjIsCi(pObj) )
{ {
if ( fPiReason && Saig_ObjIsPi(p, pObj) ) if ( fPiReason && Saig_ObjIsPi(p, pObj) )
Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjPioNum(pObj), !Abc_LitIsCompl(pObj->iData) ) ); Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjCioId(pObj), !Abc_LitIsCompl(pObj->iData) ) );
else if ( !fPiReason && Saig_ObjIsLo(p, pObj) ) else if ( !fPiReason && Saig_ObjIsLo(p, pObj) )
Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) ); Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) );
return; return;
......
src/aig/saig/saigCone.c
...@@ -53,7 +53,7 @@ void Saig_ManSupport_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp ) ...@@ -53,7 +53,7 @@ void Saig_ManSupport_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
{ {
if ( Saig_ObjIsLo(p,pObj) ) if ( Saig_ObjIsLo(p,pObj) )
{ {
pObj = Saig_ManLi( p, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); pObj = Saig_ManLi( p, Aig_ObjCioId(pObj)-Saig_ManPiNum(p) );
Vec_PtrPush( vSupp, pObj ); Vec_PtrPush( vSupp, pObj );
} }
return; return;
...@@ -111,7 +111,7 @@ void Saig_ManPrintConeOne( Aig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -111,7 +111,7 @@ void Saig_ManPrintConeOne( Aig_Man_t * p, Aig_Obj_t * pObj )
// get the current support // get the current support
vCur = Saig_ManSupport( p, vPrev ); vCur = Saig_ManSupport( p, vPrev );
Vec_PtrClear( vPrev ); Vec_PtrClear( vPrev );
printf( " PO %3d ", Aig_ObjPioNum(pObj) ); printf( " PO %3d ", Aig_ObjCioId(pObj) );
// continue computing supports as long as there are now nodes // continue computing supports as long as there are now nodes
vTotal = Vec_PtrAlloc( 100 ); vTotal = Vec_PtrAlloc( 100 );
for ( s = 0; ; s++ ) for ( s = 0; ; s++ )
...@@ -167,7 +167,7 @@ void Saig_ManPrintCones( Aig_Man_t * p ) ...@@ -167,7 +167,7 @@ void Saig_ManPrintCones( Aig_Man_t * p )
printf( "- c is the number of registers in b that are new (appear for the first time)\n" ); printf( "- c is the number of registers in b that are new (appear for the first time)\n" );
printf( "- d is the number of registers in b in common with the previous time-frame\n" ); printf( "- d is the number of registers in b in common with the previous time-frame\n" );
printf( "- e is the number of registers in b in common with other time-frames\n" ); printf( "- e is the number of registers in b in common with other time-frames\n" );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
Saig_ManForEachPo( p, pObj, i ) Saig_ManForEachPo( p, pObj, i )
Saig_ManPrintConeOne( p, pObj ); Saig_ManPrintConeOne( p, pObj );
} }
......
src/aig/saig/saigHaig.c
...@@ -109,7 +109,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) ...@@ -109,7 +109,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
Saig_ManForEachLo( pHaig, pObj, i ) Saig_ManForEachLo( pHaig, pObj, i )
pObj->pData = Aig_ObjCreateCi( pFrames ); pObj->pData = Aig_ObjCreateCi( pFrames );
// add timeframes // add timeframes
Aig_ManSetPioNumbers( pHaig ); Aig_ManSetCioIds( pHaig );
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < nFrames; f++ )
{ {
// create primary inputs // create primary inputs
...@@ -558,7 +558,7 @@ Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig ) ...@@ -558,7 +558,7 @@ Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter; Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
int Id1, Id2, i; int Id1, Id2, i;
// remove regular POs // remove regular POs
Aig_ManSetPioNumbers( pHaig ); Aig_ManSetCioIds( pHaig );
vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) ); vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
Aig_ManForEachCo( pHaig, pObj, i ) Aig_ManForEachCo( pHaig, pObj, i )
{ {
......
src/aig/saig/saigInd.c
...@@ -154,7 +154,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, ...@@ -154,7 +154,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0; int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
assert( fUnique == 0 || fUniqueAll == 0 ); assert( fUnique == 0 || fUniqueAll == 0 );
assert( Saig_ManPoNum(p) == 1 ); assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
// start the top by including the PO // start the top by including the PO
vBot = Vec_PtrAlloc( 100 ); vBot = Vec_PtrAlloc( 100 );
...@@ -201,9 +201,9 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, ...@@ -201,9 +201,9 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
pObjPiCopy = (Aig_Obj_t *)pObjPi->pData; pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
assert( Aig_ObjIsCi(pObjPiCopy) ); assert( Aig_ObjIsCi(pObjPiCopy) );
if ( Saig_ObjIsPi(p, pObjPi) ) if ( Saig_ObjIsPi(p, pObjPi) )
Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
else if ( Saig_ObjIsLo(p, pObjPi) ) else if ( Saig_ObjIsLo(p, pObjPi) )
Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
else assert( 0 ); else assert( 0 );
} }
} }
...@@ -261,7 +261,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, ...@@ -261,7 +261,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) ); Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) );
Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] ); Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] );
iReg = pObjPi->PioNum - Saig_ManPiNum(p); iReg = pObjPi->CioId - Saig_ManPiNum(p);
assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
Vec_IntWriteEntry( vState, nOldSize+iReg, pCnfPart->pVarNums[pObjPiCopy->Id] ); Vec_IntWriteEntry( vState, nOldSize+iReg, pCnfPart->pVarNums[pObjPiCopy->Id] );
} }
......
src/aig/saig/saigIoa.c
...@@ -49,13 +49,13 @@ char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -49,13 +49,13 @@ char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) ); sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
else if ( Saig_ObjIsPi(p, pObj) ) else if ( Saig_ObjIsPi(p, pObj) )
sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) ); sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) );
else if ( Saig_ObjIsPo(p, pObj) ) else if ( Saig_ObjIsPo(p, pObj) )
sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) ); sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) );
else if ( Saig_ObjIsLo(p, pObj) ) else if ( Saig_ObjIsLo(p, pObj) )
sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) ); sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) );
else if ( Saig_ObjIsLi(p, pObj) ) else if ( Saig_ObjIsLi(p, pObj) )
sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) ); sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) );
else else
assert( 0 ); assert( 0 );
return Buffer; return Buffer;
...@@ -82,7 +82,7 @@ void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) ...@@ -82,7 +82,7 @@ void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
return; return;
} }
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
// write input file // write input file
pFile = fopen( pFileName, "w" ); pFile = fopen( pFileName, "w" );
if ( pFile == NULL ) if ( pFile == NULL )
......
src/aig/saig/saigIso.c
...@@ -65,7 +65,7 @@ Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis ) ...@@ -65,7 +65,7 @@ Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis )
} }
Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareByData ); Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareByData );
Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
Vec_IntPush( vPermCos, Aig_ObjPioNum(pObj) ); Vec_IntPush( vPermCos, Aig_ObjCioId(pObj) );
Vec_PtrFree( vRoots ); Vec_PtrFree( vRoots );
} }
// add flop outputs // add flop outputs
......
src/aig/saig/saigIsoSlow.c
...@@ -929,7 +929,7 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose ) ...@@ -929,7 +929,7 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
{ {
if ( fOnlyCis ) if ( fOnlyCis )
printf( " %d", Aig_ObjPioNum( Iso_AigObj(p, pTemp) ) ); printf( " %d", Aig_ObjCioId( Iso_AigObj(p, pTemp) ) );
else else
{ {
Aig_Obj_t * pObj = Iso_AigObj(p, pTemp); Aig_Obj_t * pObj = Iso_AigObj(p, pTemp);
...@@ -1108,7 +1108,7 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) ...@@ -1108,7 +1108,7 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
Aig_ManForEachCi( p->pAig, pObj, i ) Aig_ManForEachCi( p->pAig, pObj, i )
{ {
assert( pObj->iData > 0 ); assert( pObj->iData > 0 );
if ( Aig_ObjPioNum(pObj) >= Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop if ( Aig_ObjCioId(pObj) >= Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop
Vec_PtrPush( p->vTemp2, pObj ); Vec_PtrPush( p->vTemp2, pObj );
else // PI else // PI
Vec_PtrPush( p->vTemp1, pObj ); Vec_PtrPush( p->vTemp1, pObj );
...@@ -1119,9 +1119,9 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) ...@@ -1119,9 +1119,9 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
// create the result // create the result
vRes = Vec_IntAlloc( Aig_ManCiNum(p->pAig) ); vRes = Vec_IntAlloc( Aig_ManCiNum(p->pAig) );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i ) Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i )
Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); Vec_IntPush( vRes, Aig_ObjCioId(pObj) );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i ) Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i )
Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); Vec_IntPush( vRes, Aig_ObjCioId(pObj) );
return vRes; return vRes;
} }
......
src/aig/saig/saigMiter.c
...@@ -906,7 +906,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) ...@@ -906,7 +906,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
Aig_Obj_t * pObj, * pObj0, * pObj1, * pFlop0, * pFlop1; Aig_Obj_t * pObj, * pObj0, * pObj1, * pFlop0, * pFlop1;
int i, Counter; int i, Counter;
assert( Saig_ManRegNum(p) > 0 ); assert( Saig_ManRegNum(p) > 0 );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
// check if demitering is possible // check if demitering is possible
vPairs = Vec_PtrAlloc( 2 * Saig_ManPoNum(p) ); vPairs = Vec_PtrAlloc( 2 * Saig_ManPoNum(p) );
Saig_ManForEachPo( p, pObj, i ) Saig_ManForEachPo( p, pObj, i )
...@@ -1274,14 +1274,14 @@ int Saig_ManDemiterNew( Aig_Man_t * pMan ) ...@@ -1274,14 +1274,14 @@ int Saig_ManDemiterNew( Aig_Man_t * pMan )
vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) ); vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) );
Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k ) Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k )
if ( Saig_ObjIsLo(pMan, pTemp) ) if ( Saig_ObjIsLo(pMan, pTemp) )
printf( " %d", Aig_ObjPioNum(pTemp) ); printf( " %d", Aig_ObjCioId(pTemp) );
printf( "\n" ); printf( "\n" );
Vec_PtrFree( vSupp0 ); Vec_PtrFree( vSupp0 );
vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) ); vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) );
Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k ) Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k )
if ( Saig_ObjIsLo(pMan, pTemp) ) if ( Saig_ObjIsLo(pMan, pTemp) )
printf( " %d", Aig_ObjPioNum(pTemp) ); printf( " %d", Aig_ObjCioId(pTemp) );
printf( "\n" ); printf( "\n" );
Vec_PtrFree( vSupp1 ); Vec_PtrFree( vSupp1 );
} }
......
src/aig/saig/saigRefSat.c
...@@ -124,7 +124,7 @@ void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr ...@@ -124,7 +124,7 @@ void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr
Aig_ObjSetTravIdCurrent(p, pObj); Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsCi(pObj) ) if ( Aig_ObjIsCi(pObj) )
{ {
Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
return; return;
} }
assert( Aig_ObjIsNode(pObj) ); assert( Aig_ObjIsNode(pObj) );
...@@ -316,15 +316,15 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu ...@@ -316,15 +316,15 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
pObj->pData = Aig_ManConst1(pFrames); pObj->pData = Aig_ManConst1(pFrames);
else if ( Saig_ObjIsPi(pAig, pObj) ) else if ( Saig_ObjIsPi(pAig, pObj) )
{ {
if ( Aig_ObjPioNum(pObj) < nInputs ) if ( Aig_ObjCioId(pObj) < nInputs )
{ {
int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
} }
else else
{ {
pObj->pData = Aig_ObjCreateCi( pFrames ); pObj->pData = Aig_ObjCreateCi( pFrames );
Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) ); Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
Vec_IntPush( *pvMapPiF2A, f ); Vec_IntPush( *pvMapPiF2A, f );
} }
} }
......
src/aig/saig/saigRetStep.c
...@@ -37,7 +37,7 @@ ABC_NAMESPACE_IMPL_START ...@@ -37,7 +37,7 @@ ABC_NAMESPACE_IMPL_START
Description [Returns the pointer to the register output after retiming.] Description [Returns the pointer to the register output after retiming.]
SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] SideEffects [Remember to run Aig_ManSetCioIds() in advance.]
SeeAlso [] SeeAlso []
...@@ -62,16 +62,16 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug ...@@ -62,16 +62,16 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
// skip of they are not register outputs // skip of they are not register outputs
if ( !Saig_ObjIsLo(p, pFanin0) || !Saig_ObjIsLo(p, pFanin1) ) if ( !Saig_ObjIsLo(p, pFanin0) || !Saig_ObjIsLo(p, pFanin1) )
return NULL; return NULL;
assert( Aig_ObjPioNum(pFanin0) > 0 ); assert( Aig_ObjCioId(pFanin0) > 0 );
assert( Aig_ObjPioNum(pFanin1) > 0 ); assert( Aig_ObjCioId(pFanin1) > 0 );
// skip latch guns // skip latch guns
if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) ) if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) )
return NULL; return NULL;
// get the inputs of these registers // get the inputs of these registers
pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) ); pInput0 = Saig_ManLi( p, Aig_ObjCioId(pFanin0) - Saig_ManPiNum(p) );
pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) ); pInput1 = Saig_ManLi( p, Aig_ObjCioId(pFanin1) - Saig_ManPiNum(p) );
pInput0 = Aig_ObjChild0( pInput0 ); pInput0 = Aig_ObjChild0( pInput0 );
pInput1 = Aig_ObjChild0( pInput1 ); pInput1 = Aig_ObjChild0( pInput1 );
pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) ); pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
...@@ -90,11 +90,11 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug ...@@ -90,11 +90,11 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
// create new register input // create new register input
pObjLi = Aig_ObjCreateCo( p, Aig_NotCond(pObjNew, fCompl) ); pObjLi = Aig_ObjCreateCo( p, Aig_NotCond(pObjNew, fCompl) );
pObjLi->PioNum = Aig_ManCoNum(p) - 1; pObjLi->CioId = Aig_ManCoNum(p) - 1;
// create new register output // create new register output
pObjLo = Aig_ObjCreateCi( p ); pObjLo = Aig_ObjCreateCi( p );
pObjLo->PioNum = Aig_ManCiNum(p) - 1; pObjLo->CioId = Aig_ManCiNum(p) - 1;
p->nRegs++; p->nRegs++;
// make sure the register is retimable. // make sure the register is retimable.
...@@ -113,7 +113,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug ...@@ -113,7 +113,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
Description [Returns the pointer to node after retiming.] Description [Returns the pointer to node after retiming.]
SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] SideEffects [Remember to run Aig_ManSetCioIds() in advance.]
SeeAlso [] SeeAlso []
...@@ -127,11 +127,11 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) ...@@ -127,11 +127,11 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
int fCompl0, fCompl1; int fCompl0, fCompl1;
assert( Saig_ManRegNum(p) > 0 ); assert( Saig_ManRegNum(p) > 0 );
assert( Aig_ObjPioNum(pObjLo) > 0 ); assert( Aig_ObjCioId(pObjLo) > 0 );
assert( Saig_ObjIsLo(p, pObjLo) ); assert( Saig_ObjIsLo(p, pObjLo) );
// get the corresponding latch input // get the corresponding latch input
pObjLi = Saig_ManLi( p, Aig_ObjPioNum(pObjLo) - Saig_ManPiNum(p) ); pObjLi = Saig_ManLi( p, Aig_ObjCioId(pObjLo) - Saig_ManPiNum(p) );
// get the node // get the node
pObj = Aig_ObjFanin0(pObjLi); pObj = Aig_ObjFanin0(pObjLi);
...@@ -148,15 +148,15 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) ...@@ -148,15 +148,15 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
// create latch inputs // create latch inputs
pLi0New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin0, fCompl0) ); pLi0New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin0, fCompl0) );
pLi0New->PioNum = Aig_ManCoNum(p) - 1; pLi0New->CioId = Aig_ManCoNum(p) - 1;
pLi1New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin1, fCompl1) ); pLi1New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin1, fCompl1) );
pLi1New->PioNum = Aig_ManCoNum(p) - 1; pLi1New->CioId = Aig_ManCoNum(p) - 1;
// create latch outputs // create latch outputs
pLo0New = Aig_ObjCreateCi(p); pLo0New = Aig_ObjCreateCi(p);
pLo0New->PioNum = Aig_ManCiNum(p) - 1; pLo0New->CioId = Aig_ManCiNum(p) - 1;
pLo1New = Aig_ObjCreateCi(p); pLo1New = Aig_ObjCreateCi(p);
pLo1New->PioNum = Aig_ManCiNum(p) - 1; pLo1New->CioId = Aig_ManCiNum(p) - 1;
pLo0New = Aig_NotCond( pLo0New, fCompl0 ); pLo0New = Aig_NotCond( pLo0New, fCompl0 );
pLo1New = Aig_NotCond( pLo1New, fCompl1 ); pLo1New = Aig_NotCond( pLo1New, fCompl1 );
p->nRegs += 2; p->nRegs += 2;
...@@ -173,7 +173,7 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) ...@@ -173,7 +173,7 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
Description [Returns the pointer to node after retiming.] Description [Returns the pointer to node after retiming.]
SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] SideEffects [Remember to run Aig_ManSetCioIds() in advance.]
SeeAlso [] SeeAlso []
...@@ -182,7 +182,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs ) ...@@ -182,7 +182,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
{ {
Aig_Obj_t * pObj, * pObjNew; Aig_Obj_t * pObj, * pObjNew;
int RetValue, s, i; int RetValue, s, i;
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
Aig_ManFanoutStart( p ); Aig_ManFanoutStart( p );
p->fCreatePios = 1; p->fCreatePios = 1;
if ( fForward ) if ( fForward )
......
src/aig/saig/saigScl.c
...@@ -47,7 +47,7 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ) ...@@ -47,7 +47,7 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
Aig_Obj_t * pObj, * pDriver; Aig_Obj_t * pObj, * pDriver;
int i, Counter1, Counter2; int i, Counter1, Counter2;
// set PIO numbers // set PIO numbers
Aig_ManSetPioNumbers( pAig ); Aig_ManSetCioIds( pAig );
// check how many POs are driven by a register whose ref count is 1 // check how many POs are driven by a register whose ref count is 1
Counter1 = 0; Counter1 = 0;
Saig_ManForEachPo( pAig, pObj, i ) Saig_ManForEachPo( pAig, pObj, i )
......
src/aig/saig/saigSimExt2.c
...@@ -235,7 +235,7 @@ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, ...@@ -235,7 +235,7 @@ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax,
if ( Saig_ObjIsPi(p, pObj) ) if ( Saig_ObjIsPi(p, pObj) )
{ {
// propagate implications of this assignment // propagate implications of this assignment
int i, iPiNum = Aig_ObjPioNum(pObj); int i, iPiNum = Aig_ObjCioId(pObj);
for ( i = fMax; i >= 0; i-- ) for ( i = fMax; i >= 0; i-- )
if ( i != f ) if ( i != f )
Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, iPiNum), i, fMax, vSimInfo ); Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, iPiNum), i, fMax, vSimInfo );
......
src/aig/saig/saigSimSeq.c
...@@ -124,7 +124,7 @@ int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -124,7 +124,7 @@ int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj )
else else
{ {
iFan0 = iFan1 = 0; iFan0 = iFan1 = 0;
Vec_IntPush( p->vCis2Ids, Aig_ObjPioNum(pObj) ); Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) );
} }
p->pFans0[p->nObjs] = iFan0; p->pFans0[p->nObjs] = iFan0;
p->pFans1[p->nObjs] = iFan1; p->pFans1[p->nObjs] = iFan1;
......
src/base/abci/abcDar.c
...@@ -1630,7 +1630,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig ) ...@@ -1630,7 +1630,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
} }
i = 0; i = 0;
Aig_ManSetPioNumbers( pAig ); Aig_ManSetCioIds( pAig );
Saig_ManForEachLo( pAig, pFlop, i ) Saig_ManForEachLo( pAig, pFlop, i )
{ {
p_irrelevant[i] = false; p_irrelevant[i] = false;
...@@ -1661,7 +1661,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig ) ...@@ -1661,7 +1661,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
} }
assert( Saig_ObjIsLo( pAig, pRepr ) ); assert( Saig_ObjIsLo( pAig, pRepr ) );
repr_idx = Aig_ObjPioNum(pRepr) - Saig_ManPiNum(pAig); repr_idx = Aig_ObjCioId(pRepr) - Saig_ManPiNum(pAig);
pReprName = pNames[repr_idx]; pReprName = pNames[repr_idx];
Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName ); Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName );
// Abc_Print( 1, "Original flop # %d is proved equivalent to flop # %d.\n", i, repr_idx ); // Abc_Print( 1, "Original flop # %d is proved equivalent to flop # %d.\n", i, repr_idx );
......
src/opt/cgt/cgtAig.c
...@@ -320,7 +320,7 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ) ...@@ -320,7 +320,7 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p )
} }
} }
Aig_ManCleanup( pNew ); Aig_ManCleanup( pNew );
Aig_ManSetPioNumbers( pNew ); Aig_ManSetCioIds( pNew );
return pNew; return pNew;
} }
...@@ -375,14 +375,14 @@ void Cgt_ManConstructCare( Aig_Man_t * pNew, Aig_Man_t * pCare, Vec_Vec_t * vSup ...@@ -375,14 +375,14 @@ void Cgt_ManConstructCare( Aig_Man_t * pNew, Aig_Man_t * pCare, Vec_Vec_t * vSup
Aig_ManIncrementTravId( pCare ); Aig_ManIncrementTravId( pCare );
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i ) Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i )
{ {
pPi = Aig_ManCi( pCare, Aig_ObjPioNum(pLeaf) ); pPi = Aig_ManCi( pCare, Aig_ObjCioId(pLeaf) );
Aig_ObjSetTravIdCurrent( pCare, pPi ); Aig_ObjSetTravIdCurrent( pCare, pPi );
pPi->pData = pLeaf->pData; pPi->pData = pLeaf->pData;
} }
// construct the constraints // construct the constraints
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i ) Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i )
{ {
vOuts = Vec_VecEntryInt( vSuppsInv, Aig_ObjPioNum(pLeaf) ); vOuts = Vec_VecEntryInt( vSuppsInv, Aig_ObjCioId(pLeaf) );
Vec_IntForEachEntry( vOuts, iOut, k ) Vec_IntForEachEntry( vOuts, iOut, k )
{ {
pPo = Aig_ManCo( pCare, iOut ); pPo = Aig_ManCo( pCare, iOut );
......
src/opt/cgt/cgtDecide.c
...@@ -103,7 +103,7 @@ int Cgt_ManCheckGateComplete( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, Aig_Obj_t ...@@ -103,7 +103,7 @@ int Cgt_ManCheckGateComplete( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, Aig_Obj_t
{ {
if ( Saig_ObjIsPo(pAig, pObj) ) if ( Saig_ObjIsPo(pAig, pObj) )
return 0; return 0;
vGates = Vec_VecEntry( vGatesAll, Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig) ); vGates = Vec_VecEntry( vGatesAll, Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig) );
if ( Vec_PtrFind( vGates, pGate ) == -1 ) if ( Vec_PtrFind( vGates, pGate ) == -1 )
return 0; return 0;
} }
......
src/opt/cgt/cgtMan.c
...@@ -48,7 +48,7 @@ Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPar ...@@ -48,7 +48,7 @@ Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPar
// prepare the sequential AIG // prepare the sequential AIG
assert( Saig_ManRegNum(pAig) > 0 ); assert( Saig_ManRegNum(pAig) > 0 );
Aig_ManFanoutStart( pAig ); Aig_ManFanoutStart( pAig );
Aig_ManSetPioNumbers( pAig ); Aig_ManSetCioIds( pAig );
// create interpolation manager // create interpolation manager
p = ABC_ALLOC( Cgt_Man_t, 1 ); p = ABC_ALLOC( Cgt_Man_t, 1 );
memset( p, 0, sizeof(Cgt_Man_t) ); memset( p, 0, sizeof(Cgt_Man_t) );
......
src/opt/dar/darBalance.c
...@@ -495,7 +495,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) ...@@ -495,7 +495,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
{ {
float arrTime; float arrTime;
Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime ); Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime );
Aig_ManSetPioNumbers( p ); Aig_ManSetCioIds( p );
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
{ {
if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
...@@ -507,7 +507,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) ...@@ -507,7 +507,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObj->pData = pObjNew; pObj->pData = pObjNew;
pObjNew->pHaig = pObj->pHaig; pObjNew->pHaig = pObj->pHaig;
// set the arrival time of the new PI // set the arrival time of the new PI
arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
pObjNew->Level = (int)arrTime; pObjNew->Level = (int)arrTime;
} }
else if ( Aig_ObjIsCo(pObj) ) else if ( Aig_ObjIsCo(pObj) )
...@@ -518,7 +518,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) ...@@ -518,7 +518,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
// save arrival time of the output // save arrival time of the output
arrTime = (float)Aig_Regular(pObjNew)->Level; arrTime = (float)Aig_Regular(pObjNew)->Level;
Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj), arrTime ); Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
// create PO // create PO
pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
pObjNew->pHaig = pObj->pHaig; pObjNew->pHaig = pObj->pHaig;
...@@ -526,7 +526,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) ...@@ -526,7 +526,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
else else
assert( 0 ); assert( 0 );
} }
Aig_ManCleanPioNumbers( p ); Aig_ManCleanCioIds( p );
pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 ); pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
} }
else else
......
src/proof/bbr/bbrReach.c
...@@ -563,7 +563,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) ...@@ -563,7 +563,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) ); vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
Saig_ManForEachPi( pInit, pObj, i ) Saig_ManForEachPi( pInit, pObj, i )
if ( pObj->pData != NULL ) if ( pObj->pData != NULL )
Vec_IntPush( vInputMap, Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) ); Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) );
else else
Vec_IntPush( vInputMap, -1 ); Vec_IntPush( vInputMap, -1 );
// create new pattern // create new pattern
......
src/proof/fra/fraCore.c
...@@ -81,7 +81,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p ) ...@@ -81,7 +81,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
continue; continue;
} }
// check if the output is a primary input // check if the output is a primary input
if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis ) if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjCioId(Aig_Regular(pChild)) < p->nTruePis )
{ {
CountNonConst0++; CountNonConst0++;
continue; continue;
......
src/proof/live/liveness.c
...@@ -527,7 +527,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ ...@@ -527,7 +527,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
{ {
assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
} }
...@@ -830,7 +830,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M ...@@ -830,7 +830,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
{ {
assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
} }
...@@ -2256,7 +2256,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A ...@@ -2256,7 +2256,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
{ {
assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
//assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
} }
......
src/proof/live/liveness_sim.c
...@@ -466,7 +466,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ ...@@ -466,7 +466,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
assert( Aig_ManCheck( pNew ) ); assert( Aig_ManCheck( pNew ) );
#ifndef DUPLICATE_CKT_DEBUG #ifndef DUPLICATE_CKT_DEBUG
assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPoNum( pNew ) == 1 ); assert( Saig_ManPoNum( pNew ) == 1 );
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
......
src/proof/llb/llb2Flow.c
...@@ -124,9 +124,9 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp ...@@ -124,9 +124,9 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
{ {
if ( !Saig_ObjIsPi(p, pObj) ) if ( !Saig_ObjIsPi(p, pObj) )
continue; continue;
if ( piFirst[Aig_ObjPioNum(pObj)] == -1 ) if ( piFirst[Aig_ObjCioId(pObj)] == -1 )
piFirst[Aig_ObjPioNum(pObj)] = i; piFirst[Aig_ObjCioId(pObj)] = i;
piLast[Aig_ObjPioNum(pObj)] = i; piLast[Aig_ObjCioId(pObj)] = i;
} }
} }
// PIs feeding into the flops should be extended to the last frame // PIs feeding into the flops should be extended to the last frame
...@@ -134,7 +134,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp ...@@ -134,7 +134,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
{ {
if ( !Saig_ObjIsPi(p, Aig_ObjFanin0(pObj)) ) if ( !Saig_ObjIsPi(p, Aig_ObjFanin0(pObj)) )
continue; continue;
piLast[Aig_ObjPioNum(Aig_ObjFanin0(pObj))] = Vec_PtrSize(vMaps)-1; piLast[Aig_ObjCioId(Aig_ObjFanin0(pObj))] = Vec_PtrSize(vMaps)-1;
} }
// set the PI map // set the PI map
......
src/proof/pdr/pdrCnf.c
...@@ -202,7 +202,7 @@ static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar ) ...@@ -202,7 +202,7 @@ static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar )
return -1; return -1;
pObj = Aig_ManObj( p->pAig, ObjId ); pObj = Aig_ManObj( p->pAig, ObjId );
if ( Saig_ObjIsLi( p->pAig, pObj ) ) if ( Saig_ObjIsLi( p->pAig, pObj ) )
return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig); return Aig_ObjCioId(pObj)-Saig_ManPoNum(p->pAig);
assert( 0 ); // should be called for register inputs only assert( 0 ); // should be called for register inputs only
return -1; return -1;
} }
......
src/proof/pdr/pdrTsim.c
...@@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi ...@@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
{ {
if ( Saig_ObjIsPi(pAig, pObj) ) if ( Saig_ObjIsPi(pAig, pObj) )
{ {
Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) ); Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
Vec_IntPush( vPiLits, Lit ); Vec_IntPush( vPiLits, Lit );
continue; continue;
} }
assert( Saig_ObjIsLo(pAig, pObj) ); assert( Saig_ObjIsLo(pAig, pObj) );
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
continue; continue;
Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) ); Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
Vec_IntPush( vRes, Lit ); Vec_IntPush( vRes, Lit );
} }
if ( Vec_IntSize(vRes) == 0 ) if ( Vec_IntSize(vRes) == 0 )
...@@ -323,10 +323,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals ...@@ -323,10 +323,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
pBuff[i] = '-'; pBuff[i] = '-';
pBuff[i] = 0; pBuff[i] = 0;
Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i ) Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0'); pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
if ( vCi2Rem ) if ( vCi2Rem )
Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i ) Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
pBuff[Aig_ObjPioNum(pObj)] = 'x'; pBuff[Aig_ObjCioId(pObj)] = 'x';
Abc_Print( 1, "%s\n", pBuff ); Abc_Print( 1, "%s\n", pBuff );
ABC_FREE( pBuff ); ABC_FREE( pBuff );
} }
...@@ -406,7 +406,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); ...@@ -406,7 +406,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
{ {
if ( !Saig_ObjIsLo( p->pAig, pObj ) ) if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue; continue;
Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
continue; continue;
Vec_IntClear( vUndo ); Vec_IntClear( vUndo );
...@@ -420,7 +420,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); ...@@ -420,7 +420,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
{ {
if ( !Saig_ObjIsLo( p->pAig, pObj ) ) if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue; continue;
Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
continue; continue;
Vec_IntClear( vUndo ); Vec_IntClear( vUndo );
......
src/proof/pdr/pdrUtil.c
...@@ -616,11 +616,11 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd ...@@ -616,11 +616,11 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
if ( Aig_ObjIsCi(pNode) ) if ( Aig_ObjIsCi(pNode) )
{ {
// if ( vSuppLits ) // if ( vSuppLits )
// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); // Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
if ( Saig_ObjIsLo(pAig, pNode) ) if ( Saig_ObjIsLo(pAig, pNode) )
{ {
// pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value ); // pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value );
pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value ); pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), Value );
pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63)); pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
} }
return 1; return 1;
......
src/proof/ssw/sswBmc.c
...@@ -132,7 +132,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo ...@@ -132,7 +132,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
// start managers // start managers
assert( Saig_ManRegNum(pAig) > 0 ); assert( Saig_ManRegNum(pAig) > 0 );
Aig_ManSetPioNumbers( pAig ); Aig_ManSetCioIds( pAig );
pSat = Ssw_SatStart( 0 ); pSat = Ssw_SatStart( 0 );
pFrm = Ssw_FrmStart( pAig ); pFrm = Ssw_FrmStart( pAig );
pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 ); pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
......
src/proof/ssw/sswDyn.c
...@@ -113,10 +113,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos ...@@ -113,10 +113,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos
if ( Aig_ObjIsCo(pObj) ) if ( Aig_ObjIsCo(pObj) )
{ {
// skip if it is a register input PO // skip if it is a register input PO
if ( Aig_ObjPioNum(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) ) if ( Aig_ObjCioId(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
return; return;
// add the number of this constraint // add the number of this constraint
Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 ); Vec_IntPush( vNewPos, Aig_ObjCioId(pObj)/2 );
return; return;
} }
// visit the fanouts // visit the fanouts
...@@ -225,7 +225,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) ...@@ -225,7 +225,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
} }
assert( !Aig_IsComplement(pObjFraig) ); assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsCi(pObjFraig) ); assert( Aig_ObjIsCi(pObjFraig) );
pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
} }
// set random simulation info for the second frame // set random simulation info for the second frame
...@@ -236,7 +236,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) ...@@ -236,7 +236,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
pObjFraig = Ssw_ObjFrame( p, pObj, f ); pObjFraig = Ssw_ObjFrame( p, pObj, f );
assert( !Aig_IsComplement(pObjFraig) ); assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsCi(pObjFraig) ); assert( Aig_ObjIsCi(pObjFraig) );
pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
} }
} }
...@@ -386,7 +386,7 @@ clk = clock(); ...@@ -386,7 +386,7 @@ clk = clock();
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i ) Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
Aig_ManSetPioNumbers( p->pFrames ); Aig_ManSetCioIds( p->pFrames );
// label nodes corresponding to primary inputs // label nodes corresponding to primary inputs
Ssw_ManLabelPiNodes( p ); Ssw_ManLabelPiNodes( p );
p->timeReduce += clock() - clk; p->timeReduce += clock() - clk;
......
src/proof/ssw/sswLcorr.c
...@@ -59,7 +59,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) ...@@ -59,7 +59,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
} }
assert( !Aig_IsComplement(pObjFraig) ); assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsCi(pObjFraig) ); assert( Aig_ObjIsCi(pObjFraig) );
pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
} }
} }
...@@ -116,7 +116,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) ...@@ -116,7 +116,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
Value = sat_solver_var_value( p->pMSat->pSat, nVarNum ); Value = sat_solver_var_value( p->pMSat->pSat, nVarNum );
if ( Value == 0 ) if ( Value == 0 )
continue; continue;
pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) );
Abc_InfoSetBit( pInfo, p->nPatterns ); Abc_InfoSetBit( pInfo, p->nPatterns );
} }
} }
...@@ -260,7 +260,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) ...@@ -260,7 +260,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase ); pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
Ssw_ObjSetFrame( p, pObj, 0, pTemp ); Ssw_ObjSetFrame( p, pObj, 0, pTemp );
} }
Aig_ManSetPioNumbers( p->pFrames ); Aig_ManSetCioIds( p->pFrames );
// prepare simulation info // prepare simulation info
assert( p->vSimInfo == NULL ); assert( p->vSimInfo == NULL );
......
src/proof/ssw/sswMan.c
...@@ -48,7 +48,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -48,7 +48,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// prepare the sequential AIG // prepare the sequential AIG
assert( Saig_ManRegNum(pAig) > 0 ); assert( Saig_ManRegNum(pAig) > 0 );
Aig_ManFanoutStart( pAig ); Aig_ManFanoutStart( pAig );
Aig_ManSetPioNumbers( pAig ); Aig_ManSetCioIds( pAig );
// create interpolation manager // create interpolation manager
p = ABC_ALLOC( Ssw_Man_t, 1 ); p = ABC_ALLOC( Ssw_Man_t, 1 );
memset( p, 0, sizeof(Ssw_Man_t) ); memset( p, 0, sizeof(Ssw_Man_t) );
......
src/proof/ssw/sswSweep.c
...@@ -167,7 +167,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) ...@@ -167,7 +167,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
assert( nVarNum > 0 ); assert( nVarNum > 0 );
if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) ) if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) )
{ {
pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) );
Abc_InfoSetBit( pInfo, p->nPatterns ); Abc_InfoSetBit( pInfo, p->nPatterns );
} }
} }
......
src/proof/ssw/sswUnique.c
...@@ -108,9 +108,9 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV ...@@ -108,9 +108,9 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
assert( Aig_ObjIsCi(pTemp) ); assert( Aig_ObjIsCi(pTemp) );
if ( !Saig_ObjIsLo(p->pAig, pTemp) ) if ( !Saig_ObjIsLo(p->pAig, pTemp) )
continue; continue;
assert( Aig_ObjPioNum(pTemp) > 0 ); assert( Aig_ObjCioId(pTemp) > 0 );
Vec_PtrWriteEntry( p->vCommon, k++, pTemp ); Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) ) if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjCioId(pTemp) - Saig_ManPiNum(p->pAig)) )
fFeasible = 1; fFeasible = 1;
} }
Vec_PtrShrink( p->vCommon, k ); Vec_PtrShrink( p->vCommon, k );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment