From 0871bffae307e0553e0c5186336189e8b55cf6a6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Feb 2009 08:01:00 -0800 Subject: Version abc90215 --- src/aig/saig/saig.h | 10 +++++----- src/aig/saig/saigAbs.c | 26 ++++++++++++------------- src/aig/saig/saigBmc.c | 14 +++++++------- src/aig/saig/saigBmc2.c | 12 ++++++------ src/aig/saig/saigHaig.c | 24 +++++++++++------------ src/aig/saig/saigInd.c | 4 ++-- src/aig/saig/saigIoa.c | 4 ++-- src/aig/saig/saigMiter.c | 18 ++++++++--------- src/aig/saig/saigPhase.c | 12 ++++++------ src/aig/saig/saigRetFwd.c | 8 ++++---- src/aig/saig/saigRetMin.c | 8 ++++---- src/aig/saig/saigSimExt.c | 2 +- src/aig/saig/saigSimFast.c | 27 +++++++++++++------------- src/aig/saig/saigSimMv.c | 48 +++++++++++++++++++++++----------------------- src/aig/saig/saigSimSeq.c | 32 +++++++++++++++---------------- src/aig/saig/saigStrSim.c | 16 ++++++++-------- src/aig/saig/saigSwitch.c | 34 +++++++++----------------------- src/aig/saig/saigSynch.c | 12 ++++++------ src/aig/saig/saigTrans.c | 8 ++++---- src/aig/saig/saigWnd.c | 4 ++-- 20 files changed, 154 insertions(+), 169 deletions(-) (limited to 'src/aig/saig') diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 84ff272a..3db3e396 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -21,10 +21,6 @@ #ifndef __SAIG_H__ #define __SAIG_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -35,6 +31,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -134,7 +134,7 @@ extern int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose ); /*=== saigStrSim.c ==========================================================*/ extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter ); /*=== saigSwitch.c ==========================================================*/ -extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ); +extern Vec_Int_t * Saig_ManComputeSwitchProb2s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ); /*=== saigSynch.c ==========================================================*/ extern Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p ); /*=== saigTrans.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index d2a45b4e..c9e76626 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -54,7 +54,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo Intp_Man_t * pManProof; int RetValue, clk = clock(); // solve the problem - RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_Undef ) { printf( "Conflict limit is reached.\n" ); @@ -68,7 +68,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo if ( fVerbose ) { printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } assert( RetValue == l_False ); pSatCnf = sat_solver_store_release( pSat ); @@ -81,7 +81,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo if ( fVerbose ) { printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } return vCore; } @@ -458,7 +458,7 @@ Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec Vec_PtrForEachEntry( vFrames, pCnf, f ) nSatVars += pCnf->nVars; // mark register variables - pVars = ALLOC( int, nSatVars ); + pVars = ABC_ALLOC( int, nSatVars ); for ( i = 0; i < nSatVars; i++ ) pVars[i] = -1; Vec_PtrForEachEntry( vFrames, pCnf, f ) @@ -485,7 +485,7 @@ Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec } } // mark used registers - pFlops = CALLOC( int, Aig_ManRegNum(p) ); + pFlops = ABC_CALLOC( int, Aig_ManRegNum(p) ); Vec_IntForEachEntry( vCore, iClause, i ) { nSatClauses = 0; @@ -513,8 +513,8 @@ Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec for ( i = 0; i < Aig_ManRegNum(p); i++ ) if ( pFlops[i] ) Vec_IntPush( vFlops, i ); - free( pFlops ); - free( pVars ); + ABC_FREE( pFlops ); + ABC_FREE( pVars ); return vFlops; } @@ -536,7 +536,7 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * int * pVars, * pFlops; int i, iClause, iReg, * piLit; // mark register variables - pVars = ALLOC( int, pCnf->nVars ); + pVars = ABC_ALLOC( int, pCnf->nVars ); for ( i = 0; i < pCnf->nVars; i++ ) pVars[i] = -1; Saig_ManForEachLi( pCnf->pMan, pObj, i ) @@ -544,7 +544,7 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * Saig_ManForEachLo( pCnf->pMan, pObj, i ) pVars[ pCnf->pVarNums[pObj->Id] ] = i; // mark used registers - pFlops = CALLOC( int, Aig_ManRegNum(pCnf->pMan) ); + pFlops = ABC_CALLOC( int, Aig_ManRegNum(pCnf->pMan) ); Vec_IntForEachEntry( vCore, iClause, i ) { // skip auxiliary clauses @@ -564,8 +564,8 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * for ( i = 0; i < Aig_ManRegNum(pCnf->pMan); i++ ) if ( pFlops[i] ) Vec_IntPush( vFlops, i ); - free( pFlops ); - free( pVars ); + ABC_FREE( pFlops ); + ABC_FREE( pVars ); return vFlops; } @@ -806,7 +806,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, if ( fVerbose ) { printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); - PRT( "Time", clock() - clk2 ); + ABC_PRT( "Time", clock() - clk2 ); } // compute UNSAT core vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose ); @@ -831,7 +831,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, if ( fVerbose ) { printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } } /* diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 7cccce96..d56d97a9 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -27,7 +27,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define AIG_VISITED ((Aig_Obj_t *)(PORT_PTRUINT_T)1) +#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1) typedef struct Saig_Bmc_t_ Saig_Bmc_t; struct Saig_Bmc_t_ @@ -88,7 +88,7 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, Aig_Obj_t * pObj; int i, Lit; assert( Aig_ManRegNum(pAig) > 0 ); - p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) ); + p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) ); memset( p, 0, sizeof(Saig_Bmc_t) ); // set parameters p->nFramesMax = nFramesMax; @@ -141,7 +141,7 @@ void Saig_BmcManStop( Saig_Bmc_t * p ) sat_solver_delete( p->pSat ); Vec_PtrFree( p->vTargets ); Vec_PtrFree( p->vVisited ); - free( p ); + ABC_FREE( p ); } /**Function************************************************************* @@ -311,7 +311,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) // check if the node is gone Vec_PtrForEachEntry( p->vVisited, pObj, i ) { - iFrame = (int)(PORT_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ ); + iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ ); pRes = Saig_BmcObjFrame( p, pObj, iFrame ); if ( Aig_ObjIsNone( Aig_Regular(pRes) ) ) Saig_BmcObjSetFrame( p, pObj, iFrame, NULL ); @@ -524,7 +524,7 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p ) return l_Undef; VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) ); Lit = toLitCond( VarNum, Aig_IsComplement(pObj) ); - RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_False ) // unsat continue; if ( RetValue == l_Undef ) // undecided @@ -614,7 +614,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf { printf( "%3d : F = %3d. O =%4d. And = %7d. Var = %7d. Conf = %7d. ", Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts ); - PRT( "Time", clock() - clk2 ); + ABC_PRT( "Time", clock() - clk2 ); } if ( RetValue != l_False ) break; @@ -624,7 +624,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf p->iOutputFail, p->iFrameFail ); else // if ( RetValue == l_False || RetValue == l_Undef ) printf( "No output was asserted in %d frames. ", p->iFramePrev-1 ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); if ( RetValue != l_True ) { if ( p->iFrameLast >= p->nFramesMax ) diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 5776cd4a..8ba02528 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -199,7 +199,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); fflush( stdout ); } // rewrite the timeframes @@ -213,7 +213,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim { printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); fflush( stdout ); } } @@ -230,7 +230,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim if ( fVerbose ) { printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); fflush( stdout ); } status = sat_solver_simplify(pSat); @@ -254,13 +254,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); } clk = clock(); - status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) { printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); - PRT( "T", clock() - clkPart ); + ABC_PRT( "T", clock() - clkPart ); clkPart = clock(); fflush( stdout ); } @@ -284,7 +284,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); pModel[Aig_ManPiNum(pFrames)] = pObj->Id; pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); - free( pModel ); + ABC_FREE( pModel ); Vec_IntFree( vCiIds ); // if ( piFrame ) diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index 8a75ae1f..1c7aa025 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -273,7 +273,7 @@ clk = clock(); return 0; } } -PRT( "Preparation", clock() - clk ); +ABC_PRT( "Preparation", clock() - clk ); // check in the second timeframe @@ -291,7 +291,7 @@ clk = clock(); Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 ); - RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue1 == l_False ) { Lits[0] = lit_neg( Lits[0] ); @@ -303,7 +303,7 @@ clk = clock(); Lits[0]++; Lits[1]--; - RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue2 == l_False ) { Lits[0] = lit_neg( Lits[0] ); @@ -323,7 +323,7 @@ clk = clock(); // break; } printf( " \r" ); -PRT( "Solving ", clock() - clk ); +ABC_PRT( "Solving ", clock() - clk ); clkVerif = clock() - clk; if ( Counter ) printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 ); @@ -479,7 +479,7 @@ clk = clock(); return 0; } } -PRT( "Preparation", clock() - clk ); +ABC_PRT( "Preparation", clock() - clk ); // check in the second timeframe @@ -496,12 +496,12 @@ clk = clock(); Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 ); Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 ); - RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); Lits[0]++; Lits[1]++; - RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue1 != l_False || RetValue2 != l_False ) Counter++; @@ -511,12 +511,12 @@ clk = clock(); Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 ); Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 ); - RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); Lits[0]++; Lits[1]--; - RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue1 != l_False || RetValue2 != l_False ) Counter++; @@ -527,7 +527,7 @@ clk = clock(); // if ( i / 2 > 1000 ) // break; } -PRT( "Solving ", clock() - clk ); +ABC_PRT( "Solving ", clock() - clk ); if ( Counter ) printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 ); else @@ -634,7 +634,7 @@ clk = clock(); // remove structural hashing table Aig_TableClear( pNew->pManHaig ); pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 ); -PRT( "HAIG setup time", clock() - clk ); +ABC_PRT( "HAIG setup time", clock() - clk ); clk = clock(); if ( fSeqHaig ) @@ -682,7 +682,7 @@ clk = clock(); Aig_ManStop( pTemp ); } } -PRT( "Synthesis time ", clock() - clk ); +ABC_PRT( "Synthesis time ", clock() - clk ); clkSynth = clock() - clk; // use the haig for verification diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index 69c250f6..1c26e5df 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -121,13 +121,13 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose } // run the SAT solver nConfPrev = pSat->stats.conflicts; - status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, 0, 0, 0 ); if ( fVerbose ) { printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ", f+1, Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart), nSatVarNum, pSat->stats.conflicts-nConfPrev ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } if ( status == l_Undef ) break; diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c index 70870fe9..d049489e 100644 --- a/src/aig/saig/saigIoa.c +++ b/src/aig/saig/saigIoa.c @@ -348,7 +348,7 @@ Aig_Man_t * Saig_ManReadBlif( char * pFileName ) { extern double pow( double x, double y ); int Size = (int)pow(10.0, (double)(strlen(pToken) - 1)); - pNum2Id = CALLOC( int, Size ); + pNum2Id = ABC_CALLOC( int, Size ); } // other tokens @@ -383,7 +383,7 @@ Aig_Man_t * Saig_ManReadBlif( char * pFileName ) // add non-node objects to the mapping Aig_ManForEachPi( p, pNode, i ) pNum2Id[pNode->Id] = pNode->Id; -// FREE( pNum2Id ); +// ABC_FREE( pNum2Id ); p->pData = pNum2Id; // check the new manager Aig_ManSetRegNum( p, nRegs ); diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 6c4b3af0..174a3e97 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -526,13 +526,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi if ( ppAig0 ) { *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); - FREE( (*ppAig0)->pName ); + ABC_FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); - FREE( (*ppAig1)->pName ); + ABC_FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } Vec_PtrFree( vSet0 ); @@ -596,13 +596,13 @@ int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** if ( ppAig0 ) { *ppAig0 = Aig_ManDupNodesAll( p, vSet0 ); - FREE( (*ppAig0)->pName ); + ABC_FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { *ppAig1 = Aig_ManDupNodesAll( p, vSet1 ); - FREE( (*ppAig1)->pName ); + ABC_FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } Vec_PtrFree( vSet0 ); @@ -768,14 +768,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) { assert( 0 ); *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready - FREE( (*ppAig0)->pName ); + ABC_FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { assert( 0 ); *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready - FREE( (*ppAig1)->pName ); + ABC_FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } Vec_PtrFree( vSet0 ); @@ -891,12 +891,12 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe if ( RetValue == 1 ) { printf( "Networks are equivalent. " ); -PRT( "Time", clock() - clkTotal ); +ABC_PRT( "Time", clock() - clkTotal ); } else if ( RetValue == 0 ) { printf( "Networks are NOT EQUIVALENT. " ); -PRT( "Time", clock() - clkTotal ); +ABC_PRT( "Time", clock() - clkTotal ); if ( pMiterCec->pData == NULL ) printf( "Counter-example is not available.\n" ); else @@ -919,7 +919,7 @@ PRT( "Time", clock() - clkTotal ); else { printf( "Networks are UNDECIDED. " ); -PRT( "Time", clock() - clkTotal ); +ABC_PRT( "Time", clock() - clkTotal ); } fflush( stdout ); Aig_ManStop( pMiterCec ); diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index c6d84066..9b09598c 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -139,14 +139,14 @@ static inline void Saig_TsiSetNext( unsigned * pState, int nWords, unsigne Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig ) { Saig_Tsim_t * p; - p = (Saig_Tsim_t *)malloc( sizeof(Saig_Tsim_t) ); + p = (Saig_Tsim_t *)ABC_ALLOC( char, sizeof(Saig_Tsim_t) ); memset( p, 0, sizeof(Saig_Tsim_t) ); p->pAig = pAig; p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) ); p->vStates = Vec_PtrAlloc( 1000 ); p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 ); p->nBins = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2); - p->pBins = ALLOC( unsigned *, p->nBins ); + p->pBins = ABC_ALLOC( unsigned *, p->nBins ); memset( p->pBins, 0, sizeof(unsigned *) * p->nBins ); return p; } @@ -168,8 +168,8 @@ void Saig_TsiStop( Saig_Tsim_t * p ) Vec_IntFree( p->vNonXRegs ); Aig_MmFixedStop( p->pMem, 0 ); Vec_PtrFree( p->vStates ); - free( p->pBins ); - free( p ); + ABC_FREE( p->pBins ); + ABC_FREE( p ); } /**Function************************************************************* @@ -696,7 +696,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe assert( Vec_IntSize(pTsi->vNonXRegs) > 0 ); // create mapping for the frames nodes - pObjMap = ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); + pObjMap = ABC_ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) ); // start the fraig package @@ -762,7 +762,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe //Aig_ManPrintStats( pFrames ); // Aig_ManPiCleanup( pFrames ); //Aig_ManPrintStats( pFrames ); - free( pObjMap ); + ABC_FREE( pObjMap ); return pFrames; } diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c index b6321da6..8178d26e 100644 --- a/src/aig/saig/saigRetFwd.c +++ b/src/aig/saig/saigRetFwd.c @@ -51,7 +51,7 @@ Aig_Obj_t ** Aig_ManStaticFanoutStart( Aig_Man_t * p ) int i, nFanouts, nFanoutsAlloc; // allocate fanouts nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManPiNum(p) - Aig_ManPoNum(p); - ppFanouts = ALLOC( Aig_Obj_t *, nFanoutsAlloc ); + ppFanouts = ABC_ALLOC( Aig_Obj_t *, nFanoutsAlloc ); // mark up storage nFanouts = 0; Aig_ManForEachObj( p, pObj, i ) @@ -122,7 +122,7 @@ void Saig_ManMarkAutonomous( Aig_Man_t * p ) Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) ); Saig_ManForEachPi( p, pObj, i ) Aig_ManMarkAutonomous_rec( p, pObj ); - free( ppFanouts ); + ABC_FREE( ppFanouts ); // disconnect LIs/LOs and label unreachable registers Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) { @@ -220,7 +220,7 @@ Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ) { printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ", i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } if ( pTemp != p ) Aig_ManStop( pTemp ); @@ -229,7 +229,7 @@ Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ) pNew = Aig_ManReduceLaches( pNew, fVerbose ); if ( fVerbose ) { - PRT( "Register sharing time", clock() - clk ); + ABC_PRT( "Register sharing time", clock() - clk ); } return pNew; } diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index 1820ae9a..b9204f44 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -61,7 +61,7 @@ Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p ) Cnf_DataFree( pCnf ); return NULL; } - RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); assert( RetValue != l_Undef ); // create counter-example if ( RetValue == l_True ) @@ -119,7 +119,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose ) } sat_solver_store_mark_roots( pSat ); // solve the problem - RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); assert( RetValue != l_Undef ); assert( RetValue == l_False ); pSatCnf = sat_solver_store_release( pSat ); @@ -132,7 +132,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose ) // derive the set of variables on which the core depends // collect the variable numbers nVars = 0; - pVars = ALLOC( int, pCnf->nVars ); + pVars = ABC_ALLOC( int, pCnf->nVars ); memset( pVars, 0, sizeof(int) * pCnf->nVars ); Vec_IntForEachEntry( vCore, iClause, i ) { @@ -170,7 +170,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose ) } if ( fVerbose ) printf( "UNSAT core: %d clauses, %d variables, %d POs. ", Vec_IntSize(vCore), nVars, nPos ); - free( pVars ); + ABC_FREE( pVars ); Vec_IntFree( vCore ); Cnf_DataFree( pCnf ); return iBadPo; diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index 49c85ff4..ead0ece5 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -309,7 +309,7 @@ clk = clock(); if ( fVerbose ) { printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstPi, Vec_IntSize(vRes) ); -PRT( "Time", clock() - clk ); +ABC_PRT( "Time", clock() - clk ); } Vec_PtrFree( vSimInfo ); Aig_ManFanoutStop( p ); diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c index 09bb6a06..05f77f8a 100644 --- a/src/aig/saig/saigSimFast.c +++ b/src/aig/saig/saigSimFast.c @@ -108,7 +108,7 @@ Faig_Man_t * Faig_ManAlloc( Aig_Man_t * pAig ) int nWords; // assert( Faig_ManIsCorrect(pAig) ); nWords = 2 * Aig_ManNodeNum(pAig) + Aig_ManPoNum(pAig); - p = (Faig_Man_t *)ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords ); + p = (Faig_Man_t *)ABC_ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords ); //printf( "Allocating %7.2f Mb.\n", 1.0 * (sizeof(Faig_Man_t) + sizeof(int) * nWords)/(1<<20) ); memset( p, 0, sizeof(Faig_Man_t) ); p->nPis = Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig); @@ -247,8 +247,8 @@ static inline unsigned Faig_SimulateTransferShift( unsigned uOld, unsigned uNew ***********************************************************************/ int * Faig_ManSimulateFrames( Faig_Man_t * p, int nFrames, int nPref, int fTrans ) { - int * pNumOnes = CALLOC( unsigned, p->nObjs ); - unsigned * pSimInfo = ALLOC( unsigned, p->nObjs ); + int * pNumOnes = ABC_CALLOC( unsigned, p->nObjs ); + unsigned * pSimInfo = ABC_ALLOC( unsigned, p->nObjs ); int f, i; //printf( "Allocating %7.2f Mb.\n", 1.0 * 4 * p->nObjs/(1<<20) ); //printf( "Allocating %7.2f Mb.\n", 1.0 * 4 * p->nObjs/(1<<20) ); @@ -287,7 +287,7 @@ int * Faig_ManSimulateFrames( Faig_Man_t * p, int nFrames, int nPref, int fTrans pNumOnes[i] += Aig_WordCountOnes( pSimInfo[i] ); } } - free( pSimInfo ); + ABC_FREE( pSimInfo ); return pNumOnes; } @@ -336,7 +336,7 @@ float Faig_ManComputeProbOne( int nOnes, int nSimWords ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Faig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) +Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) { extern char * Abc_FrameReadFlag( char * pFlag ); int fTrans = 1; @@ -351,7 +351,7 @@ Vec_Int_t * Faig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, i pSwitching = (float *)vSwitching->pArray; clk = clock(); pAig = Faig_ManCreate( p ); -//PRT( "\nCreation ", clock() - clk ); +//ABC_PRT( "\nCreation ", clock() - clk ); Aig_ManRandom( 1 ); // get the number of frames to simulate // if the parameter "seqsimframes" is defined, use it @@ -368,7 +368,7 @@ clk = clock(); //printf( "Simulating %d frames.\n", nFramesReal ); clk = clock(); pProbs = Faig_ManSimulateFrames( pAig, nFramesReal, nPref, fTrans ); -//PRT( "Simulation", clock() - clk ); +//ABC_PRT( "Simulation", clock() - clk ); clk = clock(); if ( fTrans ) { @@ -412,10 +412,10 @@ clk = clock(); pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref ); assert( Counter == pAig->nObjs ); } - free( pProbs ); - free( pAig ); -//PRT( "Switch ", clock() - clk ); -//PRT( "TOTAL ", clock() - clkTotal ); + ABC_FREE( pProbs ); + ABC_FREE( pAig ); +//ABC_PRT( "Switch ", clock() - clk ); +//ABC_PRT( "TOTAL ", clock() - clkTotal ); return vSwitching; } @@ -430,9 +430,10 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) +Vec_Int_t * Saig_ManComputeSwitchProb3s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) { - return Faig_ManComputeSwitchProbs( p, nFrames, nPref, fProbOne ); +// return Faig_ManComputeSwitchProbs( p, nFrames, nPref, fProbOne ); + return NULL; } diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 0e250a74..9bc6416b 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -129,7 +129,7 @@ Saig_MvObj_t * Saig_ManCreateReducedAig( Aig_Man_t * p, Vec_Ptr_t ** pvFlops ) Aig_Obj_t * pObj; int i; *pvFlops = Vec_PtrAlloc( Aig_ManRegNum(p) ); - pAig = CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 ); + pAig = ABC_CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 ); Aig_ManForEachObj( p, pObj, i ) { pEntry = pAig + i; @@ -171,8 +171,8 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 ) Saig_MvAnd_t * pNode; if ( p->nObjs == p->nObjsAlloc ) { - p->pAigNew = REALLOC( Saig_MvAnd_t, p->pAigNew, 2*p->nObjsAlloc ); - p->pLevels = REALLOC( unsigned char, p->pLevels, 2*p->nObjsAlloc ); + p->pAigNew = ABC_REALLOC( Saig_MvAnd_t, p->pAigNew, 2*p->nObjsAlloc ); + p->pLevels = ABC_REALLOC( unsigned char, p->pLevels, 2*p->nObjsAlloc ); p->nObjsAlloc *= 2; } pNode = p->pAigNew + p->nObjs; @@ -202,7 +202,7 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig ) Saig_MvMan_t * p; int i; assert( Aig_ManRegNum(pAig) > 0 ); - p = (Saig_MvMan_t *)ALLOC( Saig_MvMan_t, 1 ); + p = (Saig_MvMan_t *)ABC_ALLOC( Saig_MvMan_t, 1 ); memset( p, 0, sizeof(Saig_MvMan_t) ); // set parameters p->pAig = pAig; @@ -213,23 +213,23 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig ) // compacted AIG p->pAigOld = Saig_ManCreateReducedAig( pAig, &p->vFlops ); p->nTStatesSize = Aig_PrimeCudd( p->nStatesMax ); - p->pTStates = CALLOC( int, p->nTStatesSize ); + p->pTStates = ABC_CALLOC( int, p->nTStatesSize ); p->pMemStates = Aig_MmFixedStart( sizeof(int) * (p->nFlops+1), p->nStatesMax ); p->vStates = Vec_PtrAlloc( p->nStatesMax ); Vec_PtrPush( p->vStates, NULL ); - p->pRegsUndef = CALLOC( int, p->nFlops ); - p->pRegsValues = ALLOC( int *, p->nFlops ); - p->pRegsValues[0] = ALLOC( int, p->nValuesMax * p->nFlops ); + p->pRegsUndef = ABC_CALLOC( int, p->nFlops ); + p->pRegsValues = ABC_ALLOC( int *, p->nFlops ); + p->pRegsValues[0] = ABC_ALLOC( int, p->nValuesMax * p->nFlops ); for ( i = 1; i < p->nFlops; i++ ) p->pRegsValues[i] = p->pRegsValues[i-1] + p->nValuesMax; - p->nRegsValues = CALLOC( int, p->nFlops ); + p->nRegsValues = ABC_CALLOC( int, p->nFlops ); p->vTired = Vec_PtrAlloc( 100 ); // internal AIG p->nObjsAlloc = 1000000; - p->pAigNew = ALLOC( Saig_MvAnd_t, p->nObjsAlloc ); + p->pAigNew = ABC_ALLOC( Saig_MvAnd_t, p->nObjsAlloc ); p->nTNodesSize = Aig_PrimeCudd( p->nObjsAlloc / 3 ); - p->pTNodes = CALLOC( int, p->nTNodesSize ); - p->pLevels = ALLOC( unsigned char, p->nObjsAlloc ); + p->pTNodes = ABC_CALLOC( int, p->nTNodesSize ); + p->pLevels = ABC_ALLOC( unsigned char, p->nObjsAlloc ); Saig_MvCreateObj( p, 0, 0 ); return p; } @@ -251,16 +251,16 @@ void Saig_MvManStop( Saig_MvMan_t * p ) Vec_PtrFree( p->vStates ); Vec_PtrFree( p->vFlops ); Vec_PtrFree( p->vTired ); - free( p->pRegsValues[0] ); - free( p->pRegsValues ); - free( p->nRegsValues ); - free( p->pRegsUndef ); - free( p->pAigOld ); - free( p->pTStates ); - free( p->pAigNew ); - free( p->pTNodes ); - free( p->pLevels ); - free( p ); + ABC_FREE( p->pRegsValues[0] ); + ABC_FREE( p->pRegsValues ); + ABC_FREE( p->nRegsValues ); + ABC_FREE( p->pRegsUndef ); + ABC_FREE( p->pAigOld ); + ABC_FREE( p->pTStates ); + ABC_FREE( p->pAigNew ); + ABC_FREE( p->pTNodes ); + ABC_FREE( p->pLevels ); + ABC_FREE( p ); } /**Function************************************************************* @@ -661,7 +661,7 @@ int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose ) int f, i, k, iRegMax, iState, clk = clock(); // start the manager p = Saig_MvManStart( pAig ); -PRT( "Constructing the problem", clock() - clk ); +ABC_PRT( "Constructing the problem", clock() - clk ); clk = clock(); // initiliaze registers Vec_PtrForEachEntry( p->vFlops, pEntry, i ) @@ -710,7 +710,7 @@ PRT( "Constructing the problem", clock() - clk ); pEntry->Value = Saig_MvUndef(); } } -PRT( "Multi-value simulation", clock() - clk ); +ABC_PRT( "Multi-value simulation", clock() - clk ); // implement equivalences Saig_MvManPostProcess( p, iState-1 ); Saig_MvManStop( p ); diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index 26783346..c527b152 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -52,7 +52,7 @@ struct Raig_Man_t_ int nWordsAlloc; // the number of allocated entries int nMems; // the number of used entries int nMemsMax; // the max number of used entries - int MemFree; // next free entry + int MemFree; // next ABC_FREE entry }; static inline int Raig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } @@ -146,7 +146,7 @@ Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig ) Aig_Obj_t * pObj; int i, nObjs; Aig_ManCleanData( pAig ); - p = (Raig_Man_t *)ALLOC( Raig_Man_t, 1 ); + p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 ); memset( p, 0, sizeof(Raig_Man_t) ); p->pAig = pAig; p->nPis = Saig_ManPiNum(pAig); @@ -155,10 +155,10 @@ Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig ) p->nCos = Aig_ManPoNum(pAig); p->nNodes = Aig_ManNodeNum(pAig); nObjs = p->nCis + p->nCos + p->nNodes + 2; - p->pFans0 = ALLOC( int, nObjs ); - p->pFans1 = ALLOC( int, nObjs ); - p->pRefs = ALLOC( int, nObjs ); - p->pSims = CALLOC( unsigned, nObjs ); + p->pFans0 = ABC_ALLOC( int, nObjs ); + p->pFans1 = ABC_ALLOC( int, nObjs ); + p->pRefs = ABC_ALLOC( int, nObjs ); + p->pSims = ABC_CALLOC( unsigned, nObjs ); p->vCis2Ids = Vec_IntAlloc( Aig_ManPiNum(pAig) ); // add objects (0=unused; 1=const1) p->nObjs = 2; @@ -202,12 +202,12 @@ void Raig_ManDelete( Raig_Man_t * p ) Vec_IntFree( p->vCis2Ids ); Vec_IntFree( p->vLos ); Vec_IntFree( p->vLis ); - FREE( p->pFans0 ); - FREE( p->pFans1 ); - FREE( p->pRefs ); - FREE( p->pSims ); - FREE( p->pMems ); - FREE( p ); + ABC_FREE( p->pFans0 ); + ABC_FREE( p->pFans1 ); + ABC_FREE( p->pRefs ); + ABC_FREE( p->pSims ); + ABC_FREE( p->pMems ); + ABC_FREE( p ); } /**Function************************************************************* @@ -236,7 +236,7 @@ unsigned * Raig_ManSimRef( Raig_Man_t * p, int i ) p->nMems = 1; } p->nWordsAlloc *= 2; - p->pMems = REALLOC( unsigned, p->pMems, p->nWordsAlloc ); + p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc ); memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) ); pPlace = &p->MemFree; for ( Ent = p->nMems * (p->nWords + 1); @@ -421,7 +421,7 @@ Ssw_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int // fill in the binary data Aig_ManRandom( 1 ); Counter = p->nRegs; - pData = ALLOC( unsigned, nWords ); + pData = ABC_ALLOC( unsigned, nWords ); for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) for ( i = 0; i < Aig_ManPiNum(pAig); i++ ) { @@ -433,7 +433,7 @@ Ssw_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int if ( Aig_InfoHasBit( pData, iPat ) ) Aig_InfoSetBit( p->pData, Counter + iPioId ); } - free( pData ); + ABC_FREE( pData ); return p; } @@ -500,7 +500,7 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i p->nMemsMax, 1.0*(p->nObjs * 16)/(1<<20), 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) ); - PRT( "Total time", clock() - clkTotal ); + ABC_PRT( "Total time", clock() - clkTotal ); } Raig_ManDelete( p ); return RetValue > 0; diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c index ce4b8e05..9e50c9b6 100644 --- a/src/aig/saig/saigStrSim.c +++ b/src/aig/saig/saigStrSim.c @@ -396,9 +396,9 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 ) // allocate the hash table hashing simulation info into nodes nTableSize = Aig_PrimeCudd( Aig_ManObjNum(p0)/2 ); - ppTable = CALLOC( Aig_Obj_t *, nTableSize ); - ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); - ppCands = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); + ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); + ppCands = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); // hash nodes of the first AIG Aig_ManForEachObj( p0, pObj, i ) @@ -453,9 +453,9 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 ) // cleanup Aig_ManCleanMarkA( p0 ); - free( ppTable ); - free( ppNexts ); - free( ppCands ); + ABC_FREE( ppTable ); + ABC_FREE( ppNexts ); + ABC_FREE( ppCands ); return Counter; } @@ -926,7 +926,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis i, nMatches, nFlops, 100.0*nFlops/Aig_ManRegNum(pPart0), nNodes, 100.0*nNodes/Aig_ManNodeNum(pPart0) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } if ( i == 20 ) break; @@ -959,7 +959,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis Aig_ManFanoutStop( pPart1 ); Aig_ManStop( pPart0 ); Aig_ManStop( pPart1 ); - PRT( "Total runtime", clock() - clkTotal ); + ABC_PRT( "Total runtime", clock() - clkTotal ); return vPairs; } diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c index 684551be..122483d2 100644 --- a/src/aig/saig/saigSwitch.c +++ b/src/aig/saig/saigSwitch.c @@ -63,7 +63,7 @@ Saig_SimObj_t * Saig_ManCreateMan( Aig_Man_t * p ) Saig_SimObj_t * pAig, * pEntry; Aig_Obj_t * pObj; int i; - pAig = CALLOC( Saig_SimObj_t, Aig_ManObjNumMax(p)+1 ); + pAig = ABC_CALLOC( Saig_SimObj_t, Aig_ManObjNumMax(p)+1 ); // printf( "Allocating %7.2f Mb.\n", 1.0 * sizeof(Saig_SimObj_t) * (Aig_ManObjNumMax(p)+1)/(1<<20) ); Aig_ManForEachObj( p, pObj, i ) { @@ -258,7 +258,7 @@ float Saig_ManComputeProbOnePlus( int nOnes, int nSimWords, int fCompl ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManComputeSwitchProbs_old( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) +Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) { extern char * Abc_FrameReadFlag( char * pFlag ); Saig_SimObj_t * pAig, * pEntry; @@ -269,7 +269,7 @@ Vec_Int_t * Saig_ManComputeSwitchProbs_old( Aig_Man_t * p, int nFrames, int nPre pSwitching = (float *)vSwitching->pArray; clk = clock(); pAig = Saig_ManCreateMan( p ); -//PRT( "\nCreation ", clock() - clk ); +//ABC_PRT( "\nCreation ", clock() - clk ); Aig_ManRandom( 1 ); // get the number of frames to simulate @@ -287,7 +287,7 @@ clk = clock(); //printf( "Simulating %d frames.\n", nFramesReal ); clk = clock(); Saig_ManSimulateFrames( pAig, nFramesReal, nPref ); -//PRT( "Simulation", clock() - clk ); +//ABC_PRT( "Simulation", clock() - clk ); clk = clock(); for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ ) { @@ -312,9 +312,9 @@ clk = clock(); pSwitching[pEntry-pAig] = Saig_ManComputeSwitching( pEntry->Number, nFramesReal - nPref ); //printf( "%3d : %7.2f\n", pEntry-pAig, pSwitching[pEntry-pAig] ); } - free( pAig ); -//PRT( "Switch ", clock() - clk ); -//PRT( "TOTAL ", clock() - clkTotal ); + ABC_FREE( pAig ); +//ABC_PRT( "Switch ", clock() - clk ); +//ABC_PRT( "TOTAL ", clock() - clkTotal ); // Aig_CManCreate( p ); return vSwitching; @@ -356,7 +356,7 @@ struct Aig_CMan_t_ Aig_CMan_t * Aig_CManStart( int nIns, int nNodes, int nOuts ) { Aig_CMan_t * p; - p = (Aig_CMan_t *)ALLOC( char, sizeof(Aig_CMan_t) + 2*(2*nNodes + nOuts) ); + p = (Aig_CMan_t *)ABC_ALLOC( char, sizeof(Aig_CMan_t) + 2*(2*nNodes + nOuts) ); memset( p, 0, sizeof(Aig_CMan_t) ); // set parameters p->nIns = nIns; @@ -383,7 +383,7 @@ Aig_CMan_t * Aig_CManStart( int nIns, int nNodes, int nOuts ) ***********************************************************************/ void Aig_CManStop( Aig_CMan_t * p ) { - free( p ); + ABC_FREE( p ); } /**Function************************************************************* @@ -559,22 +559,6 @@ Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p ) return pCMan; } -/**Function************************************************************* - - Synopsis [Compute switching probabilities of all nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManComputeSwitchProbs2( Aig_Man_t * p, int nFrames, int nPref, int fProbOne ) -{ - return NULL; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index c52f2f48..ff46634e 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -280,7 +280,7 @@ int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int * int * pCounters, i, w, b; int iPatBest, iTernMin; // count the number of ternary values in each pattern - pCounters = CALLOC( int, nWords * 16 ); + pCounters = ABC_CALLOC( int, nWords * 16 ); Saig_ManForEachLi( pAig, pObj, i ) { pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); @@ -300,7 +300,7 @@ int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int * if ( iTernMin == 0 ) break; } - free( pCounters ); + ABC_FREE( pCounters ); *piPat = iPatBest; return iTernMin; } @@ -512,7 +512,7 @@ clk = clock(); printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) ); if ( fVerbose ) { - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } else printf( "\n" ); @@ -588,7 +588,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq1) / Saig_ManPiNum(pAig1) ); if ( fVerbose ) { - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } else printf( "\n" ); @@ -602,7 +602,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, printf( "Design 2: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq2) / Saig_ManPiNum(pAig2) ); if ( fVerbose ) { - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } else printf( "\n" ); @@ -646,7 +646,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, if ( fVerbose ) { printf( "Miter of the synchronized designs is constructed. " ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } return pMiter; } diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index c1c2d8e9..f50af285 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -386,7 +386,7 @@ clk = clock(); { Aig_ManPrintStats( pFrames ); Aig_ManPrintStats( pFraig ); -PRT( "Fraiging", clock() - clk ); +ABC_PRT( "Fraiging", clock() - clk ); } Aig_ManStop( pFraig ); assert( pFrames->pReprs != NULL ); @@ -397,12 +397,12 @@ PRT( "Fraiging", clock() - clk ); // create reduced initialized timeframes clk = clock(); pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); -PRT( "Mapped", clock() - clk ); - // free mapping +ABC_PRT( "Mapped", clock() - clk ); + // ABC_FREE mapping Saig_ManStopMap2( pAig ); clk = clock(); pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); -PRT( "Normal", clock() - clk ); +ABC_PRT( "Normal", clock() - clk ); // report the results if ( fVerbose ) { diff --git a/src/aig/saig/saigWnd.c b/src/aig/saig/saigWnd.c index 5524e19f..10202f1b 100644 --- a/src/aig/saig/saigWnd.c +++ b/src/aig/saig/saigWnd.c @@ -99,7 +99,7 @@ Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist ) Vec_Ptr_t * vNodes; Aig_Obj_t * pObjLi, * pObjLo; int * pDists, i; - pDists = CALLOC( int, Aig_ManObjNumMax(p) ); + pDists = ABC_CALLOC( int, Aig_ManObjNumMax(p) ); vNodes = Vec_PtrAlloc( 1000 ); Aig_ManIncrementTravId( p ); Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists ); @@ -108,7 +108,7 @@ Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) assert( Aig_ObjIsTravIdCurrent(p, pObjLi) == Aig_ObjIsTravIdCurrent(p, pObjLo) ); - free( pDists ); + ABC_FREE( pDists ); return vNodes; } -- cgit v1.2.3