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

Merge pull request #496 from zxxr1113/fix-ssw-timing 

fix timing inconsistency in calculating the "timeOther" in Ssw_ManPrintStats in sswMan.c
This commit is contained in:
alanminko 2026-04-14 10:02:22 -07:00 committed by GitHub
parent 2db6ae7848 6a52468604
commit 8762d6c667
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/proof/ssw/sswConstr.c
View File

@ -501,6 +501,7 @@ int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
int i, f, iLits;
abctime clk;
clk = Abc_Clock();
abctime timeSatBmc = p->timeSat, timeSimSatBmc = p->timeSimSat;
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@ -568,7 +569,7 @@ clk = Abc_Clock();
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
p->timeBmc += (Abc_Clock() - clk) - (p->timeSat - timeSatBmc) - (p->timeSimSat - timeSimSatBmc);
return p->fRefined;
}

3
src/proof/ssw/sswSweep.c
View File

@ -276,6 +276,7 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p )
int i, f;
abctime clk;
clk = Abc_Clock();
abctime timeSatBmc = p->timeSat, timeSimSatBmc = p->timeSimSat;
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@ -329,7 +330,7 @@ clk = Abc_Clock();
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
p->timeBmc += (Abc_Clock() - clk) - (p->timeSat - timeSatBmc) - (p->timeSimSat - timeSimSatBmc);
return p->fRefined;
}