diff options
Diffstat (limited to 'src/aig')
87 files changed, 990 insertions, 311 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 1f51f300..1750a7b7 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -215,11 +215,6 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) -#define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) -#define AIG_ABS(a) (((a) >= 0)? (a) :-(a)) -#define AIG_INFINITY (100000000) - static inline int Aig_IntAbs( int n ) { return (n < 0)? -n : n; } static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); } static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); } @@ -320,7 +315,7 @@ static inline Aig_Obj_t * Aig_ObjChild1Next( Aig_Obj_t * pObj ) { assert( !Aig static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0); } static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1); } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; } -static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } +static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + ABC_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i; } static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } @@ -483,6 +478,7 @@ extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos ); extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index db80a7f9..dfc35c83 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -407,7 +407,7 @@ int Aig_ManLevelNum( Aig_Man_t * p ) int i, LevelsMax; LevelsMax = 0; Aig_ManForEachPo( p, pObj, i ) - LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level ); + LevelsMax = ABC_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level ); return LevelsMax; } diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index 6c9cb499..febe8a0c 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "aig.h" +#include "saig.h" #include "tim.h" //////////////////////////////////////////////////////////////////////// @@ -301,6 +301,52 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ) printf( "Aig_ManDupOrdered(): The check has failed.\n" ); return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager.] + + Description [Assumes topological ordering of the nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i, nNodes; + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + // duplicate internal nodes + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) ); + else if ( Aig_ObjIsPi(pObj) ) + pObjNew = (Aig_ObjRefs(pObj) > 0 || Saig_ObjIsLo(p, pObj)) ? Aig_ObjCreatePi(pNew) : NULL; + else if ( Aig_ObjIsPo(pObj) ) + pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + else if ( Aig_ObjIsConst1(pObj) ) + pObjNew = Aig_ManConst1(pNew); + else + assert( 0 ); + pObj->pData = pObjNew; + } + assert( Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); + if ( (nNodes = Aig_ManCleanup( pNew )) ) + printf( "Aig_ManDupTrim(): Cleanup after AIG duplication removed %d nodes.\n", nNodes ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDupTrim(): The check has failed.\n" ); + return pNew; +} /**Function************************************************************* diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c index 89702087..a3b1e684 100644 --- a/src/aig/aig/aigFanout.c +++ b/src/aig/aig/aigFanout.c @@ -109,7 +109,7 @@ void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ) assert( pFanout->Id > 0 ); if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc ) { - int nFansAlloc = 2 * AIG_MAX( pObj->Id, pFanout->Id ); + int nFansAlloc = 2 * ABC_MAX( pObj->Id, pFanout->Id ); p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc ); memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) ); p->nFansAlloc = nFansAlloc; diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c index f681c76a..2c648382 100644 --- a/src/aig/aig/aigMffc.c +++ b/src/aig/aig/aigMffc.c @@ -266,13 +266,13 @@ int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves // dereference the current cut LevelMax = 0; Vec_PtrForEachEntry( vLeaves, pObj, i ) - LevelMax = AIG_MAX( LevelMax, (int)pObj->Level ); + LevelMax = ABC_MAX( LevelMax, (int)pObj->Level ); if ( LevelMax == 0 ) return 0; // dereference the cut ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL ); // try expanding each node in the boundary - ConeBest = AIG_INFINITY; + ConeBest = ABC_INFINITY; pLeafBest = NULL; Vec_PtrForEachEntry( vLeaves, pObj, i ) { diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 2c373ee1..8d243419 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -529,7 +529,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in if ( p->pFanData && Aig_ObjIsBuf(pObjOld) ) { Vec_PtrPush( p->vBufs, pObjOld ); - p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) ); + p->nBufMax = ABC_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) ); Aig_ManPropagateBuffers( p, fUpdateLevel ); } } diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c index 1e77c224..dd10e91e 100644 --- a/src/aig/aig/aigPartReg.c +++ b/src/aig/aig/aigPartReg.c @@ -39,7 +39,7 @@ struct Aig_ManPre_t_ // info about the current partition Vec_Int_t * vRegs; // registers of this partition Vec_Int_t * vUniques; // unique registers of this partition - Vec_Int_t * vFreeVars; // ABC_FREE variables of this partition + Vec_Int_t * vFreeVars; // free variables of this partition Vec_Flt_t * vPartCost; // costs of adding each variable char * pfPartVars; // input/output registers of the partition }; @@ -153,7 +153,7 @@ int Aig_ManRegFindSeed( Aig_ManPre_t * p ) int Aig_ManRegFindBestVar( Aig_ManPre_t * p ) { Vec_Int_t * vSupp; - int nNewVars, nNewVarsBest = AIG_INFINITY; + int nNewVars, nNewVarsBest = ABC_INFINITY; int iVarFree, iVarSupp, iVarBest = -1, i, k; // go through the ABC_FREE variables Vec_IntForEachEntry( p->vFreeVars, iVarFree, i ) diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c index c5cc6392..6dea6503 100644 --- a/src/aig/aig/aigRet.c +++ b/src/aig/aig/aigRet.c @@ -173,7 +173,7 @@ void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) assert( pEdge->nLats == 10 ); if ( p->nExtraCur + 1 > p->nExtraAlloc ) { - int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 ); + int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 ); p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew ); p->nExtraAlloc = nExtraAllocNew; } @@ -199,7 +199,7 @@ void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) nWords = (pEdge->nLats + 1) >> 4; if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc ) { - int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 ); + int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 ); p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew ); p->nExtraAlloc = nExtraAllocNew; } @@ -357,7 +357,7 @@ int Rtm_ManLatchMax( Rtm_Man_t * p ) assert( Val == 1 || Val == 2 ); } */ - nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats ); + nLatchMax = ABC_MAX( nLatchMax, (int)pEdge->nLats ); } return nLatchMax; } @@ -474,7 +474,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj ) Rtm_Obj_t * pFanin; int i, Degree = 0; Rtm_ObjForEachFanin( pObj, pFanin, i ) - Degree = AIG_MAX( Degree, (int)pFanin->Num ); + Degree = ABC_MAX( Degree, (int)pFanin->Num ); return Degree + 1; } @@ -494,7 +494,7 @@ int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj ) Rtm_Obj_t * pFanout; int i, Degree = 0; Rtm_ObjForEachFanout( pObj, pFanout, i ) - Degree = AIG_MAX( Degree, (int)pFanout->Num ); + Degree = ABC_MAX( Degree, (int)pFanout->Num ); return Degree + 1; } @@ -907,7 +907,7 @@ clk = clock(); if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable continue; Degree = Rtm_ObjGetDegreeFwd( pNext ); - DegreeMax = AIG_MAX( DegreeMax, Degree ); + DegreeMax = ABC_MAX( DegreeMax, Degree ); if ( Degree > nStepsMax ) // skip nodes with high degree continue; pNext->fMark = 1; @@ -928,7 +928,7 @@ clk = clock(); if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable continue; Degree = Rtm_ObjGetDegreeBwd( pNext ); - DegreeMax = AIG_MAX( DegreeMax, Degree ); + DegreeMax = ABC_MAX( DegreeMax, Degree ); if ( Degree > nStepsMax ) // skip nodes with high degree continue; pNext->fMark = 1; diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c index de8fdc7c..d0cc99e3 100644 --- a/src/aig/aig/aigTiming.c +++ b/src/aig/aig/aigTiming.c @@ -118,7 +118,7 @@ int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj ) Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) { LevelCur = Aig_ObjReverseLevel( p, pFanout ); - Level = AIG_MAX( Level, LevelCur ); + Level = ABC_MAX( Level, LevelCur ); } return Level + 1; } diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 80d1f527..d49fffd3 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -114,7 +114,7 @@ int Aig_ManLevels( Aig_Man_t * p ) Aig_Obj_t * pObj; int i, LevelMax = 0; Aig_ManForEachPo( p, pObj, i ) - LevelMax = AIG_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level ); + LevelMax = ABC_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level ); return LevelMax; } @@ -1255,7 +1255,7 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; - Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) ); + Vec_PtrGrow( vArr, ABC_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) ); pBeg = (Aig_Obj_t **)vArr->pArray; while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c index c2982856..1d43f6fb 100644 --- a/src/aig/bbr/bbrReach.c +++ b/src/aig/bbr/bbrReach.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "bbr.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -180,7 +181,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i ); pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] ); } - // ABC_FREE global BDDs + // free global BDDs Aig_ManFreeGlobalBdds( p, dd ); // reorder and disable reordering @@ -220,9 +221,6 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D int nThreshold = 10000; Vec_Ptr_t * vOnionRings; - // start the onion rings - vOnionRings = Vec_PtrAlloc( 1000 ); - // start the image computation bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs ); if ( fPartition ) @@ -237,6 +235,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D return -1; } + // start the onion rings + vOnionRings = Vec_PtrAlloc( 1000 ); + // perform reachability analisys bCurrent = bInitial; Cudd_Ref( bCurrent ); bReached = bInitial; Cudd_Ref( bReached ); @@ -256,6 +257,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D Bbr_bddImageTreeDelete( pTree ); else Bbr_bddImageTreeDelete2( pTree2 ); + Vec_PtrFree( vOnionRings ); return -1; } Cudd_Ref( bNext ); @@ -316,7 +318,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D fprintf( stdout, "\r" ); } Cudd_RecursiveDeref( dd, bNext ); - // ABC_FREE the onion rings + // free the onion rings Vec_PtrForEachEntry( vOnionRings, bTemp, i ) Cudd_RecursiveDeref( dd, bTemp ); Vec_PtrFree( vOnionRings ); @@ -353,7 +355,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D /**Function************************************************************* - Synopsis [Performs reachability to see if any .] + Synopsis [Performs reachability to see if any PO can be asserted.] Description [] @@ -362,7 +364,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D SeeAlso [] ***********************************************************************/ -int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) +int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) { DdManager * dd; DdNode ** pbParts, ** pbOutputs; @@ -372,9 +374,6 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti assert( Saig_ManRegNum(p) > 0 ); - // start the onion rings - vOnionRings = Vec_PtrAlloc( 1000 ); - // compute the global BDDs of the latches dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose ); if ( dd == NULL ) @@ -386,6 +385,9 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti if ( fVerbose ) printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + // start the onion rings + vOnionRings = Vec_PtrAlloc( 1000 ); + // save outputs pbOutputs = Aig_ManCreateOutputs( dd, p ); @@ -413,7 +415,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti break; } } - // ABC_FREE the onion rings + // free the onion rings Vec_PtrForEachEntry( vOnionRings, bTemp, i ) Cudd_RecursiveDeref( dd, bTemp ); Vec_PtrFree( vOnionRings ); @@ -443,6 +445,80 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti return RetValue; } +/**Function************************************************************* + + Synopsis [Performs reachability to see if any PO can be asserted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) +{ + Ssw_Cex_t * pCexOld, * pCexNew; + Aig_Man_t * p; + Aig_Obj_t * pObj; + Vec_Int_t * vInputMap; + int i, k, Entry, iBitOld, iBitNew, RetValue; + // check if there are PIs without fanout + Saig_ManForEachPi( pInit, pObj, i ) + if ( Aig_ObjRefs(pObj) == 0 ) + break; + if ( i == Saig_ManPiNum(pInit) ) + return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); + // create new AIG + p = Aig_ManDupTrim( pInit ); + assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) ); + assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) ); + RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); + if ( RetValue != 0 ) + { + Aig_ManStop( p ); + return RetValue; + } + // the problem is satisfiable - remap the pattern + pCexOld = p->pSeqModel; + assert( pCexOld != NULL ); + // create input map + vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) ); + Saig_ManForEachPi( pInit, pObj, i ) + if ( pObj->pData != NULL ) + Vec_IntPush( vInputMap, Aig_ObjPioNum(pObj->pData) ); + else + Vec_IntPush( vInputMap, -1 ); + // create new pattern + pCexNew = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 ); + pCexNew->iFrame = pCexOld->iFrame; + pCexNew->iPo = pCexOld->iPo; + // copy the bit-data + for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ ) + if ( Aig_InfoHasBit( pCexOld->pData, iBitOld ) ) + Aig_InfoSetBit( pCexNew->pData, iBitOld ); + // copy the primary input data + iBitNew = iBitOld; + for ( i = 0; i <= pCexNew->iFrame; i++ ) + { + Vec_IntForEachEntry( vInputMap, Entry, k ) + { + if ( Entry == -1 ) + continue; + if ( Aig_InfoHasBit( pCexOld->pData, iBitOld + Entry ) ) + Aig_InfoSetBit( pCexNew->pData, iBitNew + k ); + } + iBitOld += Saig_ManPiNum(p); + iBitNew += Saig_ManPiNum(pInit); + } + assert( iBitOld < iBitNew ); + assert( iBitOld == pCexOld->nBits ); + assert( iBitNew == pCexNew->nBits ); + Vec_IntFree( vInputMap ); + pInit->pSeqModel = pCexNew; + Aig_ManStop( p ); + return 0; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 82df6008..ee9f6d3c 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "cecInt.h" +#include "giaAig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -44,7 +45,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) int i; assert( p->pCexComb == NULL ); p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, - sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) ); + sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) ); p->pCexComb->iPo = iOut; p->pCexComb->nPis = Gia_ManCiNum(p); p->pCexComb->nBits = Gia_ManCiNum(p); diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 49930836..5a52e913 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -111,14 +111,14 @@ int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords ) { for ( w = 0; w < nWords; w++ ) if ( p[w] != ~0 ) - return 32*w + Aig_WordFindFirstBit( ~p[w] ); + return 32*w + Gia_WordFindFirstBit( ~p[w] ); return -1; } else { for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) - return 32*w + Aig_WordFindFirstBit( p[w] ); + return 32*w + Gia_WordFindFirstBit( p[w] ); return -1; } } @@ -141,14 +141,14 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords ) { for ( w = 0; w < nWords; w++ ) if ( p0[w] != p1[w] ) - return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] ); + return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] ); return -1; } else { for ( w = 0; w < nWords; w++ ) if ( p0[w] != ~p1[w] ) - return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] ); + return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] ); return -1; } } @@ -467,7 +467,7 @@ void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined ) int * pTable, nTableSize, i, k, Key; if ( Vec_IntSize(vRefined) == 0 ) return; - nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); + nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); pTable = ABC_CALLOC( int, nTableSize ); Vec_IntForEachEntry( vRefined, i, k ) { @@ -519,15 +519,15 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) assert( p->pCexComb == NULL ); assert( iPat >= 0 && iPat < 32 * p->nWords ); p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, - sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) ); + sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) ); p->pCexComb->iPo = p->iOut; p->pCexComb->nPis = Gia_ManCiNum(p->pAig); p->pCexComb->nBits = Gia_ManCiNum(p->pAig); for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) { pInfo = Vec_PtrEntry( p->vCiSimInfo, i ); - if ( Aig_InfoHasBit( pInfo, iPat ) ) - Aig_InfoSetBit( p->pCexComb->pData, i ); + if ( Gia_InfoHasBit( pInfo, iPat ) ) + Gia_InfoSetBit( p->pCexComb->pData, i ); } } @@ -560,8 +560,8 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); - if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) ) - Aig_InfoXorBit( p->pBestState->pData, i ); + if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) ) + Gia_InfoXorBit( p->pBestState->pData, i ); } p->pBestState->iPo = ScoreBest; } @@ -686,7 +686,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * else { for ( w = 1; w <= p->nWords; w++ ) - pRes[w] = Aig_ManRandom( 0 ); + pRes[w] = Gia_ManRandom( 0 ); } // make sure the first pattern is always zero pRes[1] ^= (pRes[1] & 1); @@ -798,7 +798,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v { pRes0 = Vec_PtrEntry( vInfoCis, i ); for ( w = 0; w < p->nWords; w++ ) - pRes0[w] = Aig_ManRandom( 0 ); + pRes0[w] = Gia_ManRandom( 0 ); } for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { @@ -814,7 +814,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v { pRes0 = Vec_PtrEntry( vInfoCis, i ); for ( w = 0; w < p->nWords; w++ ) - pRes0[w] = Aig_ManRandom( 0 ); + pRes0[w] = Gia_ManRandom( 0 ); } } } diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 7759428e..ca0a3665 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -246,7 +246,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) if ( pPars->fSeqSimulate ) printf( "Performing sequential simulation of %d frames with %d words.\n", pPars->nRounds, pPars->nWords ); - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); pSim = Cec_ManSimStart( pAig, pPars ); if ( pAig->pReprs == NULL ) RetValue = Cec_ManSimClassesPrepare( pSim ); @@ -283,7 +283,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) double clkTotal = clock(); // duplicate AIG and transfer equivalence classes - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); pIni = Gia_ManDup(pAig); pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL; pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL; @@ -420,7 +420,8 @@ p->timeSat += clock() - clk; printf( "Switching into reduced mode.\n" ); pPars->fColorDiff = 0; } - if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) +// if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) + else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) ) { if ( p->pPars->fVerbose ) printf( "Switching into normal mode.\n" ); @@ -431,6 +432,11 @@ p->timeSat += clock() - clk; finalize: if ( p->pPars->fVerbose ) { + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig), + 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), + Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig), + 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal ); ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal ); ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal ); diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 05259bc7..dccd90b0 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -49,6 +49,11 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f ); return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); } + if ( f == 0 ) + { + assert( Gia_ObjIsRo(p, pObj) ); + return Gia_ObjCopyF(p, f, pObj); + } assert( f && Gia_ObjIsRo(p, pObj) ); pObj = Gia_ObjRoToRi( p, pObj ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 ); @@ -107,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 ); Gia_ManForEachRo( p, pObj, i ) @@ -202,6 +207,74 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I /**Function************************************************************* + Synopsis [Derives SRM for signal correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + Vec_Int_t * vXorLits; + int f, i, iPrevNew, iObjNew; + assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) ); + assert( Gia_ManRegNum(p) > 0 ); + assert( p->pReprs != NULL ); + p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + { + Gia_ManAppendCi(pNew); + Gia_ObjSetCopyF( p, 0, pObj, 0 ); + } + for ( f = 0; f < nFrames+fScorr; f++ ) + { + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); + } + *pvOutputs = Vec_IntAlloc( 1000 ); + vXorLits = Vec_IntAlloc( 1000 ); + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachObj1( p, pObj, i ) + { + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + continue; + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + if ( iPrevNew != iObjNew ) + { + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); + } + } + } + Vec_IntForEachEntry( vXorLits, iObjNew, i ) + Gia_ManAppendCo( pNew, iObjNew ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + ABC_FREE( p->pCopies ); +//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); + pNew = Gia_ManCleanup( pTemp = pNew ); +//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Initializes simulation info for lcorr/scorr counter-examples.] Description [] @@ -227,7 +300,7 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops ) { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom( 0 ); + pInfo[w] = Gia_ManRandom( 0 ); } } @@ -351,17 +424,17 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Aig_InfoHasBit( pPres, iBit ) && - Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + if ( Gia_InfoHasBit( pPres, iBit ) && + Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Aig_InfoSetBit( pPres, iBit ); - if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Aig_InfoXorBit( pInfo, iBit ); + Gia_InfoSetBit( pPres, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + Gia_InfoXorBit( pInfo, iBit ); } return 1; } @@ -403,7 +476,7 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS for ( k = 1; k < nBits; k++ ) if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) break; - kMax = AIG_MAX( kMax, k ); + kMax = ABC_MAX( kMax, k ); if ( k == nBits-1 ) break; } @@ -443,8 +516,8 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i { iLit = Vec_IntEntry( vCexStore, iStart++ ); pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); - if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) - Aig_InfoXorBit( pInfo, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) + Gia_InfoXorBit( pInfo, iBit ); } if ( ++iBit == nBits ) break; @@ -591,7 +664,11 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int } CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; - printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits ); + if ( iIter == -1 ) + printf( "BMC : " ); + else + printf( "%3d : ", iIter ); + printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); if ( vStatus ) Vec_StrForEachEntry( vStatus, Entry, i ) { @@ -638,7 +715,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); return NULL; } - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; @@ -704,14 +781,57 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); } + // check the base case + if ( !pPars->fLatchCorr || pPars->nFrames > 1 ) + { + int fChanges = 1; + while ( fChanges ) + { + int clkBmc = clock(); + fChanges = 0; + pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + if ( Gia_ManPoNum(pSrm) == 0 ) + { + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + break; + } + pParsSat->nBTLimit *= 10; + if ( pPars->fUseCSat ) + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + else + vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); + // refine classes with these counter-examples + if ( Vec_IntSize(vCexStore) ) + { + clk2 = clock(); + RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames ); + clkSim += clock() - clk2; + Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); + fChanges = 1; + } + if ( pPars->fVerbose ) + Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc ); + // recycle + Vec_IntFree( vCexStore ); + Vec_StrFree( vStatus ); + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + } + } + else + { + if ( pPars->fVerbose ) + Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk ); + } + // check the overflow if ( r == 100000 ) printf( "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); clkTotal = clock() - clkTotal; - if ( pPars->fVerbose ) - Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk ); // derive reduced AIG Gia_ManSetProvedNodes( pAig ); + Gia_ManEquivImprove( pAig ); pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 ); //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); pNew = Gia_ManSeqCleanup( pTemp = pNew ); diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c index ddb539c2..d9aa5240 100644 --- a/src/aig/cec/cecIso.c +++ b/src/aig/cec/cecIso.c @@ -125,7 +125,7 @@ static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords ) unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id ); int w; for ( w = 0; w < nWords; w++ ) - pInfo0[w] = Aig_ManRandom( 0 ); + pInfo0[w] = Gia_ManRandom( 0 ); } /**Function************************************************************* @@ -314,7 +314,7 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p ) // start simulation info pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords ); // simulate and create table - nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 ); + nTableSize = Gia_PrimeCudd( 100 + Gia_ManObjNum(p)/2 ); pTable = ABC_CALLOC( int, nTableSize ); Gia_ManCleanValue( p ); Gia_ManForEachObj1( p, pObj, i ) diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c index a5be4c1c..8537fe4a 100644 --- a/src/aig/cec/cecPat.c +++ b/src/aig/cec/cecPat.c @@ -414,17 +414,17 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Aig_InfoHasBit( pPres, iBit ) && - Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + if ( Gia_InfoHasBit( pPres, iBit ) && + Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Aig_InfoSetBit( pPres, iBit ); - if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Aig_InfoXorBit( pInfo, iBit ); + Gia_InfoSetBit( pPres, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + Gia_InfoXorBit( pInfo, iBit ); } return 1; } @@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW int nBits = 32 * nWords; int clk = clock(); vInfo = Vec_PtrAllocSimInfo( nInputs, nWords ); - Aig_ManRandomInfo( vInfo, 0, 0, nWords ); + Gia_ManRandomInfo( vInfo, 0, 0, nWords ); vPres = Vec_PtrAllocSimInfo( nInputs, nWords ); Vec_PtrCleanSimInfo( vPres, 0, nWords ); while ( pMan->iStart < Vec_StrSize(pMan->vStorage) ) @@ -460,11 +460,11 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) ) if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) break; - kMax = AIG_MAX( kMax, k ); + kMax = ABC_MAX( kMax, k ); if ( k == nBits-1 ) { Vec_PtrReallocSimInfo( vInfo ); - Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords ); + Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords ); Vec_PtrReallocSimInfo( vPres ); Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords ); nWords *= 2; @@ -511,7 +511,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg vInfo = Vec_PtrAllocSimInfo( nInputs, nWords ); Vec_PtrCleanSimInfo( vInfo, 0, nWords ); - Aig_ManRandomInfo( vInfo, nRegs, 0, nWords ); + Gia_ManRandomInfo( vInfo, nRegs, 0, nWords ); vPres = Vec_PtrAllocSimInfo( nInputs, nWords ); Vec_PtrCleanSimInfo( vPres, 0, nWords ); @@ -538,12 +538,12 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg // RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ); // assert( RetValue == 1 ); - kMax = AIG_MAX( kMax, k ); + kMax = ABC_MAX( kMax, k ); if ( k == nBits-1 ) { Vec_PtrReallocSimInfo( vInfo ); Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords ); - Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords ); + Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords ); Vec_PtrReallocSimInfo( vPres ); Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords ); diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 3d05172f..28f3a637 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -51,7 +51,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0; + pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0; } */ for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) @@ -65,16 +65,16 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t { pInfo = Vec_PtrEntry( vInfo, k++ ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom(0); + pInfo[w] = Gia_ManRandom(0); // set simulation pattern and make sure it is second (first will be erased during simulation) - pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i ); + pInfo[0] = (pInfo[0] << 1) | Gia_InfoHasBit( pCex->pData, i ); pInfo[0] <<= 1; } for ( ; k < Vec_PtrSize(vInfo); k++ ) { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom(0); + pInfo[w] = Gia_ManRandom(0); } } @@ -100,14 +100,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0; + pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0; } for ( ; k < Vec_PtrSize(vInfo); k++ ) { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom( 0 ); + pInfo[w] = Gia_ManRandom( 0 ); } } @@ -229,7 +229,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex } if ( pPars->fVerbose ) printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 ); - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 ); Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex ); @@ -275,7 +275,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" ); return -1; } - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); // prepare starting pattern pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 ); pState->iFrame = -1; diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index fc2d5d7f..5f032b59 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -369,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) Cec_ObjSetSatNum( p, pObj, 0 ); Vec_PtrClear( p->vUsedNodes ); -// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); +// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) ); sat_solver_delete( p->pSat ); } p->pSat = sat_solver_new(); @@ -636,8 +636,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb if ( Gia_ObjIsCi(pObj) ) { unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); - if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) ) - Aig_InfoXorBit( pInfo, iPat ); + if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) ) + Gia_InfoXorBit( pInfo, iPat ); pSat->nCexLits++; // Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) ); return; diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c index f5e5bd06..1b68efe0 100644 --- a/src/aig/cec/cecSweep.c +++ b/src/aig/cec/cecSweep.c @@ -50,7 +50,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) if ( p->pPars->nLevelMax ) Gia_ManLevelNum( p->pAig ); pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); + pNew->pName = Gia_UtilStrsav( p->pAig->pName ); Gia_ManHashAlloc( pNew ); piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); @@ -70,7 +70,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); - pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); + pDepths[i] = ABC_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) ) continue; assert( Gia_ObjRepr(p->pAig, i) < i ); @@ -109,7 +109,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) ); Vec_IntPush( p->vXorNodes, i ); // add to the depth of this node - pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] ); + pDepths[i] = 1 + ABC_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] ); if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax ) piCopies[i] = -1; } diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c index 63625e6f..58c9b803 100644 --- a/src/aig/cnf/cnfMap.c +++ b/src/aig/cnf/cnfMap.c @@ -123,7 +123,7 @@ void Cnf_DeriveMapping( Cnf_Man_t * p ) // Aig_ObjCollectSuper( pObj, vSuper ); // get the area flow of this cut // AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows ); - AreaFlow = AIG_INFINITY; + AreaFlow = ABC_INFINITY; if ( AreaFlow >= (int)pCutBest->uSign ) { pAreaFlows[pObj->Id] = pCutBest->uSign; diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index 3c8423cf..83b6e08e 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -151,7 +151,7 @@ p->timeCuts += clock() - clk; // evaluate the cuts p->GainBest = -1; - Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY; + Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY; Dar_ObjForEachCut( pObj, pCut, k ) Dar_LibEval( p, pObj, pCut, Required ); // check the best gain @@ -292,7 +292,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose Dar_ObjCutPrint( pAig, pObj ); */ } - // ABC_FREE the cuts + // free the cuts pMemCuts = p->pMemCuts; p->pMemCuts = NULL; // Dar_ManCutsFree( p ); diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index c5fd4696..cfa4594d 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -472,7 +472,7 @@ void Dar_LibPrepare( int nSubgraphs ) if ( i == 1 ) // special classes p->nSubgr0[i] = p->nSubgr[i]; else - p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs ); + p->nSubgr0[i] = ABC_MIN( p->nSubgr[i], nSubgraphs ); p->nSubgr0Total += p->nSubgr0[i]; for ( k = 0; k < p->nSubgr0[i]; k++ ) p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ]; @@ -494,7 +494,7 @@ void Dar_LibPrepare( int nSubgraphs ) for ( k = 0; k < p->nSubgr0[i]; k++ ) Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 ); p->nNodes0Total += p->nNodes0[i]; - p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] ); + p->nNodes0Max = ABC_MAX( p->nNodes0Max, p->nNodes0[i] ); } // clean node counters @@ -799,7 +799,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot ) assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 ); pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num; pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num; - pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level); + pData->Level = 1 + ABC_MAX(pData0->Level, pData1->Level); if ( pData0->pFunc == NULL || pData1->pFunc == NULL ) continue; pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 ); diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index f64564fa..6118dd71 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -267,7 +267,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K return -1; } // count the number of new levels - LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level ); + LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level ); if ( pAnd ) { if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) ) @@ -527,7 +527,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) //printf( "\nConsidering node %d.\n", pObj->Id ); // get the bounded MFFC size clk = clock(); - nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 ); + nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 ); nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut ); if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider { @@ -564,7 +564,7 @@ p->timeCuts += clock() - clk; // try the cuts clk = clock(); - Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY; + Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY; Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required ); p->timeEval += clock() - clk; diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c index d8fbe8ed..9f4bd68c 100644 --- a/src/aig/dch/dchClass.c +++ b/src/aig/dch/dchClass.c @@ -544,7 +544,7 @@ void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, { int i, Limit; Vec_PtrClear( vRoots ); - Limit = AIG_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) ); + Limit = ABC_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) ); for ( i = pObj->Id; i < Limit; i++ ) { pObj = Aig_ManObj( p->pAig, i ); diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index 61d2ab93..4f31b928 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -183,7 +183,7 @@ void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); Dch_ManResimulateSolved_rec( p, pObj ); Dch_ManResimulateSolved_rec( p, pRepr ); - p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis ); + p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis ); // resimulate the cone of influence of the other nodes Vec_PtrForEachEntry( p->vSimRoots, pRoot, i ) Dch_ManResimulateOther_rec( p, pRoot ); @@ -233,7 +233,7 @@ void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); Dch_ManResimulateSolved_rec( p, pObj ); Dch_ManResimulateSolved_rec( p, pRepr ); - p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis ); + p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis ); // resimulate the cone of influence of the other nodes Vec_PtrForEachEntry( p->vSimRoots, pRoot, i ) Dch_ManResimulateOther_rec( p, pRoot ); diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index 689d7d67..7b08d74d 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -360,7 +360,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) ); printf( "\n" ); } - // ABC_FREE the BMC manager + // free the BMC manager Fra_BmcStop( p->pBmc ); p->pBmc = NULL; } diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 0cc6748c..b7a78050 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -136,7 +136,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi { pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); } - // ABC_FREE the sat_solver + // free the sat_solver if ( fVerbose ) Sat_SolverPrintStats( stdout, pSat ); //sat_solver_store_write( pSat, "trace.cnf" ); @@ -318,7 +318,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) ); fflush( stdout ); } - // ABC_FREE intermediate results + // free intermediate results Vec_PtrForEachEntry( vParts, pAig, i ) Aig_ManStop( pAig ); Vec_PtrFree( vParts ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 8554b312..94cac80a 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -652,7 +652,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) if ( pRepr == NULL ) continue; pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id ); - WeightMax = AIG_MAX( WeightMax, pWeights[i] ); + WeightMax = ABC_MAX( WeightMax, pWeights[i] ); } Fra_SmlStop( pComb ); printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) ); @@ -710,7 +710,7 @@ void Fra_ClassesSelectRepr( Fra_Cla_t * p ) // collect support sizes and find the min-support node cMinSupp = -1; pNodeMin = NULL; - nSuppSizeMin = AIG_INFINITY; + nSuppSizeMin = ABC_INFINITY; for ( c = 0; pClass[c]; c++ ) { nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] ); diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index d579146e..716e83d5 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -290,8 +290,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, ***********************************************************************/ int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 ) { - int Max1 = AIG_MAX( pImp1[0], pImp1[1] ); - int Max2 = AIG_MAX( pImp2[0], pImp2[1] ); + int Max1 = ABC_MAX( pImp1[0], pImp1[1] ); + int Max2 = ABC_MAX( pImp2[0], pImp2[1] ); if ( Max1 < Max2 ) return -1; if ( Max1 > Max2 ) @@ -323,7 +323,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in Vec_Ptr_t * vNodes; int * pImpCosts, * pNodesI, * pNodesK; int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; - int CostMin = AIG_INFINITY, CostMax = 0; + int CostMin = ABC_INFINITY, CostMax = 0; int i, k, Imp, CostRange, clk = clock(); assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) ); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); @@ -364,8 +364,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in nImpsCollected++; Imp = Fra_ImpCreate( *pNodesI, *pNodesK ); pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK); - CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] ); - CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] ); + CostMin = ABC_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] ); + CostMax = ABC_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] ); Vec_IntPush( vImps, Imp ); if ( Vec_IntSize(vImps) == nImpMaxLimit ) goto finish; @@ -508,7 +508,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in continue; Left = Fra_ImpLeft(Imp); Right = Fra_ImpRight(Imp); - Max = AIG_MAX( Left, Right ); + Max = ABC_MAX( Left, Right ); assert( Max >= pNode->Id ); if ( Max > pNode->Id ) return i; diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 4f3812c6..84b739a4 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -629,7 +629,7 @@ p->timeTotal = clock() - clk; p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); p->nNodesEnd = Aig_ManNodeNum(pManAigNew); p->nRegsEnd = Aig_ManRegNum(pManAigNew); - // ABC_FREE the manager + // free the manager finish: Fra_ManStop( p ); // check the output diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index c2eaf453..039a660f 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -539,7 +539,7 @@ clk = clock(); Aig_ManIncrementTravId( p->pManFraig ); // determine the min and max level to visit assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 ); - LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) ); + LevelMax = ABC_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) ); LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio)); // traverse if ( pOld && !Aig_ObjIsConst1(pOld) ) diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index a97af278..8064d2ee 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -170,7 +170,7 @@ clk = clock(); if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); - TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + TimeLeft = ABC_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { if ( !pParSec->fSilent ) @@ -240,7 +240,7 @@ ABC_PRT( "Time", clock() - clk ); if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); - TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + TimeLeft = ABC_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { if ( !pParSec->fSilent ) @@ -275,7 +275,7 @@ ABC_PRT( "Time", clock() - clk ); if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); - TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + TimeLeft = ABC_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { if ( !pParSec->fSilent ) @@ -315,7 +315,7 @@ ABC_PRT( "Time", clock() - clk ); if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); - TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + TimeLeft = ABC_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { if ( !pParSec->fSilent ) diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index aff21219..4f164e5c 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -436,7 +436,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) Aig_ManForEachPi( p->pAig, pObj, i ) Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); // flip one bit - Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); + Limit = ABC_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 ); } @@ -458,7 +458,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) // flip one bit of the last frame if ( fUseDist1 ) //&& p->nFrames == 2 ) { - Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); + Limit = ABC_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); } diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 5395f361..feee5472 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -24,8 +24,14 @@ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// - -#include "aig.h" + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> + +#include "vec.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -124,6 +130,7 @@ struct Gia_Man_t_ int nFansAlloc; // the size of fanout representation int * pMapping; // mapping for each node Gia_Cex_t * pCexComb; // combinational counter-example + Gia_Cex_t * pCexSeq; // sequential counter-example int * pCopies; // intermediate copies Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc unsigned char* pSwitching; // switching activity for each object @@ -174,6 +181,36 @@ extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p ); extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); +static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; } +static inline int Gia_Float2Int( float Val ) { return *((int *)&Val); } +static inline float Gia_Int2Float( int Num ) { return *((float *)&Num); } +static inline int Gia_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } +static inline int Gia_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; } +static inline char * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; } +static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } +static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } +static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } +static inline int Gia_WordCountOnes( unsigned uWord ) +{ + uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); + uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); + uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); + uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); + return (uWord & 0x0000FFFF) + (uWord>>16); +} +static inline int Gia_WordFindFirstBit( unsigned uWord ) +{ + int i; + for ( i = 0; i < 32; i++ ) + if ( uWord & (1 << i) ) + return i; + return -1; +} + static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; } @@ -265,8 +302,8 @@ static inline int Gia_ObjValue( Gia_Obj_t * pObj ) { static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLevels);return p->pLevels[Gia_ObjId(p, pObj)]; } static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; } -static inline void Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]++; } -static inline void Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]--; } +static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; } +static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; } static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); } static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); } static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); } @@ -368,6 +405,7 @@ static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; } static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; } +static inline void Gia_ObjUnsetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 0; } static inline int Gia_ObjFailed( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fFailed; } static inline void Gia_ObjSetFailed( Gia_Man_t * p, int Id ) { p->pReprs[Id].fFailed = 1; } @@ -451,10 +489,6 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== giaAig.c =============================================================*/ -extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); -extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); -extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ); /*=== giaAiger.c ===========================================================*/ extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ); extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); @@ -509,6 +543,7 @@ extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); +extern void Gia_ManEquivImprove( Gia_Man_t * p ); /*=== giaFanout.c =========================================================*/ extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); @@ -530,7 +565,7 @@ extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ); extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ); extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 ); -extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ); extern void Gia_ManHashProfile( Gia_Man_t * p ); /*=== giaLogic.c ===========================================================*/ extern void Gia_ManTestDistance( Gia_Man_t * p ); @@ -567,6 +602,10 @@ extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, /*=== giaTsim.c ============================================================*/ extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose ); /*=== giaUtil.c ===========================================================*/ +extern unsigned Gia_ManRandom( int fReset ); +extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop ); +extern unsigned int Gia_PrimeCudd( unsigned int p ); +extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ); extern void Gia_ManSetMark0( Gia_Man_t * p ); extern void Gia_ManCleanMark0( Gia_Man_t * p ); extern void Gia_ManCheckMark0( Gia_Man_t * p ); @@ -589,7 +628,7 @@ extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ); extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ); extern void Gia_ManPrintCounterExample( Gia_Cex_t * p ); - +extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); #ifdef __cplusplus } diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 1c341d6f..601b85af 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "gia.h" +#include "giaAig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h new file mode 100644 index 00000000..07cf7bae --- /dev/null +++ b/src/aig/gia/giaAig.h @@ -0,0 +1,62 @@ +/**CFile**************************************************************** + + FileName [giaAig.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __GIA_AIG_H__ +#define __GIA_AIG_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig.h" +#include "gia.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== giaAig.c =============================================================*/ +extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); +extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); +extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index adc58e6c..8dbc0cab 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -143,7 +143,7 @@ int Gia_FileSize( char * pFileName ) char * Gia_FileNameGeneric( char * FileName ) { char * pDot, * pRes; - pRes = Aig_UtilStrsav( FileName ); + pRes = Gia_UtilStrsav( FileName ); if ( (pDot = strrchr( pRes, '.' )) ) *pDot = 0; return pRes; @@ -412,7 +412,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) // allocate the empty AIG pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); pName = Gia_FileNameGeneric( pFileName ); - pNew->pName = Aig_UtilStrsav( pName ); + pNew->pName = Gia_UtilStrsav( pName ); // pNew->pSpec = Aig_UtilStrsav( pFileName ); ABC_FREE( pName ); @@ -549,7 +549,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) pCur++; // read model name ABC_FREE( pNew->pName ); - pNew->pName = Aig_UtilStrsav( pCur ); + pNew->pName = Gia_UtilStrsav( pCur ); } } diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 15faea72..832eff26 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -20,6 +20,9 @@ #include "gia.h" +//#define gia_assert(exp) ((void)0) +//#define gia_assert(exp) (assert(exp)) + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index b256100c..da48c1b0 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -580,7 +580,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p ) } // allocate storage for fanin/fanout numbers - nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); + nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) ); vFanins = Vec_IntStart( nSizeMax ); vFanouts = Vec_IntStart( nSizeMax ); @@ -714,7 +714,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar ) return NULL; } pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 2510f572..bd5297e4 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -168,7 +168,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCo( p, pObj, i ) Gia_ManDupOrderDfs_rec( pNew, p, pObj ); @@ -200,7 +200,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCoReverse( p, pObj, i ) Gia_ManDupOrderDfs_rec( pNew, p, pObj ); @@ -232,7 +232,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -265,7 +265,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { @@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ) Gia_Obj_t * pObj; int i, iCtrl; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; @@ -337,7 +337,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ) int i, Counter1 = 0, Counter2 = 0; assert( p->vFlopClasses != NULL ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachPi( p, pObj, i ) @@ -381,7 +381,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) int i, nRos = 0, nRis = 0; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { @@ -426,7 +426,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ) int i, t, Entry; assert( nTimes > 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes ); vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes ); @@ -536,7 +536,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCo( p, pObj, i ) Gia_ManDupDfs2_rec( pNew, p, pObj ); @@ -594,7 +594,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -625,7 +625,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -655,7 +655,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot ) assert( Gia_ObjIsCo(pRoot) ); Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ) int i, iLit, iLitRes; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -712,7 +712,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -743,7 +743,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManSetRefs( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -797,7 +797,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) { @@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ) assert( p->pReprsOld != NULL ); Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -1064,7 +1064,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq } // start the manager pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) ); - pNew->pName = Aig_UtilStrsav( "miter" ); + pNew->pName = Gia_UtilStrsav( "miter" ); // map combinational inputs Gia_ManFillValue( p0 ); Gia_ManFillValue( p1 ); @@ -1161,7 +1161,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ) int i, iLit; assert( (Gia_ManPoNum(p) & 1) == 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManHashAlloc( pNew ); Gia_ManForEachCi( p, pObj, i ) diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c index fa172f70..bd14eea9 100644 --- a/src/aig/gia/giaEmbed.c +++ b/src/aig/gia/giaEmbed.c @@ -691,7 +691,7 @@ void Emb_ManPrintFanio( Emb_Man_t * p ) } // allocate storage for fanin/fanout numbers - nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); + nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) ); vFanins = Vec_IntStart( nSizeMax ); vFanouts = Vec_IntStart( nSizeMax ); @@ -836,14 +836,14 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p ) int nAttempts = 20; int i, iNode, Dist, clk; Emb_Obj_t * pPivot, * pNext; - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); Emb_ManResetTravId( p ); // compute distances from several randomly selected PIs clk = clock(); printf( "From inputs: " ); for ( i = 0; i < nAttempts; i++ ) { - iNode = Aig_ManRandom( 0 ) % Emb_ManCiNum(p); + iNode = Gia_ManRandom( 0 ) % Emb_ManCiNum(p); pPivot = Emb_ManCi( p, iNode ); if ( Emb_ObjFanoutNum(pPivot) == 0 ) { i--; continue; } @@ -859,7 +859,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p ) printf( "From outputs: " ); for ( i = 0; i < nAttempts; i++ ) { - iNode = Aig_ManRandom( 0 ) % Emb_ManCoNum(p); + iNode = Gia_ManRandom( 0 ) % Emb_ManCoNum(p); pPivot = Emb_ManCo( p, iNode ); pNext = Emb_ObjFanin( pPivot, 0 ); if ( !Emb_ObjIsNode(pNext) ) @@ -873,7 +873,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p ) printf( "From nodes: " ); for ( i = 0; i < nAttempts; i++ ) { - iNode = Aig_ManRandom( 0 ) % Gia_ManObjNum(p->pGia); + iNode = Gia_ManRandom( 0 ) % Gia_ManObjNum(p->pGia); if ( !~Gia_ManObj(p->pGia, iNode)->Value ) { i--; continue; } pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value ); @@ -1043,7 +1043,7 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p ) { Emb_Obj_t * pPivot; do { - int iNode = (911 * Aig_ManRandom(0)) % Gia_ManObjNum(p->pGia); + int iNode = (911 * Gia_ManRandom(0)) % Gia_ManObjNum(p->pGia); if ( ~Gia_ManObj(p->pGia, iNode)->Value ) pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value ); else @@ -1240,7 +1240,7 @@ void Emb_ManVecRandom( float * pVec, int nDims ) { int i; for ( i = 0; i < nDims; i++ ) - pVec[i] = Aig_ManRandom( 0 ); + pVec[i] = Gia_ManRandom( 0 ); } /**Function************************************************************* @@ -1702,7 +1702,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" ); return; } - sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") ); + sprintf( Buffer, "%s%s", pDirectory, Gia_FileNameGenericAppend(pName, ".plt") ); pFile = fopen( Buffer, "w" ); fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() ); fprintf( pFile, "\n" ); @@ -1712,7 +1712,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI { // fprintf( pFile, "set terminal postscript\n" ); fprintf( pFile, "set terminal gif font \'arial\' 10 size 800,600 xffffff x000000 x000000 x000000\n" ); - fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".gif") ); + fprintf( pFile, "set output \'%s\'\n", Gia_FileNameGenericAppend(pName, ".gif") ); fprintf( pFile, "\n" ); } fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d HPWL = %.2e\\n", @@ -1806,7 +1806,7 @@ clk = clock(); // Emb_ManPrintFanio( p ); // prepare data-structure - Aig_ManRandom( 1 ); // reset random numbers for deterministic behavior + Gia_ManRandom( 1 ); // reset random numbers for deterministic behavior Emb_ManResetTravId( p ); Emb_ManSetValue( p ); clkSetup = clock() - clk; diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c index 13d6145c..c768bb43 100644 --- a/src/aig/gia/giaEnable.c +++ b/src/aig/gia/giaEnable.c @@ -362,7 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames ) ABC_FREE( p->pCopies ); p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) Gia_ObjSetCopyF( p, 0, pObj, 0 ); @@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p ) Gia_Obj_t * pThis, * pNode; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; @@ -607,7 +607,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p ) pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 79345fd0..f802e15d 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -330,7 +330,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV if ( fDualOut ) Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) if ( fDualOut ) Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -809,10 +809,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames if ( fDualOut ) Gia_ManEquivSetColors( p, 0 ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) - Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) ); + Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) ); for ( f = 0; f < nFrames; f++ ) { Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); @@ -906,6 +906,66 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ) nRemovedClas, nTotalClas, nRemovedLits, nTotalLits ); } +/**Function************************************************************* + + Synopsis [Transforms equiv classes by setting a good representative.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEquivImprove( Gia_Man_t * p ) +{ + Vec_Int_t * vClass; + int i, k, iNode, iRepr; + int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur; + assert( p->pReprs != NULL && p->pNexts != NULL ); + Gia_ManLevelNum( p ); + Gia_ManCreateRefs( p ); + // iterate over class candidates + vClass = Vec_IntAlloc( 100 ); + Gia_ManForEachClass( p, i ) + { + Vec_IntClear( vClass ); + iReprBest = -1; + iLevelBest = iMffcBest = ABC_INFINITY; + Gia_ClassForEachObj( p, i, k ) + { + iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) ); + iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) ); + if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) ) + { + iReprBest = k; + iLevelBest = iLevelCur; + iMffcBest = iMffcCur; + } + Vec_IntPush( vClass, k ); + } + assert( Vec_IntSize( vClass ) > 1 ); + assert( iReprBest > 0 ); + if ( i == iReprBest ) + continue; +/* + printf( "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n", + i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ), + Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) ); +*/ + iRepr = iReprBest; + Gia_ObjSetRepr( p, iRepr, GIA_VOID ); + Gia_ObjSetProved( p, i ); + Gia_ObjUnsetProved( p, iRepr ); + Vec_IntForEachEntry( vClass, iNode, k ) + if ( iNode != iRepr ) + Gia_ObjSetRepr( p, iNode, iRepr ); + } + Vec_IntFree( vClass ); + ABC_FREE( p->pNexts ); +// p->pNexts = Gia_ManDeriveNexts( p ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaFanout.c b/src/aig/gia/giaFanout.c index 42ccd7e7..b32484af 100644 --- a/src/aig/gia/giaFanout.c +++ b/src/aig/gia/giaFanout.c @@ -117,7 +117,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ) assert( Gia_ObjId(p, pFanout) > 0 ); if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc ) { - int nFansAlloc = 2 * AIG_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) ); + int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) ); p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc ); memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) ); p->nFansAlloc = nFansAlloc; diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c index cf4c4aa5..04c8f2e7 100644 --- a/src/aig/gia/giaForce.c +++ b/src/aig/gia/giaForce.c @@ -747,7 +747,7 @@ void Frc_ManPlaceRandom( Frc_Man_t * p ) pPlacement[i] = i; for ( i = 0; i < p->nObjs; i++ ) { - iNext = Aig_ManRandom( 0 ) % p->nObjs; + iNext = Gia_ManRandom( 0 ) % p->nObjs; Temp = pPlacement[i]; pPlacement[i] = pPlacement[iNext]; pPlacement[iNext] = Temp; @@ -774,7 +774,7 @@ void Frc_ManArrayShuffle( Vec_Int_t * vArray ) int i, iNext, Temp; for ( i = 0; i < vArray->nSize; i++ ) { - iNext = Aig_ManRandom( 0 ) % vArray->nSize; + iNext = Gia_ManRandom( 0 ) % vArray->nSize; Temp = vArray->pArray[i]; vArray->pArray[i] = vArray->pArray[iNext]; vArray->pArray[iNext] = Temp; @@ -1036,7 +1036,7 @@ void Frc_DumpGraphIntoFile( Frc_Man_t * p ) void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose ) { Frc_Man_t * p; - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); if ( fClustered ) p = Frc_ManStart( pGia ); else diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index e99ef514..c0ea6680 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -180,7 +180,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) Gia_ManFraSupports( p ); pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+ Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pName = Gia_UtilStrsav( pAig->pName ); Gia_ManHashAlloc( pFrames ); Gia_ManConst0(pAig)->Value = 0; for ( f = 0; f < pPars->nFrames; f++ ) @@ -290,7 +290,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) if ( pPars->fInit ) return Gia_ManFramesInit( pAig, pPars ); pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pName = Gia_UtilStrsav( pAig->pName ); Gia_ManHashAlloc( pFrames ); Gia_ManConst0(pAig)->Value = 0; for ( f = 0; f < pPars->nFrames; f++ ) diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c index ee9e5b5f..b3a3c2d0 100644 --- a/src/aig/gia/giaFront.c +++ b/src/aig/gia/giaFront.c @@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p ) Gia_ManSetRefs( p ); // start the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit); // start the frontier pFront = ABC_CALLOC( char, pNew->nFront ); diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c index 443a1ae8..ed636540 100644 --- a/src/aig/gia/giaGlitch.c +++ b/src/aig/gia/giaGlitch.c @@ -330,7 +330,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode ) int i, Phase = 0; for ( i = 0; i < (int)pNode->nFanins; i++ ) Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i); - return Aig_InfoHasBit( pNode->uTruth, Phase ); + return Gia_InfoHasBit( pNode->uTruth, Phase ); } /**Function************************************************************* @@ -349,7 +349,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode ) int i, Phase = 0; for ( i = 0; i < (int)pNode->nFanins; i++ ) Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i); - return Aig_InfoHasBit( pNode->uTruth, Phase ); + return Gia_InfoHasBit( pNode->uTruth, Phase ); } /**Function************************************************************* @@ -429,7 +429,7 @@ void Gli_ManSetPiRandom( Gli_Man_t * p, float PiTransProb ) assert( 0.0 < PiTransProb && PiTransProb < 1.0 ); Vec_IntClear( p->vCisChanged ); Gli_ManForEachCi( p, pObj, i ) - if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb ) + if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb ) { Vec_IntPush( p->vCisChanged, pObj->Handle ); pObj->fPhase ^= 1; @@ -590,7 +590,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode ) for ( k = 0; k < nFanins; k++ ) if ( (pSimInfos[k] >> i) & 1 ) Phase |= (1 << k); - if ( Aig_InfoHasBit( pNode->uTruth, Phase ) ) + if ( Gia_InfoHasBit( pNode->uTruth, Phase ) ) Result |= (1 << i); } return Result; @@ -612,9 +612,9 @@ static inline unsigned Gli_ManUpdateRandomInput( unsigned uInfo, float PiTransPr float Multi = 1.0 / (1 << 16); int i; if ( PiTransProb == 0.5 ) - return Aig_ManRandom(0); + return Gia_ManRandom(0); for ( i = 0; i < 32; i++ ) - if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb ) + if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb ) uInfo ^= (1 << i); return uInfo; } @@ -703,7 +703,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb ) // set changed PIs Vec_IntClear( p->vCisChanged ); Gli_ManForEachPi( p, pObj, i ) - if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb ) + if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb ) { Vec_IntPush( p->vCisChanged, pObj->Handle ); pObj->fPhase ^= 1; @@ -738,7 +738,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb ) void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose ) { int i, k, clk = clock(); - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); Gli_ManFinalize( p ); if ( p->nRegs == 0 ) { @@ -752,7 +752,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb } else { - int nIters = Aig_BitWordNum(nPatterns); + int nIters = Gia_BitWordNum(nPatterns); Gli_ManSimulateSeqPref( p, 16 ); for ( i = 0; i < 32; i++ ) { diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index a7cae8fe..97326c92 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 ) void Gia_ManHashAlloc( Gia_Man_t * p ) { assert( p->pHTable == NULL ); - p->nHTable = Aig_PrimeCudd( p->nObjsAlloc ); + p->nHTable = Gia_PrimeCudd( p->nObjsAlloc ); p->pHTable = ABC_CALLOC( int, p->nHTable ); } @@ -152,7 +152,7 @@ void Gia_ManHashResize( Gia_Man_t * p ) // replace the table pHTableOld = p->pHTable; nHTableOld = p->nHTable; - p->nHTable = Aig_PrimeCudd( 2 * Gia_ManAndNum(p) ); + p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) ); p->pHTable = ABC_CALLOC( int, p->nHTable ); // rehash the entries from the old table Counter = 0; @@ -322,14 +322,14 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O { Gia_Obj_t * pNode0, * pNode1, * pFanA, * pFanB, * pFanC, * pFanD; assert( p->fAddStrash ); - if ( !Gia_ObjIsAnd(Gia_Regular(p0)) && !Gia_ObjIsAnd(Gia_Regular(p1)) ) - return NULL; pNode0 = Gia_Regular(p0); pNode1 = Gia_Regular(p1); - pFanA = Gia_ObjChild0(pNode0); - pFanB = Gia_ObjChild1(pNode0); - pFanC = Gia_ObjChild0(pNode1); - pFanD = Gia_ObjChild1(pNode1); + if ( !Gia_ObjIsAnd(pNode0) && !Gia_ObjIsAnd(pNode1) ) + return NULL; + pFanA = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild0(pNode0) : NULL; + pFanB = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild1(pNode0) : NULL; + pFanC = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild0(pNode1) : NULL; + pFanD = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild1(pNode1) : NULL; if ( Gia_IsComplement(p0) ) { if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) ) @@ -404,6 +404,7 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O if ( pFanB == pFanD && pFanA == Gia_Not(pFanC) ) return Gia_Not(pFanB); } +/* if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) ) return NULL; if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) ) @@ -424,8 +425,12 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O } pNode0 = Gia_ManHashAndP( p, Gia_Not(pNodeC), pNodeE ); pNode1 = Gia_ManHashAndP( p, pNodeC, pNodeT ); - return Gia_NotCond( Gia_ManHashAndP( p, pNode0, pNode1 ), !fCompl ); + p->fAddStrash = 0; + pNodeC = Gia_NotCond( Gia_ManHashAndP( p, Gia_Not(pNode0), Gia_Not(pNode1) ), !fCompl ); + p->fAddStrash = 1; + return pNodeC; } +*/ return NULL; } @@ -555,13 +560,14 @@ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManRehash( Gia_Man_t * p ) +Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ) { - Gia_Man_t * pNew; + Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->fAddStrash = fAddStrash; Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj( p, pObj, i ) @@ -574,8 +580,11 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } Gia_ManHashStop( pNew ); + pNew->fAddStrash = 0; 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 ); + Gia_ManStop( pTemp ); return pNew; } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index dba90507..f69ac266 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -72,6 +72,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFree( p->vCos ); ABC_FREE( p->pPlacement ); ABC_FREE( p->pSwitching ); + ABC_FREE( p->pCexSeq ); ABC_FREE( p->pCexComb ); ABC_FREE( p->pIso ); ABC_FREE( p->pMapping ); diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c index 965b5981..69dea59d 100644 --- a/src/aig/gia/giaRetime.c +++ b/src/aig/gia/giaRetime.c @@ -122,7 +122,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut ) int i; // create the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); // create the true PIs Gia_ManFillValue( p ); diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c index 6d127223..29ade5c6 100644 --- a/src/aig/gia/giaSat.c +++ b/src/aig/gia/giaSat.c @@ -262,7 +262,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int * (*pnLeaves)++; else Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj); - return AIG_MAX( Level0, Level1 ); + return ABC_MAX( Level0, Level1 ); } /**Function************************************************************* diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 020683ad..ae9e304c 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -64,7 +64,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p ) p->nIters = 32; // the number of timeframes p->TimeLimit = 60; // time limit in seconds p->fCheckMiter = 0; // check if miter outputs are non-zero - p->fVerbose = 1; // enables verbose output + p->fVerbose = 0; // enables verbose output } /**Function************************************************************* @@ -92,7 +92,7 @@ Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) ); p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) ); Vec_IntForEachEntry( pAig->vCis, Entry, i ) - Vec_IntPush( p->vCis2Ids, Entry ); + Vec_IntPush( p->vCis2Ids, i ); // do we need p->vCis2Ids? printf( "AIG = %7.2f Mb. Front mem = %7.2f Mb. Other mem = %7.2f Mb.\n", 12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*p->pAig->nFront/(1<<20), @@ -136,7 +136,7 @@ static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo ) { int w; for ( w = p->nWords-1; w >= 0; w-- ) - pInfo[w] = Aig_ManRandom( 0 ); + pInfo[w] = Gia_ManRandom( 0 ); } /**Function************************************************************* @@ -173,7 +173,7 @@ static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo ) int w; for ( w = p->nWords-1; w >= 0; w-- ) if ( pInfo[w] ) - return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] ); + return 32*(w-1) + Gia_WordFindFirstBit( pInfo[w] ); return -1; } @@ -382,6 +382,71 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p ) /**Function************************************************************* + Synopsis [Returns index of the PO and pattern that failed it.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat ) +{ + int i, iPat; + for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) + { + iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) ); + if ( iPat >= 0 ) + { + *piPo = i; + *piPat = iPat; + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids ) +{ + Gia_Cex_t * p; + unsigned * pData; + int f, i, w, iPioId, Counter; + p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); + p->iFrame = iFrame; + p->iPo = iOut; + // fill in the binary data + Gia_ManRandom( 1 ); + Counter = p->nRegs; + pData = ABC_ALLOC( unsigned, nWords ); + for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) + for ( i = 0; i < Gia_ManPiNum(pAig); i++ ) + { + iPioId = Vec_IntEntry( vCis2Ids, i ); + if ( iPioId >= p->nPis ) + continue; + for ( w = nWords-1; w >= 0; w-- ) + pData[w] = Gia_ManRandom( 0 ); + if ( Gia_InfoHasBit( pData, iPat ) ) + Gia_InfoSetBit( p->pData, Counter + iPioId ); + } + ABC_FREE( pData ); + return p; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -394,40 +459,53 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p ) int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) { Gia_ManSim_t * p; - int i, clk = clock(); + int i, clkTotal = clock(); + int iOut, iPat, RetValue = 0; + ABC_FREE( pAig->pCexSeq ); p = Gia_ManSimCreate( pAig, pPars ); - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); Gia_ManSimInfoInit( p ); for ( i = 0; i < pPars->nIters; i++ ) { Gia_ManSimulateRound( p ); -/* + if ( pPars->fVerbose ) { printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit ); - printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC ); + printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC ); } if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) ) { - assert( pAig->pSeqModel == NULL ); - pAig->pSeqModel = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); - if ( pPars->fVerbose ) - printf( "Miter is satisfiable after simulation (output %d).\n", iOut ); + pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", iOut, i ); + if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + { + printf( "\n" ); + printf( "Generated counter-example is INVALID \n" ); + printf( "\n" ); + } + else + { + printf( "\n" ); + printf( "Generated counter-example is fine \n" ); + printf( "\n" ); + } + RetValue = 1; break; } if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) { - printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit ); + printf( "No bug detected after %d frames with time limit %d seconds. \n", i+1, pPars->TimeLimit ); break; } -*/ + if ( i < pPars->nIters - 1 ) Gia_ManSimInfoTransfer( p ); } Gia_ManSimDelete( p ); - printf( "Simulated %d frames with %d words. ", pPars->nIters, pPars->nWords ); - ABC_PRT( "Time", clock() - clk ); - return 0; + printf( "Simulated %d frames with %d words. ", i, pPars->nWords ); + ABC_PRT( "Time", clock() - clkTotal ); + return RetValue; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index 713f224b..5dac1fbc 100644 --- a/src/aig/gia/giaSwitch.c +++ b/src/aig/gia/giaSwitch.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "gia.h" +#include "giaAig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -146,23 +146,23 @@ static inline void Gia_ManSwiSimInfoRandom( Gia_ManSwi_t * p, unsigned * pInfo, int w, i; if ( nProbNum == -1 ) { // 3/8 = 1/4 + 1/8 - Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) | - (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )); + Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) | + (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )); for ( w = p->nWords-1; w >= 0; w-- ) pInfo[w] ^= Mask; } else if ( nProbNum > 0 ) { - Mask = Aig_ManRandom( 0 ); + Mask = Gia_ManRandom( 0 ); for ( i = 0; i < nProbNum; i++ ) - Mask &= Aig_ManRandom( 0 ); + Mask &= Gia_ManRandom( 0 ); for ( w = p->nWords-1; w >= 0; w-- ) pInfo[w] ^= Mask; } else if ( nProbNum == 0 ) { for ( w = p->nWords-1; w >= 0; w-- ) - pInfo[w] = Aig_ManRandom( 0 ); + pInfo[w] = Gia_ManRandom( 0 ); } else assert( 0 ); @@ -185,14 +185,14 @@ static inline void Gia_ManSwiSimInfoRandomShift( Gia_ManSwi_t * p, unsigned * pI int w, i; if ( nProbNum == -1 ) { // 3/8 = 1/4 + 1/8 - Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) | - (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )); + Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) | + (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )); } else if ( nProbNum >= 0 ) { - Mask = Aig_ManRandom( 0 ); + Mask = Gia_ManRandom( 0 ); for ( i = 0; i < nProbNum; i++ ) - Mask &= Aig_ManRandom( 0 ); + Mask &= Gia_ManRandom( 0 ); } else assert( 0 ); @@ -430,7 +430,7 @@ static inline int Gia_ManSwiSimInfoCountOnes( Gia_ManSwi_t * p, int iPlace ) int w, Counter = 0; pInfo = Gia_SwiData( p, iPlace ); for ( w = p->nWords-1; w >= 0; w-- ) - Counter += Aig_WordCountOnes( pInfo[w] ); + Counter += Gia_WordCountOnes( pInfo[w] ); return Counter; } @@ -451,7 +451,7 @@ static inline int Gia_ManSwiSimInfoCountTrans( Gia_ManSwi_t * p, int iPlace ) int w, Counter = 0; pInfo = Gia_SwiData( p, iPlace ); for ( w = p->nWords-1; w >= 0; w-- ) - Counter += 2*Aig_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff ); + Counter += 2*Gia_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff ); return Counter; } @@ -565,7 +565,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars ) { printf( "Obj = %8d (%8d). F = %6d. ", pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront, - 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) ); + 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) ); printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ", 12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*p->pAig->nFront/(1<<20), @@ -573,7 +573,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars ) ABC_PRT( "Time", clock() - clk ); } // perform simulation - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); Gia_ManSwiSimInfoInit( p ); for ( i = 0; i < pPars->nIters; i++ ) { @@ -612,7 +612,6 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars ) return vSwitching; } - /**Function************************************************************* Synopsis [Computes probability of switching (or of being 1).] diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c index 8cfe5959..a4cdf88a 100644 --- a/src/aig/gia/giaTsim.c +++ b/src/aig/gia/giaTsim.c @@ -81,15 +81,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig ) p = ABC_CALLOC( Gia_ManTer_t, 1 ); p->pAig = Gia_ManFront( pAig ); p->nIters = 300; - p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2*p->pAig->nFront) ); - p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCiNum(p->pAig)) ); - p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCoNum(p->pAig)) ); + p->pDataSim = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) ); + p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) ); + p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) ); // allocate storage for terminary states - p->nStateWords = Aig_BitWordNum( 2*Gia_ManRegNum(pAig) ); + p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) ); p->vStates = Vec_PtrAlloc( 1000 ); p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) ); p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) ); - p->nBins = Aig_PrimeCudd( 500 ); + p->nBins = Gia_PrimeCudd( 500 ); p->pBins = ABC_CALLOC( unsigned *, p->nBins ); p->vRetired = Vec_IntAlloc( 100 ); p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) ); @@ -508,7 +508,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs ) unsigned * pTemp, * pStates = Vec_PtrPop( vStates ); int i, w, nZeros, nConsts, nStateWords; // detect constant zero registers - nStateWords = Aig_BitWordNum( 2*nRegs ); + nStateWords = Gia_BitWordNum( 2*nRegs ); memset( pStates, 0, sizeof(int) * nStateWords ); Vec_PtrForEachEntry( vStates, pTemp, i ) for ( w = 0; w < nStateWords; w++ ) @@ -576,7 +576,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p ) unsigned * pState, * pFlop; int i, k, nFlopWords; vFlops = Vec_PtrAlloc( 100 ); - nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) ); + nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) ); for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { if ( p->pCount0[i] == Vec_PtrSize(p->vStates) ) @@ -631,7 +631,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose ) Gia_Obj_t * pObj; Vec_Int_t * vMapKtoI; int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0; - nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) ); + nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) ); p->vFlops = Gia_ManTerTranspose( p ); pCi2Lit = ABC_FALLOC( unsigned, Gia_ManCiNum(p->pAig) ); vMapKtoI = Vec_IntAlloc( 100 ); @@ -679,11 +679,11 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose ) { printf( "Obj = %8d (%8d). F = %6d. ", pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront, - 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) ); + 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) ); printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ", 12.0*Gia_ManObjNum(p->pAig)/(1<<20), - 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20), - 4.0*Aig_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) ); + 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20), + 4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) ); ABC_PRT( "Time", clock() - clk ); } // perform simulation diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 822f1e64..5716c1a0 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -23,6 +23,9 @@ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + +#define NUMBER1 3716960521u +#define NUMBER2 2174103536u //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -30,6 +33,113 @@ /**Function************************************************************* + Synopsis [Creates a sequence or random numbers.] + + Description [] + + SideEffects [] + + SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx] + +***********************************************************************/ +unsigned Gia_ManRandom( int fReset ) +{ + static unsigned int m_z = NUMBER1; + static unsigned int m_w = NUMBER2; + if ( fReset ) + { + m_z = NUMBER1; + m_w = NUMBER2; + } + m_z = 36969 * (m_z & 65535) + (m_z >> 16); + m_w = 18000 * (m_w & 65535) + (m_w >> 16); + return (m_z << 16) + m_w; +} + + +/**Function************************************************************* + + Synopsis [Creates random info for the primary inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop ) +{ + unsigned * pInfo; + int i, w; + Vec_PtrForEachEntryStart( vInfo, pInfo, i, iInputStart ) + for ( w = iWordStart; w < iWordStop; w++ ) + pInfo[w] = Gia_ManRandom(0); +} + +/**Function******************************************************************** + + Synopsis [Returns the next prime >= p.] + + Description [Copied from CUDD, for stand-aloneness.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +unsigned int Gia_PrimeCudd( unsigned int p ) +{ + int i,pn; + + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + + +/**Function************************************************************* + + Synopsis [Returns the composite name of the file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ) +{ + static char Buffer[1000]; + char * pDot; + strcpy( Buffer, pBase ); + if ( (pDot = strrchr( Buffer, '.' )) ) + *pDot = 0; + strcat( Buffer, pSuffix ); + if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) ) + return pDot+1; + return Buffer; +} + +/**Function************************************************************* + Synopsis [Sets phases of the internal nodes.] Description [] @@ -592,7 +702,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ) { Gia_Cex_t * pCex; - int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); + int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames ); pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); pCex->nRegs = nRegs; @@ -617,11 +727,11 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ) Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); for ( i = 0; i <= p->iFrame; i++ ) { Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); Gia_ManForEachAnd( pAig, pObj, k ) pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); @@ -657,18 +767,97 @@ void Gia_ManPrintCounterExample( Gia_Cex_t * p ) p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits ); printf( "State : " ); for ( k = 0; k < p->nRegs; k++ ) - printf( "%d", Aig_InfoHasBit(p->pData, k) ); + printf( "%d", Gia_InfoHasBit(p->pData, k) ); printf( "\n" ); for ( f = 0; f <= p->iFrame; f++ ) { printf( "Frame %2d : ", f ); for ( i = 0; i < p->nPis; i++ ) - printf( "%d", Aig_InfoHasBit(p->pData, k++) ); + printf( "%d", Gia_InfoHasBit(p->pData, k++) ); printf( "\n" ); } assert( k == p->nBits ); } +/**Function************************************************************* + + Synopsis [Dereferences the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) +{ + Gia_Obj_t * pFanin; + int Counter = 0; + if ( Gia_ObjIsCi(pNode) ) + return 0; + assert( Gia_ObjIsAnd(pNode) ); + pFanin = Gia_ObjFanin0(pNode); + assert( Gia_ObjRefs(p, pFanin) > 0 ); + if ( Gia_ObjRefDec(p, pFanin) == 0 ) + Counter += Gia_NodeDeref_rec( p, pFanin ); + pFanin = Gia_ObjFanin1(pNode); + assert( Gia_ObjRefs(p, pFanin) > 0 ); + if ( Gia_ObjRefDec(p, pFanin) == 0 ) + Counter += Gia_NodeDeref_rec( p, pFanin ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) +{ + Gia_Obj_t * pFanin; + int Counter = 0; + if ( Gia_ObjIsCi(pNode) ) + return 0; + assert( Gia_ObjIsAnd(pNode) ); + pFanin = Gia_ObjFanin0(pNode); + if ( Gia_ObjRefInc(p, pFanin) == 0 ) + Counter += Gia_NodeRef_rec( p, pFanin ); + pFanin = Gia_ObjFanin1(pNode); + if ( Gia_ObjRefInc(p, pFanin) == 0 ) + Counter += Gia_NodeRef_rec( p, pFanin ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [Returns the number of internal nodes in the MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ) +{ + int ConeSize1, ConeSize2; + assert( !Gia_IsComplement(pNode) ); + assert( Gia_ObjIsCand(pNode) ); + ConeSize1 = Gia_NodeDeref_rec( p, pNode ); + ConeSize2 = Gia_NodeRef_rec( p, pNode ); + assert( ConeSize1 == ConeSize2 ); + assert( ConeSize1 >= 0 ); + return ConeSize1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index 1e58e825..15641250 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -112,9 +112,6 @@ struct Hop_Man_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) -#define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) - static inline int Hop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } static inline int Hop_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } static inline int Hop_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } @@ -186,7 +183,7 @@ static inline Hop_Obj_t * Hop_ObjChild1( Hop_Obj_t * pObj ) { return pObj- static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL; } static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; } static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; } -static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); } +static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + ABC_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); } static inline int Hop_ObjPhaseCompl( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; } static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); } static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin ) diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c index 3dd8793c..27fb1aa6 100644 --- a/src/aig/hop/hopDfs.c +++ b/src/aig/hop/hopDfs.c @@ -125,13 +125,13 @@ int Hop_ManCountLevels( Hop_Man_t * p ) { Level0 = (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData; Level1 = (int)(ABC_PTRUINT_T)Hop_ObjFanin1(pObj)->pData; - pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1)); + pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + ABC_MAX(Level0, Level1)); } Vec_PtrFree( vNodes ); // get levels of the POs LevelsMax = 0; Hop_ManForEachPo( p, pObj, i ) - LevelsMax = AIG_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData ); + LevelsMax = ABC_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData ); return LevelsMax; } diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c index eccf58b8..f173248f 100644 --- a/src/aig/hop/hopObj.c +++ b/src/aig/hop/hopObj.c @@ -193,7 +193,7 @@ void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj ) // remove PIs/POs from the arrays if ( Hop_ObjIsPi(pObj) ) Vec_PtrRemove( p->vPis, pObj ); - // ABC_FREE the node + // free the node Hop_ManRecycleMemory( p, pObj ); } diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c index c0bbec1c..ddb0bce6 100644 --- a/src/aig/int/intCtrex.c +++ b/src/aig/int/intCtrex.c @@ -138,7 +138,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i ); ABC_FREE( pModel ); } - // ABC_FREE the sat_solver + // free the sat_solver sat_solver_delete( pSat ); Vec_IntFree( vCiIds ); // verify counter-example diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index c0ec3021..68726501 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -1218,7 +1218,7 @@ void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p ) Ivy_ObjSetClassNodeRepr( pObj, NULL ); Ivy_FraigAddClass( &p->lClasses, pObj ); } - // ABC_FREE the table + // free the table ABC_FREE( pTable ); } diff --git a/src/aig/ivy/ivyHaig.c b/src/aig/ivy/ivyHaig.c index 62624642..87021600 100644 --- a/src/aig/ivy/ivyHaig.c +++ b/src/aig/ivy/ivyHaig.c @@ -518,7 +518,7 @@ printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id ); Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) pObj->Init = pObj->Level, pObj->Level = 0; } - // ABC_FREE arrays + // free arrays Vec_IntFree( vNodes ); Vec_IntFree( vLatches ); } diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c index d09f6ffd..909548d1 100644 --- a/src/aig/ivy/ivyMan.c +++ b/src/aig/ivy/ivyMan.c @@ -143,7 +143,7 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ) // update the counters of different objects pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p); pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p); - // ABC_FREE arrays + // free arrays Vec_IntFree( vNodes ); Vec_IntFree( vLatches ); // make sure structural hashing did not change anything @@ -346,7 +346,7 @@ int Ivy_ManCleanupSeq( Ivy_Man_t * p ) // delete buffer from the array of buffers if ( p->fFanout && Ivy_ObjIsBuf(pObj) ) Vec_PtrRemove( p->vBufs, pObj ); - // ABC_FREE the node + // free the node Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Ivy_ManRecycleMemory( p, pObj ); } diff --git a/src/aig/ivy/ivyObj.c b/src/aig/ivy/ivyObj.c index d7925fab..59dda19c 100644 --- a/src/aig/ivy/ivyObj.c +++ b/src/aig/ivy/ivyObj.c @@ -268,7 +268,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) // clean and recycle the entry if ( fFreeTop ) { - // ABC_FREE the node + // free the node Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Ivy_ManRecycleMemory( p, pObj ); } diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c index c4ed70e4..a85262a9 100644 --- a/src/aig/kit/kitDsd.c +++ b/src/aig/kit/kitDsd.c @@ -2422,7 +2422,7 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit // compute the sum total of supports nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars ); nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars ); - // ABC_FREE the networks + // free the networks Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] ); Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] ); } @@ -2460,7 +2460,7 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit } } - // ABC_FREE the networks + // free the networks for ( i = 0; i < 5; i++ ) for ( k = 0; k < 16; k++ ) if ( ppNtks[i][k] ) diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c index c0d3b650..e0f6dd82 100644 --- a/src/aig/mfx/mfxCore.c +++ b/src/aig/mfx/mfxCore.c @@ -86,7 +86,7 @@ p->timeWin += clock() - clk; // compute the divisors of the window clk = clock(); p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) ); -// p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY ); +// p->vDivs = Mfx_ComputeDivisors( p, pNode, ABC_INFINITY ); p->nTotalDivs += Vec_PtrSize(p->vDivs); p->timeDiv += clock() - clk; // construct AIG for the window @@ -371,7 +371,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib ) if ( pPars->fPower ) printf( "Total switching after = %7.2f.\n", Nwl_ManComputeTotalSwitching(pNtk) ); - // ABC_FREE the manager + // free the manager p->timeTotal = clock() - clk; Mfx_ManStop( p ); diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 6923ac7a..b4abe3bf 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -185,7 +185,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) Ntl_ObjForEachFanin( pObj, pNetFanin, i ) { LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pCopy) ); - LevelMax = AIG_MAX( LevelMax, LevelCur ); + LevelMax = ABC_MAX( LevelMax, LevelCur ); Vec_PtrPush( p->vCos, pNetFanin ); Aig_ObjCreatePo( p->pAig, pNetFanin->pCopy ); } diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c index 56a13741..daea19d5 100644 --- a/src/aig/nwk/nwkFanio.c +++ b/src/aig/nwk/nwkFanio.c @@ -172,7 +172,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) pObj->pFanio[i] = pObj->pFanio[i-1]; pObj->pFanio[pObj->nFanins++] = pFanin; pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj; - pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) ); + pObj->Level = ABC_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) ); } /**Function************************************************************* diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c index d6e20672..8f971871 100644 --- a/src/aig/nwk/nwkMan.c +++ b/src/aig/nwk/nwkMan.c @@ -127,7 +127,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl ) int nPis; // the number of primary inputs int nPos; // the number of primary outputs } ParsNew, ParsBest = { 0 }; - // ABC_FREE storage for the name + // free storage for the name if ( pNtk == NULL ) { ABC_FREE( ParsBest.pName ); diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c index 80391c66..5c53038c 100644 --- a/src/aig/nwk/nwkTiming.c +++ b/src/aig/nwk/nwkTiming.c @@ -736,7 +736,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj ) for ( i = 0; i < nTerms; i++ ) { pFanin = Nwk_ManCo(pObj->pMan, iTerm1 + i); - Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) ); + Level = ABC_MAX( Level, Nwk_ObjLevel(pFanin) ); } Level++; } @@ -745,7 +745,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj ) } assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) ); Nwk_ObjForEachFanin( pObj, pFanin, i ) - Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) ); + Level = ABC_MAX( Level, Nwk_ObjLevel(pFanin) ); return Level + (Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0); } diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index fccac175..10b7b462 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -368,12 +368,12 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ) nFanouts = Nwk_ObjFanoutNum(pNode); nFaninsAll += nFanins; nFanoutsAll += nFanouts; - nFaninsMax = AIG_MAX( nFaninsMax, nFanins ); - nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts ); + nFaninsMax = ABC_MAX( nFaninsMax, nFanins ); + nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts ); } // allocate storage for fanin/fanout numbers - nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); + nSizeMax = ABC_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); vFanins = Vec_IntStart( nSizeMax ); vFanouts = Vec_IntStart( nSizeMax ); diff --git a/src/aig/nwk2/nwkFanio.c b/src/aig/nwk2/nwkFanio.c index 4068a1a5..30037a83 100644 --- a/src/aig/nwk2/nwkFanio.c +++ b/src/aig/nwk2/nwkFanio.c @@ -172,7 +172,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) pObj->pFanio[i] = pObj->pFanio[i-1]; pObj->pFanio[pObj->nFanins++] = pFanin; pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj; - pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) ); + pObj->Level = ABC_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) ); } /**Function************************************************************* diff --git a/src/aig/nwk2/nwkUtil.c b/src/aig/nwk2/nwkUtil.c index d6daca4e..5473e628 100644 --- a/src/aig/nwk2/nwkUtil.c +++ b/src/aig/nwk2/nwkUtil.c @@ -368,12 +368,12 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ) nFanouts = Nwk_ObjFanoutNum(pNode); nFaninsAll += nFanins; nFanoutsAll += nFanouts; - nFaninsMax = AIG_MAX( nFaninsMax, nFanins ); - nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts ); + nFaninsMax = ABC_MAX( nFaninsMax, nFanins ); + nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts ); } // allocate storage for fanin/fanout numbers - nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); + nSizeMax = ABC_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); vFanins = Vec_IntStart( nSizeMax ); vFanouts = Vec_IntStart( nSizeMax ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f11345eb..5ddef829 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ); +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index c9e76626..a2a915f7 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -693,15 +693,15 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int fVerbose ) -{ +Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose ) +{ extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose ); Vec_Int_t * vFlopsNew, * vPiToReg; Aig_Obj_t * pObj; int i, Entry, iFlop; - Saig_BmcPerform( pAbs, 2000, 2000, 5000, 1000000, fVerbose ); + Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose ); if ( pAbs->pSeqModel == NULL ) return NULL; // Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel ); @@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ) +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -779,11 +779,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, if ( fSkipProof ) { - assert( 0 ); +// assert( 0 ); if ( fVerbose ) printf( "Performing counter-example-based refinement.\n" ); // vFlops = Vec_IntStartNatural( 100 ); // Vec_IntPush( vFlops, 0 ); + vFlops = Vec_IntStartNatural( 1 ); } else { @@ -858,7 +859,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, printf( "Refining abstraction...\n" ); for ( Iter = 0; ; Iter++ ) { - pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose ); + pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose ); if ( pTemp == NULL ) break; Aig_ManStop( pResult ); diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 71bdadf6..0a9f230b 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -327,7 +327,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) ); assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 ); // start timeframes - p = Aig_ManStart( nFrames * AIG_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); + p = Aig_ManStart( nFrames * ABC_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); p->pName = Aig_UtilStrsav( "frames" ); // create variables for register outputs pAig = pBot; diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 9bc6416b..a3fdaf93 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -180,7 +180,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 ) pNode->iFan1 = iFan1; pNode->iNext = 0; if ( iFan0 || iFan1 ) - p->pLevels[p->nObjs] = 1 + AIG_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) ); + p->pLevels[p->nObjs] = 1 + ABC_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) ); else p->pLevels[p->nObjs] = 0, p->nPis++; return p->nObjs++; diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index ff46634e..b29fcb9b 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -616,7 +616,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, return NULL; } clk = clock(); - vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); + vSimInfo = Vec_PtrAllocSimInfo( ABC_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); // process Design 1 RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 ); diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index f50af285..a92d9369 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -398,7 +398,7 @@ ABC_PRT( "Fraiging", clock() - clk ); clk = clock(); pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); ABC_PRT( "Mapped", clock() - clk ); - // ABC_FREE mapping + // free mapping Saig_ManStopMap2( pAig ); clk = clock(); pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 967d29e9..8fce7904 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -597,7 +597,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, // int nWords = 4; // int nIters = 0; - int nFrames = AIG_MAX( nFramesK, 4 ); + int nFrames = ABC_MAX( nFramesK, 4 ); int nWords = 2; int nIters = 16; Ssw_Cla_t * p; diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 9a31a056..56b37fbe 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -204,8 +204,8 @@ clk = clock(); nSatFailsReal = p->nSatFailsReal; nUniques = p->nUniques; - p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars ); - p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); + p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars ); + p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c index d9ac07a9..04e66f09 100644 --- a/src/aig/ssw/sswDyn.c +++ b/src/aig/ssw/sswDyn.c @@ -438,8 +438,8 @@ p->timeReduce += clock() - clk; // replace the solver if ( p->pMSat ) { - p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars ); - p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); + p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars ); + p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); Ssw_SatStop( p->pMSat ); p->nRecycles++; p->nRecyclesTotal++; diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c index 80bc5853..fb36c31d 100644 --- a/src/aig/ssw/sswLcorr.c +++ b/src/aig/ssw/sswLcorr.c @@ -300,8 +300,8 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) p->pMSat->nSatVars > p->pPars->nSatVarMax && p->nRecycleCalls > p->pPars->nRecycleCalls ) { - p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars ); - p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); + p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars ); + p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); Ssw_SatStop( p->pMSat ); p->pMSat = Ssw_SatStart( 0 ); p->nRecycles++; diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c index 5f426093..1d578291 100644 --- a/src/aig/ssw/sswSemi.c +++ b/src/aig/ssw/sswSemi.c @@ -68,7 +68,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) memset( p, 0, sizeof(Ssw_Sem_t) ); p->nConfMaxStart = nConfMax; p->nConfMax = nConfMax; - p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames ); + p->nFramesSweep = ABC_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames ); p->fVerbose = fVerbose; // equivalences considered p->pMan = pMan; diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 7a2f4664..deb8d5d4 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -590,7 +590,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) Aig_ManForEachPi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); // flip one bit - Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); + Limit = ABC_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 ); } @@ -612,7 +612,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) // flip one bit of the last frame if ( fUseDist1 ) //&& p->nFrames == 2 ) { - Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); + Limit = ABC_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); } @@ -641,7 +641,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); // set distance one PIs for the first frame - Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 ); + Limit = ABC_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c index 7327606e..e565b01f 100644 --- a/src/aig/tim/tim.c +++ b/src/aig/tim/tim.c @@ -28,10 +28,6 @@ #include "mem.h" #include "tim.h" -#define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) -#define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) -#define AIG_ABS(a) (((a) >= 0)? (a) :-(a)) - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -773,7 +769,7 @@ float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi ) pDelays = pBox->pDelayTable + i * pBox->nInputs; DelayBest = -TIM_ETERNITY; Tim_ManBoxForEachInput( p, pBox, pObj, k ) - DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] ); + DelayBest = ABC_MAX( DelayBest, pObj->timeArr + pDelays[k] ); pObjRes->timeArr = DelayBest; pObjRes->TravId = p->nTravIds; } @@ -820,7 +816,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) Tim_ManBoxForEachOutput( p, pBox, pObj, k ) { pDelays = pBox->pDelayTable + k * pBox->nInputs; - DelayBest = AIG_MIN( DelayBest, pObj->timeReq - pDelays[i] ); + DelayBest = ABC_MIN( DelayBest, pObj->timeReq - pDelays[i] ); } pObjRes->timeReq = DelayBest; pObjRes->TravId = p->nTravIds; |