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

Adding callbacks to "scorr" and "&scorr".

This commit is contained in:
Alan Mishchenko 2026-02-25 20:00:28 -08:00
parent ef54c1daea
commit d5c1f2cfe1
6 changed files with 56 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/proof/cec/cecCorr.c
View File

@ -22,6 +22,13 @@
ABC_NAMESPACE_IMPL_START
static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
{
if ( pPars == NULL || pPars->pFunc == NULL )
return 0;
return ((int (*)(void *))pPars->pFunc)( pPars->pData );
}
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -808,6 +815,8 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
fChanges = 1;
for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
{
if ( Cec_ParCorShouldStop( pPars ) )
break;
abctime clkBmc = Abc_Clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
@ -836,6 +845,8 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
if ( Cec_ParCorShouldStop( pPars ) )
break;
}
Cec_ManSimStop( pSim );
}
@ -975,10 +986,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// check the base case
if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
if ( pPars->pFunc )
if ( Cec_ParCorShouldStop( pPars ) )
{
((int (*)(void *))pPars->pFunc)( pPars->pData );
((int (*)(void *))pPars->pFunc)( pPars->pData );
Cec_ManSimStop( pSim );
return 1;
}
if ( pPars->nStepsMax == 0 )
{
@ -989,6 +1000,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
if ( Cec_ParCorShouldStop( pPars ) )
{
Cec_ManSimStop( pSim );
return 1;
}
if ( pPars->nStepsMax == r )
{
Cec_ManSimStop( pSim );
@ -1036,8 +1052,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
if ( pPars->pFunc )
((int (*)(void *))pPars->pFunc)( pPars->pData );
if ( Cec_ParCorShouldStop( pPars ) )
{
Cec_ManSimStop( pSim );
return 1;
}
// quit if const is no longer there
if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
{
@ -1448,4 +1467,3 @@ Gia_Man_t * Gia_ManDupStopsTest( Gia_Man_t * p )
ABC_NAMESPACE_IMPL_END

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

@ -512,6 +512,8 @@ clk = Abc_Clock();
p->fRefined = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
if ( Ssw_ManCallbackStop(p) )
break;
// map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
@ -540,10 +542,14 @@ clk = Abc_Clock();
// sweep internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
{
if ( Ssw_ManCallbackStop(p) )
break;
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
}
if ( i < Aig_ManObjNumMax(p->pAig) )
break;
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
@ -692,6 +698,8 @@ p->timeReduce += Abc_Clock() - clk;
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( Ssw_ManCallbackStop(p) )
break;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )

20
src/proof/ssw/sswCore.c
View File

@ -238,6 +238,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Aig_Man_t * pAigNew;
int RetValue, nIter = -1, nPrev[4] = {0};
abctime clk, clkTotal = Abc_Clock();
abctime nTimeToStop = p->pPars->TimeLimit > 0 ? clkTotal + (abctime)p->pPars->TimeLimit * CLOCKS_PER_SEC : 0;
// get the starting stats
p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
p->nNodesBeg = Aig_ManNodeNum(p->pAig);
@ -251,6 +252,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
if ( !p->pPars->fLatchCorr || p->pPars->nFramesK > 1 )
{
p->pMSat = Ssw_SatStart( 0 );
if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pMSat->pSat, nTimeToStop );
if ( p->pPars->fConstrs )
Ssw_ManSweepBmcConstr( p );
else
@ -276,11 +279,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Aig_ManStop( pSRed );
}
*/
if ( p->pPars->pFunc )
{
((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
}
if ( Ssw_ManCallbackStop(p) || Ssw_ManCallbackStop(p) )
goto finalize;
if ( p->pPars->nStepsMax == 0 )
{
Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
@ -290,6 +290,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
for ( nIter = 0; ; nIter++ )
{
if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
goto finalize;
if ( p->pPars->nStepsMax == nIter )
{
Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
@ -306,9 +308,13 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
break;
}
if ( Ssw_ManCallbackStop(p) )
goto finalize;
clk = Abc_Clock();
p->pMSat = Ssw_SatStart( 0 );
if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pMSat->pSat, nTimeToStop );
if ( p->pPars->fLatchCorrOpt )
{
RetValue = Ssw_ManSweepLatch( p );
@ -379,8 +385,8 @@ clk = Abc_Clock();
Ssw_ManCleanup( p );
if ( !RetValue )
break;
if ( p->pPars->pFunc )
((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
if ( Ssw_ManCallbackStop(p) )
goto finalize;
if ( p->pPars->nLimitMax )
{
int nCur = Ssw_ClassesCand1Num(p->ppClasses);

2
src/proof/ssw/sswDyn.c
View File

@ -407,6 +407,8 @@ p->timeReduce += Abc_Clock() - clk;
p->iNodeStart = 0;
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( Ssw_ManCallbackStop(p) )
break;
if ( p->iNodeStart == 0 )
p->iNodeStart = i;
if ( p->pPars->fVerbose )

2
src/proof/ssw/sswInt.h
View File

@ -190,6 +190,7 @@ static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int
static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Ssw_ObjChild1Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
static inline int Ssw_ManCallbackStop( Ssw_Man_t * p ) { return (p && p->pPars && p->pPars->pFunc) ? ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ) : 0; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@ -299,4 +300,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -288,6 +288,8 @@ clk = Abc_Clock();
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
if ( Ssw_ManCallbackStop(p) )
break;
// map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
@ -298,12 +300,16 @@ clk = Abc_Clock();
// sweep internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
{
if ( Ssw_ManCallbackStop(p) )
break;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
}
if ( i < Aig_ManObjNumMax(p->pAig) )
break;
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
@ -415,6 +421,8 @@ p->timeReduce += Abc_Clock() - clk;
vObjPairs = (p->pPars->fEquivDump || p->pPars->fEquivDump2)? Vec_IntAlloc(1000) : NULL;
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( Ssw_ManCallbackStop(p) )
break;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )