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

14 files changed, 102 insertions, 102 deletions

diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index 7213bdff..8ab5df51 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -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 )
     {
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index f9cccae8..114db997 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -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;
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index 14a488ad..1f931eae 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -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" );
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
index 08718fa8..6378e4db 100644
--- a/src/aig/saig/saigIsoFast.c
+++ b/src/aig/saig/saigIsoFast.c
@@ -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
diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c
index 25cd68f0..58dc6596 100644
--- a/src/aig/saig/saigIsoSlow.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -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 )
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 8ebb81dd..67aed490 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -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 );
diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c
index 006167d5..bac2ee4a 100644
--- a/src/aig/saig/saigRetFwd.c
+++ b/src/aig/saig/saigRetFwd.c
@@ -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;
 }
diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c
index 39456c63..fef83675 100644
--- a/src/aig/saig/saigSimFast.c
+++ b/src/aig/saig/saigSimFast.c
@@ -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;
 }
 
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 71259930..3621cdd3 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -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 );
diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c
index d92461c8..ba414680 100644
--- a/src/aig/saig/saigSimSeq.c
+++ b/src/aig/saig/saigSimSeq.c
@@ -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;
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
index 72cf9bbe..6c4ffa8e 100644
--- a/src/aig/saig/saigStrSim.c
+++ b/src/aig/saig/saigStrSim.c
@@ -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;
 }
 
diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c
index 9217dd53..b18ca803 100644
--- a/src/aig/saig/saigSwitch.c
+++ b/src/aig/saig/saigSwitch.c
@@ -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;
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index 28c8150f..02b8ed12 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -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;
 }
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index 5e7b719b..217d3269 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -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 )
     {