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

Merge pull request #534 from zxxr1113/scorr2-upstream 

new command &scorr2 extended from &scorr
This commit is contained in:
alanminko 2026-07-27 22:56:46 +09:00 committed by GitHub
parent c1f9a942ca 77cd6f4b04
commit 4e1b34d744
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
15 changed files with 3735 additions and 604 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abclib.dsp
View File

@ -6685,6 +6685,14 @@ SOURCE=.\src\proof\cec\cecCorr.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\proof\cec\cecCorr2.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecCorrCert.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecCorrDyn.c SOURCE=.\src\proof\cec\cecCorrDyn.c
# End Source File # End Source File
# Begin Source File # Begin Source File

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

@ -1836,6 +1836,9 @@ extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p );
extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
extern void Tas_ManSetConflictNum( Tas_Man_t * p, int Num );
extern void Tas_ManSyncCore( Tas_Man_t * p );
extern Vec_Int_t * Tas_ManSolveRoots( Tas_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaDecGraph.c ===========================================================*/ /*=== giaDecGraph.c ===========================================================*/
extern Gia_Man_t* Gia_ManDecGraph( Gia_Man_t* p ); extern Gia_Man_t* Gia_ManDecGraph( Gia_Man_t* p );
@ -1884,4 +1887,3 @@ ABC_NAMESPACE_HEADER_END
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

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

@ -83,6 +83,7 @@ struct Tas_Man_t_
{ {
Tas_Par_t Pars; // parameters Tas_Par_t Pars; // parameters
Gia_Man_t * pAig; // AIG manager Gia_Man_t * pAig; // AIG manager
int nSyncedObjs; // pAig objects already prepped (Value/marks/refs) for resident reuse
Tas_Que_t pProp; // propagation queue Tas_Que_t pProp; // propagation queue
Tas_Que_t pJust; // justification queue Tas_Que_t pJust; // justification queue
Tas_Que_t pClauses; // clause queue Tas_Que_t pClauses; // clause queue
@ -90,6 +91,9 @@ struct Tas_Man_t_
Vec_Int_t * vLevReas; // levels and decisions Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vModel; // satisfying assignment Vec_Int_t * vModel; // satisfying assignment
Vec_Ptr_t * vTemp; // temporary storage Vec_Ptr_t * vTemp; // temporary storage
Vec_Int_t * vOutLits; // optional endpoint literals to sample before cancel
Vec_Int_t * vOutVals; // optional endpoint values by output
int iOutVal; // current output whose endpoints are sampled
// watched clauses // watched clauses
Tas_Sto_t pStore; // storage for watched clauses Tas_Sto_t pStore; // storage for watched clauses
int * pWatches; // watched lists for each literal int * pWatches; // watched lists for each literal
@ -308,6 +312,29 @@ static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex )
} }
} }
static inline int Tas_ManLitValue( Tas_Man_t * p, int iLit )
{
Gia_Obj_t * pObj;
if ( iLit < 0 )
return -1;
if ( Abc_Lit2Var(iLit) == 0 )
return Abc_LitIsCompl(iLit);
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(iLit) );
if ( !Tas_VarIsAssigned(pObj) )
return -1;
return Tas_VarValue(pObj) ^ Abc_LitIsCompl(iLit);
}
static inline void Tas_ManSaveOutVals( Tas_Man_t * p, Vec_Int_t * vOutLits, Vec_Int_t * vOutVals, int Out )
{
if ( vOutLits == NULL || vOutVals == NULL )
return;
if ( 2*Out + 1 >= Vec_IntSize(vOutLits) )
return;
Vec_IntWriteEntry( vOutVals, 2*Out, Tas_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out) ) );
Vec_IntWriteEntry( vOutVals, 2*Out + 1, Tas_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out + 1) ) );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -1380,7 +1407,10 @@ int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
if ( pObj2 && !Tas_VarIsAssigned(Gia_Regular(pObj2)) ) if ( pObj2 && !Tas_VarIsAssigned(Gia_Regular(pObj2)) )
Tas_ManAssign( p, pObj2, 0, NULL, NULL ); Tas_ManAssign( p, pObj2, 0, NULL, NULL );
if ( !Tas_ManSolve_rec(p, 0) && !Tas_ManCheckLimits(p) ) if ( !Tas_ManSolve_rec(p, 0) && !Tas_ManCheckLimits(p) )
{
Tas_ManSaveModel( p, p->vModel ); Tas_ManSaveModel( p, p->vModel );
Tas_ManSaveOutVals( p, p->vOutLits, p->vOutVals, p->iOutVal );
}
else else
RetValue = 1; RetValue = 1;
Tas_ManCancelUntil( p, 0 ); Tas_ManCancelUntil( p, 0 );
@ -1514,14 +1544,14 @@ void Tas_ManSatPrintStats( Tas_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ) Vec_Int_t * Tas_ManSolveMiterNcOutVals( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals )
{ {
extern void Gia_ManCollectTest( Gia_Man_t * pAig ); extern void Gia_ManCollectTest( Gia_Man_t * pAig );
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ); extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Tas_Man_t * p; Tas_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore; Vec_Int_t * vCex, * vVisit, * vCexStore, * vOutVals = NULL;
Vec_Str_t * vStatus; Vec_Str_t * vStatus;
Gia_Obj_t * pRoot;//, * pRootCopy; Gia_Obj_t * pRoot;//, * pRootCopy;
// Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp; // Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp;
int i, status; int i, status;
@ -1540,6 +1570,12 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// create resulting data-structures // create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 ); vCexStore = Vec_IntAlloc( 10000 );
if ( pvOutVals )
{
*pvOutVals = NULL;
if ( vOutLits )
vOutVals = Vec_IntStartFull( 2 * Gia_ManPoNum(pAig) );
}
vVisit = Vec_IntAlloc( 100 ); vVisit = Vec_IntAlloc( 100 );
vCex = Tas_ReadModel( p ); vCex = Tas_ReadModel( p );
// solve for each output // solve for each output
@ -1567,7 +1603,13 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// p->Pars.fUseActive = 1; // p->Pars.fUseActive = 1;
p->Pars.fUseHighest = 1; p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0; p->Pars.fUseLowest = 0;
p->vOutLits = vOutLits;
p->vOutVals = vOutVals;
p->iOutVal = i;
status = Tas_ManSolve( p, Gia_ObjChild0(pRoot), NULL ); status = Tas_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
p->vOutLits = NULL;
p->vOutVals = NULL;
p->iOutVal = -1;
// printf( "\n" ); // printf( "\n" );
/* /*
if ( status == -1 ) if ( status == -1 )
@ -1621,6 +1663,10 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro ); // printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
Tas_ManStop( p ); Tas_ManStop( p );
*pvStatus = vStatus; *pvStatus = vStatus;
if ( pvOutVals )
*pvOutVals = vOutVals;
else
Vec_IntFreeP( &vOutVals );
// printf( "Total number of cex literals = %d. (Ave = %d)\n", // printf( "Total number of cex literals = %d. (Ave = %d)\n",
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, // Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
@ -1628,6 +1674,11 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
return vCexStore; return vCexStore;
} }
Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{
return Tas_ManSolveMiterNcOutVals( pAig, nConfs, pvStatus, fVerbose, NULL, NULL );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Packs patterns into array of simulation info.] Synopsis [Packs patterns into array of simulation info.]
@ -1782,10 +1833,144 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
} }
/**Function*************************************************************
Synopsis [Sets the conflict limit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Tas_ManSetConflictNum( Tas_Man_t * p, int Num )
{
p->Pars.nBTLimit = Num;
}
/**Function*************************************************************
Synopsis [Syncs newly appended pAig objects for resident reuse.]
Description [Prepares objects appended since the last sync so the
persistent solver can reuse the same manager across rounds. Mirrors
Cbs_ManSyncCore but also resizes the TAS-specific watched-literal and
activity arrays.]
SideEffects []
SeeAlso []
***********************************************************************/
void Tas_ManSyncCore( Tas_Man_t * p )
{
Gia_Man_t * pAig = p->pAig;
Gia_Obj_t * pObj;
int i, nObjs = Gia_ManObjNum( pAig );
assert( p->nSyncedObjs <= nObjs );
if ( p->nSyncedObjs == nObjs )
return;
pAig->pRefs = ABC_REALLOC( int, pAig->pRefs, nObjs );
memset( pAig->pRefs + p->nSyncedObjs, 0, sizeof(int) * (nObjs - p->nSyncedObjs) );
p->pWatches = ABC_REALLOC( int, p->pWatches, 2 * nObjs );
memset( p->pWatches + 2 * p->nSyncedObjs, 0, sizeof(int) * 2 * (nObjs - p->nSyncedObjs) );
p->pActivity = ABC_REALLOC( float, p->pActivity, nObjs );
memset( p->pActivity + p->nSyncedObjs, 0, sizeof(float) * (nObjs - p->nSyncedObjs) );
for ( i = p->nSyncedObjs; i < nObjs; i++ )
{
pObj = Gia_ManObj( pAig, i );
pObj->fMark0 = pObj->fMark1 = 0;
pObj->Value = ~0;
pObj->fPhase = 0;
if ( Gia_ObjIsAnd(pObj) )
{
pAig->pRefs[Gia_ObjFaninId0(pObj, i)]++;
pAig->pRefs[Gia_ObjFaninId1(pObj, i)]++;
}
}
p->nSyncedObjs = nObjs;
}
/**Function*************************************************************
Synopsis [Solves a set of root literals directly on a persistent AIG.]
Description [Same prover as Tas_ManSolveMiterNc, but each problem is a root
literal of p->pAig (no CO needed) instead of a CO of a freshly built view, and
the manager is resident: it is allocated once on the persistent COless pCore
and reused across rounds, only Tas_ManSyncCore-ing the objects appended since
the last call. Output index i corresponds to vRootLits[i]; vCexStore / vStatus
format matches Tas_ManSolveMiterNc. CEX is saved by CioId, which on pCore
equals the view's CI numbering.]
SideEffects [Prepares newly appended objects via Tas_ManSyncCore.]
SeeAlso []
***********************************************************************/
Vec_Int_t * Tas_ManSolveRoots( Tas_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose )
{
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Gia_Man_t * pAig = p->pAig;
Vec_Int_t * vCex, * vCexStore;
Vec_Str_t * vStatus;
int i, iLit, status;
abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 );
Tas_ManSyncCore( p ); // prep only objects appended since the last solve
vStatus = Vec_StrAlloc( Vec_IntSize(vRootLits) );
vCexStore = Vec_IntAlloc( 10000 );
vCex = Tas_ReadModel( p );
Vec_IntForEachEntry( vRootLits, iLit, i )
{
Vec_IntClear( vCex );
if ( Abc_Lit2Var(iLit) == 0 ) // structural constant root
{
if ( Abc_LitIsCompl(iLit) ) // const 1: trivial counter-example
{
Cec_ManSatAddToStore( vCexStore, vCex, i );
Vec_StrPush( vStatus, 0 );
}
else // const 0: proved
Vec_StrPush( vStatus, 1 );
continue;
}
clk = Abc_Clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Tas_ManSolve( p, Gia_ObjFromLit(pAig, iLit), NULL );
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += Abc_Clock() - clk;
continue;
}
if ( status == 0 )
{
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += Abc_Clock() - clk;
continue;
}
assert( status == 1 );
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += Abc_Clock() - clk;
}
p->nSatTotal += Vec_IntSize(vRootLits);
p->timeTotal += Abc_Clock() - clkTotal;
*pvStatus = vStatus;
return vCexStore;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_END

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

@ -495,6 +495,7 @@ static int Abc_CommandAbc9Append ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Scorr2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatEnum ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1346,6 +1347,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&scl", Abc_CommandAbc9Scl, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&scl", Abc_CommandAbc9Scl, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&lcorr", Abc_CommandAbc9Lcorr, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&lcorr", Abc_CommandAbc9Lcorr, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&scorr", Abc_CommandAbc9Scorr, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&scorr", Abc_CommandAbc9Scorr, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&scorr2", Abc_CommandAbc9Scorr2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&choice", Abc_CommandAbc9Choice, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&choice", Abc_CommandAbc9Choice, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satenum", Abc_CommandAbc9SatEnum, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satenum", Abc_CommandAbc9SatEnum, 0 );
@ -41820,7 +41822,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManCorSetDefaultParams( pPars ); Cec_ManCorSetDefaultParams( pPars );
pPars->nProcs = 1; pPars->nProcs = 1;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqiowvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -41919,9 +41921,6 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'q': case 'q':
pPars->fStopWhenGone ^= 1; pPars->fStopWhenGone ^= 1;
break; break;
case 'i':
pPars->fIncremental ^= 1;
break;
case 'o': case 'o':
fUseOld ^= 1; fUseOld ^= 1;
break; break;
@ -41935,13 +41934,6 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage; goto usage;
} }
} }
if ( pPars->fIncremental )
{
//preserve for incremental mode, maybe should be a separate command
pPars->fDynSrm = 1; //dynamic SRM
pPars->fIncrSim = 1; //incremental simulation
pPars->fSkipFailResim = 1; //skip resimulation of failed flops
}
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9Scorr(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Scorr(): There is no AIG.\n" );
@ -42002,7 +41994,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqiowvh]\n" ); Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqowvh]\n" );
Abc_Print( -2, "\t performs signal correpondence computation\n" ); Abc_Print( -2, "\t performs signal correpondence computation\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@ -42017,7 +42009,6 @@ usage:
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" ); Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
Abc_Print( -2, "\t-i : toggle integrated incremental SRM/re-proof/resimulation [default = %s]\n", pPars->fIncremental? "yes": "no" );
Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" ); Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
@ -42025,6 +42016,267 @@ usage:
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Scorr2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pPars );
extern Gia_Man_t * Cec_ManLSCorrespondence2( Gia_Man_t * p, Cec_ParCor_t * pPars );
extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars );
extern Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars );
Cec_ParCor_t Pars, * pPars = &Pars;
Gia_Man_t * pTemp;
int fPartition = 0;
int nFlopIncFreq = 0;
int fUseOld = 0, c;
Cec_ManCorSetDefaultParams( pPars );
pPars->nProcs = 1;
pPars->fIncremental = 1;
pPars->fDynSrm = 1;
pPars->fIncrSim = 1;
pPars->fSkipFailResim = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZKYDpkrecqiIosvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFrames < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'G':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPrefix = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPrefix < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLimitMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLimitMax < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nProcs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nProcs < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPartSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPartSize < 0 )
goto usage;
break;
case 'Z':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" );
goto usage;
}
nFlopIncFreq = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFlopIncFreq < 0 )
goto usage;
break;
case 'p':
fPartition ^= 1;
break;
case 'k':
pPars->fConstCorr ^= 1;
break;
case 'r':
pPars->fUseRings ^= 1;
break;
case 'e':
pPars->fMakeChoices ^= 1;
break;
case 'c':
pPars->fUseCSat ^= 1;
break;
case 'q':
pPars->fStopWhenGone ^= 1;
break;
case 'i':
pPars->fIncremental ^= 1;
break;
case 'D':
pPars->fDynSrm ^= 1;
break;
case 'I':
pPars->fIncrSim ^= 1;
break;
case 's':
pPars->fSkipFailResim ^= 1;
break;
case 'Y':
pPars->fBmcTasAdaptive ^= 1;
break;
case 'K':
pPars->fKissatCert ^= 1;
break;
case 'o':
fUseOld ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
default:
goto usage;
}
}
if ( pPars->fDynSrm && !pPars->fIncremental )
{
Abc_Print( -1, "The dynamic SRM manager (-D) requires -i.\n" );
return 1;
}
if ( pPars->fBmcTasAdaptive && !pPars->fDynSrm )
{
Abc_Print( -1, "The adaptive BMC solver policy (-Y) requires -D.\n" );
return 1;
}
if ( pPars->fKissatCert &&
(fUseOld || fPartition || pPars->nPartSize > 0 ||
nFlopIncFreq > 0 || pPars->nPrefix > 0) )
{
Abc_Print( -1, "The strict fixed-point oracle (-K) supports the direct engine with -G 0 only.\n" );
return 1;
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "&scorr2: There is no AIG.\n" );
return 1;
}
if ( Gia_ManBoxNum(pAbc->pGia) && Gia_ManRegBoxNum(pAbc->pGia) )
{
if ( pAbc->pGia->pAigExtra == NULL )
{
printf( "Timing manager is given but there is no GIA of boxes.\n" );
return 0;
}
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, pPars, 0, 0, pPars->fVerbose, pPars->fVerboseFlops );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( 0, "The network is combinational.\n" );
return 0;
}
if ( nFlopIncFreq )
{
extern Gia_Man_t * Gia_ManDupStopsAdd( Gia_Man_t * p, Vec_Int_t * vStops );
extern Gia_Man_t * Gia_ManDupStopsRem( Gia_Man_t * p, Vec_Int_t * vStops );
extern Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose );
Vec_Int_t * vStops = Gia_ManFindStopFlops( pAbc->pGia, nFlopIncFreq, pPars->fVerbose );
if ( vStops )
{
extern void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pNew );
Gia_Man_t * pUsed = Gia_ManDupStopsAdd( pAbc->pGia, vStops );
if ( pPars->nPartSize > 0 )
pTemp = Gia_SignalCorrespondencePart( pUsed, pPars );
else if ( fUseOld )
pTemp = Cec_ManScorrCorrespondence( pUsed, pPars );
else if ( fPartition )
pTemp = Gia_ManScorrDivideTest( pUsed, pPars );
else
pTemp = Cec_ManLSCorrespondence2( pUsed, pPars );
Gia_ManTransferEquivs2( pUsed, pAbc->pGia );
Gia_ManStop( pUsed );
pTemp = Gia_ManDupStopsRem( pUsed = pTemp, vStops );
Gia_ManStop( pUsed );
Abc_FrameUpdateGia( pAbc, pTemp );
Vec_IntFree( vStops );
return 0;
}
}
if ( pPars->nPartSize > 0 )
pTemp = Gia_SignalCorrespondencePart( pAbc->pGia, pPars );
else if ( fUseOld )
pTemp = Cec_ManScorrCorrespondence( pAbc->pGia, pPars );
else if ( fPartition )
pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
else
pTemp = Cec_ManLSCorrespondence2( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &scorr2 [-FCGXPSZ num] [-pkrecqiDIsYKovh]\n" );
Abc_Print( -2, "\t performs signal correpondence computation using the incremental scorr2 engine\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
Abc_Print( -2, "\t-G num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", pPars->nProcs );
Abc_Print( -2, "\t-S num : the number of flops in one partition [default = %d]\n", pPars->nPartSize );
Abc_Print( -2, "\t-Z num : the average flop include frequency [default = %d]\n", nFlopIncFreq );
Abc_Print( -2, "\t-p : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
Abc_Print( -2, "\t-i : toggle incremental TFO-triggered re-proof [default = %s]\n", pPars->fIncremental? "yes": "no" );
Abc_Print( -2, "\t-D : toggle persistent dynamic SRM construction [default = %s]\n", pPars->fDynSrm? "yes": "no" );
Abc_Print( -2, "\t-I : toggle persistent event-driven resimulation [default = %s]\n", pPars->fIncrSim? "yes": "no" );
Abc_Print( -2, "\t-s : toggle skipping resimulation without a real CEX [default = %s]\n", pPars->fSkipFailResim? "yes": "no" );
Abc_Print( -2, "\t-Y : toggle guarded CBS-first/TAS-rescue BMC policy [default = %s]\n", pPars->fBmcTasAdaptive? "yes": "no" );
Abc_Print( -2, "\t-K : toggle strict final fixed-point Kissat audit [default = %s]\n", pPars->fKissatCert? "yes": "no" );
Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t This command was contributed by Xiran Zhao from University of Chinese Academy of Sciences (UCAS).\n" );
return 1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []

13
src/misc/util/abc_global.h
View File

@ -351,6 +351,19 @@ static inline abctime Abc_Clock()
return (abctime) clock(); return (abctime) clock();
#endif #endif
} }
// Returns monotonic wall-clock time in nanoseconds. The dynamic SRM
// heuristics use this to compare rebuild and reuse costs.
static inline abctime Abc_ClockHr()
{
#if defined(CLOCK_MONOTONIC)
struct timespec ts;
if ( clock_gettime( CLOCK_MONOTONIC, &ts ) < 0 )
return (abctime)-1;
return ((abctime) ts.tv_sec) * 1000000000 + (abctime) ts.tv_nsec;
#else
return (abctime)( (double)Abc_Clock() * 1.0e9 / CLOCKS_PER_SEC );
#endif
}
// counting thread time // counting thread time
static inline abctime Abc_ThreadClock() static inline abctime Abc_ThreadClock()
{ {

11
src/proof/cec/cec.h
View File

@ -159,6 +159,9 @@ struct Cec_ParCor_t_
int nLevelMax; // (scorr only) the max number of levels int nLevelMax; // (scorr only) the max number of levels
int nStepsMax; // (scorr only) the max number of induction steps int nStepsMax; // (scorr only) the max number of induction steps
int nLimitMax; // (scorr only) stop after this many iterations if little or no improvement int nLimitMax; // (scorr only) stop after this many iterations if little or no improvement
int nIncrFallbackPct; // (-i) fall back to full SRM when active pairs exceed this percent
int nDynSrmRebuildPct; // (-D) cold-rebuild when active pairs exceed this percent
int nDynSrmCompactMult; // (-D) cold-compact when core exceeds this multiple of reset size
int fLatchCorr; // consider only latch outputs int fLatchCorr; // consider only latch outputs
int fConstCorr; // consider only constants int fConstCorr; // consider only constants
int fUseRings; // use rings int fUseRings; // use rings
@ -167,10 +170,16 @@ struct Cec_ParCor_t_
// int fFirstStop; // stop on the first sat output // int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation int fUseSmartCnf; // use smart CNF computation
int fStopWhenGone; // quit when PO is not a candidate constant int fStopWhenGone; // quit when PO is not a candidate constant
int fIncremental; // integrated incremental mode for &scorr int fIncremental; // active-list/TFO-triggered reproof in main loop
int fIncrOracle; // internal unbounded shadow SAT for pairs skipped by -i
int fIncrSim; // persistent CEX-TFO-only resimulation after SAT int fIncrSim; // persistent CEX-TFO-only resimulation after SAT
int fDynSrm; // persistent dynamic SRM and true-unroll resimulation int fDynSrm; // persistent dynamic SRM and true-unroll resimulation
int fDynSrmNoAdapt;// disable adaptive cold-rebuilds in DynSRM
int fUseTas; // use TAS (vs CBS) for persistent solving (-D)
int fBmcTasAdaptive;// use guarded CBS-first/TAS-rescue policy in BMC
int fKissatCert; // strictly audit final base+step obligations with Kissat
int fSkipFailResim;// skip resim in rounds with no real CEX (only timeout/fail) int fSkipFailResim;// skip resim in rounds with no real CEX (only timeout/fail)
int fVerifyResim; // internal oracle: check incremental resim values vs full sweep
int fVerboseFlops; // verbose stats int fVerboseFlops; // verbose stats
int fVeryVerbose; // verbose stats int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats int fVerbose; // verbose stats

8
src/proof/cec/cecCore.c
View File

@ -192,10 +192,18 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
p->nBTLimit = 100; // conflict limit at a node p->nBTLimit = 100; // conflict limit at a node
p->nLevelMax = -1; // (scorr only) the max number of levels p->nLevelMax = -1; // (scorr only) the max number of levels
p->nStepsMax = -1; // (scorr only) the max number of induction steps p->nStepsMax = -1; // (scorr only) the max number of induction steps
p->nIncrFallbackPct = 100; // (-i) fall back to full SRM when active pairs exceed this percent
p->nDynSrmRebuildPct = 20; // (-D) cold-rebuild when active pairs exceed this percent
p->nDynSrmCompactMult = 4; // (-D) cold-compact when core exceeds this multiple of reset size
p->fLatchCorr = 0; // consider only latch outputs p->fLatchCorr = 0; // consider only latch outputs
p->fConstCorr = 0; // consider only constants p->fConstCorr = 0; // consider only constants
p->fUseRings = 1; // combine classes into rings p->fUseRings = 1; // combine classes into rings
p->fIncrOracle = 0; // internal unbounded shadow SAT for pairs skipped by -i
p->fSkipFailResim = 0; // skip resim when a round has no real CEX (only timeout/fail) p->fSkipFailResim = 0; // skip resim when a round has no real CEX (only timeout/fail)
p->fDynSrmNoAdapt = 1; // timing-guided DynSRM rebuild heuristic is opt-in
p->fUseTas = 0; // use CBS by default for persistent solving
p->fBmcTasAdaptive = 0; // guarded BMC TAS rescue is opt-in (-Y)
p->fKissatCert = 0; // strict final base+step Kissat audit is opt-in
p->fUseCSat = 1; // use circuit-based solver p->fUseCSat = 1; // use circuit-based solver
// p->fFirstStop = 0; // stop on the first sat output // p->fFirstStop = 0; // stop on the first sat output
p->fUseSmartCnf = 0; // use smart CNF computation p->fUseSmartCnf = 0; // use smart CNF computation

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

@ -34,9 +34,7 @@ static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// Shared with cecCorrIncr.c (declared in cecInt.h). static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
@ -47,13 +45,13 @@ extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pO
Synopsis [Computes the real value of the literal w/o spec reduction.] Synopsis [Computes the real value of the literal w/o spec reduction.]
Description [] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{ {
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
{ {
@ -77,7 +75,7 @@ int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int
Synopsis [Recursively performs speculative reduction for the object.] Synopsis [Recursively performs speculative reduction for the object.]
Description [] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
@ -106,7 +104,7 @@ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
Synopsis [Derives SRM for signal correspondence.] Synopsis [Derives SRM for signal correspondence.]
Description [] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
@ -223,7 +221,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
Synopsis [Derives SRM for signal correspondence.] Synopsis [Derives SRM for signal correspondence.]
Description [] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
@ -292,7 +290,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.] Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
Description [] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
@ -499,53 +497,6 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
return iStart; return iStart;
} }
/**Function*************************************************************
Synopsis [Performs bitpacking of counter-examples and records bit lanes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLoadCounterExamplesMapped( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vOutBits )
{
Vec_Int_t * vPat;
Vec_Ptr_t * vPres;
int nWords = Vec_PtrReadWordsSimInfo(vInfo);
int nBits = 32 * nWords;
int k, nSize, Out;
Vec_IntClear( vOutBits );
vPat = Vec_IntAlloc( 100 );
vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Out = Vec_IntEntry( vCexStore, iStart++ );
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize <= 0 )
continue;
Vec_IntClear( vPat );
for ( k = 0; k < nSize; k++ )
Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
if ( k < nBits )
{
Vec_IntPush( vOutBits, Out );
Vec_IntPush( vOutBits, k );
}
if ( k == nBits-1 )
break;
}
Vec_PtrFree( vPres );
Vec_IntFree( vPat );
return iStart;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs bitpacking of counter-examples.] Synopsis [Performs bitpacking of counter-examples.]
@ -587,53 +538,6 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
return iStart; return iStart;
} }
/**Function*************************************************************
Synopsis [Classifies vCexStore entries by SAT outcome.]
Description [Each entry is (Out, nLits[, lit0, ..., lit{nLits-1}]).
nLits > 0 -> real SAT CEX with usable literals;
nLits == 0 -> trivial SAT (e.g. SRM PO became const 1);
nLits == -1 -> timeout/fail, no CEX.
Counts are written via the out-pointers (any may be NULL).
Returns 1 iff there is at least one entry usable for resim
(real or trivial), preserving the prior skip-failed-resim
semantics where only timeout-only stores get skipped.]
SideEffects []
SeeAlso []
***********************************************************************/
static int Cec_ManCexStoreClassify( Vec_Int_t * vCexStore, int * pnReal, int * pnTriv, int * pnFail )
{
int iStart = 0, nSize, nReal = 0, nTriv = 0, nFail = 0;
while ( iStart < Vec_IntSize(vCexStore) )
{
iStart++; // output number
assert( iStart < Vec_IntSize(vCexStore) );
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize > 0 )
{
nReal++;
iStart += nSize;
}
else if ( nSize == 0 )
{
nTriv++;
}
else
{
assert( nSize == -1 );
nFail++;
}
}
if ( pnReal ) *pnReal = nReal;
if ( pnTriv ) *pnTriv = nTriv;
if ( pnFail ) *pnFail = nFail;
return (nReal + nTriv) > 0;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.] Synopsis [Resimulates counter-examples derived by the SAT solver.]
@ -645,104 +549,33 @@ static int Cec_ManCexStoreClassify( Vec_Int_t * vCexStore, int * pnReal, int * p
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static int Cec_ManResimulateCounterExamplesSeed( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, Cec_SeedSim_t * pSeed, Vec_Int_t * vOutputs ) int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
{ {
Vec_Int_t * vPairs = NULL; Vec_Int_t * vPairs;
Vec_Int_t * vOutBits = NULL; Vec_Ptr_t * vSimInfo;
Vec_Ptr_t * vSimInfo = NULL; int RetValue = 0, iStart = 0;
int RetValue = 0, iStart = 0, fValueRefs = 0; vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
if ( pSeed ) Gia_ManCreateValueRefs( pSim->pAig );
Cec_SeedSimBeginCall( pSeed ); // reset per-call local/full/maxdirty counters
// pSim->pPars->nWords = 63; // pSim->pPars->nWords = 63;
pSim->pPars->nFrames = nFrames; pSim->pPars->nFrames = nFrames;
if ( pSeed ) vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
{
Cec_SeedSimEnsurePersistent( pSeed, pSim );
// Defer the (possibly full-unroll-sized) class cone: it is built lazily
// inside Cec_SeedSimTryBatch() only once a batch passes the density gate,
// so rounds that fall back to full resim never pay for it.
pSeed->fUseCone = 0;
vSimInfo = pSeed->vSimInfo;
vOutBits = Vec_IntAlloc( 1000 );
}
else
{
Gia_ManCreateValueRefs( pSim->pAig );
fValueRefs = 1;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
}
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
while ( iStart < Vec_IntSize(vCexStore) ) while ( iStart < Vec_IntSize(vCexStore) )
{ {
if ( pSeed ) Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
{ iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
int LocalStatus; // iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
iStart = Cec_SeedSimLoadPersistentBatch( // Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
pSeed, vCexStore, iStart, vPairs, vOutBits ); Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
if ( pSeed->nFallbackCooldown > 0 ) RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
{
Cec_SeedSimBypassBatch( pSeed, Vec_IntSize(vOutBits) / 2 );
pSeed->nFallbackCooldown--;
}
else if ( (LocalStatus = Cec_SeedSimTryBatch(
pSeed, pSim, vSimInfo, vOutputs, vOutBits, nFrames )) ==
CEC_SEEDSIM_RESULT_LOCAL )
{
pSeed->nFallbackStreak = 0;
pSeed->nFallbackCooldown = 0;
continue;
}
else if ( LocalStatus == CEC_SEEDSIM_RESULT_FULL_WIDE )
{
int Shift;
pSeed->nFallbackStreak++;
Shift = Abc_MinInt( pSeed->nFallbackStreak - 1, 3 );
pSeed->nFallbackCooldown =
Abc_MinInt( (1 << Shift) - 1,
CEC_SEEDSIM_MAX_FALLBACK_BACKOFF );
}
else
{
pSeed->nFallbackStreak = 0;
pSeed->nFallbackCooldown = 0;
}
}
else
{
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
}
// The local path returned above. Reaching here means standard full
// resimulation, either outside incremental mode or as a fallback.
if ( pSeed )
{
if ( !fValueRefs )
{
Gia_ManCreateValueRefs( pSim->pAig );
fValueRefs = 1;
}
RetValue |= Cec_ManSeqResimulateSeed( pSim, vSimInfo, pSeed );
Cec_SeedSimRestorePersistentInputs( pSeed );
}
else
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL ); // Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
} }
//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); //Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
assert( iStart == Vec_IntSize(vCexStore) ); assert( iStart == Vec_IntSize(vCexStore) );
Vec_IntFreeP( &vOutBits ); Vec_PtrFree( vSimInfo );
if ( !pSeed ) Vec_IntFree( vPairs );
Vec_PtrFree( vSimInfo );
Vec_IntFreeP( &vPairs );
return RetValue; return RetValue;
} }
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
{
return Cec_ManResimulateCounterExamplesSeed( pSim, vCexStore, nFrames, NULL, NULL );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.] Synopsis [Resimulates counter-examples derived by the SAT solver.]
@ -772,102 +605,12 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
return RetValue; return RetValue;
} }
/**Function*************************************************************
Synopsis [Checks whether two endpoints are still in the same class.]
Description [Ring mode needs special handling for the closing edge
tail -> head because Gia_ObjHasSameRepr() compares raw
representatives and the head stores GIA_VOID.]
SideEffects []
SeeAlso []
***********************************************************************/
static int Cec_ManObjsStillMerged( Gia_Man_t * p, int iRepr, int iObj, int fRings )
{
int iReprRoot, iObjRoot;
if ( !fRings )
return Gia_ObjHasSameRepr( p, iRepr, iObj );
if ( iRepr == 0 )
return Gia_ObjIsConst( p, iObj );
if ( iObj == 0 )
return Gia_ObjIsConst( p, iRepr );
if ( !Gia_ObjIsClass( p, iRepr ) || !Gia_ObjIsClass( p, iObj ) )
return 0;
iReprRoot = Gia_ObjIsHead( p, iRepr ) ? iRepr : Gia_ObjRepr( p, iRepr );
iObjRoot = Gia_ObjIsHead( p, iObj ) ? iObj : Gia_ObjRepr( p, iObj );
return iReprRoot == iObjRoot && iReprRoot != GIA_VOID;
}
static int Cec_ManObjToSplit( Gia_Man_t * p, int iRepr, int iObj, int fRings )
{
// For the ring closing edge (tail, head), split the tail. Splitting the
// head is also correct, but it changes the representative of the whole
// remaining class and creates a much larger incremental seed set.
if ( fRings && iObj > 0 && Gia_ObjIsHead( p, iObj ) && Gia_ObjIsClass( p, iRepr ) )
return iRepr;
return iObj;
}
/**Function*************************************************************
Synopsis [Directly splits pairs whose SAT result was trivial (nLits==0).]
Description [A trivial SAT (e.g. SRM PO became const 1) is a real
disproval but carries no CEX literals, so Cec_ManResimulateCounterExamples
cannot break the pair -- only random filler can, and usually does not.
Splitting these pairs directly is sound (SAT proved disequivalence) and
recovers work that the standard resim path leaves on the table.
Only nLits==0 entries are touched; nLits>0 entries are left for resim to
refine, matching the established behaviour in Gia_ManCheckRefinements
that avoids force-splitting CEX-bearing SAT pairs (token_ring regression).
Returns the number of pairs actually split this call.]
SideEffects []
SeeAlso []
***********************************************************************/
static int Cec_ManTrivialSatSplit( Gia_Man_t * pAig, Cec_ManSim_t * pSim,
Vec_Int_t * vCexStore, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, int fRings )
{
int iStart = 0, Out, nSize, iRepr, iObj, iSplit, Count = 0;
while ( iStart < Vec_IntSize(vCexStore) )
{
Out = Vec_IntEntry( vCexStore, iStart++ );
assert( iStart < Vec_IntSize(vCexStore) );
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize > 0 )
{
iStart += nSize;
continue;
}
if ( nSize < 0 )
continue;
// nSize == 0 -> trivial SAT, no CEX literals.
assert( Out < Vec_StrSize(vStatus) );
assert( Vec_StrEntry(vStatus, Out) == 0 );
iRepr = Vec_IntEntry( vOutputs, 2*Out );
iObj = Vec_IntEntry( vOutputs, 2*Out + 1 );
if ( !Cec_ManObjsStillMerged( pAig, iRepr, iObj, fRings ) )
continue;
iSplit = Cec_ManObjToSplit( pAig, iRepr, iObj, fRings );
if ( Cec_ManSimClassRemoveOne( pSim, iSplit ) )
Count++;
}
return Count;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Updates equivalence classes by marking those that timed out.] Synopsis [Updates equivalence classes by marking those that timed out.]
Description [Returns 1 if all nodes are proved.] Description [Returns 1 if all ndoes are proved.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
@ -1049,7 +792,7 @@ int Cec_ManCountLits( Gia_Man_t * p )
***********************************************************************/ ***********************************************************************/
void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs ) void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
{ {
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Vec_Str_t * vStatus; Vec_Str_t * vStatus;
@ -1057,16 +800,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
Vec_Int_t * vCexStore; Vec_Int_t * vCexStore;
Cec_ManSim_t * pSim; Cec_ManSim_t * pSim;
Gia_Man_t * pSrm; Gia_Man_t * pSrm;
int fChanges, i; int fChanges, RetValue, i;
int nBmcResimFrames = pPars->nFrames + 1 + nPrefs;
int fBmcPersist = 0;
// BMC SRM is keyed only on pReprs (Gia_ManCorrSpecReduceInit ignores
// its fRings flag). So the incremental filter only needs pReprs-based
// seeds; pNexts changes cannot affect this SRM and there are no ring
// closing edges to reprove -- BMC is structurally simpler than the
// main inductive loop.
Cec_IncrMgr_t * pBmcMgr = NULL;
Cec_DynSrm_t * pBmcDynSrm = NULL;
// prepare simulation manager // prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim ); Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords; pParsSim->nWords = pPars->nWords;
@ -1079,102 +813,29 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
Cec_ManSatSetDefaultParams( pParsSat ); Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose; pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fIncremental )
{
pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs );
Cec_IncrMgrSnapshotClasses( pBmcMgr );
}
if ( pPars->fDynSrm && pBmcMgr )
pBmcDynSrm = Cec_DynSrmAlloc( pAig, pBmcMgr );
fBmcPersist = ( pBmcDynSrm != NULL && pPars->fUseCSat );
fChanges = 1; fChanges = 1;
for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ ) for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
{ {
int * pTfoMask = NULL;
int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0;
int nBmcPos = 0;
if ( Cec_ParCorShouldStop( pPars ) ) if ( Cec_ParCorShouldStop( pPars ) )
break; break;
abctime clkBmc = Abc_Clock(); abctime clkBmc = Abc_Clock();
fChanges = 0; fChanges = 0;
// BMC SRM is non-ring (Gia_ManCorrSpecReduceInit ignores fRings); pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
// the incremental mask filters on pReprs-derived endpoints only. if ( Gia_ManPoNum(pSrm) == 0 )
if ( pBmcMgr && i > 0 )
{ {
nReprSeeds = Cec_IncrMgrComputeSeeds( pBmcMgr ); Gia_ManStop( pSrm );
if ( nReprSeeds == 0 )
{
// No pReprs change. BMC SRM topology is unchanged.
break;
}
Cec_IncrMgrComputeTfo( pBmcMgr );
// BMC SRM is non-ring; pass fRings=0 so we count (head, member)
// pairs only and skip any ring-edge bookkeeping.
if ( pBmcDynSrm )
Cec_DynSrmCountActivePairs( pBmcDynSrm, 0, pBmcMgr->pTfoMark, &nTotalPairs, &nActivePairs );
else
Cec_IncrMgrCountActivePairs( pBmcMgr, 0, pBmcMgr->pTfoMark, &nTotalPairs, &nActivePairs );
if ( nActivePairs == 0 )
break;
// Same fallback heuristic as the main loop: above ~70% active,
// the mask plus emission filter costs more than just rebuilding
// the full SRM.
if ( !( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs ) )
pTfoMask = pBmcMgr->pTfoMark;
}
pSrm = NULL;
if ( fBmcPersist )
Cec_DynSrmBuildCoreInit( pBmcDynSrm, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
else if ( pBmcDynSrm )
pSrm = Cec_DynSrmBuildInit( pBmcDynSrm, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
else if ( pTfoMask )
pSrm = Gia_ManCorrSpecReduceInit_Active( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask );
else
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
nBmcPos = fBmcPersist ? Vec_IntSize(Cec_DynSrmOutLits(pBmcDynSrm)) : Gia_ManCoNum(pSrm);
if ( pTfoMask && pPars->fVeryVerbose )
Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n",
i, nReprSeeds, nActivePairs, nTotalPairs, nBmcPos );
// Snapshot after SRM construction, before SAT/refine: this is the
// class state whose pairs were just emitted. The next iteration's
// diff vs this snapshot tells us which pairs are stale.
if ( pBmcMgr )
Cec_IncrMgrSnapshotClasses( pBmcMgr );
if ( nBmcPos == 0 )
{
if ( pSrm )
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
break; break;
} }
pParsSat->nBTLimit *= 10; pParsSat->nBTLimit *= 10;
if ( fBmcPersist ) if ( pPars->fUseCSat )
vCexStore = Cec_DynSrmSolve( pBmcDynSrm, pPars->nBTLimit, &vStatus );
else if ( pPars->fUseCSat )
vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples // refine classes with these counter-examples
if ( Vec_IntSize(vCexStore) ) if ( Vec_IntSize(vCexStore) )
{ {
int nCexReal = 0, nCexTriv = 0; RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
// classify CEX entries: real (nLits>0) / trivial (==0) / fail (==-1)
Cec_ManCexStoreClassify( vCexStore, &nCexReal, &nCexTriv, NULL );
// only invoke resim when there is a real CEX (nLits>0). Trivial
// (nLits==0) and fail (==-1) entries carry no literals; trivial
// pairs are handled by direct split below, fail pairs by chk.
if ( nCexReal > 0 || !pPars->fSkipFailResim )
{
// Keep BMC/init CEX resimulation on the canonical full path even
// in incremental mode. BMC counterexamples are partial models
// of frame/prefix-specific SAT obligations; retaining them as a
// persistent simulation background over-refines classes and can
// significantly hurt gate QoR. The main correspondence loop
// below still uses event resim for ordinary refinement batches.
Cec_ManResimulateCounterExamples( pSim, vCexStore, nBmcResimFrames );
}
if ( nCexTriv > 0 )
Cec_ManTrivialSatSplit( pAig, pSim, vCexStore, vStatus, vOutputs, pPars->fUseRings );
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
fChanges = 1; fChanges = 1;
} }
@ -1183,14 +844,11 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
// recycle // recycle
Vec_IntFree( vCexStore ); Vec_IntFree( vCexStore );
Vec_StrFree( vStatus ); Vec_StrFree( vStatus );
if ( pSrm ) Gia_ManStop( pSrm );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
if ( Cec_ParCorShouldStop( pPars ) ) if ( Cec_ParCorShouldStop( pPars ) )
break; break;
} }
Cec_DynSrmFree( pBmcDynSrm );
Cec_IncrMgrFree( pBmcMgr );
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
} }
@ -1287,19 +945,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Cec_ManSim_t * pSim; Cec_ManSim_t * pSim;
Gia_Man_t * pSrm; Gia_Man_t * pSrm;
int r, nPrev[4] = {0}; int r, RetValue, nPrev[4] = {0};
abctime clkTotal = Abc_Clock(); abctime clkTotal = Abc_Clock();
abctime clkSat = 0, clkSim = 0, clkSrm = 0; abctime clkSat = 0, clkSim = 0, clkSrm = 0;
abctime clk2, clk = Abc_Clock(); abctime clk2, clk = Abc_Clock();
// Incremental active-list manager (NULL if -i not set)
Cec_IncrMgr_t * pMgr = NULL;
// Persistent dynamic SRM construction manager (NULL outside incremental mode).
Cec_DynSrm_t * pDynSrm = NULL;
int fPersist = 0; // incremental + circuit-SAT: solve persistent pCore directly
// Unified CEX event-resimulation manager (NULL outside incremental mode).
Cec_SeedSim_t * pSeedSim = NULL;
abctime clkIncr = 0;
int nIncrSkipped = 0, nIncrFallback = 0;
if ( Gia_ManRegNum(pAig) == 0 ) if ( Gia_ManRegNum(pAig) == 0 )
{ {
Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
@ -1330,9 +979,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 ); pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d. Incr = %d. Dyn = %d.\n", Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat, pPars->fIncremental, pPars->fDynSrm ); pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
} }
// check the base case // check the base case
@ -1350,136 +999,41 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
return 1; return 1;
} }
if ( pPars->fIncremental )
{
pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames );
Cec_IncrMgrSnapshotClasses( pMgr );
}
if ( pPars->fDynSrm && pMgr )
pDynSrm = Cec_DynSrmAlloc( pAig, pMgr );
// Incremental persistence path: solve the persistent COless pCore directly (circuit
// SAT only), skipping the per-round throwaway view that BuildView copies.
fPersist = ( pDynSrm != NULL && pPars->fUseCSat );
// Resident local-sim manager sized for the main-loop resim depth.
if ( pPars->fIncrSim )
pSeedSim = Cec_SeedSimAlloc( pAig, pPars->nFrames + 1 + nAddFrames, pPars->nFrames, pParsSim->nWords );
// perform refinement of equivalence classes // perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ ) for ( r = 0; r < nIterMax; r++ )
{ {
if ( Cec_ParCorShouldStop( pPars ) ) if ( Cec_ParCorShouldStop( pPars ) )
{ {
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
Cec_DynSrmFree( pDynSrm );
Cec_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
return 1; return 1;
} }
if ( pPars->nStepsMax == r ) if ( pPars->nStepsMax == r )
{ {
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
Cec_DynSrmFree( pDynSrm );
Cec_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r ); Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
fflush( stdout ); fflush( stdout );
return 1; return 1;
} }
clk = Abc_Clock(); clk = Abc_Clock();
// perform speculative reduction (with optional active-list filter) // perform speculative reduction
clk2 = Abc_Clock(); clk2 = Abc_Clock();
{ pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
int * pTfoMask = NULL; assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
int nReprSeeds = 0, nNextChanges = 0;
int nTotalPairs = 0, nActivePairs = 0;
// Decide whether to apply incremental TFO mask this iteration.
// Skip on r==0 because the first full SRM establishes the cache.
if ( pMgr && r > 0 )
{
abctime clkI = Abc_Clock();
nReprSeeds = Cec_IncrMgrComputeSeeds( pMgr );
nNextChanges = pPars->fUseRings ? Cec_IncrMgrCountNextChanges( pMgr ) : 0;
if ( nReprSeeds == 0 && nNextChanges == 0 )
{
// No class-state change since the full/active SRM just
// proved these pairs; this is true convergence.
clkIncr += Abc_Clock() - clkI;
clkSrm += Abc_Clock() - clk2;
break;
}
else
{
Cec_IncrMgrComputeTfo( pMgr );
if ( pDynSrm )
Cec_DynSrmCountActivePairs( pDynSrm, pPars->fUseRings, pMgr->pTfoMark, &nTotalPairs, &nActivePairs );
else
Cec_IncrMgrCountActivePairs( pMgr, pPars->fUseRings, pMgr->pTfoMark, &nTotalPairs, &nActivePairs );
if ( nActivePairs == 0 )
{
// Classes changed, but no remaining candidate pair
// depends on the changes and no new ring edge exists.
clkIncr += Abc_Clock() - clkI;
clkSrm += Abc_Clock() - clk2;
break;
}
// Fallback is based on emitted candidate pairs, not seed count.
// Above ~70% active pairs, full SRM is usually cheaper.
else if ( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs )
{
nIncrFallback++;
}
else
{
pTfoMask = pMgr->pTfoMark;
nIncrSkipped += nTotalPairs - nActivePairs;
}
}
clkIncr += Abc_Clock() - clkI;
}
// Incremental persistence under circuit-SAT: build the COless pCore and solve
// its root literals directly below; skip the per-round throwaway view.
if ( fPersist )
{
Cec_DynSrmBuildCore( pDynSrm, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
pSrm = NULL;
}
else if ( pDynSrm )
pSrm = Cec_DynSrmBuild( pDynSrm, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
else if ( pTfoMask )
pSrm = Gia_ManCorrSpecReduce_Emit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr, CEC_EMIT_ACTIVE, NULL );
else
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( pTfoMask && pPars->fVeryVerbose )
Abc_Print( 1, " [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n",
r, nReprSeeds, nNextChanges,
Vec_IntSize(pMgr->vTfoNodes), nActivePairs, nTotalPairs,
fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm) );
// Snapshot after SRM construction: the active builder still needs
// the old pNexts snapshot to recognize newly-created ring edges.
// SAT/sim refinement below is what creates the next iteration's diff.
if ( pMgr )
Cec_IncrMgrSnapshotClasses( pMgr );
}
assert( fPersist || (Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig)) );
clkSrm += Abc_Clock() - clk2; clkSrm += Abc_Clock() - clk2;
if ( (fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm)) == 0 ) if ( Gia_ManCoNum(pSrm) == 0 )
{ {
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
if ( pSrm ) Gia_ManStop( pSrm );
Gia_ManStop( pSrm );
break; break;
} }
//Gia_DumpAiger( pSrm, "corrsrm", r, 2 ); //Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
// found counter-examples to speculation // found counter-examples to speculation
clk2 = Abc_Clock(); clk2 = Abc_Clock();
if ( fPersist ) if ( pPars->fUseCSat )
vCexStore = Cec_DynSrmSolve( pDynSrm, pPars->nBTLimit, &vStatus );
else if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 ); vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
else else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
if ( pSrm ) Gia_ManStop( pSrm );
Gia_ManStop( pSrm );
clkSat += Abc_Clock() - clk2; clkSat += Abc_Clock() - clk2;
if ( Vec_IntSize(vCexStore) == 0 ) if ( Vec_IntSize(vCexStore) == 0 )
{ {
@ -1492,21 +1046,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// refine classes with these counter-examples // refine classes with these counter-examples
clk2 = Abc_Clock(); clk2 = Abc_Clock();
{ RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
int nCexReal = 0, nCexTriv = 0; Vec_IntFree( vCexStore );
Cec_ManCexStoreClassify( vCexStore, &nCexReal, &nCexTriv, NULL ); clkSim += Abc_Clock() - clk2;
if ( nCexReal > 0 || !pPars->fSkipFailResim ) Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
{
Cec_ManResimulateCounterExamplesSeed( pSim,
vCexStore, pPars->nFrames + 1 + nAddFrames,
pSeedSim, vOutputs );
}
if ( nCexTriv > 0 )
Cec_ManTrivialSatSplit( pAig, pSim, vCexStore, vStatus, vOutputs, pPars->fUseRings );
Vec_IntFree( vCexStore );
clkSim += Abc_Clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
}
if ( pPars->fVerbose ) if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk ); Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
Vec_StrFree( vStatus ); Vec_StrFree( vStatus );
@ -1515,9 +1058,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
if ( Cec_ParCorShouldStop( pPars ) ) if ( Cec_ParCorShouldStop( pPars ) )
{ {
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
Cec_DynSrmFree( pDynSrm );
Cec_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
return 1; return 1;
} }
// quit if const is no longer there // quit if const is no longer there
@ -1527,9 +1067,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
printf( "because the property output is no longer a candidate constant.\n" ); printf( "because the property output is no longer a candidate constant.\n" );
fflush( stdout ); fflush( stdout );
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
Cec_DynSrmFree( pDynSrm );
Cec_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
return 0; return 0;
} }
if ( pPars->nLimitMax ) if ( pPars->nLimitMax )
@ -1541,9 +1078,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
printf( "because refinement does not proceed quickly.\n" ); printf( "because refinement does not proceed quickly.\n" );
fflush( stdout ); fflush( stdout );
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
Cec_DynSrmFree( pDynSrm );
Cec_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts ); ABC_FREE( pAig->pNexts );
return 0; return 0;
@ -1571,21 +1105,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
ABC_PRTP( "Sat ", clkSat, clkTotal ); ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal ); ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
if ( pMgr )
{
ABC_PRTP( "Incr ", clkIncr, clkTotal );
Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped );
}
if ( pDynSrm )
Cec_DynSrmPrintStats( pDynSrm );
Abc_PrintTime( 1, "TOTAL", clkTotal ); Abc_PrintTime( 1, "TOTAL", clkTotal );
fflush( stdout ); fflush( stdout );
} }
Cec_IncrMgrFree( pMgr );
Cec_DynSrmFree( pDynSrm );
Cec_SeedSimFree( pSeedSim );
return 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************

2274
src/proof/cec/cecCorr2.c Normal file
View File

File diff suppressed because it is too large Load Diff

155
src/proof/cec/cecCorrCert.c Normal file
View File

@ -0,0 +1,155 @@
/**CFile****************************************************************
FileName [cecCorrCert.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Kissat certificate for the final &scorr2 fixed point.]
Author [Xiran Zhao]
Affiliation [University of Chinese Academy of Sciences (UCAS)]
Date [Ver. 1.0. Started - Jun 2026.]
***********************************************************************/
#include "cecInt.h"
#include "sat/cnf/cnf.h"
#include "sat/kissat/kissatSolver.h"
ABC_NAMESPACE_IMPL_START
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
/**Function*************************************************************
Synopsis [Certifies all SRM mismatch outputs in one Kissat call.]
Description [The generated CNF contains one OR clause over all SRM
outputs. UNSAT therefore proves every candidate pair simultaneously.
On SAT, one full CI assignment and one violated output are returned in
the same format used by the ordinary correspondence refinement loop.
Return values are 1 (all outputs UNSAT), 0 (SAT counterexample), and
-1 (UNKNOWN or an inconsistent model/API result).]
SideEffects [None on pSrm or the host correspondence classes.]
***********************************************************************/
int Cec_ManCorrKissatCertify( Gia_Man_t * pSrm, Vec_Int_t * vOutputs,
Vec_Int_t ** pvCexStore, Vec_Str_t ** pvStatus, int * piOut, int fVerbose )
{
Cnf_Dat_t * pCnf;
kissat_solver * pSat;
Vec_Int_t * vCexStore = Vec_IntAlloc( 16 );
Vec_Str_t * vStatus = Vec_StrAlloc( Gia_ManCoNum(pSrm) );
Gia_Obj_t * pObj;
unsigned char * pValues = NULL;
abctime clk = Abc_Clock();
int i, iVar, * pBeg, * pEnd, Status = -1, iOut = -1;
assert( Vec_IntSize(vOutputs) == 2 * Gia_ManCoNum(pSrm) );
*pvCexStore = NULL;
*pvStatus = NULL;
*piOut = -1;
for ( i = 0; i < Gia_ManCoNum(pSrm); i++ )
Vec_StrPush( vStatus, 1 );
if ( Gia_ManCoNum(pSrm) == 0 )
{
if ( fVerbose )
Abc_Print( 1, "[scorr2-audit] result=pass pairs=0 reason=structural time_sec=0.00\n" );
*pvCexStore = vCexStore;
*pvStatus = vStatus;
return 1;
}
// fAddOrCla=1 asserts that at least one mismatch output is true.
pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pSrm, 8, 0, 1, 0, 0 );
pSat = kissat_solver_new();
kissat_solver_setnvars( pSat, pCnf->nVars );
Cnf_CnfForClause( pCnf, pBeg, pEnd, i )
if ( !kissat_solver_addclause(pSat, pBeg, pEnd) )
{
// Contradiction during clause loading is already an UNSAT proof.
Status = -1;
goto finish;
}
Status = kissat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( Status == -1 )
goto finish;
if ( Status == 0 )
goto finish;
// Evaluate the GIA under the Kissat model to identify a violated pair.
pValues = ABC_CALLOC( unsigned char, Gia_ManObjNum(pSrm) );
Gia_ManForEachCi( pSrm, pObj, i )
{
iVar = pCnf->pVarNums[Gia_ObjId(pSrm, pObj)];
pValues[Gia_ObjId(pSrm, pObj)] = iVar >= 0 ? kissat_solver_get_var_value(pSat, iVar) : 0;
}
Gia_ManForEachAnd( pSrm, pObj, i )
pValues[Gia_ObjId(pSrm, pObj)] =
(pValues[Gia_ObjFaninId0p(pSrm, pObj)] ^ Gia_ObjFaninC0(pObj)) &
(pValues[Gia_ObjFaninId1p(pSrm, pObj)] ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pSrm, pObj, i )
if ( pValues[Gia_ObjFaninId0p(pSrm, pObj)] ^ Gia_ObjFaninC0(pObj) )
{
iOut = i;
break;
}
if ( iOut < 0 )
{
Status = 0;
goto finish;
}
{
Vec_Int_t * vCex = Vec_IntAlloc( Gia_ManCiNum(pSrm) );
Gia_ManForEachCi( pSrm, pObj, i )
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pObj), !pValues[Gia_ObjId(pSrm, pObj)]) );
Vec_StrWriteEntry( vStatus, iOut, 0 );
Cec_ManSatAddToStore( vCexStore, vCex, iOut );
Vec_IntFree( vCex );
}
finish:
if ( fVerbose )
{
if ( Status == -1 )
Abc_Print( 1, "[scorr2-audit] result=pass pairs=%d vars=%d clauses=%d ", Gia_ManCoNum(pSrm), pCnf->nVars, pCnf->nClauses );
else if ( Status == 1 && iOut >= 0 )
Abc_Print( 1, "[scorr2-audit] result=counterexample pair=%d/%d nodes=%d/%d ", iOut, Gia_ManCoNum(pSrm), Vec_IntEntry(vOutputs, 2*iOut), Vec_IntEntry(vOutputs, 2*iOut+1) );
else
Abc_Print( -1, "[scorr2-audit] result=unknown pairs=%d ", Gia_ManCoNum(pSrm) );
Abc_PrintTime( 1, "Kissat", Abc_Clock() - clk );
if ( Status == 1 && iOut >= 0 && pValues != NULL )
{
Abc_Print( -1, "[scorr2-audit] model" );
Gia_ManForEachCi( pSrm, pObj, i )
{
if ( i == 16 )
{
Abc_Print( -1, " ..." );
break;
}
Abc_Print( -1, " ci%d=%d", Gia_ObjCioId(pObj), pValues[Gia_ObjId(pSrm, pObj)] );
}
Abc_Print( -1, "\n" );
}
}
ABC_FREE( pValues );
kissat_solver_delete( pSat );
Cnf_DataFree( pCnf );
*pvCexStore = vCexStore;
*pvStatus = vStatus;
*piOut = iOut;
if ( Status == -1 )
return 1;
if ( Status == 1 && iOut >= 0 )
return 0;
return -1;
}
ABC_NAMESPACE_IMPL_END

573
src/proof/cec/cecCorrDyn.c
View File

@ -6,11 +6,11 @@
PackageName [Combinational equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Dynamic SRM manager for &scorr.] Synopsis [Dynamic SRM manager for &scorr2.]
Author [Xiran Zhao] Author [Xiran Zhao]
Affiliation [University of Chinese Academy of Sciences] Affiliation [University of Chinese Academy of Sciences (UCAS)]
Date [Ver. 1.0. Started - Jun 2026.] Date [Ver. 1.0. Started - Jun 2026.]
@ -20,6 +20,13 @@
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
#define CEC_BMC_TAS_PROBE_ROOTS 8
#define CEC_BMC_TAS_PROBE_SUCCESS_PCT 75
#define CEC_BMC_TAS_CORE_NORM_MAX 25000
#define CEC_BMC_TAS_CORE_ABS_MAX 200000
#define CEC_BMC_TAS_RETRY_ROOTS_MAX 8192
#define CEC_BMC_TAS_STRUCT_WORK_MAX 64000000LL
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -29,8 +36,12 @@ struct Cec_DynSrm_t_
Gia_Man_t * pAig; // host AIG; owned by caller Gia_Man_t * pAig; // host AIG; owned by caller
Cec_IncrMgr_t * pIncr; // active-list manager; owned by caller Cec_IncrMgr_t * pIncr; // active-list manager; owned by caller
Gia_Man_t * pCore; // persistent SRM core without COs Gia_Man_t * pCore; // persistent SRM core without COs
Cbs_Man_t * pCbs; // resident circuit-SAT manager on pCore Cbs_Man_t * pCbs; // resident circuit-SAT manager on pCore (-D direct solving)
Tas_Man_t * pTas; // resident TAS manager on pCore (-D direct solving)
int nCoreObjsAtReset; // real post-build pCore size after the last cold (re)build, for compaction (0 until that build finishes) int nCoreObjsAtReset; // real post-build pCore size after the last cold (re)build, for compaction (0 until that build finishes)
int fUseAdaptive; // use timing-guided cold rebuilds in addition to the hard bloat guard
int nCompactMult;
int fForceRebuild;
Vec_Int_t * vSpecLits; // cached core literals, indexed by frame/object Vec_Int_t * vSpecLits; // cached core literals, indexed by frame/object
Vec_Int_t * vOutLits; // core literals selected as current SAT outputs Vec_Int_t * vOutLits; // core literals selected as current SAT outputs
Vec_Int_t * vCopyTouched; // core ANDs copied into the current view Vec_Int_t * vCopyTouched; // core ANDs copied into the current view
@ -38,8 +49,6 @@ struct Cec_DynSrm_t_
Vec_Int_t * vRoMap; // host obj id -> RO index Vec_Int_t * vRoMap; // host obj id -> RO index
// Phase-2 measurement (behavior-preserving): per-key stamp used to count the // Phase-2 measurement (behavior-preserving): per-key stamp used to count the
// union of true-value (no repr substitution) cones of the active pairs. // union of true-value (no repr substitution) cones of the active pairs.
int * pTrueMark; // size = nFramesTotal * nObjs; 0 = unvisited
int nTrueStamp; // current visit stamp
int nObjs; int nObjs;
int nPis; int nPis;
int nRegs; int nRegs;
@ -47,8 +56,21 @@ struct Cec_DynSrm_t_
int nCoreCiNum; int nCoreCiNum;
int nBuilds; int nBuilds;
int nBuildsActive; int nBuildsActive;
int nBuildsFull;
int nCoreResets; int nCoreResets;
int nCoreCompactions; int nCoreCompactions;
int nIncrFallbackResets;
int nDynActiveResets;
int nAdaptiveResets;
int nAdaptiveBurstResets;
int nAdaptiveBurstLeft;
int nBuildsSinceReset;
int nLastBuildReset;
int nLastResetReason;
int nForceResetReason;
int nLastResetSpan;
int nAdaptResetSamples;
int nAdaptReuseSamples;
int nCoreBuilds; int nCoreBuilds;
int nViewBuilds; int nViewBuilds;
int nCacheFullClears; int nCacheFullClears;
@ -60,18 +82,66 @@ struct Cec_DynSrm_t_
int nCoreObjsMax; int nCoreObjsMax;
int nViewObjsLast; int nViewObjsLast;
int nViewObjsMax; int nViewObjsMax;
int nCoreDeltaLast;
int nCoreDeltaMax;
int nCoreBloatLastPermil;
int nCoreBloatMaxPermil;
ABC_INT64_T nOutLitsActiveSum;
ABC_INT64_T nOutLitsFullSum;
ABC_INT64_T nCoreObjsActiveSum;
ABC_INT64_T nCoreObjsFullSum;
ABC_INT64_T nSolveIters;
ABC_INT64_T nSolveCalls;
ABC_INT64_T nSolveReal;
ABC_INT64_T nSolveTriv;
ABC_INT64_T nSolveFail;
ABC_INT64_T nSolveFailIters;
ABC_INT64_T nFailCoreObjSum;
ABC_INT64_T nFailOutLitSum;
int nFailCoreObjMax;
int nFailOutLitMax;
double dAdaptResetCost;
double dAdaptReuseCost;
double dAdaptLastCost;
abctime tBuildLast;
abctime tBuildEnsureLast;
abctime tBuildInvalidateLast;
abctime tBuildEmitLast;
abctime tBuildTotal;
abctime tBuildResetTotal;
abctime tBuildReuseTotal;
abctime tBuildEnsureTotal;
abctime tBuildInvalidateTotal;
abctime tBuildEmitTotal;
abctime tViewLast;
abctime tViewTotal;
abctime tSolveLast;
ABC_INT64_T nBmcAdaptiveRounds;
ABC_INT64_T nBmcCbsRoots;
ABC_INT64_T nBmcCbsUnknown;
ABC_INT64_T nBmcTasProbeRoots;
ABC_INT64_T nBmcTasRetryRoots;
ABC_INT64_T nBmcTasResolved;
ABC_INT64_T nBmcTasUnknown;
ABC_INT64_T nBmcTasEnabledRounds;
ABC_INT64_T nBmcTasSkippedLarge;
ABC_INT64_T nBmcTasSkippedWork;
ABC_INT64_T nBmcTasSkippedBudget;
ABC_INT64_T nBmcTasStructWork;
abctime tBmcCbs;
abctime tBmcTas;
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// Active-pair selection mirrors incremental mode: a pair is active iff an endpoint is // Active-pair selection mirrors -i exactly: a pair is active iff an endpoint is
// in the alias-aware TFO (or, in ring mode, the ring edge itself changed). The // in the alias-aware TFO (or, in ring mode, the ring edge itself changed). The
// earlier "pending" set that force-re-emitted still-merged SAT pairs has been // earlier "pending" set that force-re-emitted still-merged SAT pairs has been
// removed: per md/scorr_i_correctness_bug_report.md the alias-aware TFO is the // removed: per md/scorr_i_correctness_bug_report.md the alias-aware TFO is the
// real fix, and the retry/pending protection was shown to be both unnecessary // real fix, and the retry/pending protection was shown to be both unnecessary
// and incomplete. // (alias-only passes -d) and incomplete. -d (incr-oracle) certifies soundness.
static int Cec_DynSrmActiveConst( Cec_DynSrm_t * p, int * pTfoMark, int ObjId ) static int Cec_DynSrmActiveConst( Cec_DynSrm_t * p, int * pTfoMark, int ObjId )
{ {
(void)p; (void)p;
@ -134,6 +204,9 @@ static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
if ( p->pCbs ) // stop resident solver before its pCore is freed if ( p->pCbs ) // stop resident solver before its pCore is freed
Cbs_ManStop( p->pCbs ); Cbs_ManStop( p->pCbs );
p->pCbs = NULL; p->pCbs = NULL;
if ( p->pTas )
Tas_ManStop( p->pTas );
p->pTas = NULL;
if ( p->pCore ) if ( p->pCore )
Gia_ManStop( p->pCore ); Gia_ManStop( p->pCore );
p->pCore = NULL; p->pCore = NULL;
@ -143,8 +216,6 @@ static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
Vec_IntFreeP( &p->vCopyTouched ); Vec_IntFreeP( &p->vCopyTouched );
Vec_IntFreeP( &p->vPiMap ); Vec_IntFreeP( &p->vPiMap );
Vec_IntFreeP( &p->vRoMap ); Vec_IntFreeP( &p->vRoMap );
ABC_FREE( p->pTrueMark );
p->nTrueStamp = 0;
p->nObjs = p->nPis = p->nRegs = p->nFramesTotal = p->nCoreCiNum = 0; p->nObjs = p->nPis = p->nRegs = p->nFramesTotal = p->nCoreCiNum = 0;
} }
@ -153,30 +224,104 @@ static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
// solver's per-round sync/solve walks an ever-larger graph. At a quiescent // solver's per-round sync/solve walks an ever-larger graph. At a quiescent
// point (start of a build) cold-rebuild once it exceeds a multiple of its // point (start of a build) cold-rebuild once it exceeds a multiple of its
// post-build size; the rebuilt core re-materializes only the live active cones. // post-build size; the rebuilt core re-materializes only the live active cones.
#define CEC_DYN_COMPACT_MULT 4 #define CEC_DYN_COMPACT_MULT 4
#define CEC_DYN_ADAPT_BLOAT_PERMIL 3000
#define CEC_DYN_ADAPT_WORSE_PERMIL 1500
#define CEC_DYN_ADAPT_RESET_BETTER_PERMIL 750
#define CEC_DYN_ADAPT_MIN_REUSE_SAMPLES 8
#define CEC_DYN_ADAPT_MIN_CALLS 16
#define CEC_DYN_ADAPT_MIN_BUILDS_SINCE_RESET 2
#define CEC_DYN_ADAPT_FAST_GROW_SPAN 4
#define CEC_DYN_ADAPT_BURST_ROUNDS 2
#define CEC_DYN_ADAPT_FAST_COMPACT_SPAN 2
enum {
CEC_DYN_RESET_NONE = 0,
CEC_DYN_RESET_SHAPE = 1,
CEC_DYN_RESET_COMPACT = 2,
CEC_DYN_RESET_ADAPT = 3,
CEC_DYN_RESET_BURST = 4,
CEC_DYN_RESET_IFALLBACK = 5,
CEC_DYN_RESET_DACTIVE = 6
};
static int Cec_DynSrmCurrentBloatPermil( Cec_DynSrm_t * p )
{
if ( p->nCoreObjsAtReset <= 0 || p->pCore == NULL )
return 1000;
return (int)((ABC_INT64_T)1000 * Gia_ManObjNum(p->pCore) / p->nCoreObjsAtReset);
}
static int Cec_DynSrmShouldCompact( Cec_DynSrm_t * p ) static int Cec_DynSrmShouldCompact( Cec_DynSrm_t * p )
{ {
// 64-bit multiply: nCoreObjsAtReset can reach tens of millions (the growth // 64-bit multiply: nCoreObjsAtReset can reach tens of millions (the growth
// case this guards), so CEC_DYN_COMPACT_MULT * it must not overflow int. // case this guards), so nCompactMult * it must not overflow int.
return p->nCoreObjsAtReset > 0 && return p->nCoreObjsAtReset > 0 &&
Gia_ManObjNum(p->pCore) > (ABC_INT64_T)CEC_DYN_COMPACT_MULT * p->nCoreObjsAtReset; Gia_ManObjNum(p->pCore) > (ABC_INT64_T)p->nCompactMult * p->nCoreObjsAtReset;
}
static int Cec_DynSrmShouldAdaptiveReset( Cec_DynSrm_t * p )
{
int nBloat;
if ( !p->fUseAdaptive )
return CEC_DYN_RESET_NONE;
if ( p->nAdaptiveBurstLeft > 0 )
{
p->nAdaptiveBurstLeft--;
p->nAdaptiveBurstResets++;
return CEC_DYN_RESET_BURST;
}
if ( p->nBuildsSinceReset < CEC_DYN_ADAPT_MIN_BUILDS_SINCE_RESET )
return CEC_DYN_RESET_NONE;
if ( p->nBuildsSinceReset > CEC_DYN_ADAPT_FAST_GROW_SPAN )
return CEC_DYN_RESET_NONE;
if ( p->nAdaptResetSamples == 0 || p->nAdaptReuseSamples < CEC_DYN_ADAPT_MIN_REUSE_SAMPLES )
return CEC_DYN_RESET_NONE;
nBloat = Cec_DynSrmCurrentBloatPermil( p );
if ( nBloat < CEC_DYN_ADAPT_BLOAT_PERMIL )
return CEC_DYN_RESET_NONE;
if ( 1000.0 * p->dAdaptReuseCost > (double)CEC_DYN_ADAPT_WORSE_PERMIL * p->dAdaptResetCost )
return CEC_DYN_RESET_ADAPT;
return CEC_DYN_RESET_NONE;
} }
static void Cec_DynSrmEnsureCore( Cec_DynSrm_t * p, int nFrames, int fScorr ) static void Cec_DynSrmEnsureCore( Cec_DynSrm_t * p, int nFrames, int fScorr )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int f, i, nFramesTotal = nFrames + fScorr; int f, i, nFramesTotal = nFrames + fScorr;
int ResetReason = CEC_DYN_RESET_NONE;
int fSameShape = ( p->pCore != NULL && int fSameShape = ( p->pCore != NULL &&
p->nObjs == Gia_ManObjNum(p->pAig) && p->nObjs == Gia_ManObjNum(p->pAig) &&
p->nPis == Gia_ManPiNum(p->pAig) && p->nPis == Gia_ManPiNum(p->pAig) &&
p->nRegs == Gia_ManRegNum(p->pAig) && p->nRegs == Gia_ManRegNum(p->pAig) &&
p->nFramesTotal == nFramesTotal ); p->nFramesTotal == nFramesTotal );
if ( fSameShape && !Cec_DynSrmShouldCompact(p) ) p->nLastBuildReset = 0;
p->nLastResetReason = CEC_DYN_RESET_NONE;
if ( !fSameShape )
ResetReason = CEC_DYN_RESET_SHAPE;
else if ( p->fForceRebuild )
ResetReason = p->nForceResetReason;
else if ( Cec_DynSrmShouldCompact(p) )
ResetReason = CEC_DYN_RESET_COMPACT;
else
ResetReason = Cec_DynSrmShouldAdaptiveReset( p );
if ( fSameShape && ResetReason == CEC_DYN_RESET_NONE )
return; return;
if ( fSameShape ) // reusable shape but bloated: cold-rebuild p->fForceRebuild = 0;
p->nForceResetReason = CEC_DYN_RESET_NONE;
if ( ResetReason == CEC_DYN_RESET_COMPACT ) // reusable shape but bloated: cold-rebuild
p->nCoreCompactions++; p->nCoreCompactions++;
if ( ResetReason == CEC_DYN_RESET_IFALLBACK )
p->nIncrFallbackResets++;
if ( ResetReason == CEC_DYN_RESET_DACTIVE )
p->nDynActiveResets++;
if ( ResetReason == CEC_DYN_RESET_ADAPT )
p->nAdaptiveResets++;
p->nLastResetSpan = p->nBuildsSinceReset;
Cec_DynSrmResetCore( p ); Cec_DynSrmResetCore( p );
p->nLastBuildReset = 1;
p->nLastResetReason = ResetReason;
p->nBuildsSinceReset = 0;
p->nObjs = Gia_ManObjNum( p->pAig ); p->nObjs = Gia_ManObjNum( p->pAig );
p->nPis = Gia_ManPiNum( p->pAig ); p->nPis = Gia_ManPiNum( p->pAig );
p->nRegs = Gia_ManRegNum( p->pAig ); p->nRegs = Gia_ManRegNum( p->pAig );
@ -186,8 +331,6 @@ static void Cec_DynSrmEnsureCore( Cec_DynSrm_t * p, int nFrames, int fScorr )
p->vCopyTouched = Vec_IntAlloc( 1000 ); p->vCopyTouched = Vec_IntAlloc( 1000 );
p->vPiMap = Vec_IntStartFull( p->nObjs ); p->vPiMap = Vec_IntStartFull( p->nObjs );
p->vRoMap = Vec_IntStartFull( p->nObjs ); p->vRoMap = Vec_IntStartFull( p->nObjs );
p->pTrueMark = ABC_CALLOC( int, p->nFramesTotal * p->nObjs );
p->nTrueStamp = 0;
p->pCore = Gia_ManStart( Abc_MaxInt( p->nFramesTotal * p->nObjs, 1000 ) ); p->pCore = Gia_ManStart( Abc_MaxInt( p->nFramesTotal * p->nObjs, 1000 ) );
p->pCore->pName = Abc_UtilStrsav( p->pAig->pName ); p->pCore->pName = Abc_UtilStrsav( p->pAig->pName );
p->pCore->pSpec = Abc_UtilStrsav( p->pAig->pSpec ); p->pCore->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
@ -411,14 +554,77 @@ static Gia_Man_t * Cec_DynSrmBuildView( Cec_DynSrm_t * p )
return pView; return pView;
} }
Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr ) static void Cec_DynSrmRecordBuildStats( Cec_DynSrm_t * p,
Cec_IncrEmitMode_t Mode, int nCoreObjsBefore, int nCoreResetsBefore,
abctime tBuild, abctime tEnsure, abctime tInvalidate, abctime tEmit )
{
int fReset = p->nCoreResets > nCoreResetsBefore;
p->nBuildsSinceReset++;
if ( Mode == CEC_EMIT_ACTIVE )
{
p->nOutLitsActiveSum += p->nOutLitsLast;
p->nCoreObjsActiveSum += p->nCoreObjsLast;
}
else if ( Mode == CEC_EMIT_ALL )
{
p->nBuildsFull++;
p->nOutLitsFullSum += p->nOutLitsLast;
p->nCoreObjsFullSum += p->nCoreObjsLast;
}
p->nCoreDeltaLast = Abc_MaxInt( 0, p->nCoreObjsLast - nCoreObjsBefore );
p->nCoreDeltaMax = Abc_MaxInt( p->nCoreDeltaMax, p->nCoreDeltaLast );
if ( p->nCoreObjsAtReset > 0 )
{
p->nCoreBloatLastPermil =
(int)((ABC_INT64_T)1000 * p->nCoreObjsLast / p->nCoreObjsAtReset);
p->nCoreBloatMaxPermil =
Abc_MaxInt( p->nCoreBloatMaxPermil, p->nCoreBloatLastPermil );
}
if ( tBuild )
{
p->tBuildLast = tBuild;
p->tBuildEnsureLast = tEnsure;
p->tBuildInvalidateLast = tInvalidate;
p->tBuildEmitLast = tEmit;
p->tBuildTotal += tBuild;
if ( fReset )
p->tBuildResetTotal += tBuild;
else
p->tBuildReuseTotal += tBuild;
p->tBuildEnsureTotal += tEnsure;
p->tBuildInvalidateTotal += tInvalidate;
p->tBuildEmitTotal += tEmit;
}
}
Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr, int fUseAdaptive )
{ {
Cec_DynSrm_t * p = ABC_CALLOC( Cec_DynSrm_t, 1 ); Cec_DynSrm_t * p = ABC_CALLOC( Cec_DynSrm_t, 1 );
p->pAig = pAig; p->pAig = pAig;
p->pIncr = pIncr; p->pIncr = pIncr;
p->fUseAdaptive = fUseAdaptive;
p->nCompactMult = CEC_DYN_COMPACT_MULT;
return p; return p;
} }
void Cec_DynSrmSetParams( Cec_DynSrm_t * p, Cec_ParCor_t * pPars )
{
if ( p == NULL || pPars == NULL )
return;
p->nCompactMult = Abc_MaxInt( 1, pPars->nDynSrmCompactMult );
}
void Cec_DynSrmForceRebuild( Cec_DynSrm_t * p, int fIncrFallback )
{
if ( p == NULL )
return;
p->fForceRebuild = 1;
if ( fIncrFallback )
p->nForceResetReason = CEC_DYN_RESET_IFALLBACK;
else if ( p->nForceResetReason != CEC_DYN_RESET_IFALLBACK )
p->nForceResetReason = CEC_DYN_RESET_DACTIVE;
}
void Cec_DynSrmFree( Cec_DynSrm_t * p ) void Cec_DynSrmFree( Cec_DynSrm_t * p )
{ {
if ( p == NULL ) if ( p == NULL )
@ -427,19 +633,57 @@ void Cec_DynSrmFree( Cec_DynSrm_t * p )
ABC_FREE( p ); ABC_FREE( p );
} }
void Cec_DynSrmPrintStats( Cec_DynSrm_t * p ) static void Cec_DynSrmUpdateAdaptCost( double * pCost, int * pSamples, double Value )
{ {
if ( *pSamples == 0 )
*pCost = Value;
else
*pCost = 0.75 * *pCost + 0.25 * Value;
(*pSamples)++;
}
void Cec_DynSrmRecordSolveStats( Cec_DynSrm_t * p,
int nCalls, int nReal, int nTriv, int nFail, abctime tSat )
{
int nDen;
double dCost;
if ( p == NULL ) if ( p == NULL )
return; return;
Abc_Print( 1, "DynSRM: builds = %d, active_builds = %d\n", p->nSolveIters++;
p->nBuilds, p->nBuildsActive ); p->nSolveCalls += nCalls;
Abc_Print( 1, "DynSRM: core_resets = %d, compactions = %d, core_builds = %d, view_builds = %d, out_lits_last/max = %d/%d, core_objs_last/max = %d/%d, view_objs_last/max = %d/%d\n", p->nSolveReal += nReal;
p->nCoreResets, p->nCoreCompactions, p->nCoreBuilds, p->nViewBuilds, p->nSolveTriv += nTriv;
p->nOutLitsLast, p->nOutLitsMax, p->nSolveFail += nFail;
p->nCoreObjsLast, p->nCoreObjsMax, if ( nFail > 0 )
p->nViewObjsLast, p->nViewObjsMax ); {
Abc_Print( 1, "DynSRM: cache_full_clears = %d, cache_local_clears = %d, cache_local_entries = %d\n", p->nSolveFailIters++;
p->nCacheFullClears, p->nCacheLocalClears, p->nCacheLocalEntries ); p->nFailCoreObjSum += (ABC_INT64_T)nFail * p->nCoreObjsLast;
p->nFailOutLitSum += (ABC_INT64_T)nFail * p->nOutLitsLast;
p->nFailCoreObjMax = Abc_MaxInt( p->nFailCoreObjMax, p->nCoreObjsLast );
p->nFailOutLitMax = Abc_MaxInt( p->nFailOutLitMax, p->nOutLitsLast );
}
p->tSolveLast = tSat;
if ( !p->fUseAdaptive || p->tBuildLast == 0 )
return;
nDen = nCalls > 0 ? nCalls : p->nOutLitsLast;
if ( nDen < CEC_DYN_ADAPT_MIN_CALLS )
return;
dCost = (double)(p->tBuildLast + tSat) / (double)nDen;
p->dAdaptLastCost = dCost;
if ( p->nLastBuildReset )
{
if ( p->nLastResetReason != CEC_DYN_RESET_SHAPE )
{
Cec_DynSrmUpdateAdaptCost( &p->dAdaptResetCost, &p->nAdaptResetSamples, dCost );
if ( p->nAdaptReuseSamples >= CEC_DYN_ADAPT_MIN_REUSE_SAMPLES &&
p->nLastResetReason == CEC_DYN_RESET_COMPACT &&
p->nLastResetSpan <= CEC_DYN_ADAPT_FAST_COMPACT_SPAN &&
1000.0 * dCost < (double)CEC_DYN_ADAPT_RESET_BETTER_PERMIL * p->dAdaptReuseCost )
p->nAdaptiveBurstLeft = CEC_DYN_ADAPT_BURST_ROUNDS;
}
}
else
Cec_DynSrmUpdateAdaptCost( &p->dAdaptReuseCost, &p->nAdaptReuseSamples, dCost );
} }
void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark, void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark,
@ -493,12 +737,16 @@ void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark,
// Builds (or extends) the persistent COless pCore and selects this round's // Builds (or extends) the persistent COless pCore and selects this round's
// active-pair root literals into p->vOutLits / *pvOutputs. Shared by the view // active-pair root literals into p->vOutLits / *pvOutputs. Shared by the view
// path (Cec_DynSrmBuild) and the persistent path (solve pCore directly). // path (Cec_DynSrmBuild) and the -D persistence path (solve pCore directly).
void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr, void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode ) Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode )
{ {
Gia_Obj_t * pObj, * pRepr; Gia_Obj_t * pObj, * pRepr;
int i, iPrev, iObj, iPrevNew, iObjNew, iPrevRaw, iObjRaw; int i, iPrev, iObj, iPrevNew, iObjNew, iPrevRaw, iObjRaw;
int nCoreResetsBefore, nCoreObjsBefore;
int fMeasure = p->fUseAdaptive;
abctime tBuild = fMeasure ? Abc_ClockHr() : 0;
abctime tStep, tEnsure = 0, tInvalidate = 0, tEmit = 0;
assert( p != NULL ); assert( p != NULL );
assert( nFrames > 0 ); assert( nFrames > 0 );
assert( Gia_ManRegNum(p->pAig) > 0 ); assert( Gia_ManRegNum(p->pAig) > 0 );
@ -507,8 +755,15 @@ void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
p->nBuilds++; p->nBuilds++;
if ( Mode == CEC_EMIT_ACTIVE ) if ( Mode == CEC_EMIT_ACTIVE )
p->nBuildsActive++; p->nBuildsActive++;
nCoreResetsBefore = p->nCoreResets;
tStep = fMeasure ? Abc_ClockHr() : 0;
Cec_DynSrmEnsureCore( p, nFrames, fScorr ); Cec_DynSrmEnsureCore( p, nFrames, fScorr );
if ( fMeasure ) tEnsure = Abc_ClockHr() - tStep;
nCoreObjsBefore = Gia_ManObjNum( p->pCore );
tStep = fMeasure ? Abc_ClockHr() : 0;
Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask ); Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask );
if ( fMeasure ) tInvalidate = Abc_ClockHr() - tStep;
tStep = fMeasure ? Abc_ClockHr() : 0;
Gia_ManSetPhase( p->pAig ); Gia_ManSetPhase( p->pAig );
*pvOutputs = Vec_IntAlloc( 1000 ); *pvOutputs = Vec_IntAlloc( 1000 );
Vec_IntClear( p->vOutLits ); Vec_IntClear( p->vOutLits );
@ -603,6 +858,10 @@ void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
if ( p->nCoreObjsAtReset == 0 ) // first build after a cold (re)set: record the if ( p->nCoreObjsAtReset == 0 ) // first build after a cold (re)set: record the
p->nCoreObjsAtReset = p->nCoreObjsLast; // real post-build size as the compaction baseline p->nCoreObjsAtReset = p->nCoreObjsLast; // real post-build size as the compaction baseline
p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast ); p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast );
if ( fMeasure ) tEmit = Abc_ClockHr() - tStep;
if ( fMeasure ) tBuild = Abc_ClockHr() - tBuild;
Cec_DynSrmRecordBuildStats( p, Mode, nCoreObjsBefore, nCoreResetsBefore,
tBuild, tEnsure, tInvalidate, tEmit );
} }
Gia_Man_t * Cec_DynSrmBuild( Cec_DynSrm_t * p, int nFrames, int fScorr, Gia_Man_t * Cec_DynSrmBuild( Cec_DynSrm_t * p, int nFrames, int fScorr,
@ -621,6 +880,10 @@ void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fS
{ {
Gia_Obj_t * pObj, * pRepr; Gia_Obj_t * pObj, * pRepr;
int f, i, iPrevNew, iObjNew; int f, i, iPrevNew, iObjNew;
int nCoreResetsBefore, nCoreObjsBefore;
int fMeasure = p->fUseAdaptive;
abctime tBuild = fMeasure ? Abc_ClockHr() : 0;
abctime tStep, tEnsure = 0, tInvalidate = 0, tEmit = 0;
assert( p != NULL ); assert( p != NULL );
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p->pAig) > 0 ); assert( Gia_ManRegNum(p->pAig) > 0 );
@ -629,8 +892,15 @@ void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fS
p->nBuilds++; p->nBuilds++;
if ( Mode == CEC_EMIT_ACTIVE ) if ( Mode == CEC_EMIT_ACTIVE )
p->nBuildsActive++; p->nBuildsActive++;
nCoreResetsBefore = p->nCoreResets;
tStep = fMeasure ? Abc_ClockHr() : 0;
Cec_DynSrmEnsureCore( p, nFrames + nPrefix, fScorr ); Cec_DynSrmEnsureCore( p, nFrames + nPrefix, fScorr );
if ( fMeasure ) tEnsure = Abc_ClockHr() - tStep;
nCoreObjsBefore = Gia_ManObjNum( p->pCore );
tStep = fMeasure ? Abc_ClockHr() : 0;
Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask ); Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask );
if ( fMeasure ) tInvalidate = Abc_ClockHr() - tStep;
tStep = fMeasure ? Abc_ClockHr() : 0;
Gia_ManSetPhase( p->pAig ); Gia_ManSetPhase( p->pAig );
*pvOutputs = Vec_IntAlloc( 1000 ); *pvOutputs = Vec_IntAlloc( 1000 );
Vec_IntClear( p->vOutLits ); Vec_IntClear( p->vOutLits );
@ -665,6 +935,13 @@ void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fS
if ( p->nCoreObjsAtReset == 0 ) if ( p->nCoreObjsAtReset == 0 )
p->nCoreObjsAtReset = p->nCoreObjsLast; p->nCoreObjsAtReset = p->nCoreObjsLast;
p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast ); p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast );
if ( fMeasure )
{
tEmit = Abc_ClockHr() - tStep;
tBuild = Abc_ClockHr() - tBuild;
}
Cec_DynSrmRecordBuildStats( p, Mode, nCoreObjsBefore, nCoreResetsBefore,
tBuild, tEnsure, tInvalidate, tEmit );
} }
Gia_Man_t * Cec_DynSrmBuildInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Gia_Man_t * Cec_DynSrmBuildInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr,
@ -681,16 +958,254 @@ Vec_Int_t * Cec_DynSrmOutLits( Cec_DynSrm_t * p ) { return p->vOutLits; }
// circuit-SAT manager (allocated lazily; re-created after a core reset/compaction // circuit-SAT manager (allocated lazily; re-created after a core reset/compaction
// since its pAig is freed there). The CI-layout assert guards the CEX CioId -> // since its pAig is freed there). The CI-layout assert guards the CEX CioId ->
// resim-input contract that the discarded view used to enforce in the main loop. // resim-input contract that the discarded view used to enforce in the main loop.
Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus ) Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus, int fUseTas )
{ {
assert( Gia_ManRegNum(p->pCore) == 0 ); assert( Gia_ManRegNum(p->pCore) == 0 );
assert( Gia_ManCiNum(p->pCore) == p->nRegs + p->nFramesTotal * p->nPis ); assert( Gia_ManCiNum(p->pCore) == p->nRegs + p->nFramesTotal * p->nPis );
if ( fUseTas )
{
if ( p->pTas == NULL )
p->pTas = Tas_ManAlloc( p->pCore, nConfs );
Tas_ManSetConflictNum( p->pTas, nConfs );
return Tas_ManSolveRoots( p->pTas, p->vOutLits, pvStatus, 0 );
}
if ( p->pCbs == NULL ) if ( p->pCbs == NULL )
p->pCbs = Cbs_ManAlloc( p->pCore ); p->pCbs = Cbs_ManAlloc( p->pCore );
Cbs_ManSetConflictNum( p->pCbs, nConfs ); Cbs_ManSetConflictNum( p->pCbs, nConfs );
return Cbs_ManSolveRoots( p->pCbs, p->vOutLits, pvStatus, 0 ); return Cbs_ManSolveRoots( p->pCbs, p->vOutLits, pvStatus, 0 );
} }
static void Cec_DynSrmStoreCopyEntry( Vec_Int_t * vDest, Vec_Int_t * vSrc, int iStart, int iOut )
{
int k, nLits = Vec_IntEntry( vSrc, iStart + 1 );
Vec_IntPush( vDest, iOut );
Vec_IntPush( vDest, nLits );
for ( k = 0; k < nLits; k++ )
Vec_IntPush( vDest, Vec_IntEntry(vSrc, iStart + 2 + k) );
}
static Vec_Int_t * Cec_DynSrmStoreIndex( Vec_Int_t * vStore, int nRoots )
{
Vec_Int_t * vStarts = Vec_IntStartFull( nRoots );
int iStart = 0, iOut, nLits;
while ( iStart < Vec_IntSize(vStore) )
{
iOut = Vec_IntEntry( vStore, iStart );
nLits = Vec_IntEntry( vStore, iStart + 1 );
assert( iOut >= 0 && iOut < nRoots );
assert( nLits >= -1 );
Vec_IntWriteEntry( vStarts, iOut, iStart );
iStart += 2 + Abc_MaxInt( nLits, 0 );
}
assert( iStart == Vec_IntSize(vStore) );
return vStarts;
}
// Runs TAS on a subset of roots and merges its local output indices into the
// original CBS status/store namespace. Returns the number of SAT/UNSAT roots.
static int Cec_DynSrmTasRetryBatch( Cec_DynSrm_t * p, int nConfs,
Vec_Int_t * vRoots, Vec_Int_t * vRootToOrig, Vec_Str_t * vFinalStatus,
Vec_Int_t * vTasStore, Vec_Int_t * vTasStarts )
{
Vec_Str_t * vStatus = NULL;
Vec_Int_t * vStore;
abctime clk = Abc_ClockHr();
int i, iStart = 0, iLocal, iOrig, nLits, Status, nResolved = 0;
assert( Vec_IntSize(vRoots) == Vec_IntSize(vRootToOrig) );
if ( p->pTas == NULL )
p->pTas = Tas_ManAlloc( p->pCore, nConfs );
Tas_ManSetConflictNum( p->pTas, nConfs );
vStore = Tas_ManSolveRoots( p->pTas, vRoots, &vStatus, 0 );
p->tBmcTas += Abc_ClockHr() - clk;
Vec_StrForEachEntry( vStatus, Status, i )
{
iOrig = Vec_IntEntry( vRootToOrig, i );
if ( Status != -1 )
{
Vec_StrWriteEntry( vFinalStatus, iOrig, (char)Status );
nResolved++;
}
}
while ( iStart < Vec_IntSize(vStore) )
{
iLocal = Vec_IntEntry( vStore, iStart );
nLits = Vec_IntEntry( vStore, iStart + 1 );
assert( iLocal >= 0 && iLocal < Vec_IntSize(vRootToOrig) );
iOrig = Vec_IntEntry( vRootToOrig, iLocal );
Vec_IntWriteEntry( vTasStarts, iOrig, Vec_IntSize(vTasStore) );
Cec_DynSrmStoreCopyEntry( vTasStore, vStore, iStart, iOrig );
iStart += 2 + Abc_MaxInt( nLits, 0 );
}
assert( iStart == Vec_IntSize(vStore) );
Vec_IntFree( vStore );
Vec_StrFree( vStatus );
return nResolved;
}
/**Function*************************************************************
Synopsis [CBS-first BMC solving with guarded TAS rescue.]
Description [Forced -T remains TAS-only. The default path solves every
root with CBS, then considers only CBS UNKNOWN roots. Large cores are
rejected using both absolute and frame-normalized size. Otherwise TAS is
sampled on eight roots; only a 75% successful probe enables retrying the
remainder. A deterministic node-root work budget and a retry-root cap bound
TAS use without consulting machine-dependent wall time. The final status/CEX
arrays preserve original root indices.]
***********************************************************************/
Vec_Int_t * Cec_DynSrmSolveBmcAdaptive( Cec_DynSrm_t * p, int nConfs,
Vec_Str_t ** pvStatus, int fUseTas )
{
Vec_Str_t * vStatus = NULL;
Vec_Int_t * vCbsStore, * vCbsStarts, * vUnknown;
Vec_Int_t * vProbeRoots, * vProbeMap, * vRetryRoots, * vRetryMap;
Vec_Int_t * vTasStore, * vTasStarts, * vFinalStore;
abctime clk;
int i, Status, nRoots = Vec_IntSize(p->vOutLits), nProbe, nProbeResolved;
int nFrames = Abc_MaxInt( 1, p->nFramesTotal );
int nCore = Gia_ManObjNum( p->pCore );
int nCoreNorm = (nCore + nFrames - 1) / nFrames;
int fCoreEligible;
if ( fUseTas )
return Cec_DynSrmSolve( p, nConfs, pvStatus, 1 );
p->nBmcAdaptiveRounds++;
p->nBmcCbsRoots += nRoots;
clk = Abc_ClockHr();
vCbsStore = Cec_DynSrmSolve( p, nConfs, &vStatus, 0 );
p->tBmcCbs += Abc_ClockHr() - clk;
vUnknown = Vec_IntAlloc( 64 );
Vec_StrForEachEntry( vStatus, Status, i )
if ( Status == -1 )
Vec_IntPush( vUnknown, i );
p->nBmcCbsUnknown += Vec_IntSize(vUnknown);
if ( Vec_IntSize(vUnknown) == 0 )
{
Vec_IntFree( vUnknown );
*pvStatus = vStatus;
return vCbsStore;
}
fCoreEligible = nCore <= CEC_BMC_TAS_CORE_ABS_MAX &&
nCoreNorm <= CEC_BMC_TAS_CORE_NORM_MAX;
if ( !fCoreEligible )
{
p->nBmcTasSkippedLarge += Vec_IntSize(vUnknown);
Vec_IntFree( vUnknown );
*pvStatus = vStatus;
return vCbsStore;
}
vCbsStarts = Cec_DynSrmStoreIndex( vCbsStore, nRoots );
vTasStore = Vec_IntAlloc( 64 );
vTasStarts = Vec_IntStartFull( nRoots );
nProbe = Abc_MinInt( CEC_BMC_TAS_PROBE_ROOTS, Vec_IntSize(vUnknown) );
if ( p->nBmcTasStructWork + (ABC_INT64_T)nCoreNorm * nProbe >
CEC_BMC_TAS_STRUCT_WORK_MAX )
{
p->nBmcTasSkippedWork += Vec_IntSize(vUnknown);
Vec_IntFree( vCbsStarts );
Vec_IntFree( vTasStore );
Vec_IntFree( vTasStarts );
Vec_IntFree( vUnknown );
*pvStatus = vStatus;
return vCbsStore;
}
vProbeRoots = Vec_IntAlloc( nProbe );
vProbeMap = Vec_IntAlloc( nProbe );
for ( i = 0; i < nProbe; i++ )
{
int iOrig = Vec_IntEntry( vUnknown, i );
Vec_IntPush( vProbeRoots, Vec_IntEntry(p->vOutLits, iOrig) );
Vec_IntPush( vProbeMap, iOrig );
}
p->nBmcTasProbeRoots += nProbe;
nProbeResolved = Cec_DynSrmTasRetryBatch( p, nConfs, vProbeRoots, vProbeMap,
vStatus, vTasStore, vTasStarts );
p->nBmcTasStructWork += (ABC_INT64_T)nCoreNorm * nProbe;
p->nBmcTasResolved += nProbeResolved;
p->nBmcTasUnknown += nProbe - nProbeResolved;
Vec_IntFree( vProbeRoots );
Vec_IntFree( vProbeMap );
if ( nProbeResolved * 100 >= CEC_BMC_TAS_PROBE_SUCCESS_PCT * nProbe &&
Vec_IntSize(vUnknown) > nProbe )
{
int nRetryAvail = Vec_IntSize(vUnknown) - nProbe;
int nRetryBudget = CEC_BMC_TAS_RETRY_ROOTS_MAX - (int)p->nBmcTasRetryRoots;
ABC_INT64_T nWorkLeft = CEC_BMC_TAS_STRUCT_WORK_MAX - p->nBmcTasStructWork;
int nRetryWork = nWorkLeft > 0 ? (int)(nWorkLeft / nCoreNorm) : 0;
int nRetry = Abc_MinInt( nRetryAvail,
Abc_MinInt( Abc_MaxInt(0, nRetryBudget), Abc_MaxInt(0, nRetryWork) ) );
if ( nRetryBudget <= 0 )
p->nBmcTasSkippedBudget += nRetryAvail;
else if ( nRetryWork <= 0 )
p->nBmcTasSkippedWork += nRetryAvail;
else
{
vRetryRoots = Vec_IntAlloc( nRetry );
vRetryMap = Vec_IntAlloc( nRetry );
for ( i = nProbe; i < nProbe + nRetry; i++ )
{
int iOrig = Vec_IntEntry( vUnknown, i );
Vec_IntPush( vRetryRoots, Vec_IntEntry(p->vOutLits, iOrig) );
Vec_IntPush( vRetryMap, iOrig );
}
p->nBmcTasEnabledRounds++;
p->nBmcTasRetryRoots += Vec_IntSize(vRetryRoots);
i = Cec_DynSrmTasRetryBatch( p, nConfs, vRetryRoots, vRetryMap,
vStatus, vTasStore, vTasStarts );
p->nBmcTasResolved += i;
p->nBmcTasUnknown += Vec_IntSize(vRetryRoots) - i;
p->nBmcTasStructWork += (ABC_INT64_T)nCoreNorm * nRetry;
if ( nRetry < nRetryAvail )
{
if ( nRetry == nRetryBudget )
p->nBmcTasSkippedBudget += nRetryAvail - nRetry;
else
p->nBmcTasSkippedWork += nRetryAvail - nRetry;
}
Vec_IntFree( vRetryRoots );
Vec_IntFree( vRetryMap );
}
}
// Rebuild the CEX store once so a TAS answer cleanly replaces the CBS
// UNKNOWN entry instead of leaving both records for Gia_ManCheckRefinements.
vFinalStore = Vec_IntAlloc( Vec_IntSize(vCbsStore) + Vec_IntSize(vTasStore) );
Vec_StrForEachEntry( vStatus, Status, i )
{
int iStart;
if ( Status == 1 )
continue;
if ( Status == -1 )
{
Vec_IntPush( vFinalStore, i );
Vec_IntPush( vFinalStore, -1 );
continue;
}
iStart = Vec_IntEntry( vCbsStarts, i );
if ( iStart >= 0 && Vec_StrEntry(vStatus, i) == 0 &&
Vec_IntEntry(vCbsStore, iStart + 1) >= 0 )
Cec_DynSrmStoreCopyEntry( vFinalStore, vCbsStore, iStart, i );
else
{
iStart = Vec_IntEntry( vTasStarts, i );
assert( iStart >= 0 );
Cec_DynSrmStoreCopyEntry( vFinalStore, vTasStore, iStart, i );
}
}
Vec_IntFree( vCbsStore );
Vec_IntFree( vCbsStarts );
Vec_IntFree( vTasStore );
Vec_IntFree( vTasStarts );
Vec_IntFree( vUnknown );
*pvStatus = vStatus;
return vFinalStore;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

22
src/proof/cec/cecCorrIncr.c
View File

@ -6,11 +6,11 @@
PackageName [Combinational equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Incremental active-list / TFO filter for &scorr.] Synopsis [Incremental active-list / TFO filter for &scorr2.]
Author [Xiran Zhao] Author [Xiran Zhao]
Affiliation [University of Chinese Academy of Sciences] Affiliation [University of Chinese Academy of Sciences (UCAS)]
Date [Ver. 1.0. Started - May 2026.] Date [Ver. 1.0. Started - May 2026.]
@ -477,7 +477,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
(Mode == CEC_EMIT_SKIPPED && !fActive); (Mode == CEC_EMIT_SKIPPED && !fActive);
if ( !fEmit ) if ( !fEmit )
continue; continue;
iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjRaw = Gia_ManCorr2SpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ); iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 ) if ( iObjNew != 0 )
{ {
@ -507,8 +507,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
(Mode == CEC_EMIT_SKIPPED && !fActive); (Mode == CEC_EMIT_SKIPPED && !fActive);
if ( fEmit ) if ( fEmit )
{ {
iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); iPrevRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iObjRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
@ -536,8 +536,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
(Mode == CEC_EMIT_SKIPPED && !fActive); (Mode == CEC_EMIT_SKIPPED && !fActive);
if ( fEmit ) if ( fEmit )
{ {
iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); iPrevRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iObjRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
@ -572,8 +572,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
if ( !fEmit ) if ( !fEmit )
continue; continue;
} }
iPrevRaw = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); iPrevRaw = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorr2SpecReal( pNew, p, pRepr, nFrames, 0 );
iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjRaw = Gia_ManCorr2SpecReal( pNew, p, pObj, nFrames, 0 );
iPrevNew = iPrevRaw; iPrevNew = iPrevRaw;
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew ) if ( iPrevNew != iObjNew )
@ -662,8 +662,8 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nP
if ( !pTfoMark[i] && !pTfoMark[idR] ) if ( !pTfoMark[i] && !pTfoMark[idR] )
continue; continue;
} }
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix ); iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorr2SpecReal( pNew, p, pRepr, f, nPrefix );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); iObjNew = Gia_ManCorr2SpecReal( pNew, p, pObj, f, nPrefix );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew ) if ( iPrevNew != iObjNew )
{ {

168
src/proof/cec/cecCorrIncrSim.c
View File

@ -6,7 +6,7 @@
PackageName [Combinational equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Persistent event-driven incremental simulation for &scorr.] Synopsis [Persistent event-driven incremental simulation for &scorr2.]
Description [Keeps packed CI patterns and host-AIG values across CEX batches. Description [Keeps packed CI patterns and host-AIG values across CEX batches.
Only changed CI words are propagated through the frame-aware fanout graph. Only changed CI words are propagated through the frame-aware fanout graph.
@ -15,7 +15,7 @@
Author [Xiran Zhao] Author [Xiran Zhao]
Affiliation [University of Chinese Academy of Sciences] Affiliation [University of Chinese Academy of Sciences (UCAS)]
Date [Ver. 1.0. Started - Jun 2026.] Date [Ver. 1.0. Started - Jun 2026.]
@ -389,6 +389,8 @@ void Cec_SeedSimFree( Cec_SeedSim_t * p )
ABC_FREE( p->pEventWords ); ABC_FREE( p->pEventWords );
ABC_FREE( p->pCone ); ABC_FREE( p->pCone );
ABC_FREE( p->pConeClose ); ABC_FREE( p->pConeClose );
ABC_FREE( p->pReprPre );
ABC_FREE( p->pNextPre );
ABC_FREE( p->pRootMark ); ABC_FREE( p->pRootMark );
ABC_FREE( p->pTxnMark ); ABC_FREE( p->pTxnMark );
ABC_FREE( p->pPackPres ); ABC_FREE( p->pPackPres );
@ -1327,6 +1329,149 @@ static void Cec_SeedSimBuildPersistentValues( Cec_SeedSim_t * p )
} }
} }
// (-V) Oracle for incremental-resim correctness. The maintained pVal must equal
// the true value of every IN-CONE key under the current persistent inputs. We
// snapshot the under-test values, recompute the trusted values by a full sweep
// from vSimInfo (no class side effects), compare on cone keys, then restore the
// under-test values so the run trajectory is unchanged (purely observational).
// Out-of-cone keys are intentionally stale and are not checked.
int Cec_SeedSimVerifyValues( Cec_SeedSim_t * p )
{
size_t nKeys, nVals;
unsigned * pTest;
int Key, w, nBad = 0;
if ( p->pVal == NULL )
return 0;
nKeys = (size_t)p->nFrames * p->nObjs;
nVals = nKeys * (size_t)p->nWords;
pTest = ABC_ALLOC( unsigned, nVals );
memcpy( pTest, p->pVal, sizeof(unsigned) * nVals ); // maintained (under test)
Cec_SeedSimBuildPersistentValues( p ); // p->pVal := true values
for ( Key = 0; Key < (int)nKeys; Key++ )
{
if ( p->fUseCone && !Abc_InfoHasBit(p->pCone, Key) )
continue;
for ( w = 0; w < p->nWords; w++ )
{
size_t Flat = (size_t)Key * p->nWords + w;
if ( pTest[Flat] != p->pVal[Flat] )
{
if ( nBad < 20 )
Abc_Print( 1, " [resim-oracle] STALE key f=%d obj=%d w=%d "
"maintained=%08x true=%08x\n",
Key / p->nObjs, Key % p->nObjs, w,
pTest[Flat], p->pVal[Flat] );
nBad++;
break;
}
}
}
if ( nBad )
Abc_Print( 1, " [resim-oracle] %d in-cone keys STALE "
"(maintained != true under persistent inputs)\n", nBad );
memcpy( p->pVal, pTest, sizeof(unsigned) * nVals ); // restore: stay observational
ABC_FREE( pTest );
return nBad;
}
// (-V) Capture the class partition (pReprs/pNexts) before a batch is resimulated.
// Cec_SeedSimVerifyRefine() replays the trusted full resim from this snapshot.
void Cec_SeedSimVerifySnapshot( Cec_SeedSim_t * p )
{
int nObjs = p->nObjs;
if ( p->pAig->pReprs == NULL || p->pAig->pNexts == NULL )
return;
if ( p->pReprPre == NULL )
{
p->pReprPre = ABC_ALLOC( int, nObjs );
p->pNextPre = ABC_ALLOC( int, nObjs );
}
memcpy( p->pReprPre, p->pAig->pReprs, sizeof(int) * nObjs );
memcpy( p->pNextPre, p->pAig->pNexts, sizeof(int) * nObjs );
}
static inline int Cec_SeedSimSavedRoot( int * pReprs, int ObjId )
{
return pReprs[ObjId] == GIA_VOID ? ObjId : pReprs[ObjId];
}
// (-V) Oracle for class refinement (not just the value cache). The incremental
// resim has just committed its splits for this batch (P_incr). We re-run the
// TRUSTED full resim on the SAME packed CEX inputs starting from the pre-batch
// partition (P0), giving the reference partition P_full.
//
// Both directions matter:
// * P_incr merged, P_full split: missed split, a correctness risk.
// * P_incr split, P_full merged: extra split, a QoR regression.
//
// The check reuses the production refinement code (correct phase/const handling),
// then restores P_incr so the run stays observational. Returns #mismatches.
int Cec_SeedSimVerifyRefine( Cec_SeedSim_t * p, Cec_ManSim_t * pSim,
Vec_Ptr_t * vSimInfo, int nFrames )
{
Gia_Man_t * pAig = p->pAig;
int nObjs = p->nObjs;
int * pReprIncr, * pNextIncr;
int i, nMissed = 0, nExtra = 0;
if ( pAig->pReprs == NULL || p->pReprPre == NULL )
return 0;
pReprIncr = ABC_ALLOC( int, nObjs );
pNextIncr = ABC_ALLOC( int, nObjs );
memcpy( pReprIncr, pAig->pReprs, sizeof(int) * nObjs ); // P_incr (committed)
memcpy( pNextIncr, pAig->pNexts, sizeof(int) * nObjs );
// restore the pre-batch partition and run the trusted full resim
memcpy( pAig->pReprs, p->pReprPre, sizeof(int) * nObjs );
memcpy( pAig->pNexts, p->pNextPre, sizeof(int) * nObjs );
Gia_ManCreateValueRefs( pAig );
pSim->pPars->nFrames = nFrames;
Cec_ManSeqResimulate( pSim, vSimInfo ); // pAig now holds P_full
// a pair merged in P_incr but split in P_full is a missed (unsound) split
for ( i = 1; i < nObjs; i++ )
{
int rIncr = pReprIncr[i], ci, cr;
if ( rIncr == GIA_VOID )
continue; // i was a head/none in P_incr
ci = Gia_ObjRepr(pAig, i) == GIA_VOID ? i : Gia_ObjRepr(pAig, i);
cr = Gia_ObjRepr(pAig, rIncr) == GIA_VOID ? rIncr : Gia_ObjRepr(pAig, rIncr);
if ( ci != cr )
{
if ( nMissed < 20 )
Abc_Print( 1, " [resim-oracle] MISSED SPLIT obj=%d repr=%d "
"(merged by incremental, split by full resim)\n", i, rIncr );
nMissed++;
}
}
// a pair split in P_incr but merged in P_full is an extra split (QoR loss)
for ( i = 1; i < nObjs; i++ )
{
int rFull = Gia_ObjRepr(pAig, i), ci, cr;
if ( rFull == GIA_VOID )
continue; // i was a head/none in P_full
ci = Cec_SeedSimSavedRoot( pReprIncr, i );
cr = Cec_SeedSimSavedRoot( pReprIncr, rFull );
if ( ci != cr )
{
if ( nExtra < 20 )
Abc_Print( 1, " [resim-oracle] EXTRA SPLIT obj=%d repr=%d "
"(split by incremental roots %d/%d, merged by full resim)\n",
i, rFull, ci, cr );
nExtra++;
}
}
// restore the committed (incremental) partition: stay observational
memcpy( pAig->pReprs, pReprIncr, sizeof(int) * nObjs );
memcpy( pAig->pNexts, pNextIncr, sizeof(int) * nObjs );
ABC_FREE( pReprIncr );
ABC_FREE( pNextIncr );
if ( nMissed )
Abc_Print( 1, " [resim-oracle] %d MISSED SPLITS this batch "
"(incremental coarser than full resim)\n", nMissed );
if ( nExtra )
Abc_Print( 1, " [resim-oracle] %d EXTRA SPLITS this batch "
"(incremental finer than full resim; QoR regression)\n", nExtra );
return nMissed + nExtra;
}
void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim ) void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim )
{ {
int nInputs = p->nRegs + p->nPis * p->nFrames; int nInputs = p->nRegs + p->nPis * p->nFrames;
@ -1928,6 +2073,11 @@ int Cec_SeedSimTryBatch( Cec_SeedSim_t * p, Cec_ManSim_t * pSim,
Cec_SeedSimRecordBatch( p, Vec_IntSize(vOutBits) / 2 ); Cec_SeedSimRecordBatch( p, Vec_IntSize(vOutBits) / 2 );
p->nEventInputVarsMax = Abc_MaxInt( p->nEventInputVarsMax, nInputVars ); p->nEventInputVarsMax = Abc_MaxInt( p->nEventInputVarsMax, nInputVars );
p->nEventInputWordsMax = Abc_MaxInt( p->nEventInputWordsMax, nInputWords ); p->nEventInputWordsMax = Abc_MaxInt( p->nEventInputWordsMax, nInputWords );
// Up-front density gate. A batch whose changed-CI seed is a large fraction
// of all unrolled inputs will dirty a near-full closure, so event
// propagation cannot beat a bit-parallel full sweep. Reject it here before
// mutating any persistent value, instead of propagating until a mid-flight
// budget abort discards the work (and then still falling back to full).
if ( (ABC_INT64_T)nInputVars * CEC_EVENT_INPUT_FRAC_DEN > if ( (ABC_INT64_T)nInputVars * CEC_EVENT_INPUT_FRAC_DEN >
(ABC_INT64_T)nTotalInputs * CEC_EVENT_INPUT_FRAC_NUM ) (ABC_INT64_T)nTotalInputs * CEC_EVENT_INPUT_FRAC_NUM )
{ {
@ -1935,6 +2085,17 @@ int Cec_SeedSimTryBatch( Cec_SeedSim_t * p, Cec_ManSim_t * pSim,
p->nBatchFull++; p->nBatchFull++;
return CEC_SEEDSIM_RESULT_FULL_WIDE; return CEC_SEEDSIM_RESULT_FULL_WIDE;
} }
// No class-cone gate. Event propagation below follows the full forward TFO of
// this batch's changed CIs (bounded only by the deterministic nNodeLimit /
// nEdgeLimit work budget; exceeding it falls back to a full sweep without
// committing). This keeps the persistent pVal globally consistent with the
// committed inputs, so Cec_SeedSimEventRefine() never reads a stale value and
// never misses a split. pSeed->fUseCone stays 0 (reset in
// Cec_ManResimulateCounterExamples), so Cec_SeedSimConeHasKey() is always true.
// The old per-call active-pair cone was too narrow -> stale values across calls
// -> missed splits -> unsound merges; see md/I_resim_soundness_bug.md. The
// cone scaffolding (Cec_SeedSimBuildClassCone / pCone / ...) is retained, unused,
// for a future adaptive *full-candidate* cone on sparse-candidate designs.
(void)vOutputs; (void)vOutputs;
Cec_SeedSimReset( p ); Cec_SeedSimReset( p );
Vec_IntClear( p->vValueUndo ); Vec_IntClear( p->vValueUndo );
@ -2023,7 +2184,8 @@ void Cec_SeedSimBeginCall( Cec_SeedSim_t * p )
p->nEventLocal = p->nEventFallback = 0; p->nEventLocal = p->nEventFallback = 0;
p->nEventPopsMax = p->nEventEdgesMax = 0; p->nEventPopsMax = p->nEventEdgesMax = 0;
p->nEventInputVarsMax = p->nEventInputWordsMax = 0; p->nEventInputVarsMax = p->nEventInputWordsMax = 0;
p->nEventFallbackWork = 0; p->nEventFallbackWork = p->nEventFallbackTime = 0;
p->nAdaptTrips = 0;
} }
void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex ) void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex )

52
src/proof/cec/cecInt.h
View File

@ -191,7 +191,7 @@ typedef enum Cec_IncrEmitMode_t_
CEC_EMIT_SKIPPED CEC_EMIT_SKIPPED
} Cec_IncrEmitMode_t; } Cec_IncrEmitMode_t;
// Persistent event-driven simulation manager for &scorr incremental mode. // Persistent event-driven simulation manager for &scorr2 -I.
// Packed input patterns and host-AIG values survive across CEX batches. A // Packed input patterns and host-AIG values survive across CEX batches. A
// batch records only the input words it changes; real value deltas propagate // batch records only the input words it changes; real value deltas propagate
// through the frame-aware fanout graph and dirty classes are fully regrouped. // through the frame-aware fanout graph and dirty classes are fully regrouped.
@ -268,8 +268,14 @@ struct Cec_SeedSim_t_
Vec_Int_t * vConeQueue; // newly marked keys used to class-close pCone Vec_Int_t * vConeQueue; // newly marked keys used to class-close pCone
int * pConeClose; // (frame,root) stamp: class already closed this build int * pConeClose; // (frame,root) stamp: class already closed this build
int nConeCloseVer; // version for pConeClose int nConeCloseVer; // version for pConeClose
int fVerify; // (-V) check maintained values vs full sweep each batch
int * pReprPre; // (-V) class-repr snapshot captured before a batch
int * pNextPre; // (-V) class-next snapshot captured before a batch
int nFallbackStreak; // persists across resimulation calls int nFallbackStreak; // persists across resimulation calls
int nFallbackCooldown; // batches bypassed before next event probe int nFallbackCooldown; // batches bypassed before next event probe
int nAdaptLocal; // decaying window: recent successful event batches
int nAdaptFail; // decaying window: recent event batches that fell back
int nAdaptTrips; // per-call adaptive cooldown activations
// Class-refinement scratch. // Class-refinement scratch.
int * pRootMark; // per-objId "root already queued" stamp int * pRootMark; // per-objId "root already queued" stamp
int nRootVersion; int nRootVersion;
@ -288,7 +294,7 @@ struct Cec_SeedSim_t_
unsigned * pPhase0; // nWords of 0 (phase-0 vector, used by refine) unsigned * pPhase0; // nWords of 0 (phase-0 vector, used by refine)
unsigned * pPhase1; // nWords of ~0 (phase-1 vector) unsigned * pPhase1; // nWords of ~0 (phase-1 vector)
int fOwnsFanout; // 1 if we built static fanout (must free) int fOwnsFanout; // 1 if we built static fanout (must free)
// Profile counters (reset per resim call) // Per-call work state used by bounded fallback and adaptive control.
int nBatchLocal; // rounds handled by local TFO sim int nBatchLocal; // rounds handled by local TFO sim
int nBatchFull; // rounds that fell back to full sweep int nBatchFull; // rounds that fell back to full sweep
int nBatchTrunc; // local rounds that stopped optional TFO expansion int nBatchTrunc; // local rounds that stopped optional TFO expansion
@ -313,10 +319,12 @@ struct Cec_SeedSim_t_
int nEventInputVarsMax; // largest changed-CI count in one batch int nEventInputVarsMax; // largest changed-CI count in one batch
int nEventInputWordsMax; // largest changed-CI-word count in one batch int nEventInputWordsMax; // largest changed-CI-word count in one batch
int nEventFallbackWork; // structural word-operation budget exceeded int nEventFallbackWork; // structural word-operation budget exceeded
int nEventFallbackTime; // adaptive elapsed-time budget exceeded
}; };
// Dynamic SRM construction manager for &scorr incremental mode. It keeps the // Dynamic SRM construction manager for &scorr2 -D. It keeps the speculative SRM
// speculative SRM core used by SAT. // core used by SAT; counterexample resimulation is selected independently by
// -I and otherwise uses the original host-AIG path.
typedef struct Cec_DynSrm_t_ Cec_DynSrm_t; typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
// Recursive diagnosis has a much higher constant factor than a linear sweep. // Recursive diagnosis has a much higher constant factor than a linear sweep.
@ -337,6 +345,15 @@ typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
// Consecutive wide cones use bounded exponential backoff. A successful local // Consecutive wide cones use bounded exponential backoff. A successful local
// batch clears both the streak and cooldown immediately. // batch clears both the streak and cooldown immediately.
#define CEC_SEEDSIM_MAX_FALLBACK_BACKOFF 7 #define CEC_SEEDSIM_MAX_FALLBACK_BACKOFF 7
// Adaptive event-resim circuit breaker. Logs showed good cases are strongly
// local-heavy (400k: 161/0, fermat: 451/6) while bad cases are fallback-heavy
// (RAV: 122/1335). Use a small decaying window to probe again after cooldown
// without repeatedly paying the failed event propagation cost.
#define CEC_SEEDSIM_ADAPT_WINDOW 16
#define CEC_SEEDSIM_ADAPT_MIN_SAMPLES 8
#define CEC_SEEDSIM_ADAPT_FAIL_MUL 2
#define CEC_SEEDSIM_ADAPT_FAIL_EXTRA 4
#define CEC_SEEDSIM_ADAPT_MAX_COOLDOWN 31
#define CEC_EVENT_NODE_WORD_FRAC_NUM 1 #define CEC_EVENT_NODE_WORD_FRAC_NUM 1
#define CEC_EVENT_NODE_WORD_FRAC_DEN 10 #define CEC_EVENT_NODE_WORD_FRAC_DEN 10
#define CEC_EVENT_EDGE_WORD_FRAC_NUM 1 #define CEC_EVENT_EDGE_WORD_FRAC_NUM 1
@ -361,13 +378,13 @@ typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
/*=== cecCorr.c ============================================================*/ /*=== cecCorr.c ============================================================*/
extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time ); extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time );
extern void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops ); /*=== cecCorr2.c ===========================================================*/
extern Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p ); extern int Gia_ManCorr2SpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
extern void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo ); extern void Gia_ManCorr2SpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
extern int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ); extern Gia_Man_t * Gia_ManCorr2SpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, Vec_Int_t ** pvOutLits );
extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); extern Gia_Man_t * Cec_ManLSCorrespondence2( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); /*=== cecCorrCert.c =========================================================*/
extern Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ); extern int Cec_ManCorrKissatCertify( Gia_Man_t * pSrm, Vec_Int_t * vOutputs, Vec_Int_t ** pvCexStore, Vec_Str_t ** pvStatus, int * piOut, int fVerbose );
/*=== cecCorrIncr.c ============================================================*/ /*=== cecCorrIncr.c ============================================================*/
extern Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames ); extern Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames );
extern void Cec_IncrMgrFree( Cec_IncrMgr_t * p ); extern void Cec_IncrMgrFree( Cec_IncrMgr_t * p );
@ -380,16 +397,19 @@ extern void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p );
extern Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMark, Cec_IncrMgr_t * pIncr, Cec_IncrEmitMode_t Mode, Vec_Int_t ** pvOutLits ); extern Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMark, Cec_IncrMgr_t * pIncr, Cec_IncrEmitMode_t Mode, Vec_Int_t ** pvOutLits );
extern Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMark ); extern Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMark );
/*=== cecCorrDyn.c ============================================================*/ /*=== cecCorrDyn.c ============================================================*/
extern Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr ); extern Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr, int fUseAdaptive );
extern void Cec_DynSrmSetParams( Cec_DynSrm_t * p, Cec_ParCor_t * pPars );
extern void Cec_DynSrmForceRebuild( Cec_DynSrm_t * p, int fIncrFallback );
extern void Cec_DynSrmFree( Cec_DynSrm_t * p ); extern void Cec_DynSrmFree( Cec_DynSrm_t * p );
extern void Cec_DynSrmPrintStats( Cec_DynSrm_t * p ); extern void Cec_DynSrmRecordSolveStats( Cec_DynSrm_t * p, int nCalls, int nReal, int nTriv, int nFail, abctime tSat );
extern void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive ); extern void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive );
extern Gia_Man_t * Cec_DynSrmBuild( Cec_DynSrm_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode ); extern Gia_Man_t * Cec_DynSrmBuild( Cec_DynSrm_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode );
extern void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode ); extern void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode );
extern Gia_Man_t * Cec_DynSrmBuildInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode ); extern Gia_Man_t * Cec_DynSrmBuildInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode );
extern void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode ); extern void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode );
extern Vec_Int_t * Cec_DynSrmOutLits( Cec_DynSrm_t * p ); extern Vec_Int_t * Cec_DynSrmOutLits( Cec_DynSrm_t * p );
extern Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus ); extern Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus, int fUseTas );
extern Vec_Int_t * Cec_DynSrmSolveBmcAdaptive( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus, int fUseTas );
/*=== cecCorrIncrSim.c ============================================================*/ /*=== cecCorrIncrSim.c ============================================================*/
extern Cec_SeedSim_t * Cec_SeedSimAlloc( Gia_Man_t * pAig, int nFrames, int iSeedFrame, int nWords ); extern Cec_SeedSim_t * Cec_SeedSimAlloc( Gia_Man_t * pAig, int nFrames, int iSeedFrame, int nWords );
extern void Cec_SeedSimFree( Cec_SeedSim_t * p ); extern void Cec_SeedSimFree( Cec_SeedSim_t * p );
@ -401,6 +421,9 @@ extern void Cec_SeedSimBeginCall( Cec_SeedSim_t * p );
extern void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex ); extern void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex );
extern void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim ); extern void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim );
extern void Cec_SeedSimBuildClassCone( Cec_SeedSim_t * p, Vec_Int_t * vOutputs ); extern void Cec_SeedSimBuildClassCone( Cec_SeedSim_t * p, Vec_Int_t * vOutputs );
extern int Cec_SeedSimVerifyValues( Cec_SeedSim_t * p );
extern void Cec_SeedSimVerifySnapshot( Cec_SeedSim_t * p );
extern int Cec_SeedSimVerifyRefine( Cec_SeedSim_t * p, Cec_ManSim_t * pSim, Vec_Ptr_t * vSimInfo, int nFrames );
extern int Cec_SeedSimLoadPersistentBatch( Cec_SeedSim_t * p, Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPairs, Vec_Int_t * vOutBits ); extern int Cec_SeedSimLoadPersistentBatch( Cec_SeedSim_t * p, Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPairs, Vec_Int_t * vOutBits );
extern void Cec_SeedSimRestorePersistentInputs( Cec_SeedSim_t * p ); extern void Cec_SeedSimRestorePersistentInputs( Cec_SeedSim_t * p );
/*=== cecClass.c ============================================================*/ /*=== cecClass.c ============================================================*/
@ -466,4 +489,3 @@ ABC_NAMESPACE_HEADER_END
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

2
src/proof/cec/module.make
View File

@ -3,6 +3,8 @@ SRC += src/proof/cec/cecCec.c \
src/proof/cec/cecClass.c \ src/proof/cec/cecClass.c \
src/proof/cec/cecCore.c \ src/proof/cec/cecCore.c \
src/proof/cec/cecCorr.c \ src/proof/cec/cecCorr.c \
src/proof/cec/cecCorr2.c \
src/proof/cec/cecCorrCert.c \
src/proof/cec/cecCorrDyn.c \ src/proof/cec/cecCorrDyn.c \
src/proof/cec/cecCorrIncr.c \ src/proof/cec/cecCorrIncr.c \
src/proof/cec/cecCorrIncrSim.c \ src/proof/cec/cecCorrIncrSim.c \