luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding a wrapper around clock() for more accurate time counting in ABC.

This commit is contained in:
Alan Mishchenko 2013-05-27 15:09:23 -07:00
parent 94356f0d1f
commit 19c25fd6aa
358 changed files with 3293 additions and 3275 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/aig/aig.h
View File

@ -161,8 +161,8 @@ struct Aig_Man_t_
Vec_Int_t * vCiNumsOrig; // original CI names
int nComplEdges; // complemented edges
// timing statistics
clock_t time1;
clock_t time2;
abctime time1;
abctime time2;
};
// cut computation

6
src/aig/aig/aigCanon.c
View File

@ -176,9 +176,9 @@ void Aig_RManTableResize( Aig_RMan_t * p )
Aig_Tru_t * pEntry, * pNext;
Aig_Tru_t ** pBinsOld, ** ppPlace;
int nBinsOld, Counter, i;
clock_t clk;
abctime clk;
assert( p->pBins != NULL );
clk = clock();
clk = Abc_Clock();
// save the old Bins
pBinsOld = p->pBins;
nBinsOld = p->nBins;
@ -200,7 +200,7 @@ clk = clock();
Counter++;
}
assert( Counter == p->nEntries );
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
ABC_FREE( pBinsOld );
}

4
src/aig/aig/aigCuts.c
View File

@ -633,7 +633,7 @@ Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, in
Aig_ManCut_t * p;
Aig_Obj_t * pObj;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( pAig->pManCuts == NULL );
// start the manager
p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose );
@ -652,7 +652,7 @@ Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, in
Aig_ManObjNum(pAig), nCuts, nLeafMax, nCutsK );
printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f MB ",
p->nCutSize, 4*p->nTruthWords, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
ABC_PRT( "Runtime", clock() - clk );
ABC_PRT( "Runtime", Abc_Clock() - clk );
/*
Aig_ManForEachNode( pAig, pObj, i )
if ( i % 300 == 0 )

4
src/aig/aig/aigDfs.c
View File

@ -781,12 +781,12 @@ int Aig_SupportSizeTest( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsNode(pObj) )
Counter += (Aig_SupportSize(p, pObj) <= 16);
printf( "Nodes with small support %d (out of %d)\n", Counter, Aig_ManNodeNum(p) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Counter;
}

12
src/aig/aig/aigDoms.c
View File

@ -624,7 +624,7 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit )
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
pSto = Aig_ManDomStart( pAig, Limit );
// initialize flop inputs
Saig_ManForEachLi( pAig, pObj, i )
@ -644,7 +644,7 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit )
pSto->nDomNodes, Aig_ManRegNum(pSto->pAig), pSto->nDomsTotal,
// pSto->nDomsFilter1, pSto->nDomsFilter2,
1.0 * pSto->nDomsTotal / (pSto->nDomNodes + Aig_ManRegNum(pSto->pAig)) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pSto;
}
@ -665,7 +665,7 @@ Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit )
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
pSto = Aig_ManDomStart( pAig, Limit );
// initialize flop inputs
Aig_ManForEachCo( pAig, pObj, i )
@ -685,7 +685,7 @@ Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit )
pSto->nDomNodes, Saig_ManPiNum(pSto->pAig), pSto->nDomsTotal,
// pSto->nDomsFilter1, pSto->nDomsFilter2,
1.0 * pSto->nDomsTotal / (pSto->nDomNodes + Saig_ManPiNum(pSto->pAig)) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pSto;
}
@ -706,7 +706,7 @@ Aig_Sto_t * Aig_ManComputeDomsNodes( Aig_Man_t * pAig, int Limit )
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
pSto = Aig_ManDomStart( pAig, Limit );
// initialize flop inputs
Aig_ManForEachCo( pAig, pObj, i )
@ -724,7 +724,7 @@ Aig_Sto_t * Aig_ManComputeDomsNodes( Aig_Man_t * pAig, int Limit )
pSto->nDomNodes, pSto->nDomsTotal,
// pSto->nDomsFilter1, pSto->nDomsFilter2,
1.0 * pSto->nDomsTotal / pSto->nDomNodes );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pSto;
}

24
src/aig/aig/aigInter.c
View File

@ -29,9 +29,9 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern clock_t timeCnf;
extern clock_t timeSat;
extern clock_t timeInt;
extern abctime timeCnf;
extern abctime timeSat;
extern abctime timeInt;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -54,7 +54,7 @@ void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
Cnf_Dat_t * pCnfOn, * pCnfOff;
Aig_Obj_t * pObj, * pObj2;
int Lits[3], status, i;
// clock_t clk = clock();
// abctime clk = Abc_Clock();
assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
assert( Aig_ManCoNum(pManOn) == Aig_ManCoNum(pManOff) );
@ -132,7 +132,7 @@ void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
Cnf_DataFree( pCnfOn );
Cnf_DataFree( pCnfOff );
sat_solver_delete( pSat );
// ABC_PRT( "Fast interpolation time", clock() - clk );
// ABC_PRT( "Fast interpolation time", Abc_Clock() - clk );
}
/**Function*************************************************************
@ -156,21 +156,21 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation
Vec_Int_t * vVarsAB;
Aig_Obj_t * pObj, * pObj2;
int Lits[3], status, i;
clock_t clk;
abctime clk;
int iLast = -1; // Suppress "might be used uninitialized"
assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
clk = clock();
clk = Abc_Clock();
// derive CNFs
// pCnfOn = Cnf_Derive( pManOn, 0 );
// pCnfOff = Cnf_Derive( pManOff, 0 );
pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
Cnf_DataLift( pCnfOff, pCnfOn->nVars );
timeCnf += clock() - clk;
timeCnf += Abc_Clock() - clk;
clk = clock();
clk = Abc_Clock();
// start the solver
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
@ -246,7 +246,7 @@ clk = clock();
// solve the problem
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
timeSat += clock() - clk;
timeSat += Abc_Clock() - clk;
if ( status == l_False )
{
pSatCnf = sat_solver_store_release( pSat );
@ -269,11 +269,11 @@ timeSat += clock() - clk;
}
// create the resulting manager
clk = clock();
clk = Abc_Clock();
pManInter = Inta_ManAlloc();
pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, vVarsAB, fVerbose );
Inta_ManFree( pManInter );
timeInt += clock() - clk;
timeInt += Abc_Clock() - clk;
/*
// test UNSAT core computation
{

4
src/aig/aig/aigJust.c
View File

@ -254,7 +254,7 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
Vec_Int_t * vSuppLits, * vNodes;
Aig_Obj_t * pObj;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
int Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
int nTotalLits = 0;
vSuppLits = Vec_IntAlloc( 100 );
@ -295,7 +295,7 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
Vec_IntFree( vSuppLits );
printf( "PO =%6d. C0 =%6d. C0f =%6d. C1 =%6d. C1f =%6d. (%6.2f %%) Ave =%4.1f ",
Aig_ManCoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManCoNum(pAig), 1.0*nTotalLits/(Count0+Count1) );
Abc_PrintTime( 1, "T", clock() - clk );
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
Aig_ManCleanMarkAB( pAig );
Aig_ManPackStop( pPack );
Vec_IntFree( vNodes );

28
src/aig/aig/aigPart.c
View File

@ -689,20 +689,20 @@ Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nSuppSizeLimit, int fVerbo
Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;//, * vPartPtr;
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
int i, iPart, iOut;
clock_t clk;
abctime clk;
// compute the supports for all outputs
clk = clock();
clk = Abc_Clock();
vSupports = Aig_ManSupports( p );
if ( fVerbose )
{
ABC_PRT( "Supps", clock() - clk );
ABC_PRT( "Supps", Abc_Clock() - clk );
}
// start char-based support representation
vPartSuppsBit = Vec_PtrAlloc( 1000 );
// create partitions
clk = clock();
clk = Abc_Clock();
vPartsAll = Vec_PtrAlloc( 256 );
vPartSuppsAll = Vec_PtrAlloc( 256 );
Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vOne, i )
@ -748,10 +748,10 @@ clk = clock();
//printf( "\n" );
if ( fVerbose )
{
ABC_PRT( "Parts", clock() - clk );
ABC_PRT( "Parts", Abc_Clock() - clk );
}
clk = clock();
clk = Abc_Clock();
// reorder partitions in the decreasing order of support sizes
// remember partition number in each partition support
Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
@ -774,7 +774,7 @@ clk = clock();
if ( fVerbose )
{
//ABC_PRT( "Comps", clock() - clk );
//ABC_PRT( "Comps", Abc_Clock() - clk );
}
// cleanup
@ -814,24 +814,24 @@ Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit
Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
int i, iPart, iOut;
clock_t clk;
abctime clk;
// add output number to each
clk = clock();
clk = Abc_Clock();
vSupports = Aig_ManSupportsRegisters( pAig );
assert( Vec_PtrSize(vSupports) == Aig_ManRegNum(pAig) );
Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vOne, i )
Vec_IntPush( vOne, i );
if ( fVerbose )
{
ABC_PRT( "Supps", clock() - clk );
ABC_PRT( "Supps", Abc_Clock() - clk );
}
// start char-based support representation
vPartSuppsBit = Vec_PtrAlloc( 1000 );
// create partitions
clk = clock();
clk = Abc_Clock();
vPartsAll = Vec_PtrAlloc( 256 );
vPartSuppsAll = Vec_PtrAlloc( 256 );
Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vOne, i )
@ -877,10 +877,10 @@ clk = clock();
//printf( "\n" );
if ( fVerbose )
{
ABC_PRT( "Parts", clock() - clk );
ABC_PRT( "Parts", Abc_Clock() - clk );
}
clk = clock();
clk = Abc_Clock();
// reorder partitions in the decreasing order of support sizes
// remember partition number in each partition support
Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
@ -903,7 +903,7 @@ clk = clock();
if ( fVerbose )
{
//ABC_PRT( "Comps", clock() - clk );
//ABC_PRT( "Comps", Abc_Clock() - clk );
}
// cleanup

12
src/aig/aig/aigPartSat.c
View File

@ -498,10 +498,10 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
Vec_Int_t * vNode2Part, * vNode2Var;
int nConfRemaining = nConfTotal, nNodes = 0;
int i, status, RetValue = -1;
clock_t clk;
abctime clk;
// perform partitioning according to the selected algorithm
clk = clock();
clk = Abc_Clock();
switch ( nAlgo )
{
case 0:
@ -524,7 +524,7 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
if ( fVerbose )
{
printf( "Partitioning derived %d partitions. ", Vec_IntFindMax(vNode2Part) + 1 );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// split the original AIG into partition AIGs (vAigs)
@ -536,7 +536,7 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
if ( fVerbose )
{
printf( "Partions were transformed into AIGs. " );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// synthesize partitions
@ -557,7 +557,7 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
// add partitions, one at a time, and run the SAT solver
Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
{
clk = clock();
clk = Abc_Clock();
// transform polarity of the AIG
if ( fAlignPol )
Aig_ManPartSetNodePolarity( p, pAig, Vec_VecEntryInt(vPio2Id,i) );
@ -577,7 +577,7 @@ clk = clock();
printf( "%4d : Aig = %6d. Vs = %7d. RootCs = %7d. LearnCs = %6d. ",
i, nNodes += Aig_ManNodeNum(pAig), sat_solver_nvars(pSat),
(int)pSat->stats.clauses, (int)pSat->stats.learnts );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// analize the result
if ( status == l_False )

14
src/aig/aig/aigRet.c
View File

@ -839,10 +839,10 @@ Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerb
Rtm_Obj_t * pObj, * pNext;
Aig_Obj_t * pObjAig;
int i, k, nAutos, Degree, DegreeMax = 0;
clock_t clk;
abctime clk;
// create the retiming manager
clk = clock();
clk = Abc_Clock();
pRtm = Rtm_ManFromAig( p );
// set registers
Aig_ManForEachLoSeq( p, pObjAig, i )
@ -855,7 +855,7 @@ clk = clock();
if ( fVerbose )
{
printf( "Detected %d autonomous objects. ", nAutos );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// set the current retiming number
@ -866,7 +866,7 @@ clk = clock();
pObj->Num = 0;
}
clk = clock();
clk = Abc_Clock();
// put the LOs on the queue
vQueue = Vec_PtrAlloc( 1000 );
if ( fForward )
@ -946,7 +946,7 @@ clk = clock();
printf( "Performed %d %s latch moves of max depth %d and max latch count %d.\n",
Vec_PtrSize(vQueue), fForward? "fwd":"bwd", DegreeMax, Rtm_ManLatchMax(pRtm) );
printf( "Memory usage = %d. ", pRtm->nExtraCur );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
Vec_PtrFree( vQueue );
@ -956,11 +956,11 @@ clk = clock();
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Rtm_ManFree( pRtm );
// group the registers
clk = clock();
clk = Abc_Clock();
pNew = Aig_ManReduceLaches( pNew, fVerbose );
if ( fVerbose )
{
ABC_PRT( "Register sharing time", clock() - clk );
ABC_PRT( "Register sharing time", Abc_Clock() - clk );
}
return pNew;
}

4
src/aig/aig/aigSplit.c
View File

@ -259,7 +259,7 @@ Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
DdManager * dd;
Vec_Ptr_t * vSupp, * vSubs, * vCofs;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( Saig_ManPoNum(p) != 1 )
{
printf( "Currently works only for one primary output.\n" );
@ -297,7 +297,7 @@ Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
if ( fVerbose )
printf( "Created %d cofactors (out of %d). ", Saig_ManPoNum(pRes), Vec_PtrSize(vCofs) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// dereference
Cudd_RecursiveDeref( dd, bFunc );
Vec_PtrForEachEntry( DdNode *, vCofs, bFunc, i )

6
src/aig/aig/aigTable.c
View File

@ -71,9 +71,9 @@ void Aig_TableResize( Aig_Man_t * p )
Aig_Obj_t * pEntry, * pNext;
Aig_Obj_t ** pTableOld, ** ppPlace;
int nTableSizeOld, Counter, i;
clock_t clk;
abctime clk;
assert( p->pTable != NULL );
clk = clock();
clk = Abc_Clock();
// save the old table
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
@ -97,7 +97,7 @@ clk = clock();
}
assert( Counter == Aig_ManNodeNum(p) );
// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
// replace the table and the parameters
ABC_FREE( pTableOld );
}

4
src/aig/gia/giaAig.c
View File

@ -629,7 +629,7 @@ int Gia_ManSolveSat( Gia_Man_t * p )
{
// extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
Aig_Man_t * pNew;
int RetValue;//, clk = clock();
int RetValue;//, clk = Abc_Clock();
pNew = Gia_ManToAig( p, 0 );
RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
if ( RetValue == 0 )
@ -657,7 +657,7 @@ int Gia_ManSolveSat( Gia_Man_t * p )
Abc_Print( 1, "The SAT problem is unsatisfiable. " );
else if ( RetValue == -1 )
Abc_Print( 1, "The SAT problem is undecided. " );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
*/
Aig_ManStop( pNew );
return RetValue;

4
src/aig/gia/giaBidec.c
View File

@ -237,7 +237,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
Vec_Int_t * vLeaves, * vTruth, * vVisited;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;//, clk = clock();
int i;//, clk = Abc_Clock();
pPars->nVarsMax = Gia_ManLutSizeMax( p );
pPars->fVerbose = fVerbose;
if ( pPars->nVarsMax < 2 )
@ -291,7 +291,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
if ( fVerbose )
{
// printf( "Total gain in AIG nodes = %d. ", Gia_ManObjNum(p)-Gia_ManObjNum(pNew) );
// ABC_PRT( "Total runtime", clock() - clk );
// ABC_PRT( "Total runtime", Abc_Clock() - clk );
}
return pNew;
}

14
src/aig/gia/giaCCof.c
View File

@ -221,7 +221,7 @@ int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
{
int ObjPrev = 0, ConfPrev = 0;
int Count = 0, LitOut, RetValue;
clock_t clk;
abctime clk;
// try solving for the first time and quit if converged
RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
if ( RetValue == l_False )
@ -229,7 +229,7 @@ int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
// iterate circuit cofactoring
while ( RetValue == l_True )
{
clk = clock();
clk = Abc_Clock();
// derive cofactor
LitOut = Gia_ManCofOneDerive( p, Lit );
// add the blocking clause
@ -242,7 +242,7 @@ int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
{
printf( "%3d : AIG =%7d Conf =%7d. ", Count++,
Gia_ManObjNum(p->pFrames) - ObjPrev, sat_solver_nconflicts(p->pSat) - ConfPrev );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
ObjPrev = Gia_ManObjNum(p->pFrames);
ConfPrev = sat_solver_nconflicts(p->pSat);
}
@ -269,8 +269,8 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
Ccf_Man_t * p;
Gia_Obj_t * pObj;
int f, i, Lit, RetValue = -1, fFailed = 0;
clock_t nTimeToStop = clock() + nTimeMax * CLOCKS_PER_SEC;
clock_t clk = clock();
abctime nTimeToStop = Abc_Clock() + nTimeMax * CLOCKS_PER_SEC;
abctime clk = Abc_Clock();
assert( Gia_ManPoNum(pGia) == 1 );
// create reachability manager
@ -310,7 +310,7 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
}
// report the result
if ( nTimeToStop && clock() > nTimeToStop )
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
printf( "Runtime limit (%d sec) is reached after %d frames. ", nTimeMax, f );
else if ( f == nFrameMax )
printf( "Completed %d frames without converging. ", f );
@ -318,7 +318,7 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
printf( "Backward reachability converged after %d iterations. ", f-1 );
else if ( RetValue == -1 )
printf( "Conflict limit or timeout is reached after %d frames. ", f-1 );
Abc_PrintTime( 1, "Runtime", clock() - clk );
Abc_PrintTime( 1, "Runtime", Abc_Clock() - clk );
if ( !fFailed && RetValue == 1 )
printf( "Property holds.\n" );

20
src/aig/gia/giaCSat.c
View File

@ -81,10 +81,10 @@ struct Cbs_Man_t_
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
clock_t timeSatUnsat; // unsat
clock_t timeSatSat; // sat
clock_t timeSatUndec; // undecided
clock_t timeTotal; // total runtime
abctime timeSatUnsat; // unsat
abctime timeSatSat; // sat
abctime timeSatUndec; // undecided
abctime timeTotal; // total runtime
};
static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
@ -1004,7 +1004,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
Vec_Str_t * vStatus;
Gia_Obj_t * pRoot;
int i, status;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 );
// Gia_ManCollectTest( pAig );
// prepare AIG
@ -1043,7 +1043,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
}
continue;
}
clk = clock();
clk = Abc_Clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
@ -1062,25 +1062,25 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
continue;
}
if ( status == 1 )
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
}
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs_ManSatPrintStats( p );
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );

20
src/aig/gia/giaCSatOld.c
View File

@ -73,10 +73,10 @@ struct Cbs0_Man_t_
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
clock_t timeSatUnsat; // unsat
clock_t timeSatSat; // sat
clock_t timeSatUndec; // undecided
clock_t timeTotal; // total runtime
abctime timeSatUnsat; // unsat
abctime timeSatSat; // sat
abctime timeSatUndec; // undecided
abctime timeTotal; // total runtime
};
static inline int Cbs0_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
@ -713,7 +713,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Vec_Str_t * vStatus;
Gia_Obj_t * pRoot;
int i, status;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 );
// prepare AIG
Gia_ManCreateRefs( pAig );
@ -747,7 +747,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
}
continue;
}
clk = clock();
clk = Abc_Clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
@ -765,25 +765,25 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
continue;
}
if ( status == 1 )
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
}
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs0_ManSatPrintStats( p );
Cbs0_ManStop( p );

32
src/aig/gia/giaCTas.c
View File

@ -108,10 +108,10 @@ struct Tas_Man_t_
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
clock_t timeSatUnsat; // unsat
clock_t timeSatSat; // sat
clock_t timeSatUndec; // undecided
clock_t timeTotal; // total runtime
abctime timeSatUnsat; // unsat
abctime timeSatSat; // sat
abctime timeSatUndec; // undecided
abctime timeTotal; // total runtime
};
static inline int Tas_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
@ -1525,7 +1525,7 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp;
int i, status;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 );
// Gia_ManCollectTest( pAig );
// prepare AIG
@ -1563,7 +1563,7 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
}
continue;
}
clk = clock();
clk = Abc_Clock();
// p->Pars.fUseActive = 1;
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
@ -1585,7 +1585,7 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
continue;
}
@ -1597,14 +1597,14 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
// printf( "%d ", Vec_IntSize(vCex) );
}
@ -1615,7 +1615,7 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Tas_ManSatPrintStats( p );
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
@ -1705,7 +1705,7 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
Vec_Str_t * vStatus;
Gia_Obj_t * pRoot, * pOldRoot;
int i, status;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
int Tried = 0, Stored = 0, Step = Gia_ManCoNum(pAig) / nPatMax;
assert( Gia_ManRegNum(pAig) == 0 );
// Gia_ManCollectTest( pAig );
@ -1731,7 +1731,7 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
{
assert( !Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) );
Vec_IntClear( vCex );
clk = clock();
clk = Abc_Clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Tas_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
@ -1741,7 +1741,7 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
// Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
i += Step;
continue;
@ -1750,7 +1750,7 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
// record proved
pOldRoot = (Gia_Obj_t *)Vec_PtrEntry( vOldRoots, i );
assert( !Gia_ObjProved( pAigOld, Gia_ObjId(pAigOld, pOldRoot) ) );
@ -1767,13 +1767,13 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
// save pattern
Tried++;
Stored += Tas_StorePattern( vSimInfo, vPres, vCex );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
i += Step;
}
printf( "Tried = %d Stored = %d\n", Tried, Stored );
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Tas_ManSatPrintStats( p );
Tas_ManStop( p );

4
src/aig/gia/giaCof.c
View File

@ -672,7 +672,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes )
{
Cof_Man_t * p;
clock_t clk = clock();
abctime clk = Abc_Clock();
p = Cof_ManCreateLogicSimple( pGia );
p->nLevels = 1 + Gia_ManLevelNum( pGia );
p->pLevels = ABC_CALLOC( int, p->nLevels );
@ -683,7 +683,7 @@ void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes )
Cof_ManPrintHighFanout( p, nNodes );
Gia_ManHashStop( pGia );
ABC_PRMn( "Memory for logic network", 4*p->nObjData );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
Cof_ManStop( p );
}

4
src/aig/gia/giaCone.c
View File

@ -559,7 +559,7 @@ Gia_Man_t * Gia_ManFindPoPartition( Gia_Man_t * p, int SelectShift, int fOnlyCis
Vec_Wrd_t * vSigns;
Vec_Ptr_t * vParts;
Vec_Int_t * vPart;
clock_t clk = clock();
abctime clk = Abc_Clock();
vPivots = Gia_ManFindPivots( p, SelectShift, fOnlyCis, fVerbose );
vSigns = Gia_ManDeriveSigns( p, vPivots, fVerbose );
Vec_IntFree( vPivots );
@ -574,7 +574,7 @@ Gia_Man_t * Gia_ManFindPoPartition( Gia_Man_t * p, int SelectShift, int fOnlyCis
{
*pvPosEquivs = vParts;
printf( "The algorithm divided %d POs into %d partitions. ", Gia_ManPoNum(p), Vec_PtrSize(vParts) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
else
Vec_VecFree( (Vec_Vec_t *)vParts );

12
src/aig/gia/giaDfs.c
View File

@ -210,7 +210,7 @@ void Gia_ManCollectTest( Gia_Man_t * p )
Vec_Int_t * vNodes;
Gia_Obj_t * pObj;
int i, iNode;
clock_t clk = clock();
abctime clk = Abc_Clock();
vNodes = Vec_IntAlloc( 100 );
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
@ -219,7 +219,7 @@ void Gia_ManCollectTest( Gia_Man_t * p )
Gia_ManCollectAnds( p, &iNode, 1, vNodes );
}
Vec_IntFree( vNodes );
ABC_PRT( "DFS from each output", clock() - clk );
ABC_PRT( "DFS from each output", Abc_Clock() - clk );
}
/**Function*************************************************************
@ -277,12 +277,12 @@ int Gia_ManSuppSizeTest( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjIsAnd(pObj) )
Counter += (Gia_ManSuppSizeOne(p, pObj) <= 16);
printf( "Nodes with small support %d (out of %d)\n", Counter, Gia_ManAndNum(p) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Counter;
}
@ -487,7 +487,7 @@ void Gia_ManCollectSeqTest( Gia_Man_t * p )
{
Vec_Int_t * vObjs;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
for ( i = 0; i < Gia_ManPoNum(p); i++ )
{
if ( i % 10000 == 0 )
@ -497,7 +497,7 @@ void Gia_ManCollectSeqTest( Gia_Man_t * p )
// printf( "%d ", Vec_IntSize(vObjs) );
Vec_IntFree( vObjs );
}
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

50
src/aig/gia/giaEmbed.c
View File

@ -839,12 +839,12 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
{
int nAttempts = 20;
int i, iNode, Dist;
clock_t clk;
abctime clk;
Emb_Obj_t * pPivot, * pNext;
Gia_ManRandom( 1 );
Emb_ManResetTravId( p );
// compute distances from several randomly selected PIs
clk = clock();
clk = Abc_Clock();
printf( "From inputs: " );
for ( i = 0; i < nAttempts; i++ )
{
@ -858,9 +858,9 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
Dist = Emb_ManComputeDistance_old( p, pPivot );
printf( "%d ", Dist );
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
// compute distances from several randomly selected POs
clk = clock();
clk = Abc_Clock();
printf( "From outputs: " );
for ( i = 0; i < nAttempts; i++ )
{
@ -872,9 +872,9 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
Dist = Emb_ManComputeDistance_old( p, pPivot );
printf( "%d ", Dist );
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
// compute distances from several randomly selected nodes
clk = clock();
clk = Abc_Clock();
printf( "From nodes: " );
for ( i = 0; i < nAttempts; i++ )
{
@ -887,7 +887,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
Dist = Emb_ManComputeDistance_old( p, pPivot );
printf( "%d ", Dist );
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
@ -904,11 +904,11 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
void Gia_ManTestDistance( Gia_Man_t * pGia )
{
Emb_Man_t * p;
clock_t clk = clock();
abctime clk = Abc_Clock();
p = Emb_ManStart( pGia );
// Emb_ManPrintFanio( p );
Emb_ManPrintStats( p );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
Gia_ManTestDistanceInternal( p );
Emb_ManStop( p );
}
@ -1530,7 +1530,7 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
float VertX, VertY;
int * pPermX, * pPermY;
int i, k, Iter, iMinX, iMaxX, iMinY, iMaxY;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( p->pPlacement == NULL )
return;
pEdgeX = ABC_ALLOC( float, p->nObjs );
@ -1585,7 +1585,7 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
if ( fVerbose )
{
printf( "%2d : HPWL = %e ", Iter+1, CostThis );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
}
ABC_FREE( pEdgeX );
@ -1792,12 +1792,12 @@ void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars )
{
Emb_Man_t * p;
int i;
clock_t clkSetup;
clock_t clk;
abctime clkSetup;
abctime clk;
// Gia_ManTestDistance( pGia );
// transform AIG into internal data-structure
clk = clock();
clk = Abc_Clock();
if ( pPars->fCluster )
{
p = Emb_ManStart( pGia );
@ -1816,41 +1816,41 @@ clk = clock();
Gia_ManRandom( 1 ); // reset random numbers for deterministic behavior
Emb_ManResetTravId( p );
Emb_ManSetValue( p );
clkSetup = clock() - clk;
clkSetup = Abc_Clock() - clk;
clk = clock();
clk = Abc_Clock();
Emb_ManComputeDimensions( p, pPars->nDims );
if ( pPars->fVerbose )
ABC_PRT( "Setup ", clkSetup );
if ( pPars->fVerbose )
ABC_PRT( "Dimensions", clock() - clk );
ABC_PRT( "Dimensions", Abc_Clock() - clk );
clk = clock();
clk = Abc_Clock();
Emb_ManComputeCovariance( p, pPars->nDims );
if ( pPars->fVerbose )
ABC_PRT( "Matrix ", clock() - clk );
ABC_PRT( "Matrix ", Abc_Clock() - clk );
clk = clock();
clk = Abc_Clock();
Emb_ManComputeEigenvectors( p, pPars->nDims, pPars->nSols );
Emb_ManComputeSolutions( p, pPars->nDims, pPars->nSols );
Emb_ManDerivePlacement( p, pPars->nSols );
if ( pPars->fVerbose )
ABC_PRT( "Eigenvecs ", clock() - clk );
ABC_PRT( "Eigenvecs ", Abc_Clock() - clk );
if ( pPars->fRefine )
{
clk = clock();
clk = Abc_Clock();
Emb_ManPlacementRefine( p, pPars->nIters, pPars->fVerbose );
if ( pPars->fVerbose )
ABC_PRT( "Refinement", clock() - clk );
ABC_PRT( "Refinement", Abc_Clock() - clk );
}
if ( (pPars->fDump || pPars->fDumpLarge) && pPars->nSols == 2 )
{
clk = clock();
clk = Abc_Clock();
Emb_ManDumpGnuplot( p, pGia->pName, pPars->fDumpLarge, pPars->fShowImage );
if ( pPars->fVerbose )
ABC_PRT( "Image dump", clock() - clk );
ABC_PRT( "Image dump", Abc_Clock() - clk );
}
// transfer placement

6
src/aig/gia/giaEra.c
View File

@ -529,7 +529,7 @@ int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int f
Gia_ManEra_t * p;
Gia_ObjEra_t * pState;
int Hash;
clock_t clk = clock();
abctime clk = Abc_Clock();
int RetValue = 1;
assert( Gia_ManPiNum(pAig) <= 12 );
assert( Gia_ManRegNum(pAig) > 0 );
@ -571,11 +571,11 @@ int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int f
p->iCurState, Vec_PtrSize(p->vStates), 1.0*p->iCurState/Vec_PtrSize(p->vStates), Gia_ManCountDepth(p),
(1.0/(1<<20))*(1.0*Vec_PtrSize(p->vStates)*(sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat) +
1.0*p->nBins*sizeof(unsigned) + 1.0*p->vStates->nCap * sizeof(void*)) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
}
printf( "Reachability analysis traversed %d states with depth %d. ", p->iCurState-1, Gia_ManCountDepth(p) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
if ( fDumpFile )
{
char * pFileName = "test.stg";

32
src/aig/gia/giaEra2.c
View File

@ -1537,13 +1537,13 @@ int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
Vec_Int_t * vLits, * vTfos;
Gia_Obj_t * pObj;
int i;
clock_t clk;
abctime clk;
if ( ++p->nRecCalls == MAX_CALL_NUM )
return 0;
if ( (pPivot = Gia_ManAreMostUsedPi(p)) == NULL )
{
Gia_StaAre_t * pNew;
clk = clock();
clk = Abc_Clock();
pNew = Gia_ManAreCreateStaNew( p );
pNew->iPrev = Sta;
p->fStopped = (p->fMiter && (Gia_ManCheckPOstatus(p) & 1));
@ -1554,7 +1554,7 @@ int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
return 1;
}
Gia_ManAreCubeProcess( p, pNew );
p->timeCube += clock() - clk;
p->timeCube += Abc_Clock() - clk;
return p->fStopped;
}
// remember values in the cone and perform update
@ -1613,7 +1613,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
Gia_StaAre_t * pSta;
Gia_Obj_t * pObj;
int i, RetValue;
clock_t clk = clock();
abctime clk = Abc_Clock();
pSta = Gia_ManAreSta( p, Sta );
if ( Gia_StaIsUnused(pSta) )
return 0;
@ -1657,7 +1657,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
}
// printf( "%d ", p->nRecCalls );
//printf( "%d ", Gia_ManObjNum(p->pNew) );
p->timeAig += clock() - clk;
p->timeAig += Abc_Clock() - clk;
return RetValue;
}
@ -1673,7 +1673,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
SeeAlso []
***********************************************************************/
void Gia_ManArePrintReport( Gia_ManAre_t * p, clock_t Time, int fFinal )
void Gia_ManArePrintReport( Gia_ManAre_t * p, abctime Time, int fFinal )
{
printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f MB. ",
p->iStaCur, p->nStas, 1.0*p->iStaCur/p->nStas, Gia_ManAreDepth(p, p->iStaCur),
@ -1681,11 +1681,11 @@ void Gia_ManArePrintReport( Gia_ManAre_t * p, clock_t Time, int fFinal )
4.0*p->nStaPages*p->nSize*MAX_ITEM_NUM + 16.0*p->nObjPages*MAX_ITEM_NUM)/(1<<20) );
if ( fFinal )
{
ABC_PRT( "Time", clock() - Time );
ABC_PRT( "Time", Abc_Clock() - Time );
}
else
{
ABC_PRTr( "Time", clock() - Time );
ABC_PRTr( "Time", Abc_Clock() - Time );
}
}
@ -1705,7 +1705,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
// extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose );
extern Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast );
Gia_ManAre_t * p;
clock_t clk = clock();
abctime clk = Abc_Clock();
int RetValue = 1;
if ( Gia_ManRegNum(pAig) > MAX_VARS_NUM )
{
@ -1734,22 +1734,22 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
p->fStopped ? "Stopped" : "Completed",
p->nStas, Gia_ManAreListCountUsed(p),
Gia_ManAreDepth(p, p->iStaCur-1) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
if ( pAig->pCexSeq != NULL )
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n",
p->iStaCur, pAig->pName, Gia_ManAreDepth(p, p->iStaCur)-1 );
if ( fVerbose )
{
ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube, clock() - clk );
ABC_PRTP( "Containment", p->timeCube, clock() - clk );
ABC_PRTP( "Other ", clock() - clk - p->timeAig, clock() - clk );
ABC_PRTP( "TOTAL ", clock() - clk, clock() - clk );
ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube, Abc_Clock() - clk );
ABC_PRTP( "Containment", p->timeCube, Abc_Clock() - clk );
ABC_PRTP( "Other ", Abc_Clock() - clk - p->timeAig, Abc_Clock() - clk );
ABC_PRTP( "TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
}
if ( Gia_ManRegNum(pAig) <= 30 )
{
clk = clock();
clk = Abc_Clock();
printf( "The number of unique state minterms in computed state cubes is %d. ", Gia_ManCountMinterms(p) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// printf( "Compares = %d. Equals = %d. Disj = %d. Disj2 = %d. Disj3 = %d.\n",
// p->nCompares, p->nEquals, p->nDisjs, p->nDisjs2, p->nDisjs3 );

24
src/aig/gia/giaForce.c
View File

@ -714,7 +714,7 @@ Vec_Int_t * Frc_ManCollectCos( Frc_Man_t * p )
void Frc_ManCrossCutTest( Frc_Man_t * p, Vec_Int_t * vOrderInit )
{
Vec_Int_t * vOrder;
// clock_t clk = clock();
// abctime clk = Abc_Clock();
vOrder = vOrderInit? vOrderInit : Frc_ManCollectCos( p );
printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 0 ) );
printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 1 ) );
@ -724,7 +724,7 @@ void Frc_ManCrossCutTest( Frc_Man_t * p, Vec_Int_t * vOrderInit )
Vec_IntReverseOrder( vOrder );
if ( vOrder != vOrderInit )
Vec_IntFree( vOrder );
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
}
@ -892,7 +892,7 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
float * pVertX, VertX;
int * pPermX, * pHandles;
int k, h, Iter, iMinX, iMaxX, Counter, nCutStart, nCutCur, nCutCur2, nCutPrev;
clock_t clk = clock(), clk2, clk2Total = 0;
abctime clk = Abc_Clock(), clk2, clk2Total = 0;
// create starting one-dimensional placement
vCoOrder = Frc_ManCollectCos( p );
if ( fRandomize )
@ -930,9 +930,9 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
}
assert( Counter == Frc_ManObjNum(p) );
// sort these numbers
clk2 = clock();
clk2 = Abc_Clock();
pPermX = Gia_SortFloats( pVertX, pHandles, p->nObjs );
clk2Total += clock() - clk2;
clk2Total += Abc_Clock() - clk2;
assert( pPermX == pHandles );
Vec_IntClear( vCoOrder );
for ( k = 0; k < p->nObjs; k++ )
@ -954,7 +954,7 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
{
printf( "%2d : Span = %e ", Iter+1, CostThis );
printf( "Cut = %6d (%5.2f %%) CutR = %6d ", nCutCur, 100.0*(nCutStart-nCutCur)/nCutStart, nCutCur2 );
ABC_PRTn( "Total", clock() - clk );
ABC_PRTn( "Total", Abc_Clock() - clk );
ABC_PRT( "Sort", clk2Total );
// Frc_ManCrossCutTest( p, vCoOrder );
}
@ -1068,7 +1068,7 @@ void For_ManFileExperiment()
FILE * pFile;
int * pBuffer;
int i, Size, Exp = 25;
clock_t clk = clock();
abctime clk = Abc_Clock();
int RetValue;
Size = (1 << Exp);
@ -1077,19 +1077,19 @@ void For_ManFileExperiment()
pBuffer = ABC_ALLOC( int, Size );
for ( i = 0; i < Size; i++ )
pBuffer[i] = i;
ABC_PRT( "Fillup", clock() - clk );
ABC_PRT( "Fillup", Abc_Clock() - clk );
clk = clock();
clk = Abc_Clock();
pFile = fopen( "test.txt", "rb" );
RetValue = fread( pBuffer, 1, sizeof(int) * Size, pFile );
fclose( pFile );
ABC_PRT( "Read ", clock() - clk );
ABC_PRT( "Read ", Abc_Clock() - clk );
clk = clock();
clk = Abc_Clock();
pFile = fopen( "test.txt", "wb" );
fwrite( pBuffer, 1, sizeof(int) * Size, pFile );
fclose( pFile );
ABC_PRT( "Write ", clock() - clk );
ABC_PRT( "Write ", Abc_Clock() - clk );
/*
2^25 machine words (134217728 bytes).
Fillup = 0.06 sec

8
src/aig/gia/giaFrames.c
View File

@ -227,7 +227,7 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Gia_ManUnr_t * p;
Gia_Obj_t * pObj;
int i, k, iRank, iFanin, Degree, Shift;
clock_t clk = clock();
abctime clk = Abc_Clock();
p = ABC_CALLOC( Gia_ManUnr_t, 1 );
p->pAig = pAig;
@ -291,7 +291,7 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Vec_IntSize(p->vLimit) - 1,
Gia_ManObjNum(pAig) - Gia_ManObjNum(p->pOrder),
1.0*Vec_IntSize(p->vStore)/Gia_ManObjNum(p->pOrder) - 1.0 );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return p;
}
@ -608,10 +608,10 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
Gia_Man_t * Gia_ManFrames2( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
{
Gia_Man_t * pNew;
clock_t clk = clock();
abctime clk = Abc_Clock();
pNew = Gia_ManUnroll( pAig, pPars );
if ( pPars->fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pNew;
}

4
src/aig/gia/giaFront.c
View File

@ -151,7 +151,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
char * pFront; // places used for the frontier
int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
int iFront = 0;//, clk = clock();
int iFront = 0;//, clk = Abc_Clock();
// set references for all objects
Gia_ManCreateValueRefs( p );
// start the new manager
@ -243,7 +243,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
assert( pFront[i] == 0 );
ABC_FREE( pFront );
//printf( "Crosscut = %6d. Frontier = %6d. ", nCrossCutMaxInit, pNew->nFront );
//ABC_PRT( "Time", clock() - clk );
//ABC_PRT( "Time", Abc_Clock() - clk );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}

4
src/aig/gia/giaGlitch.c
View File

@ -741,7 +741,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;
clock_t clk = clock();
abctime clk = Abc_Clock();
Gia_ManRandom( 1 );
Gli_ManFinalize( p );
if ( p->nRegs == 0 )
@ -774,7 +774,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
{
printf( "\nSimulated %d patterns. ", nPatterns );
ABC_PRMn( "Memory", 4*p->nObjData );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
}

70
src/aig/gia/giaIso.c
View File

@ -82,12 +82,12 @@ struct Gia_IsoMan_t_
Vec_Int_t * vClasses;
Vec_Int_t * vClasses2;
// statistics
clock_t timeStart;
clock_t timeSim;
clock_t timeRefine;
clock_t timeSort;
clock_t timeOther;
clock_t timeTotal;
abctime timeStart;
abctime timeSim;
abctime timeRefine;
abctime timeSort;
abctime timeOther;
abctime timeTotal;
};
static inline unsigned Gia_IsoGetValue( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i]); }
@ -178,7 +178,7 @@ void Gia_IsoPrintClasses( Gia_IsoMan_t * p )
printf( "\n" );
}
}
void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, clock_t Time )
void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, abctime Time )
{
printf( "Iter %4d : ", Iter );
printf( "Entries =%8d. ", p->nEntries );
@ -301,7 +301,7 @@ int Gia_IsoSort( Gia_IsoMan_t * p )
Gia_Obj_t * pObj, * pObj0;
int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew;
int fRefined = 0;
clock_t clk;
abctime clk;
// go through the equiv classes
p->nSingles = 0;
@ -326,9 +326,9 @@ int Gia_IsoSort( Gia_IsoMan_t * p )
}
fRefined = 1;
// sort objects
clk = clock();
clk = Abc_Clock();
Abc_QuickSort3( p->pStoreW + iBegin, nSize, 0 );
p->timeSort += clock() - clk;
p->timeSort += Abc_Clock() - clk;
// divide into new classes
iBeginOld = iBegin;
pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) );
@ -725,7 +725,7 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
Vec_Ptr_t * vEquivs = NULL;
int fRefined, fRefinedAll;
int i, c;
clock_t clk = clock(), clkTotal = clock();
abctime clk = Abc_Clock(), clkTotal = Abc_Clock();
assert( Gia_ManCiNum(pGia) > 0 );
assert( Gia_ManPoNum(pGia) > 0 );
@ -733,9 +733,9 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
p = Gia_IsoManStart( pGia );
Gia_IsoPrepare( p );
Gia_IsoAssignUnique( p );
p->timeStart = clock() - clk;
p->timeStart = Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, 0, clock() - clkTotal );
Gia_IsoPrint( p, 0, Abc_Clock() - clkTotal );
// Gia_IsoRecognizeMuxes( pGia );
@ -744,10 +744,10 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
{
for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
{
clk = clock(); Gia_IsoSimulate( p, i ); p->timeSim += clock() - clk;
clk = clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += clock() - clk;
clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, clock() - clkTotal );
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
}
}
else
@ -759,18 +759,18 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
fRefinedAll = 0;
for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
{
clk = clock(); Gia_IsoSimulate( p, i ); p->timeSim += clock() - clk;
clk = clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += clock() - clk;
clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, clock() - clkTotal );
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
}
for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
{
clk = clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += clock() - clk;
clk = clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += clock() - clk;
clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, clock() - clkTotal );
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
}
}
@ -788,18 +788,18 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
fRefinedAll = 0;
for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 )
{
clk = clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += clock() - clk;
clk = clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += clock() - clk;
clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, clock() - clkTotal );
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
}
for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 )
{
clk = clock(); Gia_IsoSimulate( p, i ); p->timeSim += clock() - clk;
clk = clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += clock() - clk;
clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, clock() - clkTotal );
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
// if ( fRefined )
// printf( "Refinedment happened.\n" );
@ -808,12 +808,12 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
}
if ( fVerbose )
Gia_IsoPrint( p, i+2, clock() - clkTotal );
Gia_IsoPrint( p, i+2, Abc_Clock() - clkTotal );
}
// Gia_IsoPrintClasses( p );
if ( fVerbose )
{
p->timeTotal = clock() - clkTotal;
p->timeTotal = Abc_Clock() - clkTotal;
p->timeOther = p->timeTotal - p->timeStart - p->timeSim - p->timeRefine;
ABC_PRTP( "Start ", p->timeStart, p->timeTotal );
ABC_PRTP( "Simulate ", p->timeSim, p->timeTotal );
@ -1080,7 +1080,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
Vec_Str_t * vStr, * vStr2;
int i, k, s, sStart, iPo, Counter;
int nClasses, nUsedPos;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( pvPosEquivs )
*pvPosEquivs = NULL;
if ( pvPiPerms )
@ -1113,7 +1113,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
printf( "Reduced %d outputs to %d candidate classes (%d outputs are in %d non-trivial classes). ",
Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fEstimate )
{
Vec_VecFree( (Vec_Vec_t *)vEquivs );
@ -1212,7 +1212,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
else
printf( "Reduced %d dual outputs to %d dual outputs. ", Gia_ManPoNum(p)/2, Gia_ManPoNum(pPart)/2 );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose )
{
printf( "Nontrivial classes:\n" );
@ -1241,10 +1241,10 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
void Gia_IsoTestOld( Gia_Man_t * p, int fVerbose )
{
Vec_Ptr_t * vEquivs;
clock_t clk = clock();
abctime clk = Abc_Clock();
vEquivs = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(p), vEquivs ? Vec_PtrSize(vEquivs) : 1 );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose && vEquivs && Gia_ManPoNum(p) != Vec_PtrSize(vEquivs) )
{
printf( "Nontrivial classes:\n" );

32
src/aig/gia/giaIso2.c
View File

@ -89,12 +89,12 @@ struct Gia_Iso2Man_t_
Vec_Int_t * vMap1; // isomorphism map
// statistics
int nIters;
clock_t timeStart;
clock_t timeSim;
clock_t timeRefine;
clock_t timeSort;
clock_t timeOther;
clock_t timeTotal;
abctime timeStart;
abctime timeSim;
abctime timeRefine;
abctime timeSort;
abctime timeOther;
abctime timeTotal;
};
////////////////////////////////////////////////////////////////////////
@ -245,7 +245,7 @@ void Gia_Iso2ManStop( Gia_Iso2Man_t * p )
Vec_IntFree( p->vVec1 );
ABC_FREE( p );
}
void Gia_Iso2ManPrint( Gia_Iso2Man_t * p, clock_t Time, int fVerbose )
void Gia_Iso2ManPrint( Gia_Iso2Man_t * p, abctime Time, int fVerbose )
{
if ( !fVerbose )
return;
@ -611,25 +611,25 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
Vec_Wec_t * Gia_Iso2ManPerform( Gia_Man_t * pGia, int fVerbose )
{
Gia_Iso2Man_t * p;
clock_t clk = clock();
abctime clk = Abc_Clock();
p = Gia_Iso2ManStart( pGia );
Gia_Iso2ManPrepare( pGia );
Gia_Iso2ManPropagate( pGia );
Gia_Iso2ManPrint( p, clock() - clk, fVerbose );
Gia_Iso2ManPrint( p, Abc_Clock() - clk, fVerbose );
while ( Gia_Iso2ManUniqify( p ) )
{
Gia_Iso2ManPrint( p, clock() - clk, fVerbose );
Gia_Iso2ManPrint( p, Abc_Clock() - clk, fVerbose );
Gia_Iso2ManPropagate( pGia );
}
Gia_Iso2ManPrint( p, clock() - clk, fVerbose );
Gia_Iso2ManPrint( p, Abc_Clock() - clk, fVerbose );
/*
Gia_Iso2ManUpdate( p, 20 );
while ( Gia_Iso2ManUniqify( p ) )
{
Gia_Iso2ManPrint( p, clock() - clk, fVerbose );
Gia_Iso2ManPrint( p, Abc_Clock() - clk, fVerbose );
Gia_Iso2ManPropagate( pGia );
}
Gia_Iso2ManPrint( p, clock() - clk, fVerbose );
Gia_Iso2ManPrint( p, Abc_Clock() - clk, fVerbose );
*/
Gia_Iso2ManStop( p );
return Gia_Iso2ManDerivePoClasses( pGia );
@ -652,13 +652,13 @@ Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_P
Vec_Wec_t * vEquivs, * vEquivs2;
Vec_Int_t * vRemains;
int nClasses, nUsedPos;
clock_t clk = clock();
abctime clk = Abc_Clock();
vEquivs = Gia_Iso2ManPerform( pGia, fVeryVerbose );
// report class stats
nClasses = Vec_WecCountNonTrivial( vEquivs, &nUsedPos );
printf( "Reduced %d outputs to %d candidate classes (%d outputs are in %d non-trivial classes). ",
Gia_ManPoNum(pGia), Vec_WecSize(vEquivs), nUsedPos, nClasses );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fEstimate )
{
Vec_WecFree( vEquivs );
@ -677,7 +677,7 @@ Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_P
nClasses = Vec_WecCountNonTrivial( vEquivs, &nUsedPos );
printf( "Reduced %d outputs to %d equivalence classes (%d outputs are in %d non-trivial classes). ",
Gia_ManPoNum(pGia), Vec_WecSize(vEquivs), nUsedPos, nClasses );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose )
{
printf( "Nontrivial classes:\n" );

10
src/aig/gia/giaRetime.c
View File

@ -268,27 +268,27 @@ Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
int i, nRegFixed, nRegMoves = 1;
clock_t clk;
abctime clk;
pNew = p;
for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
{
clk = clock();
clk = Abc_Clock();
pNew = Gia_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
if ( fVerbose )
{
printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ",
i + 1, Gia_ManAndNum(pTemp), Gia_ManRegNum(pTemp), nRegFixed, nRegMoves );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( pTemp != p )
Gia_ManStop( pTemp );
}
/*
clk = clock();
clk = Abc_Clock();
pNew = Gia_ManReduceLaches( pNew, fVerbose );
if ( fVerbose )
{
ABC_PRT( "Register sharing time", clock() - clk );
ABC_PRT( "Register sharing time", Abc_Clock() - clk );
}
*/
return pNew;

4
src/aig/gia/giaShrink.c
View File

@ -53,7 +53,7 @@ Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose )
Gia_Obj_t * pObj, * pFanin;
unsigned * pTruth;
int i, k, iFan;
clock_t clk = clock();
abctime clk = Abc_Clock();
// int ClassCounts[222] = {0};
int * pLutClass, Counter = 0;
assert( p->pMapping != NULL );
@ -139,7 +139,7 @@ Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose )
if ( fVerbose )
{
printf( "Total gain in AIG nodes = %d. ", Gia_ManObjNum(p)-Gia_ManObjNum(pNew) );
ABC_PRT( "Total runtime", clock() - clk );
ABC_PRT( "Total runtime", Abc_Clock() - clk );
}
ABC_FREE( pLutClass );
return pNew;

10
src/aig/gia/giaShrink6.c
View File

@ -402,8 +402,8 @@ Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, in
word uTruth, uTruth0, uTruth1;
int i, k, nDivs, iNode;
int RetValue, Counter1 = 0, Counter2 = 0;
clock_t clk2, clk = clock();
clock_t timeFanout = 0;
abctime clk2, clk = Abc_Clock();
abctime timeFanout = 0;
assert( p->pMapping != NULL );
pMan = Shr_ManAlloc( p );
Gia_ManFillValue( p );
@ -446,10 +446,10 @@ Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, in
Vec_IntWriteEntry( pMan->vLeaves, k, Abc_Lit2Var(pFanin->Value) );
}
// compute divisors
clk2 = clock();
clk2 = Abc_Clock();
nDivs = Shr_ManCollectDivisors( pMan, pMan->vLeaves, pMan->nDivMax, nFanoutMax );
assert( nDivs <= pMan->nDivMax );
timeFanout += clock() - clk2;
timeFanout += Abc_Clock() - clk2;
// compute truth tables
Shr_ManComputeTruths( pMan->pNew, Vec_IntSize(pMan->vLeaves), pMan->vDivs, pMan->vDivTruths, pMan->vTruths );
// perform resubstitution
@ -474,7 +474,7 @@ Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, in
{
printf( "Performed %d resubs and %d decomps. ", Counter1, Counter2 );
printf( "Gain in AIG nodes = %d. ", Gia_ManObjNum(p)-Gia_ManObjNum(pMan->pNew) );
ABC_PRT( "Runtime", clock() - clk );
ABC_PRT( "Runtime", Abc_Clock() - clk );
// ABC_PRT( "Divisors", timeFanout );
}
return Shr_ManFree( pMan );

14
src/aig/gia/giaSim.c
View File

@ -109,7 +109,7 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
int i, k, Lit, Count;
int Counter0 = 0, Counter1 = 0;
int CounterPi0 = 0, CounterPi1 = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
// create reset counters for each literal
vCountLits = Vec_IntStart( 2 * Gia_ManObjNum(pGia) );
@ -155,7 +155,7 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
Vec_IntFree( vCountLits );
printf( "Logic0 = %d (%d). Logic1 = %d (%d). ", Counter0, CounterPi0, Counter1, CounterPi1 );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return vResult;
}
@ -609,9 +609,9 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
Gia_ManSim_t * p;
clock_t clkTotal = clock();
abctime clkTotal = Abc_Clock();
int i, iOut, iPat, RetValue = 0;
clock_t nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
if ( pAig->pReprs && pAig->pNexts )
return Gia_ManSimSimulateEquiv( pAig, pPars );
ABC_FREE( pAig->pCexSeq );
@ -624,7 +624,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
if ( pPars->fVerbose )
{
Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
Abc_Print( 1, "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
}
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{
@ -648,7 +648,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
RetValue = 1;
break;
}
if ( clock() > nTimeToStop )
if ( Abc_Clock() > nTimeToStop )
{
i++;
break;
@ -659,7 +659,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
Gia_ManSimDelete( p );
if ( pAig->pCexSeq == NULL )
Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
return RetValue;
}

10
src/aig/gia/giaSim2.c
View File

@ -639,9 +639,9 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
Gia_Sim2_t * p;
Gia_Obj_t * pObj;
clock_t clkTotal = clock();
abctime clkTotal = Abc_Clock();
int i, RetValue = 0, iOut, iPat;
clock_t nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
assert( pAig->pReprs && pAig->pNexts );
ABC_FREE( pAig->pCexSeq );
p = Gia_Sim2Create( pAig, pPars );
@ -656,7 +656,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
if ( pAig->pReprs && pAig->pNexts )
Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
Abc_Print( 1, "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
}
if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
{
@ -682,7 +682,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
}
if ( pAig->pReprs && pAig->pNexts )
Gia_Sim2InfoRefineEquivs( p );
if ( clock() > nTimeToStop )
if ( Abc_Clock() > nTimeToStop )
{
i++;
break;
@ -693,7 +693,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
Gia_Sim2Delete( p );
if ( pAig->pCexSeq == NULL )
Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
return RetValue;
}

14
src/aig/gia/giaSort.c
View File

@ -160,27 +160,27 @@ void Gia_SortTest()
{
int nSize = 100000000;
int * pArray;
clock_t clk = clock();
abctime clk = Abc_Clock();
printf( "Sorting %d integers\n", nSize );
pArray = Gia_SortGetTest( nSize );
clk = clock();
clk = Abc_Clock();
qsort( pArray, nSize, 4, (int (*)(const void *, const void *)) num_cmp1 );
ABC_PRT( "qsort ", clock() - clk );
ABC_PRT( "qsort ", Abc_Clock() - clk );
Gia_SortVerifySorted( pArray, nSize );
ABC_FREE( pArray );
pArray = Gia_SortGetTest( nSize );
clk = clock();
clk = Abc_Clock();
minisat_sort( pArray, nSize, (int (*)(const void *, const void *)) num_cmp2 );
ABC_PRT( "minisat", clock() - clk );
ABC_PRT( "minisat", Abc_Clock() - clk );
Gia_SortVerifySorted( pArray, nSize );
ABC_FREE( pArray );
pArray = Gia_SortGetTest( nSize );
clk = clock();
clk = Abc_Clock();
minisat_sort2( pArray, nSize );
ABC_PRT( "minisat with inlined comparison", clock() - clk );
ABC_PRT( "minisat with inlined comparison", Abc_Clock() - clk );
Gia_SortVerifySorted( pArray, nSize );
ABC_FREE( pArray );
}

64
src/aig/gia/giaSweeper.c
View File

@ -83,13 +83,13 @@ struct Swp_Man_t_
int nSatCallsUnsat;
int nSatCallsUndec;
int nSatProofs;
clock_t timeStart;
clock_t timeTotal;
clock_t timeCnf;
clock_t timeSat;
clock_t timeSatSat;
clock_t timeSatUnsat;
clock_t timeSatUndec;
abctime timeStart;
abctime timeTotal;
abctime timeCnf;
abctime timeSat;
abctime timeSatSat;
abctime timeSatUnsat;
abctime timeSatUndec;
};
static inline int Swp_ManObj2Lit( Swp_Man_t * p, int Id ) { return Vec_IntGetEntry( p->vId2Lit, Id ); }
@ -134,7 +134,7 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
Swp_ManSetObj2Lit( p, 0, (Lit = Abc_Var2Lit(p->nSatVars++, 0)) );
Lit = Abc_LitNot(Lit);
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
p->timeStart = clock();
p->timeStart = Abc_Clock();
return p;
}
static inline void Swp_ManStop( Gia_Man_t * pGia )
@ -205,7 +205,7 @@ void Gia_SweeperPrintStats( Gia_Man_t * pGia )
ABC_PRMP( "SAT solver ", nMemSat, nMemTot );
ABC_PRMP( "TOTAL ", nMemTot, nMemTot );
printf( "Runtime usage:\n" );
p->timeTotal = clock() - p->timeStart;
p->timeTotal = Abc_Clock() - p->timeStart;
ABC_PRTP( "CNF construction", p->timeCnf, p->timeTotal );
ABC_PRTP( "SAT solving ", p->timeSat, p->timeTotal );
ABC_PRTP( " Sat ", p->timeSatSat, p->timeTotal );
@ -492,7 +492,7 @@ Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime )
Swp_ManSetObj2Lit( pSwp, 0, (iLit = Abc_Var2Lit(pSwp->nSatVars++, 0)) );
iLit = Abc_LitNot(iLit);
sat_solver_addclause( pSwp->pSat, &iLit, &iLit + 1 );
pSwp->timeStart = clock();
pSwp->timeStart = Abc_Clock();
// return the result
pNew->pData = p->pData; p->pData = NULL;
Gia_ManStop( p );
@ -673,11 +673,11 @@ static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
{
Gia_Obj_t * pNode;
int i, k, Id, Lit;
clock_t clk;
abctime clk;
// quit if CNF is ready
if ( NodeId == 0 || Swp_ManObj2Lit(p, NodeId) )
return;
clk = clock();
clk = Abc_Clock();
// start the frontier
Vec_IntClear( p->vFront );
Gia_ManObjAddToFrontier( p, NodeId, p->vFront );
@ -706,7 +706,7 @@ clk = clock();
}
assert( Vec_IntSize(p->vFanins) > 1 );
}
p->timeCnf += clock() - clk;
p->timeCnf += Abc_Clock() - clk;
}
@ -756,7 +756,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
int iLitOld, iLitNew, iLitAig, pLitsSat[2], RetValue, RetValue1, ProbeId, i;
clock_t clk;
abctime clk;
p->nSatCalls++;
assert( p->pSat != NULL );
p->vCexUser = NULL;
@ -802,32 +802,32 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
// set runtime limit for this call
if ( p->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
clk = clock();
clk = Abc_Clock();
RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
p->timeSat += clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
assert( RetValue );
pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
p->nSatCallsUndec++;
return -1;
}
@ -844,30 +844,30 @@ p->timeSatUndec += clock() - clk;
Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[0]) );
Vec_IntPush( p->vCondAssump, pLitsSat[1] );
clk = clock();
clk = Abc_Clock();
RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
p->timeSat += clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
assert( RetValue );
pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
p->nSatCallsUndec++;
return -1;
}
@ -891,7 +891,7 @@ int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
int RetValue, ProbeId, iLitAig, i;
clock_t clk;
abctime clk;
assert( p->pSat != NULL );
p->nSatCalls++;
p->vCexUser = NULL;
@ -908,16 +908,16 @@ int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
// set runtime limit for this call
if ( p->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
clk = clock();
clk = Abc_Clock();
RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( RetValue == l_False )
{
assert( Vec_IntSize(p->vCondProbes) > 0 );
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
p->nSatCallsUnsat++;
p->nSatProofs++;
return 1;
@ -925,13 +925,13 @@ p->timeSatUnsat += clock() - clk;
else if ( RetValue == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->timeSatUndec += Abc_Clock() - clk;
p->nSatCallsUndec++;
return -1;
}

8
src/aig/gia/giaSwitch.c
View File

@ -560,11 +560,11 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
Vec_Int_t * vSwitching;
float * pSwitching;
int i;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
if ( pPars->fProbOne && pPars->fProbTrans )
printf( "Conflict of options: Can either compute probability of 1, or probability of switching by observing transitions.\n" );
// create manager
clk = clock();
clk = Abc_Clock();
p = Gia_ManSwiCreate( pAig, pPars );
if ( pPars->fVerbose )
{
@ -574,7 +574,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
4.0*p->nWords*(Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig))/(1<<20) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// perform simulation
Gia_ManRandom( 1 );
@ -592,7 +592,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
if ( pPars->fVerbose )
{
printf( "Simulated %d frames with %d words. ", pPars->nIters, pPars->nWords );
ABC_PRT( "Simulation time", clock() - clkTotal );
ABC_PRT( "Simulation time", Abc_Clock() - clkTotal );
}
// derive the result
vSwitching = Vec_IntStart( Gia_ManObjNum(pAig) );

12
src/aig/gia/giaTest.c
View File

@ -379,7 +379,7 @@ void Mig_ManSetRefs( Mig_Man_t * p )
{
Mig_Obj_t * pObj;
int i, iFanin;
clock_t clk = clock();
abctime clk = Abc_Clock();
Vec_IntFill( &p->vRefs, Mig_ManObjNum(p), 0 );
// increment references
Mig_ManForEachObj( p, pObj )
@ -389,7 +389,7 @@ void Mig_ManSetRefs( Mig_Man_t * p )
// check that internal nodes have fanins
Mig_ManForEachNode( p, pObj )
assert( Vec_IntEntry(&p->vRefs, Mig_ObjId(pObj)) > 0 );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
@ -443,12 +443,12 @@ int Mig_ManSuppSizeTest( Mig_Man_t * p )
{
Mig_Obj_t * pObj;
int Counter = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
Mig_ManForEachObj( p, pObj )
if ( Mig_ObjIsNode(pObj) )
Counter += (Mig_ManSuppSizeOne(pObj) <= 16);
printf( "Nodes with small support %d (out of %d)\n", Counter, Mig_ManNodeNum(p) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Counter;
}
@ -1343,13 +1343,13 @@ finish:
void Mpm_ManPerform( Mpm_Man_t * p )
{
Mig_Obj_t * pObj;
clock_t clk = clock();
abctime clk = Abc_Clock();
int i;
Mig_ManForEachCi( p->pMig, pObj, i )
Mpm_ManObj(p, pObj)->iCutList = Mpm_CutCreateUnit( p, pObj );
Mig_ManForEachNode( p->pMig, pObj )
Mpm_ManDeriveCuts( p, pObj );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
void Mpm_ManPerformTest( Mig_Man_t * pMig )
{

4
src/aig/gia/giaTruth.c
View File

@ -223,14 +223,14 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
unsigned * pTruth;
clock_t clk = clock();
abctime clk = Abc_Clock();
int i;
Gia_ManForEachPo( p, pObj, i )
{
pTruth = (unsigned *)Gia_ObjComputeTruthTable( p, pObj );
// Extra_PrintHex( stdout, pTruth, Gia_ManPiNum(p) ); printf( "\n" );
}
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

8
src/aig/gia/giaTsim.c
View File

@ -670,10 +670,10 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
Gia_ManTer_t * p;
unsigned * pState, * pPrev, * pLoop;
int i, Counter;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) > 0 );
// create manager
clk = clock();
clk = Abc_Clock();
p = Gia_ManTerCreate( pAig );
if ( 0 )
{
@ -683,7 +683,7 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20),
4.0*Abc_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
// perform simulation
Gia_ManTerSimInfoInit( p );
@ -718,7 +718,7 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
if ( fVerbose )
{
printf( "Ternary simulation saturated after %d iterations. ", i+1 );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
return p;
}

14
src/aig/gia/giaUtil.c
View File

@ -1255,7 +1255,7 @@ unsigned * Gia_ManComputePoTruthTables( Gia_Man_t * p, int nBytesMax )
int nTotalNodes = 0, nRounds = 0;
Vec_Int_t * vObjs;
Gia_Obj_t * pObj;
clock_t clk = clock();
abctime clk = Abc_Clock();
int i;
printf( "Var = %d. Words = %d. Truths = %d.\n", nVars, nTruthWords, nTruths );
vObjs = Vec_IntAlloc( nTruths );
@ -1277,7 +1277,7 @@ unsigned * Gia_ManComputePoTruthTables( Gia_Man_t * p, int nBytesMax )
Vec_IntFree( vObjs );
printf( "Rounds = %d. Objects = %d. Total = %d. ", nRounds, Gia_ManObjNum(p), nTotalNodes );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return NULL;
}
@ -1427,8 +1427,8 @@ Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSi
Vec_Int_t * vOutMap;
Vec_Ptr_t * vCexes;
int i, k, nGroupCur, nGroups;
clock_t clk, timeComm = 0;
clock_t timeStart = clock();
abctime clk, timeComm = 0;
abctime timeStart = Abc_Clock();
// pre-conditions
assert( nGroupSize > 0 );
assert( pCommLine != NULL );
@ -1448,9 +1448,9 @@ Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSi
// set the current GIA
Abc_FrameUpdateGia( pAbc, pGroup );
// solve the group
clk = clock();
clk = Abc_Clock();
Cmd_CommandExecute( pAbc, pCommLine );
timeComm += clock() - clk;
timeComm += Abc_Clock() - clk;
// get the solution status
if ( nGroupSize == 1 )
{
@ -1485,7 +1485,7 @@ Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSi
Abc_Print( 1, "UNDEC = %6d. ", Vec_IntCountEntry(vOutMap, -1) );
Abc_Print( 1, "\n" );
Abc_PrintTime( 1, "Command time", timeComm );
Abc_PrintTime( 1, "Total time ", clock() - timeStart );
Abc_PrintTime( 1, "Total time ", Abc_Clock() - timeStart );
// cleanup
Vec_IntFree( vOuts );
Gia_ManStop( p );

4
src/aig/hop/hop.h
View File

@ -106,8 +106,8 @@ struct Hop_Man_t_
Vec_Ptr_t * vPages; // memory pages used by nodes
Hop_Obj_t * pListFree; // the list of free nodes
// timing statistics
clock_t time1;
clock_t time2;
abctime time1;
abctime time2;
};
////////////////////////////////////////////////////////////////////////

6
src/aig/hop/hopTable.c
View File

@ -168,8 +168,8 @@ void Hop_TableResize( Hop_Man_t * p )
Hop_Obj_t * pEntry, * pNext;
Hop_Obj_t ** pTableOld, ** ppPlace;
int nTableSizeOld, Counter, nEntries, i;
clock_t clk;
clk = clock();
abctime clk;
clk = Abc_Clock();
// save the old table
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
@ -193,7 +193,7 @@ clk = clock();
nEntries = Hop_ManNodeNum(p);
assert( Counter == nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
// replace the table and the parameters
ABC_FREE( pTableOld );
}

4
src/aig/ivy/ivy.h
View File

@ -125,8 +125,8 @@ struct Ivy_Man_t_
Vec_Ptr_t * vPages; // memory pages used by nodes
Ivy_Obj_t * pListFree; // the list of free nodes
// timing statistics
clock_t time1;
clock_t time2;
abctime time1;
abctime time2;
};
struct Ivy_FraigParams_t_

4
src/aig/ivy/ivyCut.c
View File

@ -969,7 +969,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
{
Ivy_Obj_t * pObj;
int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
clock_t clk = clock();
abctime clk = Abc_Clock();
nNodeTotal = nNodeOver = 0;
nCutsTotal = -Ivy_ManNodeNum(p);
Ivy_ManForEachObj( p, pObj, i )
@ -983,7 +983,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
}
printf( "Total cuts = %6d. Trivial = %6d. Nodes = %6d. Satur = %6d. ",
nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
////////////////////////////////////////////////////////////////////////

4
src/aig/ivy/ivyCutTrav.c
View File

@ -439,7 +439,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
Vec_Int_t * vStore;
Vec_Vec_t * vBitCuts;
int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
clock_t clk = clock();
abctime clk = Abc_Clock();
vNodes = Vec_PtrAlloc( 100 );
vFront = Vec_PtrAlloc( 100 );
@ -460,7 +460,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
}
printf( "Total cuts = %6d. Trivial = %6d. Nodes = %6d. Satur = %6d. ",
nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
Vec_PtrFree( vNodes );
Vec_PtrFree( vFront );

26
src/aig/ivy/ivyFastMap.c
View File

@ -67,7 +67,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj
return pSupp;
}
static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr );
static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, abctime Time, char * pStr );
static int Ivy_FastMapDelay( Ivy_Man_t * pAig );
static int Ivy_FastMapArea( Ivy_Man_t * pAig );
static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
@ -83,7 +83,7 @@ static int Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
static int Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
extern clock_t s_MappingTime;
extern abctime s_MappingTime;
extern int s_MappingMem;
@ -107,7 +107,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo
Ivy_SuppMan_t * pMan;
Ivy_Obj_t * pObj;
int i, Delay, Area;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
// start the memory for supports
pMan = ABC_ALLOC( Ivy_SuppMan_t, 1 );
memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
@ -118,7 +118,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo
memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize );
pMan->vLuts = Vec_VecAlloc( 100 );
pAig->pData = pMan;
clk = clock();
clk = Abc_Clock();
// set the PI mapping
Ivy_ObjSuppStart( pAig, Ivy_ManConst1(pAig) );
Ivy_ManForEachPi( pAig, pObj, i )
@ -130,22 +130,22 @@ clk = clock();
Delay = Ivy_FastMapDelay( pAig );
Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Delay oriented mapping: " );
Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Delay oriented mapping: " );
// 2-1-2 (doing 2-1-2-1-2 improves 0.5%)
if ( fRecovery )
{
clk = clock();
clk = Abc_Clock();
Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes
Ivy_FastMapRecover( pAig, nLimit );
Delay = Ivy_FastMapDelay( pAig );
Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " );
Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 2 : " );
clk = clock();
clk = Abc_Clock();
Ivy_FastMapRequired( pAig, Delay, 0 );
// iterate through all nodes in the topological order
Ivy_ManForEachNode( pAig, pObj, i )
@ -153,20 +153,20 @@ clk = clock();
Delay = Ivy_FastMapDelay( pAig );
Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 1 : " );
Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 1 : " );
clk = clock();
clk = Abc_Clock();
Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes
Ivy_FastMapRecover( pAig, nLimit );
Delay = Ivy_FastMapDelay( pAig );
Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " );
Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 2 : " );
}
s_MappingTime = clock() - clkTotal;
s_MappingTime = Abc_Clock() - clkTotal;
s_MappingMem = pMan->nObjs * pMan->nSize;
/*
{
@ -211,7 +211,7 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
SeeAlso []
***********************************************************************/
void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr )
void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, abctime Time, char * pStr )
{
printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area );
ABC_PRT( "Time", Time );

128
src/aig/ivy/ivyFraig.c
View File

@ -93,16 +93,16 @@ struct Ivy_FraigMan_t_
int nSatFails;
int nSatFailsReal;
// runtime
clock_t timeSim;
clock_t timeTrav;
clock_t timeSat;
clock_t timeSatUnsat;
clock_t timeSatSat;
clock_t timeSatFail;
clock_t timeRef;
clock_t timeTotal;
clock_t time1;
clock_t time2;
abctime timeSim;
abctime timeTrav;
abctime timeSat;
abctime timeSatUnsat;
abctime timeSatSat;
abctime timeSatFail;
abctime timeRef;
abctime timeTotal;
abctime time1;
abctime time2;
};
typedef struct Prove_ParamsStruct_t_ Prove_Params_t;
@ -198,7 +198,7 @@ static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t
static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose );
static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose );
static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
@ -258,7 +258,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
Ivy_FraigParams_t Params, * pIvyParams = &Params;
Ivy_Man_t * pManAig, * pManTemp;
int RetValue, nIter;
clock_t clk;//, Counter;
abctime clk;//, Counter;
ABC_INT64_T nSatConfs = 0, nSatInspects = 0;
// start the network and parameters
@ -280,7 +280,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
// if SAT only, solve without iteration
if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
{
clk = clock();
clk = Abc_Clock();
pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
RetValue = Ivy_FraigMiterStatus( pManAig );
@ -292,7 +292,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
if ( Ivy_ManNodeNum(pManAig) < 500 )
{
// run the first mitering
clk = clock();
clk = Abc_Clock();
pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
RetValue = Ivy_FraigMiterStatus( pManAig );
@ -320,7 +320,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
if ( pParams->fUseRewriting )
{ // bug in Ivy_NodeFindCutsAll() when leaves are identical!
/*
clk = clock();
clk = Abc_Clock();
Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
pManAig = Ivy_ManRwsat( pManAig, 0 );
RetValue = Ivy_FraigMiterStatus( pManAig );
@ -338,7 +338,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
// try fraiging followed by mitering
if ( pParams->fUseFraiging )
{
clk = clock();
clk = Abc_Clock();
pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp );
@ -368,7 +368,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
fflush( stdout );
}
clk = clock();
clk = Abc_Clock();
pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
if ( pParams->nTotalBacktrackLimit )
s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
@ -415,10 +415,10 @@ Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pPara
{
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
clock_t clk;
abctime clk;
if ( Ivy_ManNodeNum(pManAig) == 0 )
return Ivy_ManDup(pManAig);
clk = clock();
clk = Abc_Clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStart( pManAig, pParams );
// set global limits
@ -428,7 +428,7 @@ clk = clock();
Ivy_FraigSimulate( p );
Ivy_FraigSweep( p );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
p->timeTotal = Abc_Clock() - clk;
if ( pnSatConfs )
*pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
if ( pnSatInspects )
@ -452,16 +452,16 @@ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
clock_t clk;
abctime clk;
if ( Ivy_ManNodeNum(pManAig) == 0 )
return Ivy_ManDup(pManAig);
clk = clock();
clk = Abc_Clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStart( pManAig, pParams );
Ivy_FraigSimulate( p );
Ivy_FraigSweep( p );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
p->timeTotal = Abc_Clock() - clk;
Ivy_FraigStop( p );
return pManAigNew;
}
@ -483,8 +483,8 @@ Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
Ivy_Man_t * pManAigNew;
Ivy_Obj_t * pObj;
int i;
clock_t clk;
clk = clock();
abctime clk;
clk = Abc_Clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStartSimple( pManAig, pParams );
// set global limits
@ -508,7 +508,7 @@ clk = clock();
// remove dangling nodes
Ivy_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
p->timeTotal = Abc_Clock() - clk;
//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
//ABC_PRT( "Time", p->timeTotal );
@ -991,8 +991,8 @@ void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
clock_t clk;
clk = clock();
abctime clk;
clk = Abc_Clock();
Ivy_ManForEachNode( p->pManAig, pObj, i )
{
Ivy_NodeSimulate( p, pObj );
@ -1005,7 +1005,7 @@ clk = clock();
printf( "\n" );
*/
}
p->timeSim += clock() - clk;
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}
@ -1023,11 +1023,11 @@ p->nSimRounds++;
void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
{
Ivy_FraigSim_t * pSims;
clock_t clk;
clk = clock();
abctime clk;
clk = Abc_Clock();
for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
Ivy_NodeSimulateSim( p, pSims );
p->timeSim += clock() - clk;
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}
@ -1388,7 +1388,7 @@ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass, * pClass2;
int RetValue, Counter = 0;
clock_t clk;
abctime clk;
// check if some outputs already became non-constant
// this is a special case when computation can be stopped!!!
if ( p->pParams->fProve )
@ -1396,7 +1396,7 @@ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
if ( p->pManFraig->pData )
return 0;
// refine the classed
clk = clock();
clk = Abc_Clock();
Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
{
if ( pClass->fMarkA )
@ -1406,9 +1406,9 @@ clk = clock();
//if ( Ivy_ObjIsConst1(pClass) )
//printf( "%d ", RetValue );
//if ( Ivy_ObjIsConst1(pClass) )
// p->time1 += clock() - clk;
// p->time1 += Abc_Clock() - clk;
}
p->timeRef += clock() - clk;
p->timeRef += Abc_Clock() - clk;
return Counter;
}
@ -1793,12 +1793,12 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
SeeAlso []
***********************************************************************/
void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose )
void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose )
{
if ( !fVerbose )
return;
printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
ABC_PRT( pString, clock() - clk );
ABC_PRT( pString, Abc_Clock() - clk );
}
/**Function*************************************************************
@ -1881,13 +1881,13 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj, * pObjNew;
int i, RetValue;
clock_t clk = clock();
abctime clk = Abc_Clock();
int fVerbose = 0;
Ivy_ManForEachPo( p->pManAig, pObj, i )
{
if ( i && fVerbose )
{
ABC_PRT( "Time", clock() -clk );
ABC_PRT( "Time", Abc_Clock() -clk );
}
pObjNew = Ivy_ObjChild0Equiv(pObj);
// check if the output is constant 1
@ -1950,7 +1950,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
}
if ( fVerbose )
{
ABC_PRT( "Time", clock() -clk );
ABC_PRT( "Time", Abc_Clock() -clk );
}
}
@ -2099,7 +2099,7 @@ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
{
int pLits[4], RetValue, RetValue1, nBTLimit;
clock_t clk; //, clk2 = clock();
abctime clk; //, clk2 = Abc_Clock();
// make sure the nodes are not complemented
assert( !Ivy_IsComplement(pNew) );
@ -2141,17 +2141,17 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
clk = clock();
clk = Abc_Clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@ -2161,14 +2161,14 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
p->timeSatFail += Abc_Clock() - clk;
/*
if ( nBTLimit > 1000 )
{
@ -2194,16 +2194,16 @@ p->timeSatFail += clock() - clk;
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
clk = clock();
clk = Abc_Clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@ -2212,14 +2212,14 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
p->timeSatFail += Abc_Clock() - clk;
/*
if ( nBTLimit > 1000 )
{
@ -2238,12 +2238,12 @@ p->timeSatFail += clock() - clk;
// check BDD proof
{
int RetVal;
ABC_PRT( "Sat", clock() - clk2 );
clk2 = clock();
ABC_PRT( "Sat", Abc_Clock() - clk2 );
clk2 = Abc_Clock();
RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
// printf( "%d ", RetVal );
assert( RetVal );
ABC_PRT( "Bdd", clock() - clk2 );
ABC_PRT( "Bdd", Abc_Clock() - clk2 );
printf( "\n" );
}
*/
@ -2266,7 +2266,7 @@ p->timeSatFail += clock() - clk;
int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
{
int pLits[2], RetValue1;
clock_t clk;
abctime clk;
int RetValue;
// make sure the nodes are not complemented
@ -2293,15 +2293,15 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
Ivy_FraigSetActivityFactors( p, NULL, pNew );
// solve under assumptions
clk = clock();
clk = Abc_Clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
(ABC_INT64_T)p->pParams->nBTLimitMiter, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
@ -2310,7 +2310,7 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
p->timeSatSat += Abc_Clock() - clk;
if ( p->pPatWords )
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
@ -2318,7 +2318,7 @@ p->timeSatSat += clock() - clk;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
p->timeSatFail += Abc_Clock() - clk;
/*
if ( p->pParams->nBTLimitMiter > 1000 )
{
@ -2636,9 +2636,9 @@ int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int L
int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
{
int LevelMin, LevelMax;
clock_t clk;
abctime clk;
assert( pOld || pNew );
clk = clock();
clk = Abc_Clock();
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
@ -2653,7 +2653,7 @@ clk = clock();
if ( pNew && !Ivy_ObjIsConst1(pNew) )
Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Ivy_FraigPrintActivity( p );
p->timeTrav += clock() - clk;
p->timeTrav += Abc_Clock() - clk;
return 1;
}

8
src/aig/ivy/ivyObj.c
View File

@ -354,7 +354,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
assert( !Ivy_IsComplement(pObjNew) );
if ( fUpdateLevel )
{
//clk = clock();
//clk = Abc_Clock();
// if the new node's arrival time is different, recursively update arrival time of the fanouts
if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
{
@ -362,9 +362,9 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
pObjOld->Level = pObjNew->Level;
Ivy_ObjUpdateLevel_rec( p, pObjOld );
}
//p->time1 += clock() - clk;
//p->time1 += Abc_Clock() - clk;
// if the new node's required time has changed, recursively update required time of the fanins
//clk = clock();
//clk = Abc_Clock();
if ( p->vRequired )
{
int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
@ -374,7 +374,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
}
}
//p->time2 += clock() - clk;
//p->time2 += Abc_Clock() - clk;
}
// delete the old object
if ( fDeleteOld )

62
src/aig/ivy/ivyResyn.c
View File

@ -44,30 +44,30 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
{
clock_t clk;
abctime clk;
Ivy_Man_t * pTemp;
if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pMan, fUpdateLevel );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
clk = clock();
clk = Abc_Clock();
Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
return pMan;
}
@ -85,58 +85,58 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
***********************************************************************/
Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
{
clock_t clk;
abctime clk;
Ivy_Man_t * pTemp;
if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pMan, fUpdateLevel );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
clk = clock();
clk = Abc_Clock();
Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
clk = clock();
clk = Abc_Clock();
Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
clk = clock();
clk = Abc_Clock();
Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
return pMan;
}
@ -154,38 +154,38 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
***********************************************************************/
Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose )
{
clock_t clk;
abctime clk;
Ivy_Man_t * pTemp;
if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
Ivy_ManRewritePre( pMan, 0, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pTemp = pMan, 0 );
// pMan = Ivy_ManDup( pTemp = pMan );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
/*
clk = clock();
clk = Abc_Clock();
Ivy_ManRewritePre( pMan, 0, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Ivy_ManBalance( pTemp = pMan, 0 );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
*/
return pMan;

30
src/aig/ivy/ivyRwr.c
View File

@ -57,7 +57,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
Rwt_Man_t * pManRwt;
Ivy_Obj_t * pNode;
int i, nNodes, nGain;
clock_t clk, clkStart = clock();
abctime clk, clkStart = Abc_Clock();
// start the rewriting manager
pManRwt = Rwt_ManStart( 0 );
p->pData = pManRwt;
@ -105,14 +105,14 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
}
*/
// complement the FF if needed
clk = clock();
clk = Abc_Clock();
if ( fCompl ) Dec_GraphComplement( pGraph );
Ivy_GraphUpdateNetwork( p, pNode, pGraph, fUpdateLevel, nGain );
if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
}
}
Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
// print stats
if ( fVerbose )
Rwt_ManPrintStats( pManRwt );
@ -164,18 +164,18 @@ int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUp
int Required, nNodesSaved;
int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
int i, c, GainCur, GainBest = -1;
clock_t clk, clk2;
abctime clk, clk2;
p->nNodesConsidered++;
// get the required times
Required = fUpdateLevel? Vec_IntEntry( pMan->vRequired, pNode->Id ) : 1000000;
// get the node's cuts
clk = clock();
clk = Abc_Clock();
pStore = Ivy_NodeFindCutsAll( pMan, pNode, 5 );
p->timeCut += clock() - clk;
p->timeCut += Abc_Clock() - clk;
// go through the cuts
clk = clock();
clk = Abc_Clock();
for ( c = 1; c < pStore->nCuts; c++ )
{
pCut = pStore->pCuts + c;
@ -193,9 +193,9 @@ clk = clock();
}
p->nCutsGood++;
// get the fanin permutation
clk2 = clock();
clk2 = Abc_Clock();
uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table
p->timeTruth += clock() - clk2;
p->timeTruth += Abc_Clock() - clk2;
pPerm = p->pPerms4[ (int) p->pPerms[uTruth] ];
uPhase = p->pPhases[uTruth];
// collect fanins with the corresponding permutation/phase
@ -208,7 +208,7 @@ p->timeTruth += clock() - clk2;
pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
}
clk2 = clock();
clk2 = Abc_Clock();
/*
printf( "Considering: (" );
Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
@ -224,12 +224,12 @@ clk2 = clock();
// unmark the fanin boundary
Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
p->timeMffc += clock() - clk2;
p->timeMffc += Abc_Clock() - clk2;
// evaluate the cut
clk2 = clock();
clk2 = Abc_Clock();
pGraph = Rwt_CutEvaluate( pMan, p, pNode, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
p->timeEval += clock() - clk2;
p->timeEval += Abc_Clock() - clk2;
// check if the cut is better than the current best one
if ( pGraph != NULL && GainBest < GainCur )
@ -246,7 +246,7 @@ p->timeEval += clock() - clk2;
Vec_PtrPush( p->vFanins, pFanin );
}
}
p->timeRes += clock() - clk;
p->timeRes += Abc_Clock() - clk;
if ( GainBest == -1 )
return -1;

38
src/aig/ivy/ivySeq.c
View File

@ -65,7 +65,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
Rwt_Man_t * pManRwt;
Ivy_Obj_t * pNode;
int i, nNodes, nGain;
clock_t clk, clkStart = clock();
abctime clk, clkStart = Abc_Clock();
// set the DC latch values
Ivy_ManForEachLatch( p, pNode, i )
@ -99,14 +99,14 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
Dec_Graph_t * pGraph = (Dec_Graph_t *)Rwt_ManReadDecs(pManRwt);
int fCompl = Rwt_ManReadCompl(pManRwt);
// complement the FF if needed
clk = clock();
clk = Abc_Clock();
if ( fCompl ) Dec_GraphComplement( pGraph );
Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
}
}
Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
// print stats
if ( fVerbose )
Rwt_ManPrintStats( pManRwt );
@ -157,16 +157,16 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
int nNodesSaved;
int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
int i, c, GainCur, GainBest = -1;
clock_t clk, clk2;//, clk3;
abctime clk, clk2;//, clk3;
p->nNodesConsidered++;
// get the node's cuts
clk = clock();
clk = Abc_Clock();
pStore = Ivy_CutComputeForNode( pMan, pNode, 5 );
p->timeCut += clock() - clk;
p->timeCut += Abc_Clock() - clk;
// go through the cuts
clk = clock();
clk = Abc_Clock();
vFanout = Vec_PtrAlloc( 100 );
for ( c = 1; c < pStore->nCuts; c++ )
{
@ -185,9 +185,9 @@ clk = clock();
}
p->nCutsGood++;
// get the fanin permutation
clk2 = clock();
clk2 = Abc_Clock();
uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize ); // truth table
p->timeTruth += clock() - clk2;
p->timeTruth += Abc_Clock() - clk2;
pPerm = p->pPerms4[ (int)p->pPerms[uTruth] ];
uPhase = p->pPhases[uTruth];
// collect fanins with the corresponding permutation/phase
@ -200,7 +200,7 @@ p->timeTruth += clock() - clk2;
pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
}
clk2 = clock();
clk2 = Abc_Clock();
// mark the fanin boundary
Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
@ -213,12 +213,12 @@ clk2 = clock();
// unmark the fanin boundary
Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
p->timeMffc += clock() - clk2;
p->timeMffc += Abc_Clock() - clk2;
// evaluate the cut
clk2 = clock();
clk2 = Abc_Clock();
pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth );
p->timeEval += clock() - clk2;
p->timeEval += Abc_Clock() - clk2;
// check if the cut is better than the current best one
@ -239,7 +239,7 @@ p->timeEval += clock() - clk2;
}
}
Vec_PtrFree( vFanout );
p->timeRes += clock() - clk;
p->timeRes += Abc_Clock() - clk;
if ( GainBest == -1 )
return -1;
@ -253,9 +253,9 @@ p->timeRes += clock() - clk;
}
*/
//clk3 = clock();
//clk3 = Abc_Clock();
//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
//timeInv += clock() - clk;
//timeInv += Abc_Clock() - clk;
// nClauses += nNewClauses;
// nMoves++;
@ -1110,7 +1110,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
Ivy_Store_t * pStore;
Ivy_Obj_t * pObj;
int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( nInputs > IVY_CUT_INPUT )
{
printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
@ -1130,7 +1130,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
}
printf( "All = %6d. Minus = %6d. Triv = %6d. Node = %6d. Satur = %6d. ",
nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
////////////////////////////////////////////////////////////////////////

6
src/aig/ivy/ivyTable.c
View File

@ -207,8 +207,8 @@ void Ivy_TableResize( Ivy_Man_t * p )
{
int * pTableOld, * pPlace;
int nTableSizeOld, Counter, nEntries, e;
clock_t clk;
clk = clock();
abctime clk;
clk = Abc_Clock();
// save the old table
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
@ -231,7 +231,7 @@ clk = clock();
nEntries = Ivy_ManHashObjNum(p);
// assert( Counter == nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
// replace the table and the parameters
ABC_FREE( pTableOld );
}

4
src/aig/saig/saigConstr2.c
View File

@ -60,7 +60,7 @@ int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerb
Aig_Obj_t * pObj, * pObjLi;
unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2;
int i, w, f, RetValue = 1;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( fVerbose )
printf( "Simulating %d nodes and %d flops for %d frames with %d words... ",
Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords );
@ -196,7 +196,7 @@ int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerb
}
}
if ( fVerbose )
Abc_PrintTime( 1, "T", clock() - clk );
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
// print the state
if ( fVerbose )
{

6
src/aig/saig/saigInd.c
View File

@ -152,7 +152,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
clock_t clk;
abctime clk;
assert( fUnique == 0 || fUniqueAll == 0 );
assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetCioIds( p );
@ -180,7 +180,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
Aig_ManStop( pAigPart );
Cnf_DataFree( pCnfPart );
}
clk = clock();
clk = Abc_Clock();
// get the bottom
Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
// derive AIG for the part between top and bottom
@ -289,7 +289,7 @@ nextrun:
printf( "%4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ",
f, Aig_ManCiNum(pAigPart), Aig_ManCoNum(pAigPart), Aig_ManNodeNum(pAigPart),
nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( status == l_Undef )
break;

30
src/aig/saig/saigIso.c
View File

@ -427,8 +427,8 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
Vec_Int_t * vLevel, * vRemain;
Vec_Str_t * vStr, * vPrev;
int i, nPos;
clock_t clk = clock();
clock_t clkDup = 0, clkAig = 0, clkIso = 0, clk2;
abctime clk = Abc_Clock();
abctime clkDup = 0, clkAig = 0, clkIso = 0, clk2;
*pvPosEquivs = NULL;
// derive AIG for each PO
@ -439,17 +439,17 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
if ( i % 100 == 0 )
printf( "%6d finished...\r", i );
clk2 = clock();
clk2 = Abc_Clock();
pPart = Saig_ManDupCones( pAig, &i, 1 );
clkDup += clock() - clk2;
clkDup += Abc_Clock() - clk2;
clk2 = clock();
clk2 = Abc_Clock();
pTemp = Saig_ManDupIsoCanonical( pPart, 0 );
clkIso += clock() - clk2;
clkIso += Abc_Clock() - clk2;
clk2 = clock();
clk2 = Abc_Clock();
vStr = Ioa_WriteAigerIntoMemoryStr( pTemp );
clkAig += clock() - clk2;
clkAig += Abc_Clock() - clk2;
Vec_PtrPush( vBuffers, vStr );
Aig_ManStop( pTemp );
@ -466,11 +466,11 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
}
// sort the infos
clk = clock();
clk = Abc_Clock();
Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr );
// create classes
clk = clock();
clk = Abc_Clock();
vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
// start the first class
Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
@ -488,7 +488,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
Vec_VecFree( (Vec_Vec_t *)vBuffers );
if ( fVerbose )
Abc_PrintTime( 1, "Sorting time", clock() - clk );
Abc_PrintTime( 1, "Sorting time", Abc_Clock() - clk );
// Abc_PrintTime( 1, "Traversal time", time_Trav );
// report the results
@ -540,10 +540,10 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
{
Vec_Int_t * vPerm;
clock_t clk = clock();
abctime clk = Abc_Clock();
vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
Vec_IntFree( vPerm );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return NULL;
}
@ -561,10 +561,10 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
{
Aig_Man_t * pPart;
clock_t clk = clock();
abctime clk = Abc_Clock();
pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose && *pvPosEquivs && Saig_ManPoNum(pAig) != Vec_PtrSize(*pvPosEquivs) )
{
printf( "Nontrivial classes:\n" );

16
src/aig/saig/saigIsoFast.c
View File

@ -160,7 +160,7 @@ void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_In
Vec_IntPush( vVisited, Aig_ObjId(pObj) );
}
//static clock_t time_Trav = 0;
//static abctime time_Trav = 0;
/**Function*************************************************************
@ -181,7 +181,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
Aig_Man_t * pAig = p->pAig;
Aig_Obj_t * pObj;
int i, Value, Entry, * pPerm;
// clock_t clk = clock();
// abctime clk = Abc_Clock();
assert( Aig_ObjIsCo(pPo) );
@ -194,7 +194,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
Vec_PtrForEachEntry( Aig_Obj_t *, p->vRoots, pObj, i )
if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
Iso_StoCollectInfo_rec( pAig, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), p->vVisited, p->pData, p->vRoots );
// time_Trav += clock() - clk;
// time_Trav += Abc_Clock() - clk;
// count how many times each data entry appears
Vec_IntClear( p->vPlaces );
@ -287,7 +287,7 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
Vec_Ptr_t * vClasses, * vInfos;
Vec_Int_t * vInfo, * vPrev, * vLevel;
int i, Number, nUnique = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
// collect infos and remember their number
pMan = Iso_StoStart( pAig );
@ -299,14 +299,14 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
Vec_PtrPush( vInfos, vInfo );
}
Iso_StoStop( pMan );
Abc_PrintTime( 1, "Info computation time", clock() - clk );
Abc_PrintTime( 1, "Info computation time", Abc_Clock() - clk );
// sort the infos
clk = clock();
clk = Abc_Clock();
Vec_PtrSort( vInfos, (int (*)(void))Iso_StoCompareVecInt );
// create classes
clk = clock();
clk = Abc_Clock();
vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
// start the first class
Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
@ -323,7 +323,7 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
vPrev = vInfo;
}
Vec_VecFree( (Vec_Vec_t *)vInfos );
Abc_PrintTime( 1, "Sorting time", clock() - clk );
Abc_PrintTime( 1, "Sorting time", Abc_Clock() - clk );
// Abc_PrintTime( 1, "Traversal time", time_Trav );
// report the results

38
src/aig/saig/saigIsoSlow.c
View File

@ -290,11 +290,11 @@ struct Iso_Man_t_
Vec_Ptr_t * vClasses; // other classes
Vec_Ptr_t * vTemp1; // other classes
Vec_Ptr_t * vTemp2; // other classes
clock_t timeHash;
clock_t timeFout;
clock_t timeSort;
clock_t timeOther;
clock_t timeTotal;
abctime timeHash;
abctime timeFout;
abctime timeSort;
abctime timeOther;
abctime timeTotal;
};
static inline Iso_Obj_t * Iso_ManObj( Iso_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
@ -557,7 +557,7 @@ void Iso_ManCollectClasses( Iso_Man_t * p )
{
Iso_Obj_t * pIso;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
Vec_PtrClear( p->vSingles );
Vec_PtrClear( p->vClasses );
for ( i = 0; i < p->nBins; i++ )
@ -571,10 +571,10 @@ void Iso_ManCollectClasses( Iso_Man_t * p )
Vec_PtrPush( p->vSingles, pIso );
}
}
clk = clock();
clk = Abc_Clock();
Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
p->timeSort += clock() - clk;
p->timeSort += Abc_Clock() - clk;
assert( Vec_PtrSize(p->vSingles) == p->nSingles );
assert( Vec_PtrSize(p->vClasses) == p->nClasses );
// assign IDs to singletons
@ -1172,20 +1172,20 @@ Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose )
int fVeryVerbose = 0;
Vec_Int_t * vRes;
Iso_Man_t * p;
clock_t clk = clock(), clk2 = clock();
abctime clk = Abc_Clock(), clk2 = Abc_Clock();
p = Iso_ManCreate( pAig );
p->timeFout += clock() - clk;
p->timeFout += Abc_Clock() - clk;
Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
while ( p->nClasses )
{
// assign adjacency to classes
clk = clock();
clk = Abc_Clock();
Iso_ManAssignAdjacency( p );
p->timeFout += clock() - clk;
p->timeFout += Abc_Clock() - clk;
// rehash the class nodes
clk = clock();
clk = Abc_Clock();
Iso_ManRehashClassNodes( p );
p->timeHash += clock() - clk;
p->timeHash += Abc_Clock() - clk;
Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
// force refinement
while ( p->nSingles == 0 && p->nClasses )
@ -1194,17 +1194,17 @@ Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose )
// assign IDs to the topmost level of classes
Iso_ManBreakTies( p, fVerbose );
// assign adjacency to classes
clk = clock();
clk = Abc_Clock();
Iso_ManAssignAdjacency( p );
p->timeFout += clock() - clk;
p->timeFout += Abc_Clock() - clk;
// rehash the class nodes
clk = clock();
clk = Abc_Clock();
Iso_ManRehashClassNodes( p );
p->timeHash += clock() - clk;
p->timeHash += Abc_Clock() - clk;
Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
}
}
p->timeTotal = clock() - clk2;
p->timeTotal = Abc_Clock() - clk2;
// printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
assert( p->nObjIds == 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
// if ( p->nClasses )

8
src/aig/saig/saigMiter.c
View File

@ -1077,7 +1077,7 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe
int iOut, nOuts;
Aig_Man_t * pMiterCec;
int RetValue;
clock_t clkTotal = clock();
abctime clkTotal = Abc_Clock();
if ( fVerbose )
{
Aig_ManPrintStats( pPart0 );
@ -1112,12 +1112,12 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
if ( pMiterCec->pData == NULL )
printf( "Counter-example is not available.\n" );
else
@ -1140,7 +1140,7 @@ ABC_PRT( "Time", clock() - clkTotal );
else
{
printf( "Networks are UNDECIDED. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );
Aig_ManStop( pMiterCec );

10
src/aig/saig/saigRetFwd.c
View File

@ -214,26 +214,26 @@ Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
{
Aig_Man_t * pNew, * pTemp;
int i, nRegFixed, nRegMoves = 1;
clock_t clk;
abctime clk;
pNew = p;
for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
{
clk = clock();
clk = Abc_Clock();
pNew = Saig_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
if ( fVerbose )
{
printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ",
i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( pTemp != p )
Aig_ManStop( pTemp );
}
clk = clock();
clk = Abc_Clock();
pNew = Aig_ManReduceLaches( pNew, fVerbose );
if ( fVerbose )
{
ABC_PRT( "Register sharing time", clock() - clk );
ABC_PRT( "Register sharing time", Abc_Clock() - clk );
}
return pNew;
}

16
src/aig/saig/saigSimFast.c
View File

@ -349,14 +349,14 @@ Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref,
int * pProbs;
float * pSwitching;
int nFramesReal;
clock_t clk;//, clkTotal = clock();
abctime clk;//, clkTotal = Abc_Clock();
if ( fProbOne )
fTrans = 0;
vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
pSwitching = (float *)vSwitching->pArray;
clk = clock();
clk = Abc_Clock();
pAig = Faig_ManCreate( p );
//ABC_PRT( "\nCreation ", clock() - clk );
//ABC_PRT( "\nCreation ", Abc_Clock() - clk );
Aig_ManRandom( 1 );
// get the number of frames to simulate
// if the parameter "seqsimframes" is defined, use it
@ -371,10 +371,10 @@ clk = clock();
nFramesReal = nFrames;
}
//printf( "Simulating %d frames.\n", nFramesReal );
clk = clock();
clk = Abc_Clock();
pProbs = Faig_ManSimulateFrames( pAig, nFramesReal, nPref, fTrans );
//ABC_PRT( "Simulation", clock() - clk );
clk = clock();
//ABC_PRT( "Simulation", Abc_Clock() - clk );
clk = Abc_Clock();
if ( fTrans )
{
Aig_Obj_t * pObj;
@ -419,8 +419,8 @@ clk = clock();
}
ABC_FREE( pProbs );
ABC_FREE( pAig );
//ABC_PRT( "Switch ", clock() - clk );
//ABC_PRT( "TOTAL ", clock() - clkTotal );
//ABC_PRT( "Switch ", Abc_Clock() - clk );
//ABC_PRT( "TOTAL ", Abc_Clock() - clkTotal );
return vSwitching;
}

8
src/aig/saig/saigSimMv.c
View File

@ -882,13 +882,13 @@ Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSa
Saig_MvMan_t * p;
Saig_MvObj_t * pEntry;
int f, i, iState;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );
// start manager
p = Saig_MvManStart( pAig, nFramesSatur );
if ( fVerbose )
ABC_PRT( "Constructing the problem", clock() - clk );
ABC_PRT( "Constructing the problem", Abc_Clock() - clk );
// initialize registers
Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
@ -897,7 +897,7 @@ ABC_PRT( "Constructing the problem", clock() - clk );
if ( fVeryVerbose )
Saig_MvPrintState( 0, p );
// simulate until convergence
clk = clock();
clk = Abc_Clock();
for ( f = 0; ; f++ )
{
if ( f == nFramesSatur )
@ -937,7 +937,7 @@ ABC_PRT( "Constructing the problem", clock() - clk );
}
// printf( "Coverged after %d frames.\n", f );
if ( fVerbose )
ABC_PRT( "Multi-valued simulation", clock() - clk );
ABC_PRT( "Multi-valued simulation", Abc_Clock() - clk );
// implement equivalences
// Saig_MvManPostProcess( p, iState-1 );
vMap = Saig_MvManDeriveMap( p, fVerbose );

10
src/aig/saig/saigSimSeq.c
View File

@ -456,7 +456,7 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i
Raig_Man_t * p;
Sec_MtrStatus_t Status;
int i, iPat, RetValue = 0;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
assert( Aig_ManRegNum(pAig) > 0 );
Status = Sec_MiterStatus( pAig );
if ( Status.nSat > 0 )
@ -475,12 +475,12 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i
// iterate through objects
for ( i = 0; i < nIters; i++ )
{
clk = clock();
clk = Abc_Clock();
RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat );
if ( fVerbose )
{
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit );
printf("Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC);
printf("Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC);
}
if ( RetValue > 0 )
{
@ -491,7 +491,7 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i
printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
break;
}
if ( (clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
if ( (Abc_Clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
{
printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit );
break;
@ -503,7 +503,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) );
ABC_PRT( "Total time", clock() - clkTotal );
ABC_PRT( "Total time", Abc_Clock() - clkTotal );
}
Raig_ManDelete( p );
return RetValue > 0;

8
src/aig/saig/saigStrSim.c
View File

@ -878,7 +878,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
Aig_Man_t * pPart0, * pPart1;
Aig_Obj_t * pObj0, * pObj1;
int i, nMatches;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
Aig_ManRandom( 1 );
// consider the case when a miter is given
if ( p1 == NULL )
@ -919,7 +919,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
nMatches = 1;
for ( i = 0; nMatches > 0; i++ )
{
clk = clock();
clk = Abc_Clock();
Saig_StrSimulateRound( pPart0, pPart1 );
nMatches = Saig_StrSimDetectUnique( pPart0, pPart1 );
if ( fVerbose )
@ -930,7 +930,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) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( i == 20 )
break;
@ -963,7 +963,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 );
ABC_PRT( "Total runtime", clock() - clkTotal );
ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
return vPairs;
}

16
src/aig/saig/saigSwitch.c
View File

@ -269,12 +269,12 @@ Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref,
Vec_Int_t * vSwitching;
float * pSwitching;
int nFramesReal;
clock_t clk;//, clkTotal = clock();
abctime clk;//, clkTotal = Abc_Clock();
vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
pSwitching = (float *)vSwitching->pArray;
clk = clock();
clk = Abc_Clock();
pAig = Saig_ManCreateMan( p );
//ABC_PRT( "\nCreation ", clock() - clk );
//ABC_PRT( "\nCreation ", Abc_Clock() - clk );
Aig_ManRandom( 1 );
// get the number of frames to simulate
@ -290,10 +290,10 @@ clk = clock();
nFramesReal = nFrames;
}
//printf( "Simulating %d frames.\n", nFramesReal );
clk = clock();
clk = Abc_Clock();
Saig_ManSimulateFrames( pAig, nFramesReal, nPref );
//ABC_PRT( "Simulation", clock() - clk );
clk = clock();
//ABC_PRT( "Simulation", Abc_Clock() - clk );
clk = Abc_Clock();
for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
{
/*
@ -318,8 +318,8 @@ clk = clock();
//printf( "%3d : %7.2f\n", pEntry-pAig, pSwitching[pEntry-pAig] );
}
ABC_FREE( pAig );
//ABC_PRT( "Switch ", clock() - clk );
//ABC_PRT( "TOTAL ", clock() - clkTotal );
//ABC_PRT( "Switch ", Abc_Clock() - clk );
//ABC_PRT( "TOTAL ", Abc_Clock() - clkTotal );
// Aig_CManCreate( p );
return vSwitching;

20
src/aig/saig/saigSynch.c
View File

@ -505,9 +505,9 @@ Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose
Vec_Str_t * vSequence;
Vec_Ptr_t * vSimInfo;
int RetValue;
clock_t clk;
abctime clk;
clk = clock();
clk = Abc_Clock();
// derive synchronization sequence
vSequence = Saig_SynchSequence( pAig, nWords );
if ( vSequence == NULL )
@ -516,7 +516,7 @@ clk = clock();
printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) );
if ( fVerbose )
{
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
else
printf( "\n" );
@ -559,7 +559,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
Vec_Str_t * vSeq1, * vSeq2;
Vec_Ptr_t * vSimInfo;
int RetValue;
clock_t clk;
abctime clk;
/*
{
unsigned u = Saig_SynchRandomTernary();
@ -585,7 +585,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
}
// synchronize the first design
clk = clock();
clk = Abc_Clock();
vSeq1 = Saig_SynchSequence( pAig1, nWords );
if ( vSeq1 == NULL )
printf( "Design 1: Synchronizing sequence is not found. " );
@ -593,13 +593,13 @@ 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 )
{
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
else
printf( "\n" );
// synchronize the first design
clk = clock();
clk = Abc_Clock();
vSeq2 = Saig_SynchSequence( pAig2, nWords );
if ( vSeq2 == NULL )
printf( "Design 2: Synchronizing sequence is not found. " );
@ -607,7 +607,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 )
{
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
else
printf( "\n" );
@ -620,7 +620,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
if ( vSeq2 ) Vec_StrFree( vSeq2 );
return NULL;
}
clk = clock();
clk = Abc_Clock();
vSimInfo = Vec_PtrAllocSimInfo( Abc_MaxInt( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
// process Design 1
@ -651,7 +651,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. " );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
return pMiter;
}

14
src/aig/saig/saigTrans.c
View File

@ -379,18 +379,18 @@ Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFrame
{
// extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
clock_t clk;
abctime clk;
// create uninitialized timeframes with map1
pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
// perform fraiging for the unrolled timeframes
clk = clock();
clk = Abc_Clock();
pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
// report the results
if ( fVerbose )
{
Aig_ManPrintStats( pFrames );
Aig_ManPrintStats( pFraig );
ABC_PRT( "Fraiging", clock() - clk );
ABC_PRT( "Fraiging", Abc_Clock() - clk );
}
Aig_ManStop( pFraig );
assert( pFrames->pReprs != NULL );
@ -399,14 +399,14 @@ ABC_PRT( "Fraiging", clock() - clk );
Aig_ManStop( pFrames );
Saig_ManStopMap1( pAig );
// create reduced initialized timeframes
clk = clock();
clk = Abc_Clock();
pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
ABC_PRT( "Mapped", clock() - clk );
ABC_PRT( "Mapped", Abc_Clock() - clk );
// free mapping
Saig_ManStopMap2( pAig );
clk = clock();
clk = Abc_Clock();
pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
ABC_PRT( "Normal", clock() - clk );
ABC_PRT( "Normal", Abc_Clock() - clk );
// report the results
if ( fVerbose )
{

6
src/base/abc/abcAig.c
View File

@ -584,10 +584,10 @@ void Abc_AigResize( Abc_Aig_t * pMan )
Abc_Obj_t ** pBinsNew;
Abc_Obj_t * pEnt, * pEnt2;
int nBinsNew, Counter, i;
clock_t clk;
abctime clk;
unsigned Key;
clk = clock();
clk = Abc_Clock();
// get the new table size
nBinsNew = Abc_PrimeCudd( 3 * pMan->nBins );
// allocate a new array
@ -605,7 +605,7 @@ clk = clock();
}
assert( Counter == pMan->nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
// replace the table and the parameters
ABC_FREE( pMan->pBins );
pMan->pBins = pBinsNew;

4
src/base/abc/abcCheck.c
View File

@ -188,13 +188,13 @@ int Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
return 0;
// finally, check for combinational loops
// clk = clock();
// clk = Abc_Clock();
if ( !Abc_NtkIsAcyclic( pNtk ) )
{
fprintf( stdout, "NetworkCheck: Network contains a combinational loop.\n" );
return 0;
}
// ABC_PRT( "Acyclic ", clock() - clk );
// ABC_PRT( "Acyclic ", Abc_Clock() - clk );
// check the EXDC network if present
if ( pNtk->pExdc )

4
src/base/abc/abcDfs.c
View File

@ -836,12 +836,12 @@ int Abc_NtkSuppSizeTest( Abc_Ntk_t * p )
{
Abc_Obj_t * pObj;
int i, Counter = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
Abc_NtkForEachObj( p, pObj, i )
if ( Abc_ObjIsNode(pObj) )
Counter += (Abc_ObjSuppSize(pObj) <= 16);
printf( "Nodes with small support %d (out of %d)\n", Counter, Abc_NtkNodeNum(p) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Counter;
}

24
src/base/abc/abcHieCec.c
View File

@ -670,7 +670,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
Abc_Ntk_t * pNtk, * pModel;
Gia_Man_t * pGia;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
// read hierarchical netlist
pNtk = Io_ReadBlifMv( pFileName, 0, fCheck );
@ -685,16 +685,16 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
// Abc_NtkDelete( pNtk );
// return NULL;
}
Abc_PrintTime( 1, "Reading file", clock() - clk );
Abc_PrintTime( 1, "Reading file", Abc_Clock() - clk );
assert( Abc_NtkIsNetlist(pNtk) );
assert( !Abc_NtkLatchNum(pNtk) );
/*
if ( pNtk->pDesign != NULL )
{
clk = clock();
clk = Abc_Clock();
Abc_NtkCountNodes( pNtk );
Abc_PrintTime( 1, "Count nodes", clock() - clk );
Abc_PrintTime( 1, "Count nodes", Abc_Clock() - clk );
}
*/
// print stats
@ -716,14 +716,14 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
if ( fUseNew )
{
clk = clock();
clk = Abc_Clock();
vOrder = Abc_NtkCollectHie( pNtk );
Abc_PrintTime( 1, "Collect DFS ", clock() - clk );
Abc_PrintTime( 1, "Collect DFS ", Abc_Clock() - clk );
// derive GIA
clk = clock();
clk = Abc_Clock();
pGia = Abc_NtkDeriveFlatGia2( pNtk, vOrder );
Abc_PrintTime( 1, "Deriving GIA", clock() - clk );
Abc_PrintTime( 1, "Deriving GIA", Abc_Clock() - clk );
Gia_ManPrintStats( pGia, 0, 0, 0 );
// Gia_ManStop( pGia );
@ -737,9 +737,9 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
pModel->pData = Abc_NtkDfsBoxes( pModel );
// derive GIA
clk = clock();
clk = Abc_Clock();
pGia = Abc_NtkDeriveFlatGia( pNtk );
Abc_PrintTime( 1, "Deriving GIA", clock() - clk );
Abc_PrintTime( 1, "Deriving GIA", Abc_Clock() - clk );
Gia_ManPrintStats( pGia, 0, 0, 0 );
// clean nodes/boxes of all nodes
@ -747,9 +747,9 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
Vec_PtrFree( (Vec_Ptr_t *)pModel->pData );
}
clk = clock();
clk = Abc_Clock();
Abc_NtkCountInst( pNtk );
Abc_PrintTime( 1, "Gather stats", clock() - clk );
Abc_PrintTime( 1, "Gather stats", Abc_Clock() - clk );
Abc_NtkDelete( pNtk );
return pGia;

40
src/base/abc/abcHieNew.c
View File

@ -493,7 +493,7 @@ void Au_ManCountThings( Au_Man_t * p )
{
Au_Ntk_t * pNtk, * pBoxModel;
Au_Obj_t * pBox;
int i, k;//, clk = clock();
int i, k;//, clk = Abc_Clock();
Au_ManForEachNtkReverse( p, pNtk, i )
{
pNtk->nBoxes = Au_NtkBoxNum(pNtk);
@ -533,7 +533,7 @@ void Au_ManCountThings( Au_Man_t * p )
printf( "Total ANDs = %15.0f.\n", pNtk->nNodeAnds );
printf( "Total XORs = %15.0f.\n", pNtk->nNodeXors );
printf( "Total MUXes = %15.0f.\n", pNtk->nNodeMuxs );
// Abc_PrintTime( 1, "Time", clock() - clk );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
int Au_NtkCompareNames( Au_Ntk_t ** p1, Au_Ntk_t ** p2 )
@ -1494,24 +1494,24 @@ Gia_Man_t * Au_ManDeriveTest( Abc_Ntk_t * pRoot )
Abc_Ntk_t * pMod;
Au_Man_t * pMan;
Au_Ntk_t * pNtk = NULL;
clock_t clk1, clk2 = 0, clk3 = 0, clk = clock();
abctime clk1, clk2 = 0, clk3 = 0, clk = Abc_Clock();
int i;
clk1 = clock();
clk1 = Abc_Clock();
pMan = Au_ManAlloc( pRoot->pDesign ? pRoot->pDesign->pName : pRoot->pName );
pMan->pFuncs = Abc_NamStart( 100, 16 );
clk2 += clock() - clk1;
clk2 += Abc_Clock() - clk1;
vModels = Abc_NtkCollectHie( pRoot );
Vec_PtrForEachEntry( Abc_Ntk_t *, vModels, pMod, i )
{
vOrder = Abc_NtkDfsBoxes( pMod );
clk1 = clock();
clk1 = Abc_Clock();
pNtk = Au_NtkDerive( pMan, pMod, vOrder );
pMod->iStep = pNtk->Id;
pMod->pData = pNtk;
clk2 += clock() - clk1;
clk2 += Abc_Clock() - clk1;
Vec_PtrFree( vOrder );
}
@ -1536,21 +1536,21 @@ Gia_Man_t * Au_ManDeriveTest( Abc_Ntk_t * pRoot )
// if ( !Abc_NtkCheckRecursive(pRoot) )
{
clk1 = clock();
clk1 = Abc_Clock();
pGia = Au_NtkDeriveFlatGia( pNtk );
clk3 = clock() - clk1;
clk3 = Abc_Clock() - clk1;
// printf( "GIA objects max = %d.\n", pMan->nGiaObjMax );
}
// clk1 = clock();
// clk1 = Abc_Clock();
// Au_NtkSuppSizeTest( (Au_Ntk_t *)pRoot->pData );
// clk4 = clock() - clk1;
// clk4 = Abc_Clock() - clk1;
clk1 = clock();
clk1 = Abc_Clock();
Au_ManDelete( pMan );
clk2 += clock() - clk1;
clk2 += Abc_Clock() - clk1;
Abc_PrintTime( 1, "Time all ", clock() - clk );
Abc_PrintTime( 1, "Time all ", Abc_Clock() - clk );
Abc_PrintTime( 1, "Time new ", clk2 );
Abc_PrintTime( 1, "Time GIA ", clk3 );
// Abc_PrintTime( 1, "Time supp", clk4 );
@ -1573,7 +1573,7 @@ Gia_Man_t * Abc_NtkHieCecTest2( char * pFileName, char * pModelName, int fVerbos
int fSimulation = 0;
Gia_Man_t * pGia = NULL;
Au_Ntk_t * pNtk, * pNtkClp = NULL;
clock_t clk1 = 0, clk = clock();
abctime clk1 = 0, clk = Abc_Clock();
// read hierarchical netlist
pNtk = Au_NtkParseCBlif( pFileName );
@ -1588,7 +1588,7 @@ Gia_Man_t * Abc_NtkHieCecTest2( char * pFileName, char * pModelName, int fVerbos
Au_NtkFree( pNtk );
return NULL;
}
Abc_PrintTime( 1, "Reading file", clock() - clk );
Abc_PrintTime( 1, "Reading file", Abc_Clock() - clk );
if ( fVerbose )
{
@ -1608,21 +1608,21 @@ Gia_Man_t * Abc_NtkHieCecTest2( char * pFileName, char * pModelName, int fVerbos
Au_NtkCheckRecursive( pNtkClp );
// collapse
clk1 = clock();
clk1 = Abc_Clock();
if ( fSimulation )
{
Au_NtkTerSimulate( pNtkClp );
Abc_PrintTime( 1, "Time sim ", clock() - clk1 );
Abc_PrintTime( 1, "Time sim ", Abc_Clock() - clk1 );
}
else
{
pGia = Au_NtkDeriveFlatGia( pNtkClp );
Abc_PrintTime( 1, "Time GIA ", clock() - clk1 );
Abc_PrintTime( 1, "Time GIA ", Abc_Clock() - clk1 );
}
// delete
Au_ManDelete( pNtk->pMan );
Abc_PrintTime( 1, "Time all ", clock() - clk );
Abc_PrintTime( 1, "Time all ", Abc_Clock() - clk );
return pGia;
}

8
src/base/abc/abcUtil.c
View File

@ -2543,7 +2543,7 @@ void Abc_NtkReverseTopoOrderTest( Abc_Ntk_t * p )
Vec_Int_t * vVisited;
Abc_Obj_t * pObj;
int i;//, k, iBeg, iEnd;
clock_t clk = clock();
abctime clk = Abc_Clock();
Abc_NtkReverseTopoOrder( p );
/*
printf( "Reverse topological order for nodes:\n" );
@ -2558,9 +2558,9 @@ void Abc_NtkReverseTopoOrderTest( Abc_Ntk_t * p )
}
*/
Vec_IntFreeP( &p->vTopo );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// compute regular fanout orders
clk = clock();
clk = Abc_Clock();
vVisited = Vec_IntAlloc( 1000 );
Abc_NtkForEachNode( p, pObj, i )
{
@ -2569,7 +2569,7 @@ void Abc_NtkReverseTopoOrderTest( Abc_Ntk_t * p )
Abc_NtkReverse_rec( pObj, vVisited );
}
Vec_IntFree( vVisited );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************

30
src/base/abci/abc.c
View File

@ -11692,7 +11692,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Prove_Params_t Params, * pParams = &Params;
Abc_Ntk_t * pNtk, * pNtkTemp;
int c, RetValue, iOut = -1;
clock_t clk;
abctime clk;
extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
@ -11802,7 +11802,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
clk = clock();
clk = Abc_Clock();
if ( Abc_NtkIsStrash(pNtk) )
pNtkTemp = Abc_NtkDup( pNtk );
@ -11836,7 +11836,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
// update counter example
@ -20308,7 +20308,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int nConfLimit;
int nInsLimit;
clock_t clk;
abctime clk;
// set defaults
fVerbose = 0;
nConfLimit = 0;
@ -20361,7 +20361,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
clk = clock();
clk = Abc_Clock();
if ( Abc_NtkIsStrash(pNtk) )
{
RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fVerbose, NULL, NULL );
@ -20401,7 +20401,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
else
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 0;
usage:
@ -20441,7 +20441,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int nLearnedDelta;
int nLearnedPerce;
int nInsLimit;
clock_t clk;
abctime clk;
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
// set defaults
@ -20556,7 +20556,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
clk = clock();
clk = Abc_Clock();
RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
// verify that the pattern is correct
if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
@ -20575,7 +20575,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
else
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 0;
usage:
@ -20618,7 +20618,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAlignPol;
int fSynthesize;
int fVerbose;
clock_t clk;
abctime clk;
extern int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
// set defaults
@ -20699,7 +20699,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
clk = clock();
clk = Abc_Clock();
RetValue = Abc_NtkPartitionedSat( pNtk, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
// verify that the pattern is correct
if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
@ -20729,7 +20729,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
else
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 0;
usage:
@ -20770,7 +20770,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkTemp;
Prove_Params_t Params, * pParams = &Params;
int c, RetValue;
clock_t clk;
abctime clk;
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
@ -20880,7 +20880,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Currently can only solve the miter with one output.\n" );
return 0;
}
clk = clock();
clk = Abc_Clock();
if ( Abc_NtkIsStrash(pNtk) )
pNtkTemp = Abc_NtkDup( pNtk );
@ -20906,7 +20906,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
return 0;

6
src/base/abci/abcAuto.c
View File

@ -128,14 +128,14 @@ void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
int nAutoSymsMaxSupp;
int nAutoSymOuts;
int nSuppSizeMax;
clock_t clk;
abctime clk;
nAutoSymOuts = 0;
nAutoSyms = 0;
nAutoSymsMax = 0;
nAutoSymsMaxSupp = 0;
nSuppSizeMax = 0;
clk = clock();
clk = Abc_Clock();
SigCounter = 0;
for ( o = 0; o < nOutputs; o++ )
@ -196,7 +196,7 @@ void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
printf( "SumK=%3d ", nAutoSyms );
printf( "KMax=%2d ", nAutoSymsMax );
printf( "Supp=%3d ", nAutoSymsMaxSupp );
printf( "Time=%4.2f ", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
printf( "Time=%4.2f ", (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC) );
printf( "\n" );
}

4
src/base/abci/abcBidec.c
View File

@ -114,7 +114,7 @@ void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
Abc_Obj_t * pObj;
Vec_Int_t * vTruth;
int i, nGainTotal = 0, nNodes1, nNodes2;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( Abc_NtkIsLogic(pNtk) );
if ( !Abc_NtkToAig(pNtk) )
return;
@ -142,7 +142,7 @@ void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
if ( fVerbose )
{
printf( "Total gain in AIG nodes = %d. ", nGainTotal );
ABC_PRT( "Total runtime", clock() - clk );
ABC_PRT( "Total runtime", Abc_Clock() - clk );
}
}

26
src/base/abci/abcBm.c
View File

@ -871,7 +871,7 @@ int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nIn
static sat_solver * pSat = NULL;
lbool status;
int RetValue;
clock_t clk;
abctime clk;
extern int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
@ -887,7 +887,7 @@ int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nIn
// fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
// load clauses into the sat_solver
clk = clock();
clk = Abc_Clock();
@ -900,13 +900,13 @@ int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nIn
//return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
// PRT( "Time", Abc_Clock() - clk );
// simplify the problem
clk = clock();
clk = Abc_Clock();
status = sat_solver_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
// PRT( "Time", Abc_Clock() - clk );
if ( status == 0 )
{
sat_solver_delete( pSat );
@ -915,7 +915,7 @@ int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nIn
}
// solve the miter
clk = clock();
clk = Abc_Clock();
if ( fVerbose )
pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@ -936,7 +936,7 @@ int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nIn
}
else
assert( 0 );
// PRT( "SAT sat_solver time", clock() - clk );
// PRT( "SAT sat_solver time", Abc_Clock() - clk );
// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
// if the problem is SAT, get the counterexample
@ -1583,7 +1583,7 @@ float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_In
Vec_Int_t * oMatchedGroups;
FILE *result;
int matchFound;
clock_t clk = clock();
abctime clk = Abc_Clock();
float satTime = 0.0;
/*matchFile = fopen("satmatch.txt", "w");*/
@ -1712,7 +1712,7 @@ float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_In
Abc_NtkDelete(subNtk2);
}
satTime = (float)(clock() - clk)/(float)(CLOCKS_PER_SEC);
satTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC);
if( matchFound )
{
@ -1788,7 +1788,7 @@ void bmGateWay( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int p_equivalence )
char * vPiValues1, * vPiValues2;
int * observability1, * observability2;
clock_t clk = clock();
abctime clk = Abc_Clock();
float initTime;
float simulTime;
float satTime;
@ -1930,8 +1930,8 @@ void bmGateWay( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int p_equivalence )
printf(" done!\n");
initTime = ((float)(clock() - clk)/(float)(CLOCKS_PER_SEC));
clk = clock();
initTime = ((float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC));
clk = Abc_Clock();
topOrder1 = findTopologicalOrder(pNtk1);
topOrder2 = findTopologicalOrder(pNtk2);
@ -1982,7 +1982,7 @@ void bmGateWay( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int p_equivalence )
printf(" done!\n");
simulTime = (float)(clock() - clk)/(float)(CLOCKS_PER_SEC);
simulTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC);
printf("SAT-based search started ...\n");
satTime = refineBySAT(pNtk1, iMatch1, iGroup1, iDep1, &iLastItem1, oMatch1, oGroup1, oDep1, &oLastItem1, observability1,

4
src/base/abci/abcCas.c
View File

@ -61,7 +61,7 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
char * pFileGeneric;
int fBddSizeMax = 500000;
int i, fReorder = 1;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
@ -72,7 +72,7 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
{
DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
ABC_PRT( "BDD construction time", clock() - clk );
ABC_PRT( "BDD construction time", Abc_Clock() - clk );
}
// collect global BDDs

4
src/base/abci/abcCollapse.c
View File

@ -49,7 +49,7 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
@ -59,7 +59,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
{
DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
ABC_PRT( "BDD construction time", clock() - clk );
ABC_PRT( "BDD construction time", Abc_Clock() - clk );
}
// create the new network

14
src/base/abci/abcCut.c
View File

@ -128,7 +128,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
Vec_Ptr_t * vNodes;
Vec_Int_t * vChoices;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
@ -201,10 +201,10 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
Vec_PtrFree( vNodes );
Vec_IntFree( vChoices );
Cut_ManPrintStats( p );
ABC_PRT( "TOTAL", clock() - clk );
ABC_PRT( "TOTAL", Abc_Clock() - clk );
// printf( "Area = %d.\n", Abc_NtkComputeArea( pNtk, p ) );
//Abc_NtkPrintCuts( p, pNtk, 0 );
// Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
// Cut_ManPrintStatsToFile( p, pNtk->pSpec, Abc_Clock() - clk );
// temporary printout of stats
if ( nTotal )
@ -229,7 +229,7 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
{
Abc_Obj_t * pObj;
Vec_Ptr_t * vNodes;
int i; //, clk = clock();
int i; //, clk = Abc_Clock();
int fDrop = Cut_OracleReadDrop(p);
assert( Abc_NtkIsStrash(pNtk) );
@ -268,7 +268,7 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
}
}
Vec_PtrFree( vNodes );
//ABC_PRT( "Total", clock() - clk );
//ABC_PRT( "Total", Abc_Clock() - clk );
//Abc_NtkPrintCuts_( p, pNtk, 0 );
}
@ -291,7 +291,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
Abc_Obj_t * pObj, * pNode;
int i, nIters, fStatus;
Vec_Int_t * vChoices;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( Abc_NtkIsSeq(pNtk) );
assert( pParams->fSeq );
@ -368,7 +368,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
if ( pParams->fVerbose )
{
Cut_ManPrintStats( p );
ABC_PRT( "TOTAL ", clock() - clk );
ABC_PRT( "TOTAL ", Abc_Clock() - clk );
printf( "Converged after %d iterations.\n", nIters );
}
//Abc_NtkPrintCuts( p, pNtk, 1 );

116
src/base/abci/abcDar.c
View File

@ -1225,7 +1225,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
clock_t clk;
abctime clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
@ -1243,10 +1243,10 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
// Aig_ManStop( pTemp );
clk = clock();
clk = Abc_Clock();
pMan = Aig_ManDupDfs( pTemp = pMan );
Aig_ManStop( pTemp );
//ABC_PRT( "time", clock() - clk );
//ABC_PRT( "time", Abc_Clock() - clk );
// Aig_ManPrintStats( pMan );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@ -1269,7 +1269,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
clock_t clk;
abctime clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
@ -1280,10 +1280,10 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
// Aig_ManStop( pTemp );
clk = clock();
clk = Abc_Clock();
pMan = Aig_ManDupDfs( pTemp = pMan );
Aig_ManStop( pTemp );
//ABC_PRT( "time", clock() - clk );
//ABC_PRT( "time", Abc_Clock() - clk );
// Aig_ManPrintStats( pMan );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@ -1306,17 +1306,17 @@ Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fF
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
clock_t clk;
abctime clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
// Aig_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
Aig_ManStop( pTemp );
//ABC_PRT( "time", clock() - clk );
//ABC_PRT( "time", Abc_Clock() - clk );
// Aig_ManPrintStats( pMan );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@ -1369,12 +1369,12 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
Gia_Man_t * pGia;
clock_t clk;
abctime clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
clk = clock();
clk = Abc_Clock();
if ( pPars->fSynthesis )
pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
else
@ -1382,7 +1382,7 @@ clk = clock();
pGia = Gia_ManFromAig( pMan );
Aig_ManStop( pMan );
}
pPars->timeSynth = clock() - clk;
pPars->timeSynth = Abc_Clock() - clk;
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else
@ -1412,17 +1412,17 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
clock_t clk;
abctime clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
// Aig_ManPrintStats( pMan );
clk = clock();
clk = Abc_Clock();
pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose );
Aig_ManStop( pTemp );
//ABC_PRT( "time", clock() - clk );
//ABC_PRT( "time", Abc_Clock() - clk );
// Aig_ManPrintStats( pMan );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@ -1520,7 +1520,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
// Cnf_Man_t * pManCnf = NULL;
Cnf_Dat_t * pCnf;
Abc_Ntk_t * pNtkNew = NULL;
clock_t clk = clock();
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
// convert to the AIG manager
@ -1551,7 +1551,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
if ( fVerbose )
{
Abc_Print( 1, "Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/*
@ -1584,7 +1584,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
{
Aig_Man_t * pMan;
int RetValue;//, clk = clock();
int RetValue;//, clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
// assert( Abc_NtkPoNum(pNtk) == 1 );
@ -1610,7 +1610,7 @@ int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConf
{
extern int Aig_ManPartitionedSat( Aig_Man_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
Aig_Man_t * pMan;
int RetValue;//, clk = clock();
int RetValue;//, clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
@ -1636,7 +1636,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa
Aig_Man_t * pMan, * pMan1, * pMan2;
Abc_Ntk_t * pMiter;
int RetValue;
clock_t clkTotal = clock();
abctime clkTotal = Abc_Clock();
/*
{
extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose );
@ -1721,17 +1721,17 @@ finish:
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else
{
Abc_Print( 1, "Networks are UNDECIDED. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );
return RetValue;
@ -1753,7 +1753,7 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
Aig_Man_t * pMan, * pTemp;
clock_t clk = clock();
abctime clk = Abc_Clock();
// preprocess the miter by fraiging it
// (note that for each functional class, fraiging leaves one representative;
@ -1765,7 +1765,7 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
if ( pPars->fVerbose )
{
ABC_PRT( "Initial fraiging time", clock() - clk );
ABC_PRT( "Initial fraiging time", Abc_Clock() - clk );
}
}
else
@ -2037,8 +2037,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
Aig_Man_t * pMan;
Vec_Int_t * vMap = NULL;
int status, RetValue = -1;
clock_t clk = clock();
clock_t nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
abctime clk = Abc_Clock();
abctime nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
// derive the AIG manager
if ( fOrDecomp )
pMan = Abc_NtkToDarBmc( pNtk, &vMap );
@ -2069,7 +2069,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
else if ( RetValue == -1 )
{
Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame,0) );
if ( nTimeLimit && clock() > nTimeLimit )
if ( nTimeLimit && Abc_Clock() > nTimeLimit )
Abc_Print( 1, "(timeout %d sec). ", nTimeLimit );
else
Abc_Print( 1, "(conf limit %d). ", nBTLimit );
@ -2079,7 +2079,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
Abc_Cex_t * pCex = pNtk->pSeqModel;
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
}
else
{
@ -2119,8 +2119,8 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
Aig_Man_t * pMan;
Vec_Int_t * vMap = NULL;
int status, RetValue = -1;
clock_t clk = clock();
clock_t nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
abctime clk = Abc_Clock();
abctime nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
if ( fOrDecomp && !pPars->fSolveAll )
pMan = Abc_NtkToDarBmc( pNtk, &vMap );
else
@ -2147,7 +2147,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
if ( pPars->nFailOuts == 0 )
{
Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
if ( nTimeOut && clock() > nTimeOut )
if ( nTimeOut && Abc_Clock() > nTimeOut )
Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
else
Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
@ -2155,7 +2155,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
else
{
Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
if ( clock() > nTimeOut )
if ( Abc_Clock() > nTimeOut )
Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
else
Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
@ -2187,7 +2187,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
if ( pNtk->pSeqModel )
{
status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
@ -2216,7 +2216,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man_t ** ppNtkRes )
{
int RetValue = -1, iFrame;
clock_t clk = clock();
abctime clk = Abc_Clock();
int nTotalProvedSat = 0;
assert( pMan->nRegs > 0 );
if ( ppNtkRes )
@ -2307,7 +2307,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
Abc_Print( 1, "Property UNDECIDED. " );
else
assert( 0 );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
return RetValue;
}
@ -2541,13 +2541,13 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
{
Aig_Man_t * pMan;
int iFrame = -1, RetValue = -1;
clock_t clkTotal = clock();
abctime clkTotal = Abc_Clock();
if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
{
Prove_Params_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkComb;
int RetValue;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( Abc_NtkLatchNum(pNtk) == 0 )
Abc_Print( 1, "The network has no latches. Running CEC.\n" );
// create combinational network
@ -2563,11 +2563,11 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
{
pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
Abc_Print( 1, "Networks are not equivalent.\n" );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
if ( pSecPar->fReportSolution )
{
Abc_Print( 1, "SOLUTION: FAIL " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
return RetValue;
}
@ -2576,11 +2576,11 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent after CEC. " );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
if ( pSecPar->fReportSolution )
{
Abc_Print( 1, "SOLUTION: PASS " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
return RetValue;
}
@ -2603,7 +2603,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
if ( pSecPar->fReportSolution )
{
Abc_Print( 1, "SOLUTION: FAIL " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
// return the counter-example generated
ABC_FREE( pNtk->pModel );
@ -2738,7 +2738,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
{
int RetValue = -1;
clock_t clk = clock();
abctime clk = Abc_Clock();
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@ -2773,7 +2773,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
else
assert( 0 );
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
/*
Abc_Print( 1, "Status: " );
if ( pPars->pOutMap )
@ -3219,7 +3219,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
Aig_Man_t * pMan;
Abc_Cex_t * pCex;
int status, RetValue = -1;
clock_t clk = clock();
abctime clk = Abc_Clock();
if ( Abc_NtkGetChoiceNum(pNtk) )
{
Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
@ -3296,7 +3296,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
}
Fra_SmlStop( pSml );
}
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
Aig_ManStop( pMan );
return RetValue;
}
@ -3316,7 +3316,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars )
{
Aig_Man_t * pMan;
int status, RetValue = -1;
// clock_t clk = clock();
// abctime clk = Abc_Clock();
if ( Abc_NtkGetChoiceNum(pNtk) )
{
Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
@ -3346,7 +3346,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars )
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
// ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", Abc_Clock() - clk );
pNtk->pData = pMan->pData; pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
@ -3454,7 +3454,7 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC
int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pMan;
clock_t clkTotal = clock();
abctime clkTotal = Abc_Clock();
int RetValue;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@ -3463,17 +3463,17 @@ int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUn
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else
{
Abc_Print( 1, "Networks are UNDECIDED. " );
ABC_PRT( "Time", clock() - clkTotal );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( fGetCex )
{
@ -3568,9 +3568,9 @@ void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
Aig_ManStop( pManOff );
}
clock_t timeCnf;
clock_t timeSat;
clock_t timeInt;
abctime timeCnf;
abctime timeSat;
abctime timeInt;
/**Function*************************************************************
@ -3587,7 +3587,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation
{
Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
Abc_Obj_t * pObj;
int i; //, clk = clock();
int i; //, clk = Abc_Clock();
if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
{
Abc_Print( 1, "Currently works only for networks with equal number of POs.\n" );
@ -3639,7 +3639,7 @@ timeInt = 0;
// ABC_PRT( "CNF", timeCnf );
// ABC_PRT( "SAT", timeSat );
// ABC_PRT( "Int", timeInt );
// ABC_PRT( "Slow interpolation time", clock() - clk );
// ABC_PRT( "Slow interpolation time", Abc_Clock() - clk );
// return the network
if ( !Abc_NtkCheck( pNtkInter ) )

8
src/base/abci/abcDebug.c
View File

@ -52,7 +52,7 @@ void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
Abc_Ntk_t * pNtkMod;
char * pFileName = "bug_found.blif";
int i, nSteps, nIter, ModNum, RandNum = 1;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
assert( Abc_NtkIsLogic(pNtk) );
srand( 0x123123 );
// create internal copy of the network
@ -66,7 +66,7 @@ void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
// perform incremental modifications
for ( nIter = 0; ; nIter++ )
{
clk = clock();
clk = Abc_Clock();
// count how many ways of modifying the network exists
nSteps = 2 * Abc_NtkCountFaninsTotal(pNtk);
// try modifying the network as many times
@ -91,14 +91,14 @@ void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
}
printf( "Iter %6d : Latches = %6d. Nodes = %6d. Steps = %6d. Error step = %3d. ",
nIter, Abc_NtkLatchNum(pNtk), Abc_NtkNodeNum(pNtk), nSteps, i );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
if ( i == nSteps ) // could not modify it while preserving the bug
break;
}
// write out the final network
Io_WriteBlifLogic( pNtk, pFileName, 1 );
printf( "Final network written into file \"%s\". ", pFileName );
ABC_PRT( "Total time", clock() - clkTotal );
ABC_PRT( "Total time", Abc_Clock() - clkTotal );
Abc_NtkDelete( pNtk );
}

4
src/base/abci/abcDec.c
View File

@ -464,7 +464,7 @@ void Abc_TtStoreTest( char * pFileName )
***********************************************************************/
void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
{
clock_t clk = clock();
abctime clk = Abc_Clock();
int i, nNodes = 0;
char * pAlgoName = NULL;
@ -556,7 +556,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
else assert( 0 );
printf( "AIG nodes =%9d ", nNodes );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************

6
src/base/abci/abcDress2.c
View File

@ -358,7 +358,7 @@ void Abc_NtkDressPrintEquivs( Vec_Ptr_t * vRes )
SeeAlso []
***********************************************************************/
void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, clock_t Time )
void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, abctime Time )
{
Vec_Int_t * vClass;
int i, k, Entry;
@ -419,10 +419,10 @@ void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, clock_t
void Abc_NtkDress2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConflictLimit, int fVerbose )
{
Vec_Ptr_t * vRes;
clock_t clk = clock();
abctime clk = Abc_Clock();
vRes = Abc_NtkDressComputeEquivs( pNtk1, pNtk2, nConflictLimit, fVerbose );
// Abc_NtkDressPrintEquivs( vRes );
Abc_NtkDressPrintStats( vRes, Abc_NtkNodeNum(pNtk1), Abc_NtkNodeNum(pNtk1), clock() - clk );
Abc_NtkDressPrintStats( vRes, Abc_NtkNodeNum(pNtk1), Abc_NtkNodeNum(pNtk1), Abc_Clock() - clk );
Vec_VecFree( (Vec_Vec_t *)vRes );
}

4
src/base/abci/abcFraig.c
View File

@ -698,7 +698,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
Vec_Ptr_t * vStore;
Abc_Ntk_t * pNtk, * pFraig;
int nWords1, nWords2, nWordsMin;
// clock_t clk = clock();
// abctime clk = Abc_Clock();
// get the stored network
vStore = Abc_FrameReadStore();
@ -744,7 +744,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
// perform partitioned computation of structural choices
pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
Abc_NtkFraigStoreClean();
//ABC_PRT( "Total choicing time", clock() - clk );
//ABC_PRT( "Total choicing time", Abc_Clock() - clk );
return pFraig;
}

12
src/base/abci/abcFx.c
View File

@ -102,7 +102,7 @@ struct Fx_Man_t_
Vec_Int_t * vCubeFree; // cube-free divisor
Vec_Int_t * vDiv; // selected divisor
// statistics
clock_t timeStart; // starting time
abctime timeStart; // starting time
int nVars; // original problem variables
int nLits; // the number of SOP literals
int nDivs; // the number of extracted divisors
@ -435,7 +435,7 @@ static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv )
printf( " " );
printf( "Lits =%7d ", p->nLits );
printf( "Divs =%8d ", Hsh_VecSize(p->pHash) );
Abc_PrintTime( 1, "Time", clock() - p->timeStart );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->timeStart );
}
static void Fx_PrintDivisors( Fx_Man_t * p )
{
@ -480,7 +480,7 @@ static void Fx_PrintMatrix( Fx_Man_t * p )
Fx_PrintLiterals( p );
Fx_PrintDivisors( p );
}
static void Fx_PrintStats( Fx_Man_t * p, clock_t clk )
static void Fx_PrintStats( Fx_Man_t * p, abctime clk )
{
printf( "Cubes =%7d ", Vec_WecSizeUsed(p->vCubes) );
printf( "Lits =%7d ", Vec_WecSizeUsed(p->vLits) );
@ -1116,7 +1116,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC
int fVeryVerbose = 0;
int i, iDiv;
Fx_Man_t * p;
clock_t clk = clock();
abctime clk = Abc_Clock();
// initialize the data-structure
p = Fx_ManStart( vCubes );
p->LitCountMax = LitCountMax;
@ -1125,9 +1125,9 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC
if ( fVeryVerbose )
Fx_PrintMatrix( p );
if ( fVerbose )
Fx_PrintStats( p, clock() - clk );
Fx_PrintStats( p, Abc_Clock() - clk );
// perform extraction
p->timeStart = clock();
p->timeStart = Abc_Clock();
for ( i = 0; i < nNewNodesMax && Vec_QueTopCost(p->vPrio) > 0.0; i++ )
{
iDiv = Vec_QuePop(p->vPrio);

4
src/base/abci/abcIf.c
View File

@ -71,7 +71,7 @@ void Abc_NtkIfComputeSwitching( Abc_Ntk_t * pNtk, If_Man_t * pIfMan )
Aig_Man_t * pAig;
If_Obj_t * pObjIf;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
// map IF objects into old network
Abc_NtkForEachObj( pNtk, pObjAbc, i )
if ( (pObjIf = (If_Obj_t *)pObjAbc->pTemp) )
@ -99,7 +99,7 @@ void Abc_NtkIfComputeSwitching( Abc_Ntk_t * pNtk, If_Man_t * pIfMan )
pSwitching[i] = pObjAbc->dTemp;
if ( pIfMan->pPars->fVerbose )
{
ABC_PRT( "Computing switching activity", clock() - clk );
ABC_PRT( "Computing switching activity", Abc_Clock() - clk );
}
}

26
src/base/abci/abcIvy.c
View File

@ -84,7 +84,7 @@ extern int timeRetime;
Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
{
Ivy_Man_t * pMan;
//timeRetime = clock();
//timeRetime = Abc_Clock();
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
@ -119,7 +119,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
Vec_IntFree( vInit );
// Ivy_ManPrintStats( pMan );
}
//timeRetime = clock() - timeRetime;
//timeRetime = Abc_Clock() - timeRetime;
return pMan;
}
@ -197,7 +197,7 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
clock_t clk;
abctime clk;
// int i;
/*
extern int nMoves;
@ -213,9 +213,9 @@ timeInv = 0;
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
//timeRetime = clock();
//timeRetime = Abc_Clock();
clk = clock();
clk = Abc_Clock();
Ivy_ManHaigStart( pMan, fVerbose );
// Ivy_ManRewriteSeq( pMan, 0, 0 );
// for ( i = 0; i < nIters; i++ )
@ -227,7 +227,7 @@ clk = clock();
Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "%d ", Ivy_ManNodeNum(pMan) );
//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
//ABC_PRT( " ", clock() - clk );
//ABC_PRT( " ", Abc_Clock() - clk );
//printf( "\n" );
/*
printf( "Moves = %d. ", nMoves );
@ -238,7 +238,7 @@ clk = clock();
// Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
// Ivy_ManHaigPostprocess( pMan, fVerbose );
//timeRetime = clock() - timeRetime;
//timeRetime = Abc_Clock() - timeRetime;
// write working AIG into the current network
// pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
@ -289,9 +289,9 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
//timeRetime = clock();
//timeRetime = Abc_Clock();
Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
//timeRetime = clock() - timeRetime;
//timeRetime = Abc_Clock() - timeRetime;
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
@ -315,9 +315,9 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
//timeRetime = clock();
//timeRetime = Abc_Clock();
Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
//timeRetime = clock() - timeRetime;
//timeRetime = Abc_Clock() - timeRetime;
// Ivy_ManRewriteSeq( pMan, 1, 0 );
// Ivy_ManRewriteSeq( pMan, 1, 0 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
@ -543,7 +543,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
// apply AIG rewriting
if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
{
// clock_t clk = clock();
// abctime clk = Abc_Clock();
//printf( "Before rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
pParams->fUseRewriting = 0;
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
@ -554,7 +554,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
//printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
//ABC_PRT( "Time", clock() - clk );
//ABC_PRT( "Time", Abc_Clock() - clk );
}
// convert ABC network into IVY network

4
src/base/abci/abcLutmin.c
View File

@ -86,7 +86,7 @@ void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
Vec_Ptr_t * vFanins;
Abc_Obj_t * pObj, * pFanin;
int i, k, Counter = 0, Counter2 = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
vCounts = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
vFanins = Vec_PtrAlloc( 100 );
Abc_NtkForEachNode( pNtk, pObj, i )
@ -106,7 +106,7 @@ void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
printf( "Absorted = %6d. (%6.2f %%) Fully = %6d. (%6.2f %%) ",
Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk),
Counter2, 100.0 * Counter2 / Abc_NtkNodeNum(pNtk) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************

8
src/base/abci/abcMap.c
View File

@ -65,7 +65,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti,
Map_Man_t * pMan;
Vec_Int_t * vSwitching = NULL;
float * pSwitching = NULL;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
assert( Abc_NtkIsStrash(pNtk) );
@ -124,14 +124,14 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti,
if ( pSwitching ) Vec_IntFree( vSwitching );
if ( pMan == NULL )
return NULL;
clk = clock();
clk = Abc_Clock();
Map_ManSetSwitching( pMan, fSwitching );
if ( !Map_Mapping( pMan ) )
{
Map_ManFree( pMan );
return NULL;
}
// Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
// Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), Abc_Clock()-clk );
// reconstruct the network after mapping
pNtkNew = Abc_NtkFromMap( pMan, pNtk );
@ -143,7 +143,7 @@ clk = clock();
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
if ( fVerbose )
{
ABC_PRT( "Total runtime", clock() - clkTotal );
ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
}
// make sure that everything is okay

8
src/base/abci/abcMerge.c
View File

@ -286,7 +286,7 @@ Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
Abc_Obj_t * pLut, * pCand;
int i, k, nVertsMax, nCands;
clock_t clk = clock();
abctime clk = Abc_Clock();
// count the number of vertices
nVertsMax = 0;
Abc_NtkForEachNode( pNtk, pLut, i )
@ -326,16 +326,16 @@ Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
if ( pPars->fVerbose )
{
printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
ABC_PRT( "Deriving graph", clock() - clk );
ABC_PRT( "Deriving graph", Abc_Clock() - clk );
}
// solve the graph problem
clk = clock();
clk = Abc_Clock();
Nwk_ManGraphSolve( p );
if ( pPars->fVerbose )
{
printf( "GRAPH: Nodes = %6d. Edges = %6d. Pairs = %6d. ",
p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
ABC_PRT( "Solving", clock() - clk );
ABC_PRT( "Solving", Abc_Clock() - clk );
Nwk_ManGraphReportMemoryUsage( p );
}
vResult = p->vPairs; p->vPairs = NULL;

10
src/base/abci/abcMffc.c
View File

@ -546,7 +546,7 @@ void Abc_NktMffcTestSuper( Abc_Ntk_t * pNtk )
Vec_Int_t * vCounts, * vNumbers, * vSizes, * vMarks;
Vec_Int_t * vNode1, * vNode2;
int i, k, Entry, nSizes;
clock_t clk = clock();
abctime clk = Abc_Clock();
vRoots = Abc_NktMffcMarkRoots( pNtk, 1 );
vFanins = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
vFanouts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
@ -658,7 +658,7 @@ if ( Entry == 2 )
if ( Vec_IntEntry(vNumbers,31) )
printf( " n > 1000 %6d\n", Vec_IntEntry(vNumbers,30) );
printf( "Total MFFCs = %d. ", Vec_PtrSize(vRoots) );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_IntFree( vNumbers );
Vec_PtrFree( vNodes );
Vec_PtrFree( vLeaves );
@ -894,7 +894,7 @@ Vec_Ptr_t * Abc_NktMffcDerive( Abc_Ntk_t * pNtk, Vec_Ptr_t ** pvFanins, Vec_Ptr_
Vec_Ptr_t * vRoots, * vFanins, * vFanouts, * vVolumes, * vNodes, * vLeaves;
Abc_Obj_t * pObj, * pFanin;
int i, k;
clock_t clk = clock();
abctime clk = Abc_Clock();
// create roots
vRoots = Abc_NktMffcMarkRoots( pNtk, 0 );
// create fanins/fanouts/volumes
@ -1208,7 +1208,7 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
Vec_Int_t * vGlob, * vLeaves, * vRoots;
double Cost, CostAll = 0.0;
int i, k, Entry, nNodes = 0;
clock_t clk = clock();
abctime clk = Abc_Clock();
vGlobs = Abc_NktMffcServer( pNtk, 18, 3 );
vLeaves = Vec_IntAlloc( 100 );
vRoots = Vec_IntAlloc( 100 );
@ -1240,7 +1240,7 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
Vec_PtrFree( vGlobs );
printf( "Total = %6d. Nodes = %6d. ", Abc_NtkNodeNum(pNtk), nNodes );
printf( "Cost = %6.2f ", CostAll );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
ABC_NAMESPACE_IMPL_END

4
src/base/abci/abcNpn.c
View File

@ -177,7 +177,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
word pAuxWord[1024], pAuxWord1[1024];
char pCanonPerm[16];
unsigned uCanonPhase=0;
clock_t clk = clock();
abctime clk = Abc_Clock();
int i;
char * pAlgoName = NULL;
@ -274,7 +274,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
}
}
else assert( 0 );
clk = clock() - clk;
clk = Abc_Clock() - clk;
printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
Abc_PrintTime( 1, "Time", clk );
}

6
src/base/abci/abcNpnSave.c
View File

@ -393,9 +393,9 @@ void Npn_ManResize( Npn_Man_t * p )
Npn_Obj_t * pEntry, * pNext;
int * pBinsOld, * ppPlace;
int nBinsOld, Counter, i;
clock_t clk;
abctime clk;
assert( p->pBins != NULL );
clk = clock();
clk = Abc_Clock();
// save the old Bins
pBinsOld = p->pBins;
nBinsOld = p->nBins;
@ -420,7 +420,7 @@ clk = clock();
}
assert( Counter == p->nEntries );
ABC_FREE( pBinsOld );
//ABC_PRT( "Hash table resizing time", clock() - clk );
//ABC_PRT( "Hash table resizing time", Abc_Clock() - clk );
}
/**Function*************************************************************

6
src/base/abci/abcNtbdd.c
View File

@ -572,8 +572,8 @@ void Abc_NtkBddImplicationTest()
int nVars = 200;
int nImps = 200;
int i;
clock_t clk;
clk = clock();
abctime clk;
clk = Abc_Clock();
dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
bSum = b0; Cudd_Ref( bSum );
@ -588,7 +588,7 @@ clk = clock();
printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
printf( "The BDD after = %d.\n", Cudd_DagSize(bSum) );
ABC_PRT( "Time", clock() - clk );
ABC_PRT( "Time", Abc_Clock() - clk );
Cudd_RecursiveDeref( dd, bSum );
Cudd_Quit( dd );
}

50
src/base/abci/abcOdc.c
View File

@ -86,14 +86,14 @@ struct Odc_Man_t_
int nTotalDcs; // total percentage of DCs
// runtime
clock_t timeClean; // windowing
clock_t timeWin; // windowing
clock_t timeMiter; // computing the miter
clock_t timeSim; // simulation
clock_t timeQuant; // quantification
clock_t timeTruth; // truth table
clock_t timeTotal; // useful runtime
clock_t timeAbort; // aborted runtime
abctime timeClean; // windowing
abctime timeWin; // windowing
abctime timeMiter; // computing the miter
abctime timeSim; // simulation
abctime timeQuant; // quantification
abctime timeTruth; // truth table
abctime timeTotal; // useful runtime
abctime timeAbort; // aborted runtime
};
@ -241,7 +241,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
***********************************************************************/
void Abc_NtkDontCareClear( Odc_Man_t * p )
{
clock_t clk = clock();
abctime clk = Abc_Clock();
// clean the structural hashing table
if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
@ -257,7 +257,7 @@ void Abc_NtkDontCareClear( Odc_Man_t * p )
// reset the root node
p->iRoot = 0xffff;
p->timeClean += clock() - clk;
p->timeClean += Abc_Clock() - clk;
}
/**Function*************************************************************
@ -1033,7 +1033,7 @@ int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth )
int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth )
{
int nMints, RetValue;
clock_t clk, clkTotal = clock();
abctime clk, clkTotal = Abc_Clock();
p->nWins++;
@ -1045,12 +1045,12 @@ int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeave
p->pNode = pNode;
// compute the window
clk = clock();
clk = Abc_Clock();
RetValue = Abc_NtkDontCareWindow( p );
p->timeWin += clock() - clk;
p->timeWin += Abc_Clock() - clk;
if ( !RetValue )
{
p->timeAbort += clock() - clkTotal;
p->timeAbort += Abc_Clock() - clkTotal;
Abc_InfoFill( puTruth, p->nWords );
p->nWinsEmpty++;
return 0;
@ -1066,14 +1066,14 @@ p->timeAbort += clock() - clkTotal;
}
// transfer the window into the AIG package
clk = clock();
clk = Abc_Clock();
Abc_NtkDontCareTransfer( p );
p->timeMiter += clock() - clk;
p->timeMiter += Abc_Clock() - clk;
// simulate to estimate the amount of don't-cares
clk = clock();
clk = Abc_Clock();
nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
p->timeSim += clock() - clk;
p->timeSim += Abc_Clock() - clk;
if ( p->fVeryVerbose )
{
printf( "AIG = %5d ", Odc_NodeNum(p) );
@ -1083,7 +1083,7 @@ p->timeSim += clock() - clk;
// if there is less then the given percentage of don't-cares, skip
if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
{
p->timeAbort += clock() - clkTotal;
p->timeAbort += Abc_Clock() - clkTotal;
if ( p->fVeryVerbose )
printf( "Simulation cutoff.\n" );
Abc_InfoFill( puTruth, p->nWords );
@ -1092,12 +1092,12 @@ p->timeAbort += clock() - clkTotal;
}
// quantify external variables
clk = clock();
clk = Abc_Clock();
RetValue = Abc_NtkDontCareQuantify( p );
p->timeQuant += clock() - clk;
p->timeQuant += Abc_Clock() - clk;
if ( !RetValue )
{
p->timeAbort += clock() - clkTotal;
p->timeAbort += Abc_Clock() - clkTotal;
if ( p->fVeryVerbose )
printf( "=== Overflow! ===\n" );
Abc_InfoFill( puTruth, p->nWords );
@ -1106,17 +1106,17 @@ p->timeAbort += clock() - clkTotal;
}
// get the truth table
clk = clock();
clk = Abc_Clock();
Abc_NtkDontCareSimulateSetElem( p );
nMints = Abc_NtkDontCareSimulate( p, puTruth );
p->timeTruth += clock() - clk;
p->timeTruth += Abc_Clock() - clk;
if ( p->fVeryVerbose )
{
printf( "AIG = %5d ", Odc_NodeNum(p) );
printf( "%6.2f %% ", 100.0 * (p->nBits - nMints) / p->nBits );
printf( "\n" );
}
p->timeTotal += clock() - clkTotal;
p->timeTotal += Abc_Clock() - clkTotal;
p->nWinsFinish++;
p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
return nMints;

22
src/base/abci/abcPart.c
View File

@ -726,21 +726,21 @@ Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nSuppSizeLimit, int fVe
Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
int i, iPart, iOut, timeFind = 0;
clock_t clk, clk2;
abctime clk, clk2;
// compute the supports for all outputs
clk = clock();
clk = Abc_Clock();
// vSupps = Abc_NtkComputeSupportsNaive( pNtk );
vSupps = Abc_NtkComputeSupportsSmart( pNtk );
if ( fVerbose )
{
ABC_PRT( "Supps", clock() - clk );
ABC_PRT( "Supps", Abc_Clock() - clk );
}
// start char-based support representation
vPartSuppsChar = Vec_PtrAlloc( 1000 );
// create partitions
clk = clock();
clk = Abc_Clock();
vPartsAll = Vec_PtrAlloc( 256 );
vPartSuppsAll = Vec_PtrAlloc( 256 );
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vSupps) );
@ -753,9 +753,9 @@ clk = clock();
// get the output number
iOut = Vec_IntPop(vOne);
// find closely matching part
clk2 = clock();
clk2 = Abc_Clock();
iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nSuppSizeLimit, vOne );
timeFind += clock() - clk2;
timeFind += Abc_Clock() - clk2;
if ( iPart == -1 )
{
// create new partition
@ -794,11 +794,11 @@ timeFind += clock() - clk2;
//printf( "\n" );
if ( fVerbose )
{
ABC_PRT( "Parts", clock() - clk );
ABC_PRT( "Parts", Abc_Clock() - clk );
//ABC_PRT( "Find ", timeFind );
}
clk = clock();
clk = Abc_Clock();
// remember number of supports
Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
Vec_IntPush( vOne, i );
@ -817,7 +817,7 @@ clk = clock();
if ( fVerbose )
{
ABC_PRT( "Comps", clock() - clk );
ABC_PRT( "Comps", Abc_Clock() - clk );
}
if ( fVerbose )
printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
@ -1163,7 +1163,7 @@ void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
Vec_Int_t * vOne;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
int i;
clock_t clk = clock();
abctime clk = Abc_Clock();
// perform partitioning
assert( Abc_NtkIsStrash(pNtk) );
@ -1194,7 +1194,7 @@ void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
Abc_NtkDelete( pNtkAig );
Vec_PtrFree( vFraigs );
Vec_PtrFree( vOnePtr );
ABC_PRT( "Partitioned fraiging time", clock() - clk );
ABC_PRT( "Partitioned fraiging time", Abc_Clock() - clk );
}
////////////////////////////////////////////////////////////////////////

10
src/base/abci/abcPrint.c
View File

@ -37,10 +37,10 @@ ABC_NAMESPACE_IMPL_START
//extern int s_TotalNodes = 0;
//extern int s_TotalChanges = 0;
clock_t s_MappingTime = 0;
abctime s_MappingTime = 0;
int s_MappingMem = 0;
clock_t s_ResubTime = 0;
clock_t s_ResynTime = 0;
abctime s_ResubTime = 0;
abctime s_ResynTime = 0;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -1303,7 +1303,7 @@ void Abc_NtkPrintMiter( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj, * pChild, * pConst1 = Abc_AigConst1(pNtk);
int i, iOut = -1;
clock_t Time = clock();
abctime Time = Abc_Clock();
int nUnsat = 0;
int nSat = 0;
int nUndec = 0;
@ -1345,7 +1345,7 @@ void Abc_NtkPrintMiter( Abc_Ntk_t * pNtk )
printf( " ? =%7d", nUndec );
printf( " U =%6d", nUnsat );
printf( " S =%6d", nSat );
Time = clock() - Time;
Time = Abc_Clock() - Time;
printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC));
if ( iOut >= 0 )
printf( "The first satisfiable output is number %d (%s).\n", iOut, Abc_ObjName( Abc_NtkPo(pNtk, iOut) ) );

20
src/base/abci/abcProve.c
View File

@ -35,7 +35,7 @@ extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMa
extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects );
static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, clock_t clk, int fVerbose );
static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, abctime clk, int fVerbose );
////////////////////////////////////////////////////////////////////////
@ -61,7 +61,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
Prove_Params_t * pParams = (Prove_Params_t *)pPars;
Abc_Ntk_t * pNtk, * pNtkTemp;
int RetValue = -1, nIter, nSatFails, Counter;
clock_t clk; //, timeStart = clock();
abctime clk; //, timeStart = Abc_Clock();
ABC_INT64_T nSatConfs, nSatInspects, nInspectLimit;
// get the starting network
@ -82,7 +82,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
// if SAT only, solve without iteration
if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
{
clk = clock();
clk = Abc_Clock();
RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)0, 0, NULL, NULL );
Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
*ppNtk = pNtk;
@ -101,7 +101,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
}
// try brute-force SAT
clk = clock();
clk = Abc_Clock();
nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (ABC_INT64_T)nInspectLimit, 0, &nSatConfs, &nSatInspects );
Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
@ -123,7 +123,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
// try rewriting
if ( pParams->fUseRewriting )
{
clk = clock();
clk = Abc_Clock();
Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
// Counter = 1;
while ( 1 )
@ -165,7 +165,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
if ( pParams->fUseFraiging )
{
// try FRAIGing
clk = clock();
clk = Abc_Clock();
nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects ); Abc_NtkDelete( pNtkTemp );
Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, pParams->fVerbose );
@ -196,7 +196,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
fflush( stdout );
}
clk = clock();
clk = Abc_Clock();
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
if ( pNtk )
{
@ -215,7 +215,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
fflush( stdout );
}
clk = clock();
clk = Abc_Clock();
nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)nInspectLimit, 0, NULL, NULL );
Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
@ -308,13 +308,13 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInsp
SeeAlso []
***********************************************************************/
void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, clock_t clk, int fVerbose )
void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, abctime clk, int fVerbose )
{
if ( !fVerbose )
return;
printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk),
Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) );
ABC_PRT( pString, clock() - clk );
ABC_PRT( pString, Abc_Clock() - clk );
}

Some files were not shown because too many files have changed in this diff Show More