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

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2026-07-02 11:29:04 +02:00
parent a35f806b8c bcfdf59228
commit 4644b49364
21 changed files with 4138 additions and 207 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abclib.dsp
View File

@ -6685,10 +6685,18 @@ SOURCE=.\src\proof\cec\cecCorr.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\proof\cec\cecCorrDyn.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecCorrIncr.c SOURCE=.\src\proof\cec\cecCorrIncr.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\proof\cec\cecCorrIncrSim.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecInt.h SOURCE=.\src\proof\cec\cecInt.h
# End Source File # End Source File
# Begin Source File # Begin Source File

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

@ -1312,10 +1312,14 @@ extern void Cbs_ManStop( Cbs_Man_t * p );
extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ); extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj );
extern int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose ); extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose );
extern Vec_Int_t * Cbs_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
extern void Cbs_ManSyncCore( Cbs_Man_t * p );
extern Vec_Int_t * Cbs_ManSolveRoots( Cbs_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose );
extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num ); extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p ); extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p );
/*=== giaCTas.c ============================================================*/ /*=== giaCTas.c ============================================================*/
extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
extern Vec_Int_t * Tas_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
/*=== giaCof.c =============================================================*/ /*=== giaCof.c =============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );

181
src/aig/gia/giaCSat.c
View File

@ -64,6 +64,7 @@ struct Cbs_Man_t_
{ {
Cbs_Par_t Pars; // parameters Cbs_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
Cbs_Que_t pProp; // propagation queue Cbs_Que_t pProp; // propagation queue
Cbs_Que_t pJust; // justification queue Cbs_Que_t pJust; // justification queue
Cbs_Que_t pClauses; // clause queue Cbs_Que_t pClauses; // clause queue
@ -71,6 +72,9 @@ struct Cbs_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
// SAT calls statistics // SAT calls statistics
int nSatUnsat; // the number of proofs int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure int nSatSat; // the number of failure
@ -256,6 +260,29 @@ static inline void Cbs_ManSaveModelAll( Cbs_Man_t * p, Vec_Int_t * vCex )
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
} }
static inline int Cbs_ManLitValue( Cbs_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 ( !Cbs_VarIsAssigned(pObj) )
return -1;
return Cbs_VarValue(pObj) ^ Abc_LitIsCompl(iLit);
}
static inline void Cbs_ManSaveOutVals( Cbs_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, Cbs_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out) ) );
Vec_IntWriteEntry( vOutVals, 2*Out + 1, Cbs_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out + 1) ) );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -954,7 +981,10 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0; p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
Cbs_ManAssign( p, pObj, 0, NULL, NULL ); Cbs_ManAssign( p, pObj, 0, NULL, NULL );
if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) ) if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
{
Cbs_ManSaveModel( p, p->vModel ); Cbs_ManSaveModel( p, p->vModel );
Cbs_ManSaveOutVals( p, p->vOutLits, p->vOutVals, p->iOutVal );
}
else else
RetValue = 1; RetValue = 1;
Cbs_ManCancelUntil( p, 0 ); Cbs_ManCancelUntil( p, 0 );
@ -1034,14 +1064,14 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose ) Vec_Int_t * Cbs_ManSolveMiterNcOutVals( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, 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 );
Cbs_Man_t * p; Cbs_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; Gia_Obj_t * pRoot;
int i, status; int i, status;
abctime clk, clkTotal = Abc_Clock(); abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManRegNum(pAig) == 0 ); assert( Gia_ManRegNum(pAig) == 0 );
@ -1058,6 +1088,12 @@ Vec_Int_t * Cbs_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 = Cbs_ReadModel( p ); vCex = Cbs_ReadModel( p );
// solve for each output // solve for each output
@ -1084,7 +1120,13 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
clk = Abc_Clock(); clk = Abc_Clock();
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 = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
p->vOutLits = NULL;
p->vOutVals = NULL;
p->iOutVal = -1;
// printf( "\n" ); // printf( "\n" );
/* /*
if ( status == -1 ) if ( status == -1 )
@ -1126,6 +1168,10 @@ Vec_Int_t * Cbs_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 );
Cbs_ManStop( p ); Cbs_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,
@ -1133,6 +1179,132 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
return vCexStore; return vCexStore;
} }
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose )
{
return Cbs_ManSolveMiterNcOutVals( pAig, nConfs, pvStatus, f0Proved, fVerbose, NULL, NULL );
}
/**Function*************************************************************
Synopsis [Incrementally prepares newly appended objects of a persistent AIG.]
Description [The pAig of a resident manager is append-only across solve calls.
Cbs needs every unassigned object to carry Value=~0 and clean marks, and reads
Gia_ObjRefNum during branching. After a clean solve Cbs restores Value/marks
of the nodes it touched, and freshly appended nodes are zero-initialized, so we
only have to prep the suffix [nSyncedObjs, ObjNum): set Value=~0, clear marks,
grow pRefs and bump each new AND's fanin refs (= the global fanout counts that
Gia_ManCreateRefs would produce, computed incrementally). This replaces the
per-round O(|pAig|) refs/marks/value rebuild with O(newly appended).]
SideEffects [Allocates/grows pAig->pRefs (freed by Gia_ManStop).]
SeeAlso []
***********************************************************************/
void Cbs_ManSyncCore( Cbs_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) );
for ( i = p->nSyncedObjs; i < nObjs; i++ )
{
pObj = Gia_ManObj( pAig, i );
pObj->fMark0 = pObj->fMark1 = 0;
pObj->Value = ~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 Cbs_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 Cbs_ManSyncCore-ing the objects appended since
the last call - so neither the throwaway view (alloc + copy-all-CIs + cone
copy) nor the per-round whole-AIG prep is paid. Output index i corresponds to
vRootLits[i]; vCexStore / vStatus format matches Cbs_ManSolveMiterNc. CEX is
saved by CioId, which on pCore equals the view's CI numbering.]
SideEffects [Prepares newly appended objects via Cbs_ManSyncCore.]
SeeAlso []
***********************************************************************/
Vec_Int_t * Cbs_ManSolveRoots( Cbs_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 );
Cbs_ManSyncCore( p ); // prep only objects appended since the last solve
vStatus = Vec_StrAlloc( Vec_IntSize(vRootLits) );
vCexStore = Vec_IntAlloc( 10000 );
vCex = Cbs_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 = Cbs_ManSolve( p, Gia_ObjFromLit(pAig, iLit) );
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 == 1 )
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += Abc_Clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += Abc_Clock() - clk;
}
p->nSatTotal = Vec_IntSize( vRootLits );
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs_ManSatPrintStats( p );
// manager is resident: caller (Cec_DynSrm) owns its lifetime
*pvStatus = vStatus;
return vCexStore;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
@ -1140,4 +1312,3 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_END

2
src/aig/gia/giaCut.c
View File

@ -690,7 +690,7 @@ Vec_Wec_t * Gia_ManSelectCuts( Vec_Wec_t * vCuts, int nCuts, int nCutSizeMin )
Vec_Wec_t * vCutsSel = Vec_WecStart( nCuts ); Vec_Wec_t * vCutsSel = Vec_WecStart( nCuts );
int i; srand( time(NULL) ); int i; srand( time(NULL) );
for ( i = 0; i < nCuts; i++ ) for ( i = 0; i < nCuts; i++ )
while ( !Gia_StoSelectOneCut(vCuts, (rand() | (rand() << 15)) % Vec_WecSize(vCuts), Vec_WecEntry(vCutsSel, i), nCutSizeMin) ); while ( !Gia_StoSelectOneCut(vCuts, (int)(((unsigned)rand() | ((unsigned)rand() << 15)) % Vec_WecSize(vCuts)), Vec_WecEntry(vCutsSel, i), nCutSizeMin) );
return vCutsSel; return vCutsSel;
} }
Vec_Wec_t * Gia_ManExtractCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 ) Vec_Wec_t * Gia_ManExtractCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 )

2
src/aig/gia/giaGen.c
View File

@ -1557,7 +1557,7 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int
int * pLits = ABC_CALLOC( int, 2*nVars+10 ); int * pLits = ABC_CALLOC( int, 2*nVars+10 );
memcpy( pLits, pLitsI, sizeof(int)*2*nVars ); memcpy( pLits, pLitsI, sizeof(int)*2*nVars );
for ( i = 1; i < nVars; i++ ) for ( i = 1; i < nVars; i++ )
for ( k = 1; k < nVars; k++ ) for ( k = nVars - 1; k >= 1; k-- )
if ( pStore[i][k] >= 0 ) if ( pStore[i][k] >= 0 )
Gia_ManGenPrefix( p, &pLits[2*k], &pLits[2*k+1], pLits[2*pStore[i][k]], pLits[2*pStore[i][k]+1] ); Gia_ManGenPrefix( p, &pLits[2*k], &pLits[2*k+1], pLits[2*pStore[i][k]], pLits[2*pStore[i][k]+1] );
if ( fCarries ) if ( fCarries )

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

@ -35249,16 +35249,19 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkRedirectCiCo( Abc_Ntk_t * pNtk ); extern void Abc_NtkRedirectCiCo( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs ); extern Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs );
extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs ); extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs );
extern Abc_Ntk_t * Abc_NtkFromMappedGiaAnd5( Gia_Man_t * p, int fFindEnables, int fUseBuffs );
extern Abc_Ntk_t * Abc_NtkFromMappedGia2( Gia_Man_t * p, int fFindEnables, int fUseBuffs, int fCheckAnd5, int fVerbose );
Aig_Man_t * pMan; Aig_Man_t * pMan;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int fStatusClear = 1; int fStatusClear = 1;
int fFindEnables = 0; int fFindEnables = 0;
int fUseBuffs = 0; int fUseBuffs = 0;
int fCheckAnd5 = 0;
int c, fVerbose = 0; int c, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "seovh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "seiovh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -35268,6 +35271,9 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'e': case 'e':
fFindEnables ^= 1; fFindEnables ^= 1;
break; break;
case 'i':
fCheckAnd5 ^= 1;
break;
case 'o': case 'o':
fUseBuffs ^= 1; fUseBuffs ^= 1;
break; break;
@ -35290,7 +35296,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( Gia_ManHasCellMapping(pAbc->pGia) ) else if ( Gia_ManHasCellMapping(pAbc->pGia) )
pNtk = Abc_NtkFromCellMappedGia( pAbc->pGia, fUseBuffs ); pNtk = Abc_NtkFromCellMappedGia( pAbc->pGia, fUseBuffs );
else if ( Gia_ManHasMapping(pAbc->pGia) || pAbc->pGia->pMuxes ) else if ( Gia_ManHasMapping(pAbc->pGia) || pAbc->pGia->pMuxes )
pNtk = Abc_NtkFromMappedGia( pAbc->pGia, 0, fUseBuffs ); pNtk = Abc_NtkFromMappedGia2( pAbc->pGia, 0, fUseBuffs, fCheckAnd5, fVerbose );
else if ( Gia_ManHasDangling(pAbc->pGia) == 0 ) else if ( Gia_ManHasDangling(pAbc->pGia) == 0 )
{ {
pMan = Gia_ManToAig( pAbc->pGia, 0 ); pMan = Gia_ManToAig( pAbc->pGia, 0 );
@ -35313,6 +35319,8 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDelete( pNtkNoCh ); Abc_NtkDelete( pNtkNoCh );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
} }
if ( pNtk == NULL )
return 1;
// transfer the spec name to the pNtk // transfer the spec name to the pNtk
if( pAbc->pGia->pSpec ) if( pAbc->pGia->pSpec )
{ {
@ -35379,10 +35387,11 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &put [-seovh]\n" ); Abc_Print( -2, "usage: &put [-seiovh]\n" );
Abc_Print( -2, "\t transfer the current network into the old ABC\n" ); Abc_Print( -2, "\t transfer the current network into the old ABC\n" );
Abc_Print( -2, "\t-s : toggle clearning verification status [default = %s]\n", fStatusClear? "yes": "no" ); Abc_Print( -2, "\t-s : toggle clearning verification status [default = %s]\n", fStatusClear? "yes": "no" );
Abc_Print( -2, "\t-e : toggle extracting MUXes for flop enables [default = %s]\n", fFindEnables? "yes": "no" ); Abc_Print( -2, "\t-e : toggle extracting MUXes for flop enables [default = %s]\n", fFindEnables? "yes": "no" );
Abc_Print( -2, "\t-i : toggle AND-decomposable polarity for 5-input LUTs [default = %s]\n", fCheckAnd5? "yes": "no" );
Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", fUseBuffs? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", fUseBuffs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
@ -35621,13 +35630,16 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage; goto usage;
} }
} }
if ( fClear )
{
Gia_ManStopP( &pAbc->pGiaSaved );
return 0;
}
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Empty network.\n" ); Abc_Print( -1, "Empty network.\n" );
return 1; return 1;
} }
if ( fClear && pAbc->pGiaSaved != NULL )
Gia_ManStopP( &pAbc->pGiaSaved );
if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) ) if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) )
return 0; return 0;
if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) ) if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) )
@ -41927,6 +41939,13 @@ 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 +42021,7 @@ 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 incremental TFO-triggered re-proof in main loop [default = %s] by Xiran ZHao at University of Chinese Academy of Sciences\n", pPars->fIncremental? "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" );

158
src/base/abci/abcDar.c
View File

@ -38,6 +38,7 @@
#include "opt/csw/csw.h" #include "opt/csw/csw.h"
#include "proof/pdr/pdr.h" #include "proof/pdr/pdr.h"
#include "sat/bmc/bmc.h" #include "sat/bmc/bmc.h"
#include "misc/util/utilTruth.h"
#include "map/mio/mio.h" #include "map/mio/mio.h"
#include "misc/vec/vecMem.h" #include "misc/vec/vecMem.h"
@ -757,7 +758,7 @@ Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, V
Vec_PtrWriteEntry( vCopies, Id, gFunc ); Vec_PtrWriteEntry( vCopies, Id, gFunc );
return gFunc; return gFunc;
} }
Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies ) static Hop_Obj_t * Abc_ObjHopFromGia2( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies, Vec_Bit_t * vCompls )
{ {
int k, iFan; int k, iFan;
assert( Gia_ObjIsLut(p, GiaId) ); assert( Gia_ObjIsLut(p, GiaId) );
@ -766,10 +767,107 @@ Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Ve
Gia_LutForEachFanin( p, GiaId, iFan, k ) Gia_LutForEachFanin( p, GiaId, iFan, k )
{ {
Gia_ObjSetTravIdCurrentId(p, iFan); Gia_ObjSetTravIdCurrentId(p, iFan);
Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) ); Vec_PtrWriteEntry( vCopies, iFan, Hop_NotCond(Hop_IthVar(pHopMan, k), vCompls && Vec_BitEntry(vCompls, iFan)) );
} }
return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies ); return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
} }
Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
{
return Abc_ObjHopFromGia2( pHopMan, p, GiaId, vCopies, NULL );
}
static int Abc_Tt5HasAndDec( word Truth )
{
int v;
for ( v = 0; v < 5; v++ )
if ( Abc_Tt6Cofactor0(Truth, v) == 0 || Abc_Tt6Cofactor1(Truth, v) == 0 )
return 1;
return 0;
}
static int Abc_Tt5AndDecPolarity( word Truth )
{
if ( Abc_Tt5HasAndDec(Truth) )
return 0;
if ( Abc_Tt5HasAndDec(~Truth) )
return 1;
return -1;
}
static word Abc_Tt5CofactorTo4( word Truth, int iVar, int fCompl )
{
word Result = 0;
int a, k;
for ( a = 0; a < 16; a++ )
{
int iMint = fCompl ? 0 : (1 << iVar);
for ( k = 0; k < 4; k++ )
if ( (a >> k) & 1 )
iMint |= 1 << (k < iVar ? k : k + 1);
if ( (Truth >> iMint) & 1 )
Result |= ((word)1) << a;
}
return Result;
}
static int Abc_Tt5FindAndDec( word Truth, int * piVar, int * pfCompl, word * pTruth4 )
{
int v;
for ( v = 0; v < 5; v++ )
{
if ( Abc_Tt6Cofactor0(Truth, v) == 0 )
{
*piVar = v;
*pfCompl = 0;
*pTruth4 = Abc_Tt5CofactorTo4( Truth, v, 0 );
return 1;
}
if ( Abc_Tt6Cofactor1(Truth, v) == 0 )
{
*piVar = v;
*pfCompl = 1;
*pTruth4 = Abc_Tt5CofactorTo4( Truth, v, 1 );
return 1;
}
}
return 0;
}
static void Abc_NtkFromMappedGiaPrint5Decs( Abc_Ntk_t * pNtk )
{
Hop_Man_t * pHopMan;
Abc_Obj_t * pObj;
Vec_Int_t * vTruth;
int i, nNodes5 = 0, nNodesOver5 = 0;
assert( Abc_NtkIsLogic(pNtk) && Abc_NtkHasAig(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
{
nNodes5 += Abc_ObjFaninNum(pObj) == 5;
nNodesOver5 += Abc_ObjFaninNum(pObj) > 5;
}
if ( nNodes5 == 0 || nNodesOver5 > 0 )
return;
pHopMan = (Hop_Man_t *)pNtk->pManFunc;
vTruth = Vec_IntAlloc( 64 );
Abc_Print( 1, "Top-level AND decompositions of 5-input nodes:\n" );
Abc_NtkForEachNode( pNtk, pObj, i )
{
word Truth, Truth4;
int iVar, fCompl;
if ( Abc_ObjFaninNum(pObj) != 5 )
continue;
Truth = (word)*Hop_ManConvertAigToTruth( pHopMan, (Hop_Obj_t *)pObj->pData, 5, vTruth, 0 );
if ( !Abc_Tt5FindAndDec( Truth, &iVar, &fCompl, &Truth4 ) )
{
Abc_Print( 1, "%05d : ", Abc_ObjId(pObj) );
Abc_TtPrintHexRev( stdout, &Truth, 5 );
Abc_Print( 1, " = <none>\n" );
continue;
}
Abc_Print( 1, "%05d : ", Abc_ObjId(pObj) );
Abc_TtPrintHexRev( stdout, &Truth, 5 );
Abc_Print( 1, " = %cx%d & ", fCompl ? '~' : ' ', iVar );
Abc_TtPrintHexRev( stdout, &Truth4, 4 );
Abc_Print( 1, "\n" );
}
Vec_IntFree( vTruth );
}
/**Function************************************************************* /**Function*************************************************************
@ -804,14 +902,14 @@ Abc_Obj_t * Abc_NtkFromMappedGia_rec( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, int iO
pObjNew = Abc_NtkCreateNodeInv(pNtkNew, pObjNew); pObjNew = Abc_NtkCreateNodeInv(pNtkNew, pObjNew);
return pObjNew; return pObjNew;
} }
Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs ) Abc_Ntk_t * Abc_NtkFromMappedGiaInt( Gia_Man_t * p, int fFindEnables, int fUseBuffs, int fCheckAnd5, int fVerbose )
{ {
int fVerbose = 0;
int fDuplicate = 0; int fDuplicate = 0;
Abc_Ntk_t * pNtkNew; Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL; Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
Gia_Obj_t * pObj, * pObjLi, * pObjLo; Gia_Obj_t * pObj, * pObjLi, * pObjLo;
Vec_Ptr_t * vReflect; Vec_Ptr_t * vReflect;
Vec_Bit_t * vCompls = NULL;
int i, k, iFan, nDupGates, nCountMux = 0; int i, k, iFan, nDupGates, nCountMux = 0;
assert( Gia_ManHasMapping(p) || p->pMuxes || fFindEnables ); assert( Gia_ManHasMapping(p) || p->pMuxes || fFindEnables );
assert( !fFindEnables || !p->pMuxes ); assert( !fFindEnables || !p->pMuxes );
@ -820,6 +918,8 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
pNtkNew->pName = Extra_UtilStrsav(p->pName); pNtkNew->pName = Extra_UtilStrsav(p->pName);
pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec); pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
Gia_ManFillValue( p ); Gia_ManFillValue( p );
if ( fCheckAnd5 )
vCompls = Vec_BitStart( Gia_ManObjNum(p) );
// create constant // create constant
pConst0 = Abc_NtkCreateNodeConst0( pNtkNew ); pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
Gia_ManConst0(p)->Value = Abc_ObjId(pConst0); Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
@ -917,6 +1017,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
vReflect = Vec_PtrStart( Gia_ManObjNum(p) ); vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
Gia_ManForEachLut( p, i ) Gia_ManForEachLut( p, i )
{ {
Hop_Obj_t * pFunc;
pObj = Gia_ManObj(p, i); pObj = Gia_ManObj(p, i);
assert( pObj->Value == ~0 ); assert( pObj->Value == ~0 );
if ( Gia_ObjLutSize(p, i) == 0 ) if ( Gia_ObjLutSize(p, i) == 0 )
@ -924,10 +1025,36 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
pObj->Value = Abc_ObjId(pConst0); pObj->Value = Abc_ObjId(pConst0);
continue; continue;
} }
pFunc = Abc_ObjHopFromGia2( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect, vCompls );
if ( fCheckAnd5 && Gia_ObjLutSize(p, i) == 5 )
{
word Truth = Hop_ManComputeTruth6( (Hop_Man_t *)pNtkNew->pManFunc, pFunc, 5 );
int fCompl = Abc_Tt5AndDecPolarity( Truth );
if ( fCompl < 0 )
{
Abc_Print( -1, "Abc_NtkFromMappedGia(): 5-input node %d does not have AND-decomposition in either polarity.\n", i );
Vec_PtrFree( vReflect );
Vec_BitFreeP( &vCompls );
Abc_NtkDelete( pNtkNew );
return NULL;
}
pFunc = Hop_NotCond( pFunc, fCompl );
Truth = fCompl ? ~Truth : Truth;
assert( Abc_Tt5HasAndDec(Truth) );
if ( !Abc_Tt5HasAndDec(Truth) )
{
Abc_Print( -1, "Abc_NtkFromMappedGia(): Internal error: 5-input node %d failed AND-decomposition check.\n", i );
Vec_PtrFree( vReflect );
Vec_BitFreeP( &vCompls );
Abc_NtkDelete( pNtkNew );
return NULL;
}
Vec_BitWriteEntry( vCompls, i, fCompl );
}
pObjNew = Abc_NtkCreateNode( pNtkNew ); pObjNew = Abc_NtkCreateNode( pNtkNew );
Gia_LutForEachFanin( p, i, iFan, k ) Gia_LutForEachFanin( p, i, iFan, k )
Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) ); Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect ); pObjNew->pData = pFunc;
pObjNew->fPersist = Gia_ObjLutIsMux(p, i) && Gia_ObjLutSize(p, i) == 3; pObjNew->fPersist = Gia_ObjLutIsMux(p, i) && Gia_ObjLutSize(p, i) == 3;
pObj->Value = Abc_ObjId( pObjNew ); pObj->Value = Abc_ObjId( pObjNew );
} }
@ -939,8 +1066,12 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
if ( !fFindEnables ) if ( !fFindEnables )
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
{ {
int iFanin = Gia_ObjFaninId0p(p, pObj);
int fCompl = Gia_ObjFaninC0(pObj) ^ (vCompls && Vec_BitEntry(vCompls, iFanin));
pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) ); if ( fCheckAnd5 && fCompl && Gia_ObjIsLut(p, iFanin) && Gia_ObjLutSize(p, iFanin) == 5 )
pObjNew = Abc_NtkCreateNodeInv( pNtkNew, pObjNew ), fCompl = 0;
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, fCompl ) );
} }
// create names // create names
Abc_NtkAddDummyPiNames( pNtkNew ); Abc_NtkAddDummyPiNames( pNtkNew );
@ -967,8 +1098,23 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
// check the resulting AIG // check the resulting AIG
if ( !Abc_NtkCheck( pNtkNew ) ) if ( !Abc_NtkCheck( pNtkNew ) )
Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" ); Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
if ( fVerbose && Gia_ManHasMapping(p) )
Abc_NtkFromMappedGiaPrint5Decs( pNtkNew );
Vec_BitFreeP( &vCompls );
return pNtkNew; return pNtkNew;
} }
Abc_Ntk_t * Abc_NtkFromMappedGia2( Gia_Man_t * p, int fFindEnables, int fUseBuffs, int fCheckAnd5, int fVerbose )
{
return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, fCheckAnd5, fVerbose );
}
Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs )
{
return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, 0, 0 );
}
Abc_Ntk_t * Abc_NtkFromMappedGiaAnd5( Gia_Man_t * p, int fFindEnables, int fUseBuffs )
{
return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, 1, 0 );
}
/**Function************************************************************* /**Function*************************************************************

6
src/map/if/ifDec07.c
View File

@ -1127,9 +1127,10 @@ int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, cha
} }
int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ) int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{ {
if ( nLeaves < nVars ) if ( nLeaves < p->pPars->nLutSize )
return 1; return 1;
assert( nLeaves == nVars ); assert( nLeaves == p->pPars->nLutSize );
assert( nLeaves <= nVars );
if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) ) if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) )
return 1; return 1;
return 0; return 0;
@ -1141,4 +1142,3 @@ int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, cha
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_END

27
src/opt/eslim/eslimCirMan.cpp
View File

@ -506,6 +506,22 @@ namespace eSLIM {
fan1negated = (fan1negated != is_node_negated[(pe->fanins[0])->node_id]); fan1negated = (fan1negated != is_node_negated[(pe->fanins[0])->node_id]);
fan2negated = (fan2negated != is_node_negated[(pe->fanins[1])->node_id]); fan2negated = (fan2negated != is_node_negated[(pe->fanins[1])->node_id]);
// We need to remove gates with duplicate fanins.
// We do not use simplifyDuplicateFanins as it does not propagate duplicate fanins.
if (fan1 == fan2) {
if ((fan1negated != fan2negated ) || is_xor) {
assert (!negate_and);
node_ids[node_id] = const_false_id;
is_node_negated[node_id] = negate_and;
return const_false_id;
} else {
node_ids[node_id] = fan1;
// Gates are assumed to be normal -> x = !a && !a (x = !a || !a) is not possible.
is_node_negated[node_id] = is_node_negated[(pe->fanins[1])->node_id];
return fan1;
}
}
int id; int id;
if (is_xor) { if (is_xor) {
id = Gia_ManAppendXor(pGia, Abc_LitNotCond(fan1, fan1negated), Abc_LitNotCond(fan2, fan2negated)); id = Gia_ManAppendXor(pGia, Abc_LitNotCond(fan1, fan1negated), Abc_LitNotCond(fan2, fan2negated));
@ -523,7 +539,7 @@ namespace eSLIM {
Gia_Man_t* eSLIMCirMan::eSLIMCirManToGia() { Gia_Man_t* eSLIMCirMan::eSLIMCirManToGia() {
simplifyDuplicateFanins(); // simplifyDuplicateFanins();
Gia_Man_t * pNew = Gia_ManStart( getNofObjs() ); Gia_Man_t * pNew = Gia_ManStart( getNofObjs() );
std::vector<int> node_ids(nodes.size(), 0); std::vector<int> node_ids(nodes.size(), 0);
@ -536,15 +552,6 @@ namespace eSLIM {
} }
for (int i = nof_pis + 1; i < nodes.size() - nof_pos; i++) { for (int i = nof_pis + 1; i < nodes.size() - nof_pos; i++) {
// It is possible (but rather unlikley) that a gate has only a single fanin
// For instance it is possible that internally a gate has duplicate fanins.
// simplifyDuplicateFanins removes duplicate fanins
if (nodes[i]->getNFanins() == 1) {
eSLIMCirObj* pe = getpObj(i);
node_ids[i] = node_ids[(pe->fanins[0])->node_id];
is_node_negated[i] = pe->tt == 1;
continue;
}
assert(nodes[i]->getNFanins() == 2); assert(nodes[i]->getNFanins() == 2);
addGiaGate( pNew, i, node_ids, is_node_negated ); addGiaGate( pNew, i, node_ids, is_node_negated );
} }

7
src/opt/eslim/relationSynthesiser.cpp
View File

@ -532,7 +532,12 @@ namespace eSLIM {
std::vector<int> clause (gate_output_variables[i].begin(), gate_output_variables[i].end()); std::vector<int> clause (gate_output_variables[i].begin(), gate_output_variables[i].end());
clause.reserve(max_size - i + 1); clause.reserve(max_size - i + 1);
for (int j = i + 1; j < max_size; j++) { for (int j = i + 1; j < max_size; j++) {
clause.push_back(selection_variables[j][subcir.inputs.size() + i]); // clause.push_back(selection_variables[j][subcir.inputs.size() + i]);
int isused = getNewVariable();
// The gate is used by another (active) gate.
solver.addClause({-isused, selection_variables[j][subcir.inputs.size() + i]});
solver.addClause({-isused, gate_activation_variables[j]});
clause.push_back(isused);
} }
clause.push_back(-gate_activation_variables[i]); clause.push_back(-gate_activation_variables[i]);
solver.addClause(clause); solver.addClause(clause);

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

@ -167,7 +167,10 @@ 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; // active-list/TFO-triggered reproof in main loop int fIncremental; // integrated incremental mode for &scorr
int fIncrSim; // persistent CEX-TFO-only resimulation after SAT
int fDynSrm; // persistent dynamic SRM and true-unroll resimulation
int fSkipFailResim;// skip resim in rounds with no real CEX (only timeout/fail)
int fVerboseFlops; // verbose stats int fVerboseFlops; // verbose stats
int fVeryVerbose; // verbose stats int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats int fVerbose; // verbose stats

124
src/proof/cec/cecClass.c
View File

@ -32,6 +32,11 @@ static inline void Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n ) { p->
static inline float Cec_MemUsage( Cec_ManSim_t * p ) { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20); } static inline float Cec_MemUsage( Cec_ManSim_t * p ) { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20); }
void Cec_ManSimMemRelink( Cec_ManSim_t * p );
unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i );
unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i );
void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -310,6 +315,106 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
return Cec_ManSimClassRefineOne_rec( p, i ); return Cec_ManSimClassRefineOne_rec( p, i );
} }
static void Cec_ManSimLoadMappedValue( Cec_ManSim_t * p, int ObjId,
unsigned * pValues, int Lit, int nWords )
{
unsigned * pSim = Cec_ManSimSimRef( p, ObjId );
unsigned * pValue = pValues + (size_t)Abc_Lit2Var(Lit) * nWords;
int w;
// External values are consumed only by class refinement, not by the
// reference-counted AIG simulation below. One matching dereference should
// therefore release this entry regardless of the host node's fanout count.
pSim[0] = 1;
if ( Abc_LitIsCompl(Lit) )
for ( w = 0; w < nWords; w++ )
pSim[w+1] = ~pValue[w];
else
for ( w = 0; w < nWords; w++ )
pSim[w+1] = pValue[w];
}
/**Function*************************************************************
Synopsis [Refines classes using externally simulated host-object values.]
Description [vLits maps host object IDs to literals in pValues. This entry
point lets an unrolled SRM-side simulator reuse the established
class partitioning code without simulating the host AIG again.]
SideEffects [May split equivalence classes in p->pAig.]
SeeAlso [Cec_ManSimSimulateRound]
***********************************************************************/
int Cec_ManSimRefineMappedFrame( Cec_ManSim_t * p, unsigned * pValues,
Vec_Int_t * vLits, int iBase, int nWords )
{
Gia_Obj_t * pObj;
Vec_Int_t * vHeads = Vec_IntAlloc( 64 );
int i, k, Ent, Lit, nChanges = 0;
assert( Vec_IntSize(vLits) >= iBase + Gia_ManObjNum(p->pAig) );
p->nWords = nWords;
if ( p->nWordsOld != p->nWords )
Cec_ManSimMemRelink( p );
Vec_IntClear( p->vRefinedC );
// Snapshot the current heads before any class is split.
Gia_ManForEachObj1( p->pAig, pObj, i )
if ( Gia_ObjIsHead(p->pAig, i) )
Vec_IntPush( vHeads, i );
// Candidate constants are partitioned by their true simulated values.
Gia_ManForEachObj1( p->pAig, pObj, i )
{
if ( !Gia_ObjIsConst(p->pAig, i) )
continue;
Lit = Vec_IntEntry( vLits, iBase + i );
assert( Lit >= 0 );
Cec_ManSimLoadMappedValue( p, i, pValues, Lit, nWords );
if ( !Cec_ManSimCompareConst(Cec_ObjSim(p, i), nWords) )
Vec_IntPush( p->vRefinedC, i );
else
Cec_ManSimSimDeref( p, i );
}
// Load one class at a time so the simulation manager's recyclable storage
// remains proportional to the largest class rather than to the whole AIG.
Vec_IntForEachEntry( vHeads, i, k )
{
if ( !Gia_ObjIsHead(p->pAig, i) )
continue;
Vec_IntClear( p->vClassTemp );
Gia_ClassForEachObj( p->pAig, i, Ent )
{
Lit = Vec_IntEntry( vLits, iBase + Ent );
assert( Lit >= 0 );
Cec_ManSimLoadMappedValue( p, Ent, pValues, Lit, nWords );
Vec_IntPush( p->vClassTemp, Ent );
}
nChanges += Cec_ManSimClassRefineOne( p, i );
Vec_IntForEachEntry( p->vClassTemp, Ent, Lit )
Cec_ManSimSimDeref( p, Ent );
}
if ( p->pPars->fConstCorr )
{
Vec_IntForEachEntry( p->vRefinedC, i, k )
{
Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
Cec_ManSimSimDeref( p, i );
}
nChanges += Vec_IntSize( p->vRefinedC );
Vec_IntClear( p->vRefinedC );
}
if ( Vec_IntSize(p->vRefinedC) > 0 )
{
nChanges += Vec_IntSize( p->vRefinedC );
Cec_ManSimProcessRefined( p, p->vRefinedC );
}
assert( p->nMems == 1 );
Vec_IntFree( vHeads );
return nChanges;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Refines one equivalence class.] Synopsis [Refines one equivalence class.]
@ -665,7 +770,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) static int Cec_ManSimSimulateRoundInt( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, unsigned * pSave )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
unsigned * pRes0, * pRes1, * pRes; unsigned * pRes0, * pRes1, * pRes;
@ -751,6 +856,12 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
for ( w = 1; w <= p->nWords; w++ ) for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w] & pRes1[w]; pRes[w] = pRes0[w] & pRes1[w];
} }
if ( pSave )
{
unsigned * pWord = pSave + (i >> 5);
unsigned Bit = 1u << (i & 31);
*pWord = (*pWord & ~Bit) | ((pRes[1] & 1) ? Bit : 0);
}
references: references:
// if this node is candidate constant, collect it // if this node is candidate constant, collect it
@ -808,6 +919,17 @@ references:
return Cec_ManSimAnalyzeOutputs( p ); return Cec_ManSimAnalyzeOutputs( p );
} }
int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
{
return Cec_ManSimSimulateRoundInt( p, vInfoCis, vInfoCos, NULL );
}
int Cec_ManSimSimulateRoundSavePhase( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, unsigned * pSave )
{
assert( pSave != NULL );
return Cec_ManSimSimulateRoundInt( p, vInfoCis, vInfoCos, pSave );
}
/**Function************************************************************* /**Function*************************************************************

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

@ -195,6 +195,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
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->fSkipFailResim = 0; // skip resim when a round has no real CEX (only timeout/fail)
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

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

@ -38,7 +38,6 @@ static inline int Cec_ParCorShouldStop( 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 ); 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 ); extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -78,7 +77,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 []
@ -107,7 +106,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 []
@ -224,7 +223,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 []
@ -293,7 +292,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 []
@ -500,6 +499,53 @@ 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.]
@ -541,6 +587,53 @@ 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.]
@ -552,33 +645,104 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames ) static int Cec_ManResimulateCounterExamplesSeed( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, Cec_SeedSim_t * pSeed, Vec_Int_t * vOutputs )
{ {
Vec_Int_t * vPairs; Vec_Int_t * vPairs = NULL;
Vec_Ptr_t * vSimInfo; Vec_Int_t * vOutBits = NULL;
int RetValue = 0, iStart = 0; Vec_Ptr_t * vSimInfo = NULL;
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); int RetValue = 0, iStart = 0, fValueRefs = 0;
Gia_ManCreateValueRefs( pSim->pAig ); if ( pSeed )
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;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords ); if ( pSeed )
{
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) )
{ {
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) ); if ( pSeed )
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); {
// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); int LocalStatus;
// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); iStart = Cec_SeedSimLoadPersistentBatch(
Gia_ManCorrPerformRemapping( vPairs, vSimInfo ); pSeed, vCexStore, iStart, vPairs, vOutBits );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); if ( pSeed->nFallbackCooldown > 0 )
{
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_PtrFree( vSimInfo ); Vec_IntFreeP( &vOutBits );
Vec_IntFree( vPairs ); if ( !pSeed )
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.]
@ -608,12 +772,102 @@ 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 ndoes are proved.] Description [Returns 1 if all nodes are proved.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
@ -803,8 +1057,16 @@ 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, RetValue, i; int fChanges, 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_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;
@ -822,11 +1084,15 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs ); pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs );
Cec_IncrMgrSnapshotClasses( pBmcMgr ); 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 * pTfoMask = NULL;
int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0, fConverged = 0; 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();
@ -835,35 +1101,80 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
// the incremental mask filters on pReprs-derived endpoints only. // the incremental mask filters on pReprs-derived endpoints only.
if ( pBmcMgr && i > 0 ) if ( pBmcMgr && i > 0 )
{ {
pTfoMask = Cec_IncrMgrDecideMask( pBmcMgr, 0, &fConverged, nReprSeeds = Cec_IncrMgrComputeSeeds( pBmcMgr );
&nReprSeeds, NULL, &nTotalPairs, &nActivePairs ); if ( nReprSeeds == 0 )
if ( fConverged ) {
// No pReprs change. BMC SRM topology is unchanged.
break; 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;
} }
if ( pTfoMask ) 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 ); pSrm = Gia_ManCorrSpecReduceInit_Active( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask );
else else
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); 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 ) if ( pTfoMask && pPars->fVeryVerbose )
Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n", Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n",
i, nReprSeeds, nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) ); 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 ) if ( pBmcMgr )
Cec_IncrMgrSnapshotClasses( pBmcMgr ); Cec_IncrMgrSnapshotClasses( pBmcMgr );
if ( Gia_ManPoNum(pSrm) == 0 ) if ( nBmcPos == 0 )
{ {
Gia_ManStop( pSrm ); if ( pSrm )
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
break; break;
} }
pParsSat->nBTLimit *= 10; pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat ) if ( fBmcPersist )
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) )
{ {
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs ); int nCexReal = 0, nCexTriv = 0;
// 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;
} }
@ -872,11 +1183,13 @@ 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 );
Gia_ManStop( pSrm ); if ( 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_IncrMgrFree( pBmcMgr );
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
} }
@ -974,11 +1287,17 @@ 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, RetValue, nPrev[4] = {0}; int r, 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();
Cec_IncrMgr_t * pMgr = NULL; // incremental manager (NULL when -i is off) // 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; abctime clkIncr = 0;
int nIncrSkipped = 0, nIncrFallback = 0; int nIncrSkipped = 0, nIncrFallback = 0;
if ( Gia_ManRegNum(pAig) == 0 ) if ( Gia_ManRegNum(pAig) == 0 )
@ -1011,9 +1330,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.\n", Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d. Incr = %d. Dyn = %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->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat, pPars->fIncremental, pPars->fDynSrm );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
} }
// check the base case // check the base case
@ -1036,19 +1355,31 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames ); pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames );
Cec_IncrMgrSnapshotClasses( pMgr ); 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_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_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;
@ -1058,54 +1389,97 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
clk2 = Abc_Clock(); clk2 = Abc_Clock();
{ {
int * pTfoMask = NULL; int * pTfoMask = NULL;
int nReprSeeds = 0, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0; int nReprSeeds = 0, nNextChanges = 0;
int fConverged = 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 ) if ( pMgr && r > 0 )
{ {
abctime clkI = Abc_Clock(); abctime clkI = Abc_Clock();
pTfoMask = Cec_IncrMgrDecideMask( pMgr, pPars->fUseRings, &fConverged, nReprSeeds = Cec_IncrMgrComputeSeeds( pMgr );
&nReprSeeds, &nNextChanges, nNextChanges = pPars->fUseRings ? Cec_IncrMgrCountNextChanges( pMgr ) : 0;
&nTotalPairs, &nActivePairs ); if ( nReprSeeds == 0 && nNextChanges == 0 )
clkIncr += Abc_Clock() - clkI;
if ( fConverged )
{ {
clkSrm += Abc_Clock() - clk2; // 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; break;
} }
if ( pTfoMask == NULL )
nIncrFallback++;
else else
nIncrSkipped += nTotalPairs - nActivePairs; {
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;
} }
if ( pTfoMask )
pSrm = Gia_ManCorrSpecReduce_Active( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr ); // 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 else
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( pTfoMask && pPars->fVeryVerbose ) if ( pTfoMask && pPars->fVeryVerbose )
Abc_Print( 1, " [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n", 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), r, nReprSeeds, nNextChanges,
nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) ); Vec_IntSize(pMgr->vTfoNodes), nActivePairs, nTotalPairs,
// Snapshot AFTER SRM build: the active builder still reads the fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm) );
// previous pNexts to recognise newly-created ring edges. // 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 ) if ( pMgr )
Cec_IncrMgrSnapshotClasses( pMgr ); Cec_IncrMgrSnapshotClasses( pMgr );
} }
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) ); 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 ( Gia_ManCoNum(pSrm) == 0 ) if ( (fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm)) == 0 )
{ {
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
Gia_ManStop( pSrm ); if ( 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 ( pPars->fUseCSat ) if ( fPersist )
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 );
Gia_ManStop( pSrm ); if ( pSrm )
Gia_ManStop( pSrm );
clkSat += Abc_Clock() - clk2; clkSat += Abc_Clock() - clk2;
if ( Vec_IntSize(vCexStore) == 0 ) if ( Vec_IntSize(vCexStore) == 0 )
{ {
@ -1118,10 +1492,21 @@ 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 ); {
Vec_IntFree( vCexStore ); int nCexReal = 0, nCexTriv = 0;
clkSim += Abc_Clock() - clk2; Cec_ManCexStoreClassify( vCexStore, &nCexReal, &nCexTriv, NULL );
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); if ( nCexReal > 0 || !pPars->fSkipFailResim )
{
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 );
@ -1130,7 +1515,9 @@ 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_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
return 1; return 1;
} }
// quit if const is no longer there // quit if const is no longer there
@ -1140,7 +1527,9 @@ 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_IncrMgrFree( pMgr );
Cec_SeedSimFree( pSeedSim );
return 0; return 0;
} }
if ( pPars->nLimitMax ) if ( pPars->nLimitMax )
@ -1152,7 +1541,9 @@ 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_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;
@ -1185,10 +1576,14 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
ABC_PRTP( "Incr ", clkIncr, clkTotal ); ABC_PRTP( "Incr ", clkIncr, clkTotal );
Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped ); 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_IncrMgrFree( pMgr );
Cec_DynSrmFree( pDynSrm );
Cec_SeedSimFree( pSeedSim );
return 1; return 1;
} }

698
src/proof/cec/cecCorrDyn.c Normal file
View File

@ -0,0 +1,698 @@
/**CFile****************************************************************
FileName [cecCorrDyn.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Dynamic SRM manager for &scorr.]
Author [Xiran Zhao]
Affiliation [University of Chinese Academy of Sciences]
Date [Ver. 1.0. Started - Jun 2026.]
***********************************************************************/
#include "cecInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
struct Cec_DynSrm_t_
{
Gia_Man_t * pAig; // host AIG; owned by caller
Cec_IncrMgr_t * pIncr; // active-list manager; owned by caller
Gia_Man_t * pCore; // persistent SRM core without COs
Cbs_Man_t * pCbs; // resident circuit-SAT manager on pCore
int nCoreObjsAtReset; // real post-build pCore size after the last cold (re)build, for compaction (0 until that build finishes)
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 * vCopyTouched; // core ANDs copied into the current view
Vec_Int_t * vPiMap; // host obj id -> PI index
Vec_Int_t * vRoMap; // host obj id -> RO index
// Phase-2 measurement (behavior-preserving): per-key stamp used to count the
// 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 nPis;
int nRegs;
int nFramesTotal;
int nCoreCiNum;
int nBuilds;
int nBuildsActive;
int nCoreResets;
int nCoreCompactions;
int nCoreBuilds;
int nViewBuilds;
int nCacheFullClears;
int nCacheLocalClears;
int nCacheLocalEntries;
int nOutLitsLast;
int nOutLitsMax;
int nCoreObjsLast;
int nCoreObjsMax;
int nViewObjsLast;
int nViewObjsMax;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// Active-pair selection mirrors incremental mode: a pair is active iff an endpoint is
// 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
// 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
// and incomplete.
static int Cec_DynSrmActiveConst( Cec_DynSrm_t * p, int * pTfoMark, int ObjId )
{
(void)p;
return pTfoMark != NULL && pTfoMark[ObjId];
}
static int Cec_DynSrmActivePair( Cec_DynSrm_t * p, int * pTfoMark, int fRings, int iPrev, int iObj )
{
if ( pTfoMark == NULL )
return 0;
if ( !fRings )
return pTfoMark[iPrev] || pTfoMark[iObj];
return pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( p->pIncr, iPrev, iObj );
}
static int Cec_DynSrmEmitModeAccept( int fActive, Cec_IncrEmitMode_t Mode )
{
return Mode == CEC_EMIT_ALL ||
(Mode == CEC_EMIT_ACTIVE && fActive) ||
(Mode == CEC_EMIT_SKIPPED && !fActive);
}
static int Cec_DynSrmCacheIndex( Cec_DynSrm_t * p, int f, int ObjId )
{
assert( f >= 0 && f < p->nFramesTotal );
assert( ObjId >= 0 && ObjId < p->nObjs );
return f * p->nObjs + ObjId;
}
static int Cec_DynSrmCacheRead( Cec_DynSrm_t * p, int f, Gia_Obj_t * pObj )
{
return Vec_IntEntry( p->vSpecLits, Cec_DynSrmCacheIndex(p, f, Gia_ObjId(p->pAig, pObj)) );
}
static void Cec_DynSrmCacheWrite( Cec_DynSrm_t * p, int f, Gia_Obj_t * pObj, int Lit )
{
Vec_IntWriteEntry( p->vSpecLits, Cec_DynSrmCacheIndex(p, f, Gia_ObjId(p->pAig, pObj)), Lit );
}
static int Cec_DynSrmHostPiLit( Cec_DynSrm_t * p, int f, Gia_Obj_t * pObj )
{
int ObjId = Gia_ObjId( p->pAig, pObj );
int iPi = Vec_IntEntry( p->vPiMap, ObjId );
assert( iPi >= 0 && iPi < p->nPis );
assert( f >= 0 && f < p->nFramesTotal );
return Gia_ManCiLit( p->pCore, p->nRegs + f * p->nPis + iPi );
}
static int Cec_DynSrmHostRoLit( Cec_DynSrm_t * p, Gia_Obj_t * pObj )
{
int ObjId = Gia_ObjId( p->pAig, pObj );
int iRo = Vec_IntEntry( p->vRoMap, ObjId );
assert( iRo >= 0 && iRo < p->nRegs );
return Gia_ManCiLit( p->pCore, iRo );
}
static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
{
if ( p->pCbs ) // stop resident solver before its pCore is freed
Cbs_ManStop( p->pCbs );
p->pCbs = NULL;
if ( p->pCore )
Gia_ManStop( p->pCore );
p->pCore = NULL;
p->nCoreObjsAtReset = 0;
Vec_IntFreeP( &p->vSpecLits );
Vec_IntFreeP( &p->vOutLits );
Vec_IntFreeP( &p->vCopyTouched );
Vec_IntFreeP( &p->vPiMap );
Vec_IntFreeP( &p->vRoMap );
ABC_FREE( p->pTrueMark );
p->nTrueStamp = 0;
p->nObjs = p->nPis = p->nRegs = p->nFramesTotal = p->nCoreCiNum = 0;
}
// pCore is append-only (strash never frees stale nodes from earlier rounds'
// reductions), so under long refinement it grows unboundedly and the resident
// 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
// post-build size; the rebuilt core re-materializes only the live active cones.
#define CEC_DYN_COMPACT_MULT 4
static int Cec_DynSrmShouldCompact( Cec_DynSrm_t * p )
{
// 64-bit multiply: nCoreObjsAtReset can reach tens of millions (the growth
// case this guards), so CEC_DYN_COMPACT_MULT * it must not overflow int.
return p->nCoreObjsAtReset > 0 &&
Gia_ManObjNum(p->pCore) > (ABC_INT64_T)CEC_DYN_COMPACT_MULT * p->nCoreObjsAtReset;
}
static void Cec_DynSrmEnsureCore( Cec_DynSrm_t * p, int nFrames, int fScorr )
{
Gia_Obj_t * pObj;
int f, i, nFramesTotal = nFrames + fScorr;
int fSameShape = ( p->pCore != NULL &&
p->nObjs == Gia_ManObjNum(p->pAig) &&
p->nPis == Gia_ManPiNum(p->pAig) &&
p->nRegs == Gia_ManRegNum(p->pAig) &&
p->nFramesTotal == nFramesTotal );
if ( fSameShape && !Cec_DynSrmShouldCompact(p) )
return;
if ( fSameShape ) // reusable shape but bloated: cold-rebuild
p->nCoreCompactions++;
Cec_DynSrmResetCore( p );
p->nObjs = Gia_ManObjNum( p->pAig );
p->nPis = Gia_ManPiNum( p->pAig );
p->nRegs = Gia_ManRegNum( p->pAig );
p->nFramesTotal = nFramesTotal;
p->vSpecLits = Vec_IntStartFull( p->nFramesTotal * p->nObjs );
p->vOutLits = Vec_IntAlloc( 1000 );
p->vCopyTouched = Vec_IntAlloc( 1000 );
p->vPiMap = 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->pName = Abc_UtilStrsav( p->pAig->pName );
p->pCore->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
Gia_ManHashAlloc( p->pCore );
Gia_ManForEachRo( p->pAig, pObj, i )
{
Vec_IntWriteEntry( p->vRoMap, Gia_ObjId(p->pAig, pObj), i );
Gia_ManAppendCi( p->pCore );
}
Gia_ManForEachPi( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vPiMap, Gia_ObjId(p->pAig, pObj), i );
for ( f = 0; f < p->nFramesTotal; f++ )
Gia_ManForEachPi( p->pAig, pObj, i )
Gia_ManAppendCi( p->pCore );
p->nCoreCiNum = Gia_ManCiNum( p->pCore );
assert( p->nCoreCiNum == p->nRegs + p->nFramesTotal * p->nPis );
// leave nCoreObjsAtReset == 0 (set by ResetCore): only the CIs exist here, the
// live cones are materialized later in BuildCore, so the real post-build size
// is recorded there.
p->nCoreResets++;
}
static void Cec_DynSrmInvalidateCache( Cec_DynSrm_t * p, int * pTfoMask )
{
int f, i, Counter = 0;
assert( p->vSpecLits != NULL );
if ( pTfoMask == NULL )
{
Vec_IntFill( p->vSpecLits, p->nFramesTotal * p->nObjs, -1 );
p->nCacheFullClears++;
return;
}
for ( i = 0; i < p->nObjs; i++ )
{
if ( !pTfoMask[i] )
continue;
for ( f = 0; f < p->nFramesTotal; f++ )
{
Vec_IntWriteEntry( p->vSpecLits, Cec_DynSrmCacheIndex(p, f, i), -1 );
Counter++;
}
}
p->nCacheLocalClears++;
p->nCacheLocalEntries += Counter;
}
static int Cec_DynSrmSpecLit( Cec_DynSrm_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
static int Cec_DynSrmSpecLitInit( Cec_DynSrm_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
static int Cec_DynSrmRealLit( Cec_DynSrm_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
if ( Gia_ObjIsAnd(pObj) )
{
int iLit0 = Cec_DynSrmSpecLit( p, Gia_ObjFanin0(pObj), f, nPrefix );
int iLit1 = Cec_DynSrmSpecLit( p, Gia_ObjFanin1(pObj), f, nPrefix );
iLit0 = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObj) );
iLit1 = Abc_LitNotCond( iLit1, Gia_ObjFaninC1(pObj) );
return Gia_ManHashAnd( p->pCore, iLit0, iLit1 );
}
if ( Gia_ObjIsPi(p->pAig, pObj) )
return Cec_DynSrmHostPiLit( p, f, pObj );
if ( f == 0 )
{
assert( Gia_ObjIsRo(p->pAig, pObj) );
return Cec_DynSrmSpecLit( p, pObj, f, nPrefix );
}
assert( Gia_ObjIsRo(p->pAig, pObj) );
pObj = Gia_ObjRoToRi( p->pAig, pObj );
{
int iLit = Cec_DynSrmSpecLit( p, Gia_ObjFanin0(pObj), f-1, nPrefix );
return Abc_LitNotCond( iLit, Gia_ObjFaninC0(pObj) );
}
}
static int Cec_DynSrmSpecLit( Cec_DynSrm_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
Gia_Obj_t * pRepr;
int iLit;
if ( Gia_ObjIsConst0(pObj) )
return 0;
iLit = Cec_DynSrmCacheRead( p, f, pObj );
if ( iLit >= 0 )
return iLit;
if ( Gia_ObjIsPi(p->pAig, pObj) )
{
iLit = Cec_DynSrmHostPiLit( p, f, pObj );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p->pAig, Gia_ObjId(p->pAig, pObj))) )
{
iLit = Cec_DynSrmSpecLit( p, pRepr, f, nPrefix );
iLit = Abc_LitNotCond( iLit, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
if ( f == 0 && Gia_ObjIsRo(p->pAig, pObj) )
{
iLit = Cec_DynSrmHostRoLit( p, pObj );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
assert( Gia_ObjIsCand(pObj) );
iLit = Cec_DynSrmRealLit( p, pObj, f, nPrefix );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
static int Cec_DynSrmRealLitInit( Cec_DynSrm_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
if ( Gia_ObjIsAnd(pObj) )
{
int iLit0 = Cec_DynSrmSpecLitInit( p, Gia_ObjFanin0(pObj), f, nPrefix );
int iLit1 = Cec_DynSrmSpecLitInit( p, Gia_ObjFanin1(pObj), f, nPrefix );
iLit0 = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObj) );
iLit1 = Abc_LitNotCond( iLit1, Gia_ObjFaninC1(pObj) );
return Gia_ManHashAnd( p->pCore, iLit0, iLit1 );
}
if ( Gia_ObjIsPi(p->pAig, pObj) )
return Cec_DynSrmHostPiLit( p, f, pObj );
if ( f == 0 )
{
assert( Gia_ObjIsRo(p->pAig, pObj) );
return Cec_DynSrmSpecLitInit( p, pObj, f, nPrefix );
}
assert( Gia_ObjIsRo(p->pAig, pObj) );
pObj = Gia_ObjRoToRi( p->pAig, pObj );
{
int iLit = Cec_DynSrmSpecLitInit( p, Gia_ObjFanin0(pObj), f-1, nPrefix );
return Abc_LitNotCond( iLit, Gia_ObjFaninC0(pObj) );
}
}
// BMC/init SRM semantics differ from the inductive SRM in one important way:
// frame-0 ROs are fixed to the all-zero initial state. The core still keeps
// RO CIs first to preserve the CEX-input layout expected by resimulation, but
// these CIs are intentionally unused in init-mode cones.
static int Cec_DynSrmSpecLitInit( Cec_DynSrm_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
Gia_Obj_t * pRepr;
int iLit;
if ( Gia_ObjIsConst0(pObj) )
return 0;
iLit = Cec_DynSrmCacheRead( p, f, pObj );
if ( iLit >= 0 )
return iLit;
if ( Gia_ObjIsPi(p->pAig, pObj) )
{
iLit = Cec_DynSrmHostPiLit( p, f, pObj );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p->pAig, Gia_ObjId(p->pAig, pObj))) )
{
iLit = Cec_DynSrmSpecLitInit( p, pRepr, f, nPrefix );
iLit = Abc_LitNotCond( iLit, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
if ( f == 0 && Gia_ObjIsRo(p->pAig, pObj) )
{
Cec_DynSrmCacheWrite( p, f, pObj, 0 );
return 0;
}
assert( Gia_ObjIsCand(pObj) );
iLit = Cec_DynSrmRealLitInit( p, pObj, f, nPrefix );
Cec_DynSrmCacheWrite( p, f, pObj, iLit );
return iLit;
}
static int Cec_DynSrmCopyLit_rec( Gia_Man_t * pCore, Gia_Man_t * pView, Vec_Int_t * vTouched, int iLit )
{
Gia_Obj_t * pObj;
int iObj, iLitCopy, iLit0, iLit1;
if ( iLit < 2 )
return iLit;
iObj = Abc_Lit2Var( iLit );
pObj = Gia_ManObj( pCore, iObj );
if ( Gia_ObjIsCi(pObj) )
{
assert( Gia_ManCiIdToId(pView, Gia_ObjCioId(pObj)) == iObj );
return iLit;
}
iLitCopy = Gia_ObjCopyArray( pCore, iObj );
if ( iLitCopy >= 0 )
return Abc_LitNotCond( iLitCopy, Abc_LitIsCompl(iLit) );
assert( Gia_ObjIsAnd(pObj) );
iLit0 = Cec_DynSrmCopyLit_rec( pCore, pView, vTouched, Gia_ObjFaninLit0p(pCore, pObj) );
iLit1 = Cec_DynSrmCopyLit_rec( pCore, pView, vTouched, Gia_ObjFaninLit1p(pCore, pObj) );
iLitCopy = Gia_ManHashAnd( pView, iLit0, iLit1 );
Gia_ObjSetCopyArray( pCore, iObj, iLitCopy );
Vec_IntPush( vTouched, iObj );
return Abc_LitNotCond( iLitCopy, Abc_LitIsCompl(iLit) );
}
static Gia_Man_t * Cec_DynSrmBuildView( Cec_DynSrm_t * p )
{
Gia_Man_t * pView;
Gia_Obj_t * pObj;
int i, iLit, iLitCopy;
pView = Gia_ManStart( Abc_MaxInt( p->nCoreCiNum + 100 * Vec_IntSize(p->vOutLits) + 100, 1000 ) );
pView->pName = Abc_UtilStrsav( p->pAig->pName );
pView->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
Gia_ManHashAlloc( pView );
Vec_IntFillExtra( &p->pCore->vCopies, Gia_ManObjNum(p->pCore), -1 );
Vec_IntClear( p->vCopyTouched );
Gia_ManForEachCi( p->pCore, pObj, i )
Gia_ManAppendCi( pView );
Vec_IntForEachEntry( p->vOutLits, iLit, i )
{
iLitCopy = Cec_DynSrmCopyLit_rec( p->pCore, pView, p->vCopyTouched, iLit );
Gia_ManAppendCo( pView, iLitCopy );
}
Vec_IntForEachEntry( p->vCopyTouched, iLit, i )
Gia_ObjSetCopyArray( p->pCore, iLit, -1 );
Vec_IntClear( p->vCopyTouched );
Gia_ManHashStop( pView );
p->nViewBuilds++;
p->nViewObjsLast = Gia_ManObjNum( pView );
p->nViewObjsMax = Abc_MaxInt( p->nViewObjsMax, p->nViewObjsLast );
return pView;
}
Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr )
{
Cec_DynSrm_t * p = ABC_CALLOC( Cec_DynSrm_t, 1 );
p->pAig = pAig;
p->pIncr = pIncr;
return p;
}
void Cec_DynSrmFree( Cec_DynSrm_t * p )
{
if ( p == NULL )
return;
Cec_DynSrmResetCore( p );
ABC_FREE( p );
}
void Cec_DynSrmPrintStats( Cec_DynSrm_t * p )
{
if ( p == NULL )
return;
Abc_Print( 1, "DynSRM: builds = %d, active_builds = %d\n",
p->nBuilds, p->nBuildsActive );
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->nCoreResets, p->nCoreCompactions, p->nCoreBuilds, p->nViewBuilds,
p->nOutLitsLast, p->nOutLitsMax,
p->nCoreObjsLast, p->nCoreObjsMax,
p->nViewObjsLast, p->nViewObjsMax );
Abc_Print( 1, "DynSRM: cache_full_clears = %d, cache_local_clears = %d, cache_local_entries = %d\n",
p->nCacheFullClears, p->nCacheLocalClears, p->nCacheLocalEntries );
}
void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark,
int * pnTotal, int * pnActive )
{
Gia_Man_t * pAig = p->pAig;
Gia_Obj_t * pObj, * pRepr;
int i, iPrev, iObj;
*pnTotal = *pnActive = 0;
assert( pAig->pReprs != NULL );
if ( fRings )
{
Gia_ManForEachObj1( pAig, pObj, i )
{
if ( Gia_ObjIsConst( pAig, i ) )
{
(*pnTotal)++;
(*pnActive) += Cec_DynSrmActiveConst( p, pTfoMark, i );
}
else if ( Gia_ObjIsHead( pAig, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( pAig, i, iObj )
{
(*pnTotal)++;
(*pnActive) += Cec_DynSrmActivePair( p, pTfoMark, 1, iPrev, iObj );
iPrev = iObj;
}
iObj = i;
{
(*pnTotal)++;
(*pnActive) += Cec_DynSrmActivePair( p, pTfoMark, 1, iPrev, iObj );
}
}
}
}
else
{
Gia_ManForEachObj1( pAig, pObj, i )
{
int idR;
pRepr = Gia_ObjReprObj( pAig, Gia_ObjId(pAig,pObj) );
if ( pRepr == NULL )
continue;
idR = Gia_ObjId( pAig, pRepr );
(*pnTotal)++;
(*pnActive) += Cec_DynSrmActivePair( p, pTfoMark, 0, idR, i );
}
}
}
// Builds (or extends) the persistent COless pCore and selects this round's
// active-pair root literals into p->vOutLits / *pvOutputs. Shared by the view
// path (Cec_DynSrmBuild) and the persistent path (solve pCore directly).
void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode )
{
Gia_Obj_t * pObj, * pRepr;
int i, iPrev, iObj, iPrevNew, iObjNew, iPrevRaw, iObjRaw;
assert( p != NULL );
assert( nFrames > 0 );
assert( Gia_ManRegNum(p->pAig) > 0 );
assert( p->pAig->pReprs != NULL );
assert( Mode == CEC_EMIT_ALL || pTfoMask != NULL );
p->nBuilds++;
if ( Mode == CEC_EMIT_ACTIVE )
p->nBuildsActive++;
Cec_DynSrmEnsureCore( p, nFrames, fScorr );
Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask );
Gia_ManSetPhase( p->pAig );
*pvOutputs = Vec_IntAlloc( 1000 );
Vec_IntClear( p->vOutLits );
if ( fRings )
{
Gia_ManForEachObj1( p->pAig, pObj, i )
{
if ( Gia_ObjIsConst( p->pAig, i ) )
{
int fActive = Cec_DynSrmActiveConst( p, pTfoMask, i );
if ( !Cec_DynSrmEmitModeAccept(fActive, Mode) )
continue;
iObjRaw = Cec_DynSrmRealLit( p, pObj, nFrames, 0 );
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
{
Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i );
Vec_IntPush( p->vOutLits, iObjNew );
}
}
else if ( Gia_ObjIsHead( p->pAig, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( p->pAig, i, iObj )
{
int fActive = Cec_DynSrmActivePair( p, pTfoMask, 1, iPrev, iObj );
if ( Cec_DynSrmEmitModeAccept(fActive, Mode) )
{
iPrevRaw = Cec_DynSrmRealLit( p, Gia_ManObj(p->pAig, iPrev), nFrames, 0 );
iObjRaw = Cec_DynSrmRealLit( p, Gia_ManObj(p->pAig, iObj), nFrames, 0 );
iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p->pAig, iPrev)) );
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p->pAig, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( p->vOutLits, Gia_ManHashAnd(p->pCore, iPrevNew, Abc_LitNot(iObjNew)) );
}
}
iPrev = iObj;
}
iObj = i;
{
int fActive = Cec_DynSrmActivePair( p, pTfoMask, 1, iPrev, iObj );
if ( Cec_DynSrmEmitModeAccept(fActive, Mode) )
{
iPrevRaw = Cec_DynSrmRealLit( p, Gia_ManObj(p->pAig, iPrev), nFrames, 0 );
iObjRaw = Cec_DynSrmRealLit( p, Gia_ManObj(p->pAig, iObj), nFrames, 0 );
iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p->pAig, iPrev)) );
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p->pAig, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( p->vOutLits, Gia_ManHashAnd(p->pCore, iPrevNew, Abc_LitNot(iObjNew)) );
}
}
}
}
}
}
else
{
Gia_ManForEachObj1( p->pAig, pObj, i )
{
pRepr = Gia_ObjReprObj( p->pAig, Gia_ObjId(p->pAig,pObj) );
if ( pRepr == NULL )
continue;
{
int idR = Gia_ObjId(p->pAig, pRepr);
int fActive = Cec_DynSrmActivePair( p, pTfoMask, 0, idR, i );
if ( !Cec_DynSrmEmitModeAccept(fActive, Mode) )
continue;
}
iPrevRaw = Gia_ObjIsConst(p->pAig, i)? 0 : Cec_DynSrmRealLit( p, pRepr, nFrames, 0 );
iObjRaw = Cec_DynSrmRealLit( p, pObj, nFrames, 0 );
iPrevNew = iPrevRaw;
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p->pAig, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p->pAig, pObj) );
Vec_IntPush( p->vOutLits, Gia_ManHashXor(p->pCore, iPrevNew, iObjNew) );
}
}
}
p->nCoreBuilds++;
p->nOutLitsLast = Vec_IntSize( p->vOutLits );
p->nOutLitsMax = Abc_MaxInt( p->nOutLitsMax, p->nOutLitsLast );
p->nCoreObjsLast = Gia_ManObjNum( p->pCore );
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->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast );
}
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 )
{
Cec_DynSrmBuildCore( p, nFrames, fScorr, pvOutputs, fRings, pTfoMask, Mode );
return Cec_DynSrmBuildView( p );
}
// BMC/init variant of Cec_DynSrmBuildCore. It mirrors
// Gia_ManCorrSpecReduceInit(): ROs at frame 0 are constants, representatives
// are applied only at frames >= nPrefix, and every BMC endpoint frame in
// [nPrefix, nPrefix+nFrames) emits the current (repr,obj) candidates.
void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr,
Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode )
{
Gia_Obj_t * pObj, * pRepr;
int f, i, iPrevNew, iObjNew;
assert( p != NULL );
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p->pAig) > 0 );
assert( p->pAig->pReprs != NULL );
assert( Mode == CEC_EMIT_ALL || pTfoMask != NULL );
p->nBuilds++;
if ( Mode == CEC_EMIT_ACTIVE )
p->nBuildsActive++;
Cec_DynSrmEnsureCore( p, nFrames + nPrefix, fScorr );
Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask );
Gia_ManSetPhase( p->pAig );
*pvOutputs = Vec_IntAlloc( 1000 );
Vec_IntClear( p->vOutLits );
for ( f = nPrefix; f < nFrames + nPrefix; f++ )
{
Gia_ManForEachObj1( p->pAig, pObj, i )
{
pRepr = Gia_ObjReprObj( p->pAig, Gia_ObjId(p->pAig,pObj) );
if ( pRepr == NULL )
continue;
{
int idR = Gia_ObjId(p->pAig, pRepr);
int fActive = pTfoMask != NULL && (pTfoMask[i] || pTfoMask[idR]);
if ( !Cec_DynSrmEmitModeAccept(fActive, Mode) )
continue;
}
iPrevNew = Gia_ObjIsConst(p->pAig, i)? 0 : Cec_DynSrmRealLitInit( p, pRepr, f, nPrefix );
iObjNew = Cec_DynSrmRealLitInit( p, pObj, f, nPrefix );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p->pAig, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p->pAig, pObj) );
Vec_IntPush( p->vOutLits, Gia_ManHashXor(p->pCore, iPrevNew, iObjNew) );
}
}
}
p->nCoreBuilds++;
p->nOutLitsLast = Vec_IntSize( p->vOutLits );
p->nOutLitsMax = Abc_MaxInt( p->nOutLitsMax, p->nOutLitsLast );
p->nCoreObjsLast = Gia_ManObjNum( p->pCore );
if ( p->nCoreObjsAtReset == 0 )
p->nCoreObjsAtReset = p->nCoreObjsLast;
p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast );
}
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 )
{
Cec_DynSrmBuildCoreInit( p, nFrames, nPrefix, fScorr, pvOutputs, pTfoMask, Mode );
return Cec_DynSrmBuildView( p );
}
// This round's active-pair root literals (used by the main loop for counts).
Vec_Int_t * Cec_DynSrmOutLits( Cec_DynSrm_t * p ) { return p->vOutLits; }
// Solves this round's root literals on the persistent pCore with the resident
// 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 ->
// 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 )
{
assert( Gia_ManRegNum(p->pCore) == 0 );
assert( Gia_ManCiNum(p->pCore) == p->nRegs + p->nFramesTotal * p->nPis );
if ( p->pCbs == NULL )
p->pCbs = Cbs_ManAlloc( p->pCore );
Cbs_ManSetConflictNum( p->pCbs, nConfs );
return Cbs_ManSolveRoots( p->pCbs, p->vOutLits, pvStatus, 0 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -50,6 +50,8 @@ Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames )
p->vSeeds = Vec_IntAlloc( 64 ); p->vSeeds = Vec_IntAlloc( 64 );
p->vTfoNodes = Vec_IntAlloc( 1024 ); p->vTfoNodes = Vec_IntAlloc( 1024 );
p->pTfoMark = ABC_CALLOC( int, p->nObjs ); p->pTfoMark = ABC_CALLOC( int, p->nObjs );
p->vAliasHeads = Vec_IntStartFull( p->nObjs );
p->vAliasNext = Vec_IntStartFull( p->nObjs );
p->vBfsCur = Vec_IntAlloc( 1024 ); p->vBfsCur = Vec_IntAlloc( 1024 );
p->vBfsNext = Vec_IntAlloc( 1024 ); p->vBfsNext = Vec_IntAlloc( 1024 );
if ( pAig->vFanout == NULL ) if ( pAig->vFanout == NULL )
@ -82,6 +84,8 @@ void Cec_IncrMgrFree( Cec_IncrMgr_t * p )
Vec_IntFree( p->vNextPrev ); Vec_IntFree( p->vNextPrev );
Vec_IntFree( p->vSeeds ); Vec_IntFree( p->vSeeds );
Vec_IntFree( p->vTfoNodes ); Vec_IntFree( p->vTfoNodes );
Vec_IntFree( p->vAliasHeads );
Vec_IntFree( p->vAliasNext );
Vec_IntFree( p->vBfsCur ); Vec_IntFree( p->vBfsCur );
Vec_IntFree( p->vBfsNext ); Vec_IntFree( p->vBfsNext );
ABC_FREE( p->pTfoMark ); ABC_FREE( p->pTfoMark );
@ -120,12 +124,13 @@ void Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p )
Synopsis [Computes the seed set for the next TFO BFS.] Synopsis [Computes the seed set for the next TFO BFS.]
Description [Returns the number of nodes whose representative changed Description [Returns the number of nodes whose representative changed
since the last snapshot; the seeds themselves are stored in vSeeds and since the last snapshot and stores them in vSeeds. Does not update
consumed by Cec_IncrMgrComputeTfo. Does not update the snapshot -- the snapshot.
the caller decides when to snapshot. pNexts changes are intentionally
excluded here: a ring-link rewrite is an edge-local event that creates pNexts changes are intentionally excluded here: a ring-link rewrite is
a new ring edge to reprove, not a new fanout cone, so it is handled by an edge-local event that creates a new ring edge to reprove, not a new
Cec_IncrMgrRingEdgeChanged at SRM emission time.] fanout cone, so it is handled by Cec_IncrMgrRingEdgeChanged at SRM
emission time.]
SideEffects [] SideEffects []
@ -231,7 +236,7 @@ int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj )
SideEffects [] SideEffects []
SeeAlso [Gia_ManCorrSpecReduce_Active] SeeAlso [Gia_ManCorrSpecReduce_Emit]
***********************************************************************/ ***********************************************************************/
void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark,
@ -287,12 +292,17 @@ void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark,
Synopsis [Forward TFO BFS from seeds across nFrames unrollings.] Synopsis [Forward TFO BFS from seeds across nFrames unrollings.]
Description [Marks pTfoMark[id]=1 for every AIG node reachable from Description [Marks pTfoMark[id]=1 for every SRM node reachable from
any seed within nFrames combinational+sequential steps. Each frame any seed within nFrames combinational+sequential steps. Besides AIG
performs a combinational fanout BFS; RI fanouts cross to the next fanouts, the walk follows representative-to-member alias edges because
frame by following Gia_ObjRiToRo to the corresponding register output. Gia_ManCorrSpecReduce_rec(member) uses repr(member) directly. Missing
After nFrames cross-frame jumps the search stops, since pairs deeper these edges can reuse an obsolete UNSAT result when a representative's
than that cannot depend on the seeds within an nFrames-deep SRM. reduced value changes through another member's fanout cone.
Each frame performs a combinational fanout BFS; RI fanouts cross to the
next frame by following Gia_ObjRiToRo to the corresponding register
output. After nFrames cross-frame jumps the search stops, since pairs
deeper than that cannot depend on the seeds within an nFrames-deep SRM.
RI nodes themselves are intentionally not marked: SRM emission is RI nodes themselves are intentionally not marked: SRM emission is
keyed on AIG candidate nodes (ANDs and CIs) and never on COs, so keyed on AIG candidate nodes (ANDs and CIs) and never on COs, so
@ -313,7 +323,7 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p )
{ {
Gia_Man_t * pAig = p->pAig; Gia_Man_t * pAig = p->pAig;
int * pMark = p->pTfoMark; int * pMark = p->pTfoMark;
int f, i, k, Id, FanId, RoId; int f, i, k, Id, FanId, RoId, ReprId, AliasId;
Vec_IntForEachEntry( p->vTfoNodes, Id, i ) Vec_IntForEachEntry( p->vTfoNodes, Id, i )
pMark[Id] = 0; pMark[Id] = 0;
@ -321,6 +331,17 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p )
Vec_IntClear( p->vBfsCur ); Vec_IntClear( p->vBfsCur );
Vec_IntClear( p->vBfsNext ); Vec_IntClear( p->vBfsNext );
Vec_IntFill( p->vAliasHeads, p->nObjs, -1 );
Vec_IntFill( p->vAliasNext, p->nObjs, -1 );
for ( Id = 1; Id < p->nObjs; Id++ )
{
ReprId = Gia_ObjRepr( pAig, Id );
if ( ReprId <= 0 || ReprId == GIA_VOID )
continue;
Vec_IntWriteEntry( p->vAliasNext, Id, Vec_IntEntry(p->vAliasHeads, ReprId) );
Vec_IntWriteEntry( p->vAliasHeads, ReprId, Id );
}
Vec_IntForEachEntry( p->vSeeds, Id, i ) Vec_IntForEachEntry( p->vSeeds, Id, i )
{ {
if ( !pMark[Id] ) if ( !pMark[Id] )
@ -338,6 +359,16 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p )
{ {
Gia_Obj_t * pFan; Gia_Obj_t * pFan;
Id = Vec_IntEntry( p->vBfsCur, head++ ); Id = Vec_IntEntry( p->vBfsCur, head++ );
for ( AliasId = Vec_IntEntry(p->vAliasHeads, Id);
AliasId >= 0;
AliasId = Vec_IntEntry(p->vAliasNext, AliasId) )
{
if ( pMark[AliasId] )
continue;
pMark[AliasId] = 1;
Vec_IntPush( p->vTfoNodes, AliasId );
Vec_IntPush( p->vBfsCur, AliasId );
}
int nFan = Gia_ObjFanoutNumId( pAig, Id ); int nFan = Gia_ObjFanoutNumId( pAig, Id );
for ( k = 0; k < nFan; k++ ) for ( k = 0; k < nFan; k++ )
{ {
@ -381,39 +412,37 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Active-filter variant of Gia_ManCorrSpecReduce.] Synopsis [Emission-filtered variant of Gia_ManCorrSpecReduce.]
Description [Identical to Gia_ManCorrSpecReduce in its SRM topology Description [Identical to Gia_ManCorrSpecReduce in its SRM topology
and speculative reduction; the only difference is the PO emission and speculative reduction; the only difference is PO emission.
filter. A candidate pair (a, b) is emitted iff pTfoMark[a] is set CEC_EMIT_ACTIVE emits pairs selected by the incremental TFO filter.
or pTfoMark[b] is set, i.e. at least one endpoint lies in the TFO of CEC_EMIT_SKIPPED emits the exact complement for shadow validation.
a recently-changed representative. In ring mode, a ring edge that is A new or rewired ring edge is always active and can never be emitted
new or rewired since the last snapshot (Cec_IncrMgrRingEdgeChanged) as skipped because it has no prior UNSAT result to reuse.
is also emitted even if neither endpoint is in the TFO -- the edge
has no prior UNSAT result to reuse and must be reproved on its own.
Walking the full ring is required (rather than skipping unmarked Walking the full ring is required (rather than skipping unmarked
members) so iPrev stays aligned with the live class order; the active members) so iPrev stays aligned with the live class order; the active
filter only suppresses the resulting PO when the edge is provably predicate is evaluated only after the edge endpoints are known.]
not new and neither endpoint is reachable from a seed. Passing
pTfoMark == NULL falls back to the unfiltered baseline behaviour.]
SideEffects [] SideEffects []
SeeAlso [Gia_ManCorrSpecReduce] SeeAlso [Gia_ManCorrSpecReduce Cec_IncrMgrCountActivePairs]
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr, Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
Vec_Int_t ** pvOutputs, int fRings, Vec_Int_t ** pvOutputs, int fRings,
int * pTfoMark, Cec_IncrMgr_t * pIncr ) int * pTfoMark, Cec_IncrMgr_t * pIncr,
Cec_IncrEmitMode_t Mode, Vec_Int_t ** pvOutLits )
{ {
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr; Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits; Vec_Int_t * vXorLits;
int f, i, iPrev, iObj, iPrevNew, iObjNew; int f, i, iPrev, iObj, iPrevNew, iObjNew, iPrevRaw, iObjRaw;
assert( nFrames > 0 ); assert( nFrames > 0 );
assert( Gia_ManRegNum(p) > 0 ); assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL ); assert( p->pReprs != NULL );
assert( Mode == CEC_EMIT_ALL || pTfoMark != NULL );
Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 ); Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
@ -433,6 +462,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
} }
*pvOutputs = Vec_IntAlloc( 1000 ); *pvOutputs = Vec_IntAlloc( 1000 );
if ( pvOutLits )
*pvOutLits = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 );
if ( fRings ) if ( fRings )
{ {
@ -440,14 +471,23 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr
{ {
if ( Gia_ObjIsConst( p, i ) ) if ( Gia_ObjIsConst( p, i ) )
{ {
if ( pTfoMark && !pTfoMark[i] ) int fActive = pTfoMark != NULL && pTfoMark[i];
int fEmit = Mode == CEC_EMIT_ALL ||
(Mode == CEC_EMIT_ACTIVE && fActive) ||
(Mode == CEC_EMIT_SKIPPED && !fActive);
if ( !fEmit )
continue; continue;
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 ) if ( iObjNew != 0 )
{ {
Vec_IntPush( *pvOutputs, 0 ); Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i ); Vec_IntPush( *pvOutputs, i );
if ( pvOutLits )
{
Vec_IntPush( *pvOutLits, 0 );
Vec_IntPush( *pvOutLits, iObjRaw );
}
Vec_IntPush( vXorLits, iObjNew ); Vec_IntPush( vXorLits, iObjNew );
} }
} }
@ -459,18 +499,27 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr
iPrev = i; iPrev = i;
Gia_ClassForEachObj1( p, i, iObj ) Gia_ClassForEachObj1( p, i, iObj )
{ {
int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] || int fActive = pTfoMark != NULL &&
Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ); (pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ));
int fEmit = Mode == CEC_EMIT_ALL ||
(Mode == CEC_EMIT_ACTIVE && fActive) ||
(Mode == CEC_EMIT_SKIPPED && !fActive);
if ( fEmit ) if ( fEmit )
{ {
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Abc_LitNotCond( iPrevNew, 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( iObjNew, 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 )
{ {
Vec_IntPush( *pvOutputs, iPrev ); Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj ); Vec_IntPush( *pvOutputs, iObj );
if ( pvOutLits )
{
Vec_IntPush( *pvOutLits, iPrevRaw );
Vec_IntPush( *pvOutLits, iObjRaw );
}
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) ); Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
} }
} }
@ -479,18 +528,27 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr
// Closing edge tail -> head // Closing edge tail -> head
iObj = i; iObj = i;
{ {
int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] || int fActive = pTfoMark != NULL &&
Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ); (pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ));
int fEmit = Mode == CEC_EMIT_ALL ||
(Mode == CEC_EMIT_ACTIVE && fActive) ||
(Mode == CEC_EMIT_SKIPPED && !fActive);
if ( fEmit ) if ( fEmit )
{ {
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Abc_LitNotCond( iPrevNew, 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( iObjNew, 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 )
{ {
Vec_IntPush( *pvOutputs, iPrev ); Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj ); Vec_IntPush( *pvOutputs, iObj );
if ( pvOutLits )
{
Vec_IntPush( *pvOutLits, iPrevRaw );
Vec_IntPush( *pvOutLits, iObjRaw );
}
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) ); Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
} }
} }
@ -505,19 +563,28 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL ) if ( pRepr == NULL )
continue; continue;
if ( pTfoMark )
{ {
int idR = Gia_ObjId(p, pRepr); int idR = Gia_ObjId(p, pRepr);
if ( !pTfoMark[i] && !pTfoMark[idR] ) int fActive = pTfoMark != NULL && (pTfoMark[i] || pTfoMark[idR]);
int fEmit = Mode == CEC_EMIT_ALL ||
(Mode == CEC_EMIT_ACTIVE && fActive) ||
(Mode == CEC_EMIT_SKIPPED && !fActive);
if ( !fEmit )
continue; continue;
} }
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); iPrevRaw = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iPrevNew = iPrevRaw;
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew ) if ( iPrevNew != iObjNew )
{ {
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
if ( pvOutLits )
{
Vec_IntPush( *pvOutLits, iPrevRaw );
Vec_IntPush( *pvOutLits, iObjRaw );
}
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
} }
} }
@ -528,6 +595,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr
Gia_ManHashStop( pNew ); Gia_ManHashStop( pNew );
Vec_IntErase( &p->vCopies ); Vec_IntErase( &p->vCopies );
pNew = Gia_ManCleanup( pTemp = pNew ); pNew = Gia_ManCleanup( pTemp = pNew );
if ( pvOutLits )
Gia_ManDupRemapLiterals( *pvOutLits, pTemp );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
return pNew; return pNew;
} }
@ -614,59 +683,6 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nP
return pNew; return pNew;
} }
/**Function*************************************************************
Synopsis [One-shot incremental decision for the refinement loop.]
Description [Computes seeds, runs the TFO BFS, counts active candidate
pairs, and applies the fallback heuristic. Returns the TFO mask to
pass to the active SRM builder, or NULL when either (a) classes have
converged since the last snapshot (in which case *pfConverged is set
to 1 and the caller should break the refinement loop), or (b) the
active-pair ratio is high enough that the full SRM is cheaper. The
out parameters pnReprSeeds / pnNextChanges / pnTotalPairs /
pnActivePairs are filled when non-NULL and are useful for verbose
printing and progress counters. fUseRings tells the helper whether
to track pNexts changes; the BMC SRM is non-ring and passes 0.]
SideEffects []
SeeAlso [Cec_IncrMgrComputeSeeds Cec_IncrMgrComputeTfo
Cec_IncrMgrCountActivePairs]
***********************************************************************/
int * Cec_IncrMgrDecideMask( Cec_IncrMgr_t * p, int fUseRings, int * pfConverged,
int * pnReprSeeds, int * pnNextChanges,
int * pnTotalPairs, int * pnActivePairs )
{
int nReprSeeds, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0;
*pfConverged = 0;
nReprSeeds = Cec_IncrMgrComputeSeeds( p );
if ( fUseRings )
nNextChanges = Cec_IncrMgrCountNextChanges( p );
if ( pnReprSeeds ) *pnReprSeeds = nReprSeeds;
if ( pnNextChanges ) *pnNextChanges = nNextChanges;
if ( nReprSeeds == 0 && nNextChanges == 0 )
{
*pfConverged = 1;
return NULL;
}
Cec_IncrMgrComputeTfo( p );
Cec_IncrMgrCountActivePairs( p, fUseRings, p->pTfoMark, &nTotalPairs, &nActivePairs );
if ( pnTotalPairs ) *pnTotalPairs = nTotalPairs;
if ( pnActivePairs ) *pnActivePairs = nActivePairs;
if ( nActivePairs == 0 )
{
*pfConverged = 1;
return NULL;
}
// Above ~70% active pairs, the mask plus emission filter costs more
// than just rebuilding the full SRM. Return NULL to signal fallback.
if ( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs )
return NULL;
return p->pTfoMark;
}
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_END
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

2040
src/proof/cec/cecCorrIncrSim.c Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -174,14 +174,183 @@ struct Cec_IncrMgr_t_
int nObjs; // cached Gia_ManObjNum(pAig) int nObjs; // cached Gia_ManObjNum(pAig)
Vec_Int_t * vReprPrev; // snapshot of pReprs from previous round Vec_Int_t * vReprPrev; // snapshot of pReprs from previous round
Vec_Int_t * vNextPrev; // snapshot of pNexts from previous round Vec_Int_t * vNextPrev; // snapshot of pNexts from previous round
Vec_Int_t * vSeeds; // nodes whose pReprs changed since snapshot Vec_Int_t * vSeeds; // repr-change TFO seeds
Vec_Int_t * vTfoNodes; // ids currently in TFO (for fast clearing) Vec_Int_t * vTfoNodes; // ids currently in TFO (for fast clearing)
int * pTfoMark; // dense mark array, size = nObjs int * pTfoMark; // dense mark array, size = nObjs
Vec_Int_t * vAliasHeads; // repr -> first member using it in the SRM
Vec_Int_t * vAliasNext; // next member with the same representative
Vec_Int_t * vBfsCur; // BFS frontier for current frame Vec_Int_t * vBfsCur; // BFS frontier for current frame
Vec_Int_t * vBfsNext; // BFS frontier carried to next frame Vec_Int_t * vBfsNext; // BFS frontier carried to next frame
int fOwnsFanout; // 1 if we built static fanout (must free) int fOwnsFanout; // 1 if we built static fanout (must free)
}; };
typedef enum Cec_IncrEmitMode_t_
{
CEC_EMIT_ALL,
CEC_EMIT_ACTIVE,
CEC_EMIT_SKIPPED
} Cec_IncrEmitMode_t;
// Persistent event-driven simulation manager for &scorr incremental mode.
// Packed input patterns and host-AIG values survive across CEX batches. A
// batch records only the input words it changes; real value deltas propagate
// through the frame-aware fanout graph and dirty classes are fully regrouped.
//
// Keying uses key = frame*nObjs + objId. pVal layout:
// pVal[(frame * nObjs + objId) * nWords + w]
typedef struct Cec_SeedSim_t_ Cec_SeedSim_t;
struct Cec_SeedSim_t_
{
Gia_Man_t * pAig; // host AIG (immutable across iterations)
int nFrames; // total unrolling depth used by resim
int iSeedFrame; // frame where SAT proved the endpoint pair
int nObjs; // cached Gia_ManObjNum(pAig)
int nPis; // cached Gia_ManPiNum(pAig)
int nRegs; // cached Gia_ManRegNum(pAig)
int nWords; // sim words per key (= pSim->pPars->nWords)
int nPhaseWords; // bitset words per frame for persistent phase anchors
int fInitialized; // persistent inputs/values have a refined baseline
// Dense persistent value storage.
unsigned * pVal; // size = (size_t)nFrames * nObjs * nWords
unsigned * pPhase; // size = (size_t)nFrames * nPhaseWords
unsigned * pActiveMask; // all packed simulation lanes except phase bit 0
unsigned * pCexMask; // packed real-CEX lanes used for diagnosis coverage
unsigned * pRefineMask; // non-owning mask selected for current regrouping phase
unsigned * pFoundMask; // CEX lanes explained by a real host-AIG split
unsigned * pDiffMask; // nWords scratch for signature differences
unsigned * pTempMask; // nWords scratch
// Dense per-key state.
int * pMark; // split-TFO visited stamp, size = nFrames * nObjs
int * pSpecMark; // sparse speculative-mask record index plus one
int * pDiagMark; // sparse diagnosis record index plus one
int * pSplitMark; // real-split worklist stamp
int * pProcessMark; // split-TFO key already refined stamp
int * pEvalMark; // current-input value version stamp
int nMarkVersion;
int nSplitVersion;
int nProcessVersion;
int nEvalVersion;
int nSpecKeys; // unrolled keys visited by speculative diagnosis
int nEvalKeys; // keys evaluated from current inputs this batch
Vec_Int_t * vDiagPairs; // failed host pairs as triples (obj0, obj1, bit)
Vec_Int_t * vSpecKeys; // sparse speculative-TFI keys
Vec_Int_t * vSpecMasks; // flat [spec record][word] lane masks
Vec_Int_t * vDiagKeys; // sparse speculative assumptions/failed endpoints
Vec_Int_t * vDiagRoots; // original class root for each diagnosis record
Vec_Int_t * vDiagMasks; // flat [diagnosis record][word] lane masks
Vec_Int_t * vSplitKeys; // nodes in classes actually split by current CEX
Vec_Int_t * vDirtyKeys; // keys reached by split-driven TFO
Vec_Int_t * vWaveKeys; // newly reached TFO keys awaiting refinement
Vec_Int_t * vQueue; // split-TFO BFS frontier
Vec_Ptr_t * vSimInfo; // reusable full-simulation CI storage
Vec_Ptr_t * vBatchInfo; // non-owning current packed CEX input vectors
// Persistent CEX packing and event propagation.
unsigned * pPackPres; // sparse-cleared assignment-presence words
int * pInputUndoMark; // input word already journaled this batch
int * pInputVarMark; // input vector already queued this batch
int nInputUndoVersion;
int nInputVarVersion;
Vec_Int_t * vPackTouched; // flat input words to clear after packing
Vec_Int_t * vInputUndo; // pairs (flat input word, old value)
Vec_Int_t * vChangedInputs; // input vector indices changed by this batch
Vec_Int_t * vValueUndo; // triples (key, word, old value)
Vec_Int_t * vChangedValues; // keys whose persistent value really changed
unsigned * pEventWords; // sparse queued-word masks, indexed by key
int nEventMaskWords; // words needed to represent nWords bits
int nEventPops; // evaluated node-word operations
int nEventEdges; // traversed fanout word-edges
// Frame-aware class-cone filter. When enabled, event propagation only
// visits keys in the true TFI of current class/constant candidates.
unsigned * pCone; // bitset indexed by key = frame*nObjs+objId
int nConeWords; // bitset words for pCone
int nConeKeys; // marked keys in the current cone
int fUseCone; // 1 after pCone was built for this resim call
Vec_Int_t * vConeQueue; // newly marked keys used to class-close pCone
int * pConeClose; // (frame,root) stamp: class already closed this build
int nConeCloseVer; // version for pConeClose
int nFallbackStreak; // persists across resimulation calls
int nFallbackCooldown; // batches bypassed before next event probe
// Class-refinement scratch.
int * pRootMark; // per-objId "root already queued" stamp
int nRootVersion;
Vec_Int_t * vDirtyRoots;
Vec_Int_t * vConstRefined;
Vec_Int_t * vClassAll;
Vec_Int_t * vClassOld;
Vec_Int_t * vClassNew;
// Sparse undo journal for diagnosis-time class refinement.
int * pTxnMark; // object already saved in the current transaction
int nTxnVersion;
int fTxnActive;
Vec_Int_t * vTxnObjs;
Vec_Int_t * vTxnReprs;
Vec_Int_t * vTxnNexts;
unsigned * pPhase0; // nWords of 0 (phase-0 vector, used by refine)
unsigned * pPhase1; // nWords of ~0 (phase-1 vector)
int fOwnsFanout; // 1 if we built static fanout (must free)
// Profile counters (reset per resim call)
int nBatchLocal; // rounds handled by local TFO sim
int nBatchFull; // rounds that fell back to full sweep
int nBatchTrunc; // local rounds that stopped optional TFO expansion
int nBatchRollback; // diagnosis transactions rolled back before full sweep
int nRollbackObjs; // class entries restored by transaction rollback
int nCoverageMiss; // packed CEX lanes unexplained by local diagnosis
int nFallbackPre; // fallback before diagnosis mutates classes
int nFallbackProcess; // fallback because diagnosis evaluation exceeded budget
int nFallbackCoverage; // fallback because diagnosis did not explain all CEX lanes
int nFallbackCex; // cheap rejection of oversized packed CEX batches
int nFallbackBypass; // batches sent directly to full after repeated fallback
int nTruncCone; // local TFO stopped while growing the structural cone
int nTruncEval; // local TFO stopped while evaluating/refining the cone
int nBatchCex; // total real CEX records across packed batches
int nBatchCexMax; // largest real-CEX count in one packed batch
int nDeferredSplits; // TFO-created splits not re-enqueued in fixed-frontier mode
int nMaxDirty; // largest TFO/evaluated closure across this call
int nEventLocal; // batches completed by value-delta propagation
int nEventFallback; // batches whose event budget was exceeded
int nEventPopsMax; // largest number of evaluated event nodes
int nEventEdgesMax; // largest number of traversed fanout edges
int nEventInputVarsMax; // largest changed-CI count in one batch
int nEventInputWordsMax; // largest changed-CI-word count in one batch
int nEventFallbackWork; // structural word-operation budget exceeded
};
// Dynamic SRM construction manager for &scorr incremental mode. It keeps the
// speculative SRM core used by SAT.
typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
// Recursive diagnosis has a much higher constant factor than a linear sweep.
// Reject wide speculative and complete-class evaluation cones before mutation.
#define CEC_SEEDSIM_DIAG_FRAC_NUM 1
#define CEC_SEEDSIM_DIAG_FRAC_DEN 20
// Detailed lane-aware diagnosis is required for correctness, but should still
// fall back before recursive work approaches the cost of a full linear sweep.
#define CEC_SEEDSIM_HARD_FRAC_NUM 1
#define CEC_SEEDSIM_HARD_FRAC_DEN 10
// Split-driven TFO refinement is optional. Stop it without a full fallback
// when its structural or demand-evaluation closure exceeds this budget.
#define CEC_SEEDSIM_TFO_FRAC_NUM 1
#define CEC_SEEDSIM_TFO_FRAC_DEN 20
// Diagnosis cost grows with the number of CEX records, even when many records
// share the same packed bit lane. Reject unusually dense batches cheaply.
#define CEC_SEEDSIM_CEX_LANE_FACTOR 8
// Consecutive wide cones use bounded exponential backoff. A successful local
// batch clears both the streak and cooldown immediately.
#define CEC_SEEDSIM_MAX_FALLBACK_BACKOFF 7
#define CEC_EVENT_NODE_WORD_FRAC_NUM 1
#define CEC_EVENT_NODE_WORD_FRAC_DEN 10
#define CEC_EVENT_EDGE_WORD_FRAC_NUM 1
#define CEC_EVENT_EDGE_WORD_FRAC_DEN 5
// Up-front density gate for the event path. When a batch's changed-CI seed
// exceeds this fraction of all unrolled inputs, its dirty closure approaches a
// full sweep and bit-parallel full resim wins; reject the batch before doing
// any propagation work that a mid-flight budget abort would otherwise discard.
#define CEC_EVENT_INPUT_FRAC_NUM 1
#define CEC_EVENT_INPUT_FRAC_DEN 8
#define CEC_SEEDSIM_RESULT_FULL 0
#define CEC_SEEDSIM_RESULT_LOCAL 1
#define CEC_SEEDSIM_RESULT_FULL_WIDE -1
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -192,8 +361,13 @@ struct Cec_IncrMgr_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 );
extern Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p );
extern void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo );
extern int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart );
extern int Gia_ManCorrSpecReal( 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 );
extern 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 Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings );
/*=== 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 );
@ -203,14 +377,42 @@ extern int Cec_IncrMgrCountNextChanges( Cec_IncrMgr_t * p );
extern int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj ); extern int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj );
extern void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive ); extern void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive );
extern void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p ); extern void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p );
extern Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMark, Cec_IncrMgr_t * pIncr ); 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 );
extern int * Cec_IncrMgrDecideMask( Cec_IncrMgr_t * p, int fUseRings, int * pfConverged, int * pnReprSeeds, int * pnNextChanges, int * pnTotalPairs, int * pnActivePairs ); /*=== cecCorrDyn.c ============================================================*/
extern Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr );
extern void Cec_DynSrmFree( Cec_DynSrm_t * p );
extern void Cec_DynSrmPrintStats( Cec_DynSrm_t * p );
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 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 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_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus );
/*=== cecCorrIncrSim.c ============================================================*/
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 int Cec_SeedSimTryBatch( Cec_SeedSim_t * p, Cec_ManSim_t * pSim, Vec_Ptr_t * vSimInfo, Vec_Int_t * vOutputs, Vec_Int_t * vOutBits, int nFrames );
extern void Cec_SeedSimSaveFrameInputs( Cec_SeedSim_t * p, Vec_Ptr_t * vInfoCis, int Frame );
extern void Cec_SeedSimSaveFrameOutputs( Cec_SeedSim_t * p, Vec_Ptr_t * vInfoCos, int Frame );
extern void Cec_SeedSimFinishFull( Cec_SeedSim_t * p );
extern void Cec_SeedSimBeginCall( Cec_SeedSim_t * p );
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_SeedSimBuildClassCone( Cec_SeedSim_t * p, Vec_Int_t * vOutputs );
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 );
/*=== cecClass.c ============================================================*/ /*=== cecClass.c ============================================================*/
extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ); extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass );
extern int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords );
extern int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize );
extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ); extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );
extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p ); extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p );
extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ); extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
extern int Cec_ManSimSimulateRoundSavePhase( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, unsigned * pSave );
extern int Cec_ManSimRefineMappedFrame( Cec_ManSim_t * p, unsigned * pValues, Vec_Int_t * vLits, int iBase, int nWords );
/*=== cecIso.c ============================================================*/ /*=== cecIso.c ============================================================*/
extern int * Cec_ManDetectIsomorphism( Gia_Man_t * p ); extern int * Cec_ManDetectIsomorphism( Gia_Man_t * p );
/*=== cecMan.c ============================================================*/ /*=== cecMan.c ============================================================*/
@ -231,6 +433,7 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int
extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit ); extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
/*=== cecSeq.c ============================================================*/ /*=== cecSeq.c ============================================================*/
extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ); extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
extern int Cec_ManSeqResimulateSeed( Cec_ManSim_t * p, Vec_Ptr_t * vInfo, Cec_SeedSim_t * pSeed );
extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter ); extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter );
extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ); extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex );
extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ); extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
@ -241,6 +444,7 @@ extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pA
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ); extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
extern Vec_Int_t * Cec_ManSatSolveMiterOutVals( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );

47
src/proof/cec/cecSeq.c
View File

@ -170,6 +170,53 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
return 0; return 0;
} }
int Cec_ManSeqResimulateSeed( Cec_ManSim_t * p, Vec_Ptr_t * vInfo, Cec_SeedSim_t * pSeed )
{
unsigned * pInfo0, * pInfo1;
int f, i, k, w, RetValue;
assert( pSeed != NULL );
assert( pSeed->pAig == p->pAig );
assert( pSeed->nFrames == p->pPars->nFrames );
assert( pSeed->nWords == p->nWords );
assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
{
pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k );
pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
for ( f = 0; f < p->pPars->nFrames; f++ )
{
unsigned * pSave = pSeed->pPhase + (size_t)f * pSeed->nPhaseWords;
for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
{
pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ );
pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
Cec_SeedSimSaveFrameInputs( pSeed, p->vCiSimInfo, f );
RetValue = Cec_ManSimSimulateRoundSavePhase( p, p->vCiSimInfo, p->vCoSimInfo, pSave );
Cec_SeedSimSaveFrameOutputs( pSeed, p->vCoSimInfo, f );
if ( RetValue )
{
pSeed->fInitialized = 0;
return 1;
}
}
assert( k == Vec_PtrSize(vInfo) );
Cec_SeedSimFinishFull( pSeed );
return 0;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Resimulates information to refine equivalence classes.] Synopsis [Resimulates information to refine equivalence classes.]

45
src/proof/cec/cecSolve.c
View File

@ -1055,6 +1055,32 @@ void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2
Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) ); Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
} }
static int Cec_ManSatLitValue( Cec_ManSat_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 ( Cec_ObjSatNum(p, pObj) == 0 )
return -1;
return Cec_ObjSatVarValue( p, pObj ) ^ Abc_LitIsCompl(iLit);
}
static void Cec_ManSatSaveOutVals( Cec_ManSat_t * p, Vec_Int_t * vOutLits, Vec_Int_t * vOutVals, int Out )
{
int Val0, Val1;
if ( vOutLits == NULL || vOutVals == NULL )
return;
if ( 2*Out + 1 >= Vec_IntSize(vOutLits) )
return;
Val0 = Cec_ManSatLitValue( p, Vec_IntEntry(vOutLits, 2*Out) );
Val1 = Cec_ManSatLitValue( p, Vec_IntEntry(vOutLits, 2*Out + 1) );
Vec_IntWriteEntry( vOutVals, 2*Out, Val0 );
Vec_IntWriteEntry( vOutVals, 2*Out + 1, Val1 );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs one round of solving for the POs of the AIG.] Synopsis [Performs one round of solving for the POs of the AIG.]
@ -1067,10 +1093,11 @@ void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ) Vec_Int_t * Cec_ManSatSolveMiterOutVals( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals )
{ {
Bar_Progress_t * pProgress = NULL; Bar_Progress_t * pProgress = NULL;
Vec_Int_t * vCexStore; Vec_Int_t * vCexStore;
Vec_Int_t * vOutVals = NULL;
Vec_Str_t * vStatus; Vec_Str_t * vStatus;
Cec_ManSat_t * p; Cec_ManSat_t * p;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
@ -1083,6 +1110,12 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
// 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) );
}
// perform solving // perform solving
p = Cec_ManSatCreate( pAig, pPars ); p = Cec_ManSatCreate( pAig, pPars );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
@ -1115,6 +1148,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
if ( status == 1 ) if ( status == 1 )
continue; continue;
assert( status == 0 ); assert( status == 0 );
Cec_ManSatSaveOutVals( p, vOutLits, vOutVals, i );
// save the pattern // save the pattern
// Gia_ManIncrementTravId( pAig ); // Gia_ManIncrementTravId( pAig );
// Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) ); // Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
@ -1128,9 +1162,18 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
// Cec_ManSatPrintStats( p ); // Cec_ManSatPrintStats( p );
Cec_ManSatStop( p ); Cec_ManSatStop( p );
*pvStatus = vStatus; *pvStatus = vStatus;
if ( pvOutVals )
*pvOutVals = vOutVals;
else
Vec_IntFreeP( &vOutVals );
return vCexStore; return vCexStore;
} }
Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus )
{
return Cec_ManSatSolveMiterOutVals( pAig, pPars, pvStatus, NULL, NULL );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///

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

@ -3,7 +3,9 @@ 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/cecCorrDyn.c \
src/proof/cec/cecCorrIncr.c \ src/proof/cec/cecCorrIncr.c \
src/proof/cec/cecCorrIncrSim.c \
src/proof/cec/cecIso.c \ src/proof/cec/cecIso.c \
src/proof/cec/cecMan.c \ src/proof/cec/cecMan.c \
src/proof/cec/cecPat.c \ src/proof/cec/cecPat.c \