summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw')
-rw-r--r--src/proof/ssw/sswBmc.c8
-rw-r--r--src/proof/ssw/sswClass.c14
-rw-r--r--src/proof/ssw/sswConstr.c18
-rw-r--r--src/proof/ssw/sswCore.c10
-rw-r--r--src/proof/ssw/sswDyn.c14
-rw-r--r--src/proof/ssw/sswFilter.c12
-rw-r--r--src/proof/ssw/sswInt.h20
-rw-r--r--src/proof/ssw/sswIslands.c4
-rw-r--r--src/proof/ssw/sswLcorr.c10
-rw-r--r--src/proof/ssw/sswPairs.c16
-rw-r--r--src/proof/ssw/sswPart.c4
-rw-r--r--src/proof/ssw/sswRarity.c48
-rw-r--r--src/proof/ssw/sswRarity2.c20
-rw-r--r--src/proof/ssw/sswSat.c22
-rw-r--r--src/proof/ssw/sswSemi.c12
-rw-r--r--src/proof/ssw/sswSim.c14
-rw-r--r--src/proof/ssw/sswSimSat.c8
-rw-r--r--src/proof/ssw/sswSweep.c18
18 files changed, 136 insertions, 136 deletions
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index c88b2dcc..61c1c2a7 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -129,7 +129,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
Ssw_Sat_t * pSat;
Aig_Obj_t * pObj, * pObjFrame;
int status, Lit, i, f, RetValue;
- clock_t clkPart;
+ abctime clkPart;
// start managers
assert( Saig_ManRegNum(pAig) > 0 );
@@ -149,7 +149,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
RetValue = -1;
for ( f = 0; f < nFramesMax; f++ )
{
- clkPart = clock();
+ clkPart = Abc_Clock();
Saig_ManForEachPo( pAig, pObj, i )
{
// unroll the circuit for this output
@@ -203,8 +203,8 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
(double)pSat->pSat->stats.conflicts,
pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
- ABC_PRT( "T", clock() - clkPart );
- clkPart = clock();
+ ABC_PRT( "T", Abc_Clock() - clkPart );
+ clkPart = Abc_Clock();
fflush( stdout );
}
if ( RetValue != 1 )
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 9cf8871b..0613302e 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -611,25 +611,25 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
Vec_Ptr_t * vCands;
Aig_Obj_t * pObj;
int i, k, RetValue;
- clock_t clk;
+ abctime clk;
// start the classes
p = Ssw_ClassesStart( pAig );
p->fConstCorr = fConstCorr;
// perform sequential simulation
-clk = clock();
+clk = Abc_Clock();
pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
if ( fVerbose )
{
Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
Abc_Print( 1, "Initial simulation of %d frames with %d words. ", nFrames, nWords );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
// set comparison procedures
-clk = clock();
+clk = Abc_Clock();
Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
// collect nodes to be considered as candidates
@@ -677,10 +677,10 @@ clk = clock();
if ( fVerbose )
{
Abc_Print( 1, "Collecting candidate equivalence classes. " );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
-clk = clock();
+clk = Abc_Clock();
// perform iterative refinement using simulation
for ( i = 1; i < nIters; i++ )
{
@@ -703,7 +703,7 @@ if ( fVerbose )
{
Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
nFrames, nWords, i-1 );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
Ssw_ClassesCheck( p );
// Ssw_ClassesPrint( p, 0 );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 3dcf0a34..a9ed17fc 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -409,8 +409,8 @@ int Ssw_ManSweepBmcConstr_old( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
int i, f, iLits;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -480,7 +480,7 @@ clk = clock();
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
return p->fRefined;
}
@@ -499,8 +499,8 @@ int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
{
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
int i, f, iLits;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -560,7 +560,7 @@ clk = clock();
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
return p->fRefined;
}
@@ -621,11 +621,11 @@ int Ssw_ManSweepConstr( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, i, f, iLits;
- clock_t clk;
+ abctime clk;
//Ssw_ManPrintPolarity( p->pAig );
// perform speculative reduction
-clk = clock();
+clk = Abc_Clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
// add constants
@@ -656,7 +656,7 @@ clk = clock();
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
}
assert( Vec_IntSize(p->vInits) == iLits );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
// add constraints to all timeframes
for ( f = 0; f <= p->pPars->nFramesK; f++ )
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index 7a9d4b9f..f944eddc 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
Aig_Man_t * pAigNew;
int RetValue, nIter = -1;
- clock_t clk, clkTotal = clock();
+ abctime clk, clkTotal = Abc_Clock();
// get the starting stats
p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
p->nNodesBeg = Aig_ManNodeNum(p->pAig);
@@ -306,7 +306,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
break;
}
-clk = clock();
+clk = Abc_Clock();
p->pMSat = Ssw_SatStart( 0 );
if ( p->pPars->fLatchCorrOpt )
{
@@ -317,7 +317,7 @@ clk = clock();
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
- ABC_PRT( "T", clock() - clk );
+ ABC_PRT( "T", Abc_Clock() - clk );
}
}
else
@@ -342,7 +342,7 @@ clk = clock();
}
Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
(Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
- ABC_PRT( "T", clock() - clk );
+ ABC_PRT( "T", Abc_Clock() - clk );
}
// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
// p->pPars->nBTLimit = 10000;
@@ -384,7 +384,7 @@ clk = clock();
finalize:
p->pPars->nIters = nIter + 1;
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
pAigNew = Aig_ManDupRepr( p->pAig, 0 );
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 5fc22fdf..316b2e4d 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -263,7 +263,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
{
int RetValue1, RetValue2;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// transfer PI simulation information from storage
// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
Ssw_ManSweepTransferDyn( p );
@@ -277,7 +277,7 @@ int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
p->nPatterns = 0;
p->nSimRounds++;
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
return RetValue1 > 0 || RetValue2 > 0;
}
@@ -296,7 +296,7 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
{
Aig_Obj_t * pObj, * pRepr, ** ppClass;
int i, k, nSize, RetValue1, RetValue2;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
p->nSimRounds++;
// transfer PI simulation information from storage
// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
@@ -355,7 +355,7 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
p->nPatterns = 0;
p->nSimRounds++;
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
return RetValue1 > 0 || RetValue2 > 0;
}
@@ -375,10 +375,10 @@ int Ssw_ManSweepDyn( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew;
int i, f;
- clock_t clk;
+ abctime clk;
// perform speculative reduction
-clk = clock();
+clk = Abc_Clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
Aig_ManFanoutStart( p->pFrames );
@@ -392,7 +392,7 @@ clk = clock();
Aig_ManSetCioIds( p->pFrames );
// label nodes corresponding to primary inputs
Ssw_ManLabelPiNodes( p );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
// prepare simulation info
assert( p->vSimInfo == NULL );
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 534fc275..9027d773 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -279,7 +279,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
{
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
int f, f1, i;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
Saig_ManForEachLo( p->pAig, pObj, i )
@@ -349,7 +349,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
break;
}
// check timeout
- if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( TimeLimit && ((float)TimeLimit <= (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
break;
// transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
@@ -383,8 +383,8 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
{
Ssw_Pars_t Pars, * pPars = &Pars;
Ssw_Man_t * p;
- int r, TimeLimitPart;//, clkTotal = clock();
- clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
+ int r, TimeLimitPart;//, clkTotal = Abc_Clock();
+ abctime nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
// consider the case of empty AIG
@@ -430,7 +430,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
Ssw_ClassesPrint( p->ppClasses, 0 );
}
p->pMSat = Ssw_SatStart( 0 );
- TimeLimitPart = TimeLimit ? (nTimeToStop - clock()) / CLOCKS_PER_SEC : 0;
+ TimeLimitPart = TimeLimit ? (nTimeToStop - Abc_Clock()) / CLOCKS_PER_SEC : 0;
if ( TimeLimit2 )
{
if ( TimeLimitPart )
@@ -445,7 +445,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
// simulate pattern forward
Ssw_ManRollForward( p, p->pPars->nFramesK );
// check timeout
- if ( TimeLimit && clock() > nTimeToStop )
+ if ( TimeLimit && Abc_Clock() > nTimeToStop )
{
Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeLimit );
break;
diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h
index 1edf2087..00681923 100644
--- a/src/proof/ssw/sswInt.h
+++ b/src/proof/ssw/sswInt.h
@@ -127,16 +127,16 @@ struct Ssw_Man_t_
int nRegsBegC;
int nRegsEndC;
// runtime stats
- clock_t timeBmc; // bounded model checking
- clock_t timeReduce; // speculative reduction
- clock_t timeMarkCones; // marking the cones not to be refined
- clock_t timeSimSat; // simulation of the counter-examples
- clock_t timeSat; // solving SAT
- clock_t timeSatSat; // sat
- clock_t timeSatUnsat; // unsat
- clock_t timeSatUndec; // undecided
- clock_t timeOther; // other runtime
- clock_t timeTotal; // total runtime
+ abctime timeBmc; // bounded model checking
+ abctime timeReduce; // speculative reduction
+ abctime timeMarkCones; // marking the cones not to be refined
+ abctime timeSimSat; // simulation of the counter-examples
+ abctime timeSat; // solving SAT
+ abctime timeSatSat; // sat
+ abctime timeSatUnsat; // unsat
+ abctime timeSatUndec; // undecided
+ abctime timeOther; // other runtime
+ abctime timeTotal; // total runtime
};
// internal SAT manager
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index d1758b75..87df4ebf 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -480,7 +480,7 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
Ssw_Pars_t Pars;
Aig_Man_t * pAigRes;
int RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// derive parameters if not given
if ( pPars == NULL )
Ssw_ManSetDefaultParams( pPars = &Pars );
@@ -495,7 +495,7 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
else
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
Aig_ManStop( pAigRes );
return RetValue;
}
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index cd212e0b..d020ef00 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -78,7 +78,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
int Ssw_ManSweepResimulate( Ssw_Man_t * p )
{
int RetValue1, RetValue2;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// transfer PI simulation information from storage
Ssw_ManSweepTransfer( p );
// simulate internal nodes
@@ -90,7 +90,7 @@ int Ssw_ManSweepResimulate( Ssw_Man_t * p )
Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
p->nPatterns = 0;
p->nSimRounds++;
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
return RetValue1 > 0 || RetValue2 > 0;
}
@@ -161,7 +161,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
{
Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
int RetValue;
- clock_t clk;
+ abctime clk;
assert( Aig_ObjIsCi(pObj) );
assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
// check if it makes sense to skip some calls
@@ -171,7 +171,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
return;
}
p->nCallsDelta = 0;
-clk = clock();
+clk = Abc_Clock();
// get the fraiged node
pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
@@ -185,7 +185,7 @@ clk = clock();
}
else
pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return;
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index 3068adc4..fe389191 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -321,7 +321,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
Vec_Int_t * vIds1, * vIds2;
Aig_Obj_t * pObj, * pRepr;
int RetValue, i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Ssw_ManSetDefaultParams( pPars );
pPars->fVerbose = 1;
pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
@@ -360,7 +360,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
else
Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
// cleanup
Aig_ManStop( pAigNew );
return pAigRes;
@@ -381,7 +381,7 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
{
Aig_Man_t * pAigRes;
int RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
assert( vIds1 != NULL && vIds2 != NULL );
// try the new AIGs
Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
@@ -395,7 +395,7 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
else
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
// cleanup
Aig_ManStop( pAigRes );
return RetValue;
@@ -416,7 +416,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
{
Aig_Man_t * pAigRes, * pMiter;
int RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// try the new AIGs
Abc_Print( 1, "Performing general verification without node pairs.\n" );
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
@@ -432,7 +432,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
else
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
// cleanup
Aig_ManStop( pAigRes );
return RetValue;
@@ -453,7 +453,7 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
{
Aig_Man_t * pAigRes;
int RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// try the new AIGs
// Abc_Print( 1, "Performing general verification without node pairs.\n" );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
@@ -466,7 +466,7 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
else
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
// cleanup
Aig_ManStop( pAigRes );
return RetValue;
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index dbe8a877..30afddca 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -53,7 +53,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( pPars->fConstrs )
{
Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
@@ -126,7 +126,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
- ABC_PRT( "Total time", clock() - clk );
+ ABC_PRT( "Total time", Abc_Clock() - clk );
}
return pNew;
}
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index d780b915..10e19b5a 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -314,7 +314,7 @@ void TransposeTest()
{
word M[64], N[64];
int i;
- clock_t clk;
+ abctime clk;
Aig_ManRandom64( 1 );
// for ( i = 0; i < 64; i++ )
// M[i] = Aig_ManRandom64( 0 );
@@ -323,15 +323,15 @@ void TransposeTest()
// for ( i = 0; i < 64; i++ )
// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
- clk = clock();
+ clk = Abc_Clock();
for ( i = 0; i < 100001; i++ )
transpose64Simple( M, N );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
- clk = clock();
+ clk = Abc_Clock();
for ( i = 0; i < 100001; i++ )
transpose64( M );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
@@ -594,7 +594,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, clock_t Time )
+int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, abctime Time )
{
Aig_Obj_t * pObj;
int i;
@@ -976,9 +976,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
int fMiter = 1;
Ssw_RarMan_t * p;
int r, f = -1;
- clock_t clk, clkTotal = clock();
- clock_t nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + clock(): 0;
- clock_t timeLastSolved = 0;
+ abctime clk, clkTotal = Abc_Clock();
+ abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
+ abctime timeLastSolved = 0;
int nNumRestart = 0;
int nSavedSeed = pPars->nRandSeed;
int RetValue = -1;
@@ -1004,10 +1004,10 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
// perform simulation rounds
pPars->nSolved = 0;
- timeLastSolved = clock();
+ timeLastSolved = Abc_Clock();
for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{
- clk = clock();
+ clk = Abc_Clock();
if ( fTryBmc )
{
Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
@@ -1022,7 +1022,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter )
{
- int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, clock() - clkTotal);
+ int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, Abc_Clock() - clkTotal);
if ( Status == 2 )
{
Abc_Print( 1, "Quitting due to callback on fail.\n" );
@@ -1041,22 +1041,22 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
goto finish;
}
- timeLastSolved = clock();
+ timeLastSolved = Abc_Clock();
}
// else - did not find a counter example
}
// check timeout
- if ( pPars->TimeOut && clock() > nTimeToStop )
+ if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
goto finish;
}
- if ( pPars->TimeOutGap && timeLastSolved && clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
+ if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
@@ -1090,7 +1090,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
Abc_Print( 1, "CEX =%6d (%6.2f %%) ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
else
Abc_Print( 1, "." );
@@ -1108,13 +1108,13 @@ finish:
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
else if ( r == pPars->nRounds && f == pPars->nFrames )
{
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
@@ -1161,8 +1161,8 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{
Ssw_RarMan_t * p;
int r, f = -1, i, k;
- clock_t clkTotal = clock();
- clock_t nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + clock(): 0;
+ abctime clkTotal = Abc_Clock();
+ abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
int nNumRestart = 0;
int nSavedSeed = pPars->nRandSeed;
int RetValue = -1;
@@ -1234,12 +1234,12 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
RetValue = 0;
goto finish;
}
// check timeout
- if ( pPars->TimeOut && clock() > nTimeToStop )
+ if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
{
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
@@ -1279,7 +1279,7 @@ finish:
if ( !pPars->fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index f6b2c319..01f288c1 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -309,8 +309,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
int fMiter = 1;
Ssw_RarMan_t * p;
int r;
- clock_t clk, clkTotal = clock();
- clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
+ abctime clk, clkTotal = Abc_Clock();
+ abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
@@ -331,7 +331,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
// perform simulation rounds
for ( r = 0; r < nRounds; r++ )
{
- clk = clock();
+ clk = Abc_Clock();
// simulate
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
@@ -349,11 +349,11 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
if ( fVerbose )
{
// Abc_Print( 1, "Round %3d: ", r );
-// Abc_PrintTime( 1, "Time", clock() - clk );
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_Print( 1, "." );
}
// check timeout
- if ( TimeOut && clock() > nTimeToStop )
+ if ( TimeOut && Abc_Clock() > nTimeToStop )
{
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut );
@@ -364,7 +364,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
{
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
@@ -388,8 +388,8 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
int fMiter = 0;
Ssw_RarMan_t * p;
int r, i, k;
- clock_t clkTotal = clock();
- clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
+ abctime clkTotal = Abc_Clock();
+ abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
@@ -462,7 +462,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// check timeout
- if ( TimeOut && clock() > nTimeToStop )
+ if ( TimeOut && Abc_Clock() > nTimeToStop )
{
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut );
@@ -472,7 +472,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
if ( r == nRounds )
{
Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c
index e5971a64..59ed6945 100644
--- a/src/proof/ssw/sswSat.c
+++ b/src/proof/ssw/sswSat.c
@@ -46,7 +46,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int nBTLimit = p->pPars->nBTLimit;
int pLits[3], nLits, RetValue, RetValue1;
- clock_t clk;//, status;
+ abctime clk;//, status;
p->nSatCalls++;
p->pMSat->nSolverCalls++;
@@ -80,13 +80,13 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( RetValue != 0 );
}
-clk = clock();
+clk = Abc_Clock();
RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
if ( nLits == 2 )
{
pLits[0] = lit_neg( pLits[0] );
@@ -105,13 +105,13 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-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->nSatFailsReal++;
return -1;
}
@@ -142,13 +142,13 @@ p->timeSatUndec += clock() - clk;
assert( RetValue != 0 );
}
-clk = clock();
+clk = Abc_Clock();
RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
if ( nLits == 2 )
{
pLits[0] = lit_neg( pLits[0] );
@@ -167,13 +167,13 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-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->nSatFailsReal++;
return -1;
}
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index 822f63f5..d5af1394 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -180,8 +180,8 @@ int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
unsigned * pInfo;
int i, f, RetValue, fFirst = 0;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
@@ -243,7 +243,7 @@ clk = clock();
// cleanup
Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
return RetValue;
}
@@ -262,7 +262,7 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
{
Ssw_Sem_t * p;
int RetValue, Frames, Iter;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
{
@@ -279,7 +279,7 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
RetValue = 0;
for ( Iter = 0; Iter < p->nPatterns; Iter++ )
{
-clk = clock();
+clk = Abc_Clock();
pMan->pMSat = Ssw_SatStart( 0 );
Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
if ( fVerbose )
@@ -288,7 +288,7 @@ clk = clock();
Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
p->pMan->nSatFailsReal? "f" : " " );
- ABC_PRT( "T", clock() - clk );
+ ABC_PRT( "T", Abc_Clock() - clk );
}
Ssw_ManCleanup( p->pMan );
if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index 469af654..c458855d 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -38,7 +38,7 @@ struct Ssw_Sml_t_
int nWordsPref; // the number of word in the prefix
int fNonConstOut; // have seen a non-const-0 output during simulation
int nSimRounds; // statistics
- clock_t timeSim; // statistics
+ abctime timeSim; // statistics
unsigned pData[0]; // simulation data for the nodes
};
@@ -1006,8 +1006,8 @@ void Ssw_SmlSimulateOne( Ssw_Sml_t * p )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int f, i;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
for ( f = 0; f < p->nFrames; f++ )
{
// simulate the nodes
@@ -1026,7 +1026,7 @@ clk = clock();
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
}
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}
@@ -1118,8 +1118,8 @@ void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
// simulate the nodes
Aig_ManForEachNode( p->pAig, pObj, i )
Ssw_SmlNodeSimulate( p, pObj, 0 );
@@ -1129,7 +1129,7 @@ clk = clock();
// copy simulation info into the inputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 6e5944d1..74c65c00 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -46,7 +46,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
{
Aig_Obj_t * pObj;
int i, RetValue1, RetValue2;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// set the PI simulation information
Aig_ManConst1(p->pAig)->fMarkB = 1;
Aig_ManForEachCi( p->pAig, pObj, i )
@@ -75,7 +75,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
}
}
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
}
/**Function*************************************************************
@@ -92,7 +92,7 @@ p->timeSimSat += clock() - clk;
void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
{
int RetValue1, RetValue2;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// set the PI simulation information
Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
// simulate internal nodes
@@ -113,7 +113,7 @@ void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr,
if ( RetValue2 == 0 )
Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index bccc6aa4..6db673cc 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -188,7 +188,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
- clock_t clk;
+ abctime clk;
// get representative of this class
pObjRepr = Aig_ObjRepr( p->pAig, pObj );
if ( pObjRepr == NULL )
@@ -206,10 +206,10 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_
// add constraints on demand
if ( !fBmc && p->pPars->fDynamic )
{
-clk = clock();
+clk = Abc_Clock();
Ssw_ManLoadSolver( p, pObjRepr, pObj );
p->nRecycleCalls++;
-p->timeMarkCones += clock() - clk;
+p->timeMarkCones += Abc_Clock() - clk;
}
// call equivalence checking
if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
@@ -269,8 +269,8 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
int i, f;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -315,7 +315,7 @@ clk = clock();
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
return p->fRefined;
}
@@ -368,11 +368,11 @@ int Ssw_ManSweep( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, i, f;
- clock_t clk;
+ abctime clk;
Vec_Int_t * vDisproved;
// perform speculative reduction
-clk = clock();
+clk = Abc_Clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
// add constants
@@ -397,7 +397,7 @@ clk = clock();
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
// sweep internal nodes
p->fRefined = 0;
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:41:25 +0000