diff --git a/abclib.dsp b/abclib.dsp index 4aa3a34ce5..9a01de2b19 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -6685,10 +6685,18 @@ SOURCE=.\src\proof\cec\cecCorr.c # End Source File # Begin Source File +SOURCE=.\src\proof\cec\cecCorrDyn.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\cec\cecCorrIncr.c # End Source File # Begin Source File +SOURCE=.\src\proof\cec\cecCorrIncrSim.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\cec\cecInt.h # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 6fddcac96b..b4d2ba35bc 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -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_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_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 Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p ); /*=== 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_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals ); /*=== giaCof.c =============================================================*/ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 67b62655e0..91dfe60653 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -64,6 +64,7 @@ struct Cbs_Man_t_ { Cbs_Par_t Pars; // parameters 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 pJust; // justification 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 * vModel; // satisfying assignment 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 int nSatUnsat; // the number of proofs 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)) ); } +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************************************************************* 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; Cbs_ManAssign( p, pObj, 0, NULL, NULL ); if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) ) + { Cbs_ManSaveModel( p, p->vModel ); + Cbs_ManSaveOutVals( p, p->vOutLits, p->vOutVals, p->iOutVal ); + } else RetValue = 1; Cbs_ManCancelUntil( p, 0 ); @@ -1034,14 +1064,14 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p ) 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 Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ); - Cbs_Man_t * p; - Vec_Int_t * vCex, * vVisit, * vCexStore; + Cbs_Man_t * p; + Vec_Int_t * vCex, * vVisit, * vCexStore, * vOutVals = NULL; Vec_Str_t * vStatus; - Gia_Obj_t * pRoot; + Gia_Obj_t * pRoot; int i, status; abctime clk, clkTotal = Abc_Clock(); 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 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); vCexStore = Vec_IntAlloc( 10000 ); + if ( pvOutVals ) + { + *pvOutVals = NULL; + if ( vOutLits ) + vOutVals = Vec_IntStartFull( 2 * Gia_ManPoNum(pAig) ); + } vVisit = Vec_IntAlloc( 100 ); vCex = Cbs_ReadModel( p ); // 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(); p->Pars.fUseHighest = 1; p->Pars.fUseLowest = 0; + p->vOutLits = vOutLits; + p->vOutVals = vOutVals; + p->iOutVal = i; status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); + p->vOutLits = NULL; + p->vOutVals = NULL; + p->iOutVal = -1; // printf( "\n" ); /* 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 ); Cbs_ManStop( p ); *pvStatus = vStatus; + if ( pvOutVals ) + *pvOutVals = vOutVals; + else + Vec_IntFreeP( &vOutVals ); // printf( "Total number of cex literals = %d. (Ave = %d)\n", // 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; } +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 /// @@ -1140,4 +1312,3 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5b41f8fd03..775c3f7074 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -41924,6 +41924,13 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 ) { Abc_Print( -1, "Abc_CommandAbc9Scorr(): There is no AIG.\n" ); @@ -41999,7 +42006,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" ); - Abc_Print( -2, "\t-i : toggle incremental TFO-triggered re-proof 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-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" ); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index eed2cfaf93..6c75447a09 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -167,7 +167,10 @@ struct Cec_ParCor_t_ // int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation 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 fVeryVerbose; // verbose stats int fVerbose; // verbose stats diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c index 60fdbc8952..8ee64339ef 100644 --- a/src/proof/cec/cecClass.c +++ b/src/proof/cec/cecClass.c @@ -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); } +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 /// //////////////////////////////////////////////////////////////////////// @@ -310,6 +315,106 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int 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************************************************************* Synopsis [Refines one equivalence class.] @@ -665,7 +770,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) 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; 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++ ) 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: // if this node is candidate constant, collect it @@ -808,6 +919,17 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * 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************************************************************* diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index fdba94f005..3365046b90 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -195,6 +195,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ) p->fLatchCorr = 0; // consider only latch outputs p->fConstCorr = 0; // consider only constants 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->fFirstStop = 0; // stop on the first sat output p->fUseSmartCnf = 0; // use smart CNF computation diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index d5a0918082..5c53356c60 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -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 int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); - //////////////////////////////////////////////////////////////////////// /// 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.] Description [] - + SideEffects [] 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.] Description [] - + SideEffects [] 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.] Description [] - + SideEffects [] 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.] Description [] - + SideEffects [] SeeAlso [] @@ -500,6 +499,53 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS 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************************************************************* 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; } +/**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************************************************************* 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 [] ***********************************************************************/ -int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames ) -{ - Vec_Int_t * vPairs; - Vec_Ptr_t * vSimInfo; - int RetValue = 0, iStart = 0; - vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); - Gia_ManCreateValueRefs( pSim->pAig ); +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 = NULL; + Vec_Int_t * vOutBits = NULL; + Vec_Ptr_t * vSimInfo = NULL; + int RetValue = 0, iStart = 0, fValueRefs = 0; + if ( pSeed ) + Cec_SeedSimBeginCall( pSeed ); // reset per-call local/full/maxdirty counters // pSim->pPars->nWords = 63; 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) ) { - Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) ); - iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); -// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); -// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); - Gia_ManCorrPerformRemapping( vPairs, vSimInfo ); - RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); + if ( pSeed ) + { + int LocalStatus; + iStart = Cec_SeedSimLoadPersistentBatch( + pSeed, vCexStore, iStart, vPairs, vOutBits ); + 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 ); } //Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); assert( iStart == Vec_IntSize(vCexStore) ); - Vec_PtrFree( vSimInfo ); - Vec_IntFree( vPairs ); + Vec_IntFreeP( &vOutBits ); + if ( !pSeed ) + Vec_PtrFree( vSimInfo ); + Vec_IntFreeP( &vPairs ); return RetValue; } +int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames ) +{ + return Cec_ManResimulateCounterExamplesSeed( pSim, vCexStore, nFrames, NULL, NULL ); +} + /**Function************************************************************* 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; } +/**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************************************************************* 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 [] SeeAlso [] @@ -803,8 +1057,16 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr Vec_Int_t * vCexStore; Cec_ManSim_t * pSim; 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_DynSrm_t * pBmcDynSrm = NULL; // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); 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 ); Cec_IncrMgrSnapshotClasses( pBmcMgr ); } + if ( pPars->fDynSrm && pBmcMgr ) + pBmcDynSrm = Cec_DynSrmAlloc( pAig, pBmcMgr ); + fBmcPersist = ( pBmcDynSrm != NULL && pPars->fUseCSat ); fChanges = 1; for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ ) { 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 ) ) break; 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. if ( pBmcMgr && i > 0 ) { - pTfoMask = Cec_IncrMgrDecideMask( pBmcMgr, 0, &fConverged, - &nReprSeeds, NULL, &nTotalPairs, &nActivePairs ); - if ( fConverged ) + nReprSeeds = Cec_IncrMgrComputeSeeds( pBmcMgr ); + if ( nReprSeeds == 0 ) + { + // No pReprs change. BMC SRM topology is unchanged. break; + } + Cec_IncrMgrComputeTfo( pBmcMgr ); + // BMC SRM is non-ring; pass fRings=0 so we count (head, member) + // pairs only and skip any ring-edge bookkeeping. + if ( pBmcDynSrm ) + Cec_DynSrmCountActivePairs( pBmcDynSrm, 0, pBmcMgr->pTfoMark, &nTotalPairs, &nActivePairs ); + else + Cec_IncrMgrCountActivePairs( pBmcMgr, 0, pBmcMgr->pTfoMark, &nTotalPairs, &nActivePairs ); + if ( nActivePairs == 0 ) + break; + // Same fallback heuristic as the main loop: above ~70% active, + // the mask plus emission filter costs more than just rebuilding + // the full SRM. + if ( !( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs ) ) + pTfoMask = pBmcMgr->pTfoMark; } - 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 ); else pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + nBmcPos = fBmcPersist ? Vec_IntSize(Cec_DynSrmOutLits(pBmcDynSrm)) : Gia_ManCoNum(pSrm); if ( pTfoMask && pPars->fVeryVerbose ) Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n", - i, nReprSeeds, nActivePairs, nTotalPairs, 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 ) Cec_IncrMgrSnapshotClasses( pBmcMgr ); - if ( Gia_ManPoNum(pSrm) == 0 ) + if ( nBmcPos == 0 ) { - Gia_ManStop( pSrm ); + if ( pSrm ) + Gia_ManStop( pSrm ); Vec_IntFree( vOutputs ); break; } 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 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); // refine classes with these counter-examples 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 ); fChanges = 1; } @@ -872,11 +1183,13 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr // recycle Vec_IntFree( vCexStore ); Vec_StrFree( vStatus ); - Gia_ManStop( pSrm ); + if ( pSrm ) + Gia_ManStop( pSrm ); Vec_IntFree( vOutputs ); if ( Cec_ParCorShouldStop( pPars ) ) break; } + Cec_DynSrmFree( pBmcDynSrm ); Cec_IncrMgrFree( pBmcMgr ); 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_ManSim_t * pSim; Gia_Man_t * pSrm; - int r, RetValue, nPrev[4] = {0}; + int r, nPrev[4] = {0}; abctime clkTotal = Abc_Clock(); abctime clkSat = 0, clkSim = 0, clkSrm = 0; 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; int nIncrSkipped = 0, nIncrFallback = 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 ); 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), - 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 ); } // 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 ); 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 for ( r = 0; r < nIterMax; r++ ) { if ( Cec_ParCorShouldStop( pPars ) ) { Cec_ManSimStop( pSim ); + Cec_DynSrmFree( pDynSrm ); Cec_IncrMgrFree( pMgr ); + Cec_SeedSimFree( pSeedSim ); return 1; } if ( pPars->nStepsMax == r ) { Cec_ManSimStop( pSim ); + Cec_DynSrmFree( pDynSrm ); Cec_IncrMgrFree( pMgr ); + Cec_SeedSimFree( pSeedSim ); Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r ); fflush( stdout ); return 1; @@ -1058,54 +1389,97 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) clk2 = Abc_Clock(); { int * pTfoMask = NULL; - int nReprSeeds = 0, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0; - int fConverged = 0; + int nReprSeeds = 0, nNextChanges = 0; + int nTotalPairs = 0, nActivePairs = 0; + // Decide whether to apply incremental TFO mask this iteration. + // Skip on r==0 because the first full SRM establishes the cache. if ( pMgr && r > 0 ) { abctime clkI = Abc_Clock(); - pTfoMask = Cec_IncrMgrDecideMask( pMgr, pPars->fUseRings, &fConverged, - &nReprSeeds, &nNextChanges, - &nTotalPairs, &nActivePairs ); - clkIncr += Abc_Clock() - clkI; - if ( fConverged ) + nReprSeeds = Cec_IncrMgrComputeSeeds( pMgr ); + nNextChanges = pPars->fUseRings ? Cec_IncrMgrCountNextChanges( pMgr ) : 0; + if ( nReprSeeds == 0 && nNextChanges == 0 ) { - 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; } - if ( pTfoMask == NULL ) - nIncrFallback++; 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 pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); if ( pTfoMask && pPars->fVeryVerbose ) Abc_Print( 1, " [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n", - r, nReprSeeds, nNextChanges, Vec_IntSize(pMgr->vTfoNodes), - nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) ); - // Snapshot AFTER SRM build: the active builder still reads the - // previous pNexts to recognise newly-created ring edges. + r, nReprSeeds, nNextChanges, + Vec_IntSize(pMgr->vTfoNodes), nActivePairs, nTotalPairs, + fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm) ); + // Snapshot after SRM construction: the active builder still needs + // the old pNexts snapshot to recognize newly-created ring edges. + // SAT/sim refinement below is what creates the next iteration's diff. if ( pMgr ) Cec_IncrMgrSnapshotClasses( pMgr ); } - assert( 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; - if ( Gia_ManCoNum(pSrm) == 0 ) + if ( (fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm)) == 0 ) { Vec_IntFree( vOutputs ); - Gia_ManStop( pSrm ); + if ( pSrm ) + Gia_ManStop( pSrm ); break; } //Gia_DumpAiger( pSrm, "corrsrm", r, 2 ); // found counter-examples to speculation 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 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - Gia_ManStop( pSrm ); + if ( pSrm ) + Gia_ManStop( pSrm ); clkSat += Abc_Clock() - clk2; 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 clk2 = Abc_Clock(); - RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames ); - Vec_IntFree( vCexStore ); - clkSim += Abc_Clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); + { + int nCexReal = 0, nCexTriv = 0; + Cec_ManCexStoreClassify( vCexStore, &nCexReal, &nCexTriv, NULL ); + 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 ) Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk ); Vec_StrFree( vStatus ); @@ -1130,7 +1515,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) if ( Cec_ParCorShouldStop( pPars ) ) { Cec_ManSimStop( pSim ); + Cec_DynSrmFree( pDynSrm ); Cec_IncrMgrFree( pMgr ); + Cec_SeedSimFree( pSeedSim ); return 1; } // 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" ); fflush( stdout ); Cec_ManSimStop( pSim ); + Cec_DynSrmFree( pDynSrm ); Cec_IncrMgrFree( pMgr ); + Cec_SeedSimFree( pSeedSim ); return 0; } 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" ); fflush( stdout ); Cec_ManSimStop( pSim ); + Cec_DynSrmFree( pDynSrm ); Cec_IncrMgrFree( pMgr ); + Cec_SeedSimFree( pSeedSim ); ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pNexts ); return 0; @@ -1185,10 +1576,14 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ABC_PRTP( "Incr ", clkIncr, clkTotal ); Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped ); } + if ( pDynSrm ) + Cec_DynSrmPrintStats( pDynSrm ); Abc_PrintTime( 1, "TOTAL", clkTotal ); fflush( stdout ); } Cec_IncrMgrFree( pMgr ); + Cec_DynSrmFree( pDynSrm ); + Cec_SeedSimFree( pSeedSim ); return 1; } diff --git a/src/proof/cec/cecCorrDyn.c b/src/proof/cec/cecCorrDyn.c new file mode 100644 index 0000000000..2d9beca7f7 --- /dev/null +++ b/src/proof/cec/cecCorrDyn.c @@ -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 diff --git a/src/proof/cec/cecCorrIncr.c b/src/proof/cec/cecCorrIncr.c index fcc61c0b25..8d5a1f2446 100644 --- a/src/proof/cec/cecCorrIncr.c +++ b/src/proof/cec/cecCorrIncr.c @@ -50,6 +50,8 @@ Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames ) p->vSeeds = Vec_IntAlloc( 64 ); p->vTfoNodes = Vec_IntAlloc( 1024 ); 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->vBfsNext = Vec_IntAlloc( 1024 ); if ( pAig->vFanout == NULL ) @@ -82,6 +84,8 @@ void Cec_IncrMgrFree( Cec_IncrMgr_t * p ) Vec_IntFree( p->vNextPrev ); Vec_IntFree( p->vSeeds ); Vec_IntFree( p->vTfoNodes ); + Vec_IntFree( p->vAliasHeads ); + Vec_IntFree( p->vAliasNext ); Vec_IntFree( p->vBfsCur ); Vec_IntFree( p->vBfsNext ); 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.] Description [Returns the number of nodes whose representative changed - since the last snapshot; the seeds themselves are stored in vSeeds and - consumed by Cec_IncrMgrComputeTfo. Does not update 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 - a new ring edge to reprove, not a new fanout cone, so it is handled by - Cec_IncrMgrRingEdgeChanged at SRM emission time.] + since the last snapshot and stores them in vSeeds. Does not update + the snapshot. + + pNexts changes are intentionally excluded here: a ring-link rewrite is + an edge-local event that creates a new ring edge to reprove, not a new + fanout cone, so it is handled by Cec_IncrMgrRingEdgeChanged at SRM + emission time.] SideEffects [] @@ -231,7 +236,7 @@ int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj ) SideEffects [] - SeeAlso [Gia_ManCorrSpecReduce_Active] + SeeAlso [Gia_ManCorrSpecReduce_Emit] ***********************************************************************/ 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.] - Description [Marks pTfoMark[id]=1 for every AIG node reachable from - any seed within nFrames combinational+sequential steps. 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. + Description [Marks pTfoMark[id]=1 for every SRM node reachable from + any seed within nFrames combinational+sequential steps. Besides AIG + fanouts, the walk follows representative-to-member alias edges because + Gia_ManCorrSpecReduce_rec(member) uses repr(member) directly. Missing + these edges can reuse an obsolete UNSAT result when a representative's + 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 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; 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 ) pMark[Id] = 0; @@ -321,6 +331,17 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p ) Vec_IntClear( p->vBfsCur ); 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 ) { if ( !pMark[Id] ) @@ -338,6 +359,16 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p ) { Gia_Obj_t * pFan; 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 ); for ( k = 0; k < nFan; k++ ) { @@ -381,39 +412,37 @@ void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p ) /**Function************************************************************* - Synopsis [Active-filter variant of Gia_ManCorrSpecReduce.] + Synopsis [Emission-filtered variant of Gia_ManCorrSpecReduce.] Description [Identical to Gia_ManCorrSpecReduce in its SRM topology - and speculative reduction; the only difference is the PO emission - filter. A candidate pair (a, b) is emitted iff pTfoMark[a] is set - or pTfoMark[b] is set, i.e. at least one endpoint lies in the TFO of - a recently-changed representative. In ring mode, a ring edge that is - new or rewired since the last snapshot (Cec_IncrMgrRingEdgeChanged) - 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. + and speculative reduction; the only difference is PO emission. + CEC_EMIT_ACTIVE emits pairs selected by the incremental TFO filter. + CEC_EMIT_SKIPPED emits the exact complement for shadow validation. + A new or rewired ring edge is always active and can never be emitted + as skipped because it has no prior UNSAT result to reuse. Walking the full ring is required (rather than skipping unmarked members) so iPrev stays aligned with the live class order; the active - filter only suppresses the resulting PO when the edge is provably - not new and neither endpoint is reachable from a seed. Passing - pTfoMark == NULL falls back to the unfiltered baseline behaviour.] + predicate is evaluated only after the edge endpoints are known.] SideEffects [] - SeeAlso [Gia_ManCorrSpecReduce] + SeeAlso [Gia_ManCorrSpecReduce Cec_IncrMgrCountActivePairs] ***********************************************************************/ -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 ) +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 ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pRepr; Vec_Int_t * vXorLits; - int f, i, iPrev, iObj, iPrevNew, iObjNew; + int f, i, iPrev, iObj, iPrevNew, iObjNew, iPrevRaw, iObjRaw; assert( nFrames > 0 ); assert( Gia_ManRegNum(p) > 0 ); assert( p->pReprs != NULL ); + assert( Mode == CEC_EMIT_ALL || pTfoMark != NULL ); Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 ); Gia_ManSetPhase( 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) ); } *pvOutputs = Vec_IntAlloc( 1000 ); + if ( pvOutLits ) + *pvOutLits = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 ); 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 ( 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; - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); - iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); + iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); + iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ); if ( iObjNew != 0 ) { Vec_IntPush( *pvOutputs, 0 ); Vec_IntPush( *pvOutputs, i ); + if ( pvOutLits ) + { + Vec_IntPush( *pvOutLits, 0 ); + Vec_IntPush( *pvOutLits, iObjRaw ); + } Vec_IntPush( vXorLits, iObjNew ); } } @@ -459,18 +499,27 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr iPrev = i; Gia_ClassForEachObj1( p, i, iObj ) { - int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] || - Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ); + int fActive = pTfoMark != NULL && + (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 ) { - iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); - iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); + iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); + iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); + iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) { Vec_IntPush( *pvOutputs, iPrev ); Vec_IntPush( *pvOutputs, iObj ); + if ( pvOutLits ) + { + Vec_IntPush( *pvOutLits, iPrevRaw ); + Vec_IntPush( *pvOutLits, iObjRaw ); + } 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 iObj = i; { - int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] || - Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj ); + int fActive = pTfoMark != NULL && + (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 ) { - iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); - iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); + iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); + iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); + iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) { Vec_IntPush( *pvOutputs, iPrev ); Vec_IntPush( *pvOutputs, iObj ); + if ( pvOutLits ) + { + Vec_IntPush( *pvOutLits, iPrevRaw ); + Vec_IntPush( *pvOutLits, iObjRaw ); + } 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) ); if ( pRepr == NULL ) continue; - if ( pTfoMark ) { 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; } - iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); - iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + iPrevRaw = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); + iObjRaw = Gia_ManCorrSpecReal( pNew, 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, pRepr) ); 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) ); } } @@ -528,6 +595,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr Gia_ManHashStop( pNew ); Vec_IntErase( &p->vCopies ); pNew = Gia_ManCleanup( pTemp = pNew ); + if ( pvOutLits ) + Gia_ManDupRemapLiterals( *pvOutLits, pTemp ); Gia_ManStop( pTemp ); return pNew; } @@ -614,59 +683,6 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nP 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 //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecCorrIncrSim.c b/src/proof/cec/cecCorrIncrSim.c new file mode 100644 index 0000000000..8bb92809df --- /dev/null +++ b/src/proof/cec/cecCorrIncrSim.c @@ -0,0 +1,2040 @@ +/**CFile**************************************************************** + + FileName [cecCorrIncrSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Persistent event-driven incremental simulation for &scorr.] + + Description [Keeps packed CI patterns and host-AIG values across CEX batches. + Only changed CI words are propagated through the frame-aware fanout graph. + Classes containing truly changed values are fully regrouped. Structural and + measured-time budgets fall back to the standard full sweep.] + + Author [Xiran Zhao] + + Affiliation [University of Chinese Academy of Sciences] + + Date [Ver. 1.0. Started - Jun 2026.] + +***********************************************************************/ + +#include "cecInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Cec_SeedSimKey( Cec_SeedSim_t * p, int frame, int objId ) +{ + return frame * p->nObjs + objId; +} + +static inline unsigned * Cec_SeedSimVal( Cec_SeedSim_t * p, int frame, int objId ) +{ + size_t Key = (size_t)Cec_SeedSimKey( p, frame, objId ); + assert( frame >= 0 && frame < p->nFrames ); + assert( objId >= 0 && objId < p->nObjs ); + return p->pVal + Key * p->nWords; +} + +static inline int Cec_SeedSimPhase( Cec_SeedSim_t * p, int frame, int objId ) +{ + assert( frame >= 0 && frame < p->nFrames ); + assert( objId >= 0 && objId < p->nObjs ); + return Abc_InfoHasBit( p->pPhase + (size_t)frame * p->nPhaseWords, objId ); +} + +static inline void Cec_SeedSimSetPhase( Cec_SeedSim_t * p, + int frame, int objId, int Value ) +{ + unsigned * pWord = p->pPhase + (size_t)frame * p->nPhaseWords + (objId >> 5); + unsigned Bit = 1u << (objId & 31); + *pWord = (*pWord & ~Bit) | (Value ? Bit : 0); +} + +static inline int Cec_SeedSimMark( Cec_SeedSim_t * p, int frame, int objId ) +{ + int Key = Cec_SeedSimKey( p, frame, objId ); + if ( p->pMark[Key] == p->nMarkVersion ) + return 0; + p->pMark[Key] = p->nMarkVersion; + Vec_IntPush( p->vDirtyKeys, Key ); + return 1; +} + +static inline int Cec_SeedSimConeHasKey( Cec_SeedSim_t * p, int Key ) +{ + return !p->fUseCone || Abc_InfoHasBit( p->pCone, Key ); +} + +static inline int Cec_SeedSimConeHas( Cec_SeedSim_t * p, int Frame, int ObjId ) +{ + return Cec_SeedSimConeHasKey( p, Cec_SeedSimKey(p, Frame, ObjId) ); +} + +static void Cec_SeedSimConeMark_rec( Cec_SeedSim_t * p, int Frame, int ObjId ) +{ + Gia_Obj_t * pObj; + int Key; + if ( Frame < 0 || Frame >= p->nFrames || ObjId < 0 || ObjId >= p->nObjs ) + return; + Key = Cec_SeedSimKey( p, Frame, ObjId ); + if ( Abc_InfoHasBit(p->pCone, Key) ) + return; + Abc_InfoSetBit( p->pCone, Key ); + p->nConeKeys++; + Vec_IntPush( p->vConeQueue, Key ); + if ( ObjId == 0 ) + return; + pObj = Gia_ManObj( p->pAig, ObjId ); + if ( Gia_ObjIsPi(p->pAig, pObj) ) + return; + if ( Gia_ObjIsRo(p->pAig, pObj) ) + { + Gia_Obj_t * pRi; + int RiId; + if ( Frame == 0 ) + return; + pRi = Gia_ObjRoToRi( p->pAig, pObj ); + RiId = Gia_ObjId( p->pAig, pRi ); + Cec_SeedSimConeMark_rec( p, Frame - 1, + Gia_ObjFaninId0(pRi, RiId) ); + return; + } + if ( Gia_ObjIsAnd(pObj) ) + { + Cec_SeedSimConeMark_rec( p, Frame, + Gia_ObjFaninId0(pObj, ObjId) ); + Cec_SeedSimConeMark_rec( p, Frame, + Gia_ObjFaninId1(pObj, ObjId) ); + } +} + +static void Cec_SeedSimConeCloseClasses( Cec_SeedSim_t * p ) +{ + int i; + for ( i = 0; i < Vec_IntSize(p->vConeQueue); i++ ) + { + int Key = Vec_IntEntry( p->vConeQueue, i ); + int Frame = Key / p->nObjs; + int ObjId = Key % p->nObjs; + int Root, Member, RootKey; + if ( ObjId == 0 ) + continue; + if ( Gia_ObjIsConst(p->pAig, ObjId) ) + continue; + if ( !Gia_ObjIsClass(p->pAig, ObjId) ) + continue; + Root = Gia_ObjIsHead(p->pAig, ObjId) ? ObjId : + Gia_ObjRepr(p->pAig, ObjId); + // close each (frame, class-root) at most once: members and frames repeat + // in the queue, and re-closing a large class is quadratic + RootKey = Frame * p->nObjs + Root; + if ( p->pConeClose[RootKey] == p->nConeCloseVer ) + continue; + p->pConeClose[RootKey] = p->nConeCloseVer; + Cec_SeedSimConeMark_rec( p, Frame, Root ); + Gia_ClassForEachObj1( p->pAig, Root, Member ) + Cec_SeedSimConeMark_rec( p, Frame, Member ); + } +} + +static void Cec_SeedSimBuildFullClassCone( Cec_SeedSim_t * p ) +{ + Gia_Obj_t * pObj; + int Frame, i; + Gia_ManForEachObj1( p->pAig, pObj, i ) + { + if ( !Gia_ObjIsConst(p->pAig, i) && !Gia_ObjIsClass(p->pAig, i) ) + continue; + for ( Frame = 0; Frame < p->nFrames; Frame++ ) + Cec_SeedSimConeMark_rec( p, Frame, i ); + } + Cec_SeedSimConeCloseClasses( p ); +} + +void Cec_SeedSimBuildClassCone( Cec_SeedSim_t * p, Vec_Int_t * vOutputs ) +{ + int i, Obj0, Obj1; + memset( p->pCone, 0, sizeof(unsigned) * p->nConeWords ); + Vec_IntClear( p->vConeQueue ); + p->nConeKeys = 0; + p->fUseCone = 1; + if ( ++p->nConeCloseVer == 0 ) // fresh "class already closed" stamps + { + memset( p->pConeClose, 0, sizeof(int) * (size_t)p->nFrames * p->nObjs ); + p->nConeCloseVer = 1; + } + if ( vOutputs && Vec_IntSize(vOutputs) > 0 ) + { + Vec_IntForEachEntryDouble( vOutputs, Obj0, Obj1, i ) + { + Cec_SeedSimConeMark_rec( p, p->iSeedFrame, Obj0 ); + Cec_SeedSimConeMark_rec( p, p->iSeedFrame, Obj1 ); + } + Cec_SeedSimConeCloseClasses( p ); + if ( p->nConeKeys > 0 ) + return; + } + Cec_SeedSimBuildFullClassCone( p ); +} + +static int Cec_SeedSimEvalActive( Cec_SeedSim_t * p, int Frame, int ObjId, int nLimit ) +{ + Gia_Man_t * pAig = p->pAig; + Gia_Obj_t * pObj = Gia_ManObj( pAig, ObjId ); + int Key = Cec_SeedSimKey( p, Frame, ObjId ); + unsigned * pRes = Cec_SeedSimVal( p, Frame, ObjId ); + int Phase, w; + if ( p->pEvalMark[Key] == p->nEvalVersion ) + return 1; + if ( ++p->nEvalKeys > nLimit ) + return 0; + p->pEvalMark[Key] = p->nEvalVersion; + Phase = Cec_SeedSimPhase( p, Frame, ObjId ); + pRes[0] = (pRes[0] & ~(unsigned)1) | Phase; + for ( w = 0; w < p->nWords; w++ ) + if ( p->pActiveMask[w] ) + pRes[w] = Phase ? ~(unsigned)0 : 0; + if ( ObjId == 0 ) + return 1; + if ( Gia_ObjIsPi(pAig, pObj) ) + { + int iPi = Gia_ObjCioId( pObj ); + unsigned * pInput = (unsigned *)Vec_PtrEntry( p->vBatchInfo, + p->nRegs + Frame * p->nPis + iPi ); + for ( w = 0; w < p->nWords; w++ ) + if ( p->pActiveMask[w] ) + pRes[w] = (pRes[w] & ~p->pActiveMask[w]) | + (pInput[w] & p->pActiveMask[w]); + return 1; + } + if ( Gia_ObjIsRo(pAig, pObj) ) + { + if ( Frame == 0 ) + { + int iReg = Gia_ObjCioId(pObj) - p->nPis; + unsigned * pInput = (unsigned *)Vec_PtrEntry( p->vBatchInfo, iReg ); + for ( w = 0; w < p->nWords; w++ ) + if ( p->pActiveMask[w] ) + pRes[w] = (pRes[w] & ~p->pActiveMask[w]) | + (pInput[w] & p->pActiveMask[w]); + } + else + { + Gia_Obj_t * pRi = Gia_ObjRoToRi( pAig, pObj ); + int RiId = Gia_ObjId( pAig, pRi ); + int DrvId = Gia_ObjFaninId0( pRi, RiId ); + unsigned * pDrv; + if ( !Cec_SeedSimEvalActive(p, Frame - 1, DrvId, nLimit) ) + return 0; + pDrv = Cec_SeedSimVal( p, Frame - 1, DrvId ); + for ( w = 0; w < p->nWords; w++ ) + { + unsigned Value = Gia_ObjFaninC0(pRi) ? ~pDrv[w] : pDrv[w]; + if ( p->pActiveMask[w] ) + pRes[w] = (pRes[w] & ~p->pActiveMask[w]) | + (Value & p->pActiveMask[w]); + } + } + return 1; + } + if ( Gia_ObjIsAnd(pObj) ) + { + int Fan0 = Gia_ObjFaninId0( pObj, ObjId ); + int Fan1 = Gia_ObjFaninId1( pObj, ObjId ); + unsigned * pVal0, * pVal1; + if ( !Cec_SeedSimEvalActive(p, Frame, Fan0, nLimit) || + !Cec_SeedSimEvalActive(p, Frame, Fan1, nLimit) ) + return 0; + pVal0 = Cec_SeedSimVal( p, Frame, Fan0 ); + pVal1 = Cec_SeedSimVal( p, Frame, Fan1 ); + for ( w = 0; w < p->nWords; w++ ) + { + unsigned Val0 = Gia_ObjFaninC0(pObj) ? ~pVal0[w] : pVal0[w]; + unsigned Val1 = Gia_ObjFaninC1(pObj) ? ~pVal1[w] : pVal1[w]; + unsigned Value = Val0 & Val1; + if ( p->pActiveMask[w] ) + pRes[w] = (pRes[w] & ~p->pActiveMask[w]) | + (Value & p->pActiveMask[w]); + } + return 1; + } + return 0; +} + +Cec_SeedSim_t * Cec_SeedSimAlloc( Gia_Man_t * pAig, int nFrames, int iSeedFrame, int nWords ) +{ + Cec_SeedSim_t * p = ABC_CALLOC( Cec_SeedSim_t, 1 ); + size_t nKeys = (size_t)nFrames * Gia_ManObjNum(pAig); + int w; + assert( iSeedFrame >= 0 && iSeedFrame < nFrames ); + p->pAig = pAig; + p->nFrames = nFrames; + p->iSeedFrame = iSeedFrame; + p->nObjs = Gia_ManObjNum( pAig ); + p->nPis = Gia_ManPiNum( pAig ); + p->nRegs = Gia_ManRegNum( pAig ); + p->nWords = nWords; + p->nPhaseWords = Abc_BitWordNum( p->nObjs ); + p->nEventMaskWords = Abc_BitWordNum( nWords ); + p->nConeWords = Abc_BitWordNum( (int)nKeys ); + p->pVal = ABC_CALLOC( unsigned, nKeys * nWords ); + p->pPhase = ABC_CALLOC( unsigned, (size_t)nFrames * p->nPhaseWords ); + p->pActiveMask = ABC_CALLOC( unsigned, nWords ); + p->pCexMask = ABC_CALLOC( unsigned, nWords ); + p->pFoundMask = ABC_CALLOC( unsigned, nWords ); + p->pDiffMask = ABC_CALLOC( unsigned, nWords ); + p->pTempMask = ABC_CALLOC( unsigned, nWords ); + p->pMark = ABC_CALLOC( int, nKeys ); + p->pSpecMark = ABC_CALLOC( int, nKeys ); + p->pDiagMark = ABC_CALLOC( int, nKeys ); + p->pSplitMark = ABC_CALLOC( int, nKeys ); + p->pProcessMark = ABC_CALLOC( int, nKeys ); + p->pEvalMark = ABC_CALLOC( int, nKeys ); + p->pEventWords = ABC_CALLOC( unsigned, nKeys * p->nEventMaskWords ); + p->pCone = ABC_CALLOC( unsigned, p->nConeWords ); + p->pConeClose = ABC_CALLOC( int, nKeys ); + p->pRootMark = ABC_CALLOC( int, p->nObjs ); + p->pTxnMark = ABC_CALLOC( int, p->nObjs ); + p->pInputVarMark = ABC_CALLOC( int, p->nRegs + p->nPis * p->nFrames ); + p->vDiagPairs = Vec_IntAlloc( 192 ); + p->vSpecKeys = Vec_IntAlloc( 1024 ); + p->vSpecMasks = Vec_IntAlloc( 1024 * nWords ); + p->vDiagKeys = Vec_IntAlloc( 1024 ); + p->vDiagRoots = Vec_IntAlloc( 1024 ); + p->vDiagMasks = Vec_IntAlloc( 1024 * nWords ); + p->vSplitKeys = Vec_IntAlloc( 1024 ); + p->vDirtyKeys = Vec_IntAlloc( 4096 ); + p->vWaveKeys = Vec_IntAlloc( 4096 ); + p->vQueue = Vec_IntAlloc( 4096 ); + p->vDirtyRoots = Vec_IntAlloc( 1024 ); + p->vConstRefined = Vec_IntAlloc( 64 ); + p->vClassAll = Vec_IntAlloc( 64 ); + p->vClassOld = Vec_IntAlloc( 64 ); + p->vClassNew = Vec_IntAlloc( 64 ); + p->vTxnObjs = Vec_IntAlloc( 1024 ); + p->vTxnReprs = Vec_IntAlloc( 1024 ); + p->vTxnNexts = Vec_IntAlloc( 1024 ); + p->vPackTouched = Vec_IntAlloc( 1024 ); + p->vInputUndo = Vec_IntAlloc( 2048 ); + p->vChangedInputs = Vec_IntAlloc( 1024 ); + p->vValueUndo = Vec_IntAlloc( 4096 ); + p->vChangedValues = Vec_IntAlloc( 4096 ); + p->vConeQueue = Vec_IntAlloc( 4096 ); + p->pPhase0 = ABC_ALLOC( unsigned, nWords ); + p->pPhase1 = ABC_ALLOC( unsigned, nWords ); + for ( w = 0; w < nWords; w++ ) + { + p->pPhase0[w] = 0; + p->pPhase1[w] = ~(unsigned)0; + } + if ( pAig->vFanout == NULL ) + { + Gia_ManStaticFanoutStart( pAig ); + p->fOwnsFanout = 1; + } + return p; +} + +void Cec_SeedSimFree( Cec_SeedSim_t * p ) +{ + if ( p == NULL ) + return; + if ( p->fOwnsFanout ) + Gia_ManStaticFanoutStop( p->pAig ); + Vec_IntFreeP( &p->vDiagPairs ); + Vec_IntFreeP( &p->vSpecKeys ); + Vec_IntFreeP( &p->vSpecMasks ); + Vec_IntFreeP( &p->vDiagKeys ); + Vec_IntFreeP( &p->vDiagRoots ); + Vec_IntFreeP( &p->vDiagMasks ); + Vec_IntFreeP( &p->vSplitKeys ); + Vec_IntFreeP( &p->vDirtyKeys ); + Vec_IntFreeP( &p->vWaveKeys ); + Vec_IntFreeP( &p->vQueue ); + Vec_IntFreeP( &p->vDirtyRoots ); + Vec_IntFreeP( &p->vConstRefined ); + Vec_IntFreeP( &p->vClassAll ); + Vec_IntFreeP( &p->vClassOld ); + Vec_IntFreeP( &p->vClassNew ); + Vec_IntFreeP( &p->vTxnObjs ); + Vec_IntFreeP( &p->vTxnReprs ); + Vec_IntFreeP( &p->vTxnNexts ); + Vec_IntFreeP( &p->vPackTouched ); + Vec_IntFreeP( &p->vInputUndo ); + Vec_IntFreeP( &p->vChangedInputs ); + Vec_IntFreeP( &p->vValueUndo ); + Vec_IntFreeP( &p->vChangedValues ); + Vec_IntFreeP( &p->vConeQueue ); + Vec_PtrFreeP( &p->vSimInfo ); + ABC_FREE( p->pVal ); + ABC_FREE( p->pPhase ); + ABC_FREE( p->pActiveMask ); + ABC_FREE( p->pCexMask ); + ABC_FREE( p->pFoundMask ); + ABC_FREE( p->pDiffMask ); + ABC_FREE( p->pTempMask ); + ABC_FREE( p->pMark ); + ABC_FREE( p->pSpecMark ); + ABC_FREE( p->pDiagMark ); + ABC_FREE( p->pSplitMark ); + ABC_FREE( p->pProcessMark ); + ABC_FREE( p->pEvalMark ); + ABC_FREE( p->pEventWords ); + ABC_FREE( p->pCone ); + ABC_FREE( p->pConeClose ); + ABC_FREE( p->pRootMark ); + ABC_FREE( p->pTxnMark ); + ABC_FREE( p->pPackPres ); + ABC_FREE( p->pInputUndoMark ); + ABC_FREE( p->pInputVarMark ); + ABC_FREE( p->pPhase0 ); + ABC_FREE( p->pPhase1 ); + ABC_FREE( p ); +} + +static void Cec_SeedSimReset( Cec_SeedSim_t * p ) +{ + size_t nKeys = (size_t)p->nFrames * p->nObjs; + int i, Key; + Vec_IntForEachEntry( p->vSpecKeys, Key, i ) + p->pSpecMark[Key] = 0; + Vec_IntForEachEntry( p->vDiagKeys, Key, i ) + p->pDiagMark[Key] = 0; + Vec_IntClear( p->vDiagPairs ); + Vec_IntClear( p->vSpecKeys ); + Vec_IntClear( p->vSpecMasks ); + Vec_IntClear( p->vDiagKeys ); + Vec_IntClear( p->vDiagRoots ); + Vec_IntClear( p->vDiagMasks ); + Vec_IntClear( p->vSplitKeys ); + Vec_IntClear( p->vDirtyKeys ); + Vec_IntClear( p->vWaveKeys ); + Vec_IntClear( p->vQueue ); + for ( i = 0; i < p->nWords; i++ ) + p->pActiveMask[i] = ~(unsigned)0; + p->pActiveMask[0] &= ~(unsigned)1; + memset( p->pCexMask, 0, sizeof(unsigned) * p->nWords ); + memset( p->pFoundMask, 0, sizeof(unsigned) * p->nWords ); + p->vBatchInfo = NULL; + p->nSpecKeys = 0; + p->nEvalKeys = 0; + p->nMarkVersion++; + p->nSplitVersion++; + p->nProcessVersion++; + p->nEvalVersion++; + if ( p->nMarkVersion == 0 ) + { + memset( p->pMark, 0, sizeof(int) * nKeys ); + p->nMarkVersion = 1; + } + if ( p->nSplitVersion == 0 ) + { + memset( p->pSplitMark, 0, sizeof(int) * nKeys ); + p->nSplitVersion = 1; + } + if ( p->nProcessVersion == 0 ) + { + memset( p->pProcessMark, 0, sizeof(int) * nKeys ); + p->nProcessVersion = 1; + } + if ( p->nEvalVersion == 0 ) + { + memset( p->pEvalMark, 0, sizeof(int) * nKeys ); + p->nEvalVersion = 1; + } +} + +static int Cec_SeedSimAddDiagKey( Cec_SeedSim_t * p, int Frame, int ObjId ) +{ + int Key, iDiag, Repr, w; + if ( ObjId <= 0 || ObjId >= p->nObjs ) + return ObjId == 0; + Key = Cec_SeedSimKey( p, Frame, ObjId ); + iDiag = p->pDiagMark[Key] - 1; + if ( iDiag < 0 ) + { + Repr = Gia_ObjRepr( p->pAig, ObjId ); + iDiag = Vec_IntSize( p->vDiagKeys ); + p->pDiagMark[Key] = iDiag + 1; + Vec_IntPush( p->vDiagKeys, Key ); + Vec_IntPush( p->vDiagRoots, Repr == 0 ? 0 : + (Gia_ObjIsHead(p->pAig, ObjId) ? ObjId : Repr) ); + for ( w = 0; w < p->nWords; w++ ) + Vec_IntPush( p->vDiagMasks, 0 ); + } + return 1; +} + +static int Cec_SeedSimAddDiagBit( Cec_SeedSim_t * p, int Frame, int ObjId, int iBit ) +{ + int Key, iDiag; + unsigned * pMask; + if ( !Cec_SeedSimAddDiagKey(p, Frame, ObjId) ) + return 0; + if ( ObjId == 0 ) + return 1; + Key = Cec_SeedSimKey( p, Frame, ObjId ); + iDiag = p->pDiagMark[Key] - 1; + assert( iDiag >= 0 ); + pMask = (unsigned *)Vec_IntArray(p->vDiagMasks) + (size_t)iDiag * p->nWords; + Abc_InfoSetBit( pMask, iBit ); + return 1; +} + +static int Cec_SeedSimCollectSpecBit( Cec_SeedSim_t * p, int Frame, int ObjId, int iBit, int nLimit ); + +static int Cec_SeedSimCollectRealBit( Cec_SeedSim_t * p, int Frame, int ObjId, int iBit, int nLimit ) +{ + Gia_Obj_t * pObj; + if ( ObjId < 0 || ObjId >= p->nObjs || Frame < 0 || Frame >= p->nFrames ) + return 0; + if ( ObjId == 0 ) + return 1; + pObj = Gia_ManObj( p->pAig, ObjId ); + if ( Gia_ObjIsAnd(pObj) ) + { + return Cec_SeedSimCollectSpecBit( p, Frame, Gia_ObjFaninId0(pObj, ObjId), iBit, nLimit ) && + Cec_SeedSimCollectSpecBit( p, Frame, Gia_ObjFaninId1(pObj, ObjId), iBit, nLimit ); + } + if ( Gia_ObjIsRo(p->pAig, pObj) && Frame > 0 ) + { + Gia_Obj_t * pRi = Gia_ObjRoToRi( p->pAig, pObj ); + int RiId = Gia_ObjId( p->pAig, pRi ); + return Cec_SeedSimCollectSpecBit( p, Frame - 1, + Gia_ObjFaninId0(pRi, RiId), iBit, nLimit ); + } + return 1; +} + +static int Cec_SeedSimCollectSpecBit( Cec_SeedSim_t * p, int Frame, int ObjId, int iBit, int nLimit ) +{ + int Key, Repr, iSpec, iWord = iBit >> 5, w; + unsigned Bit = (unsigned)1 << (iBit & 31); + unsigned * pMask; + if ( ObjId < 0 || ObjId >= p->nObjs || Frame < 0 || Frame >= p->nFrames ) + return 0; + if ( ObjId == 0 ) + return 1; + Key = Cec_SeedSimKey( p, Frame, ObjId ); + iSpec = p->pSpecMark[Key] - 1; + if ( iSpec < 0 ) + { + if ( ++p->nSpecKeys > nLimit ) + return 0; + iSpec = Vec_IntSize( p->vSpecKeys ); + p->pSpecMark[Key] = iSpec + 1; + Vec_IntPush( p->vSpecKeys, Key ); + for ( w = 0; w < p->nWords; w++ ) + Vec_IntPush( p->vSpecMasks, 0 ); + } + pMask = (unsigned *)Vec_IntArray(p->vSpecMasks) + (size_t)iSpec * p->nWords; + if ( pMask[iWord] & Bit ) + return 1; + pMask[iWord] |= Bit; + Repr = Gia_ObjRepr( p->pAig, ObjId ); + if ( Repr != GIA_VOID ) + { + if ( !Cec_SeedSimAddDiagBit(p, Frame, ObjId, iBit) ) + return 0; + return Repr == 0 || + Cec_SeedSimCollectSpecBit( p, Frame, Repr, iBit, nLimit ); + } + return Cec_SeedSimCollectRealBit( p, Frame, ObjId, iBit, nLimit ); +} + +static int Cec_SeedSimCollectDiagnosis( Cec_SeedSim_t * p, Vec_Int_t * vOutputs, Vec_Int_t * vOutBits, int nLimit ) +{ + int i, Out, iBit; + if ( vOutputs == NULL || vOutBits == NULL ) + return 0; + Vec_IntForEachEntryDouble( vOutBits, Out, iBit, i ) + { + int Obj0, Obj1; + if ( Out < 0 || 2*Out + 1 >= Vec_IntSize(vOutputs) ) + return 0; + Obj0 = Vec_IntEntry( vOutputs, 2*Out ); + Obj1 = Vec_IntEntry( vOutputs, 2*Out + 1 ); + Abc_InfoSetBit( p->pCexMask, iBit ); + Vec_IntPush( p->vDiagPairs, Obj0 ); + Vec_IntPush( p->vDiagPairs, Obj1 ); + Vec_IntPush( p->vDiagPairs, iBit ); + if ( !Cec_SeedSimAddDiagKey(p, p->iSeedFrame, Obj0) || + !Cec_SeedSimAddDiagKey(p, p->iSeedFrame, Obj1) ) + return 0; + if ( !Cec_SeedSimCollectRealBit(p, p->iSeedFrame, Obj0, iBit, nLimit) || + !Cec_SeedSimCollectRealBit(p, p->iSeedFrame, Obj1, iBit, nLimit) ) + return 0; + } + return Vec_IntSize(vOutBits) > 0; +} + +static int Cec_SeedSimCollectShapeSpec( Cec_SeedSim_t * p, int Frame, int ObjId, int nLimit ); + +static int Cec_SeedSimCollectShapeReal( Cec_SeedSim_t * p, int Frame, int ObjId, int nLimit ) +{ + Gia_Obj_t * pObj; + int Key; + if ( ObjId < 0 || ObjId >= p->nObjs || Frame < 0 || Frame >= p->nFrames ) + return 0; + if ( ObjId == 0 ) + return 1; + Key = Cec_SeedSimKey( p, Frame, ObjId ); + if ( p->pProcessMark[Key] == p->nProcessVersion ) + return 1; + p->pProcessMark[Key] = p->nProcessVersion; + Vec_IntPush( p->vDirtyKeys, Key ); + if ( Vec_IntSize(p->vDirtyKeys) > nLimit ) + return 0; + pObj = Gia_ManObj( p->pAig, ObjId ); + if ( Gia_ObjIsAnd(pObj) ) + return Cec_SeedSimCollectShapeSpec( p, Frame, Gia_ObjFaninId0(pObj, ObjId), nLimit ) && + Cec_SeedSimCollectShapeSpec( p, Frame, Gia_ObjFaninId1(pObj, ObjId), nLimit ); + if ( Gia_ObjIsRo(p->pAig, pObj) && Frame > 0 ) + { + Gia_Obj_t * pRi = Gia_ObjRoToRi( p->pAig, pObj ); + int RiId = Gia_ObjId( p->pAig, pRi ); + return Cec_SeedSimCollectShapeSpec( p, Frame - 1, + Gia_ObjFaninId0(pRi, RiId), nLimit ); + } + return 1; +} + +static int Cec_SeedSimCollectShapeSpec( Cec_SeedSim_t * p, int Frame, int ObjId, int nLimit ) +{ + Gia_Obj_t * pObj; + int Repr; + if ( ObjId < 0 || ObjId >= p->nObjs || Frame < 0 || Frame >= p->nFrames ) + return 0; + if ( ObjId == 0 || !Cec_SeedSimMark(p, Frame, ObjId) ) + return 1; + if ( Vec_IntSize(p->vDirtyKeys) > nLimit ) + return 0; + Repr = Gia_ObjRepr( p->pAig, ObjId ); + if ( Repr != GIA_VOID ) + return Repr == 0 || Cec_SeedSimCollectShapeSpec( p, Frame, Repr, nLimit ); + pObj = Gia_ManObj( p->pAig, ObjId ); + if ( Gia_ObjIsAnd(pObj) ) + return Cec_SeedSimCollectShapeSpec( p, Frame, Gia_ObjFaninId0(pObj, ObjId), nLimit ) && + Cec_SeedSimCollectShapeSpec( p, Frame, Gia_ObjFaninId1(pObj, ObjId), nLimit ); + if ( Gia_ObjIsRo(p->pAig, pObj) && Frame > 0 ) + { + Gia_Obj_t * pRi = Gia_ObjRoToRi( p->pAig, pObj ); + int RiId = Gia_ObjId( p->pAig, pRi ); + return Cec_SeedSimCollectShapeSpec( p, Frame - 1, + Gia_ObjFaninId0(pRi, RiId), nLimit ); + } + return 1; +} + +static int Cec_SeedSimDiagnosisShapeSmall( Cec_SeedSim_t * p, + Vec_Int_t * vOutputs, Vec_Int_t * vOutBits, int nLimit ) +{ + int i, Out, iBit; + Vec_IntForEachEntryDouble( vOutBits, Out, iBit, i ) + { + int Obj0, Obj1; + (void)iBit; + if ( Out < 0 || 2*Out + 1 >= Vec_IntSize(vOutputs) ) + return 0; + Obj0 = Vec_IntEntry( vOutputs, 2*Out ); + Obj1 = Vec_IntEntry( vOutputs, 2*Out + 1 ); + if ( !Cec_SeedSimCollectShapeReal(p, p->iSeedFrame, Obj0, nLimit) || + !Cec_SeedSimCollectShapeReal(p, p->iSeedFrame, Obj1, nLimit) ) + return 0; + } + return 1; +} + +static void Cec_SeedSimRestartTfoMarks( Cec_SeedSim_t * p ) +{ + size_t nKeys = (size_t)p->nFrames * p->nObjs; + Vec_IntClear( p->vDirtyKeys ); + Vec_IntClear( p->vQueue ); + p->nMarkVersion++; + p->nProcessVersion++; + if ( p->nMarkVersion == 0 ) + { + memset( p->pMark, 0, sizeof(int) * nKeys ); + p->nMarkVersion = 1; + } + if ( p->nProcessVersion == 0 ) + { + memset( p->pProcessMark, 0, sizeof(int) * nKeys ); + p->nProcessVersion = 1; + } +} + +static void Cec_SeedSimUseCexLanes( Cec_SeedSim_t * p ) +{ + int w; + for ( w = 0; w < p->nWords; w++ ) + p->pActiveMask[w] = p->pCexMask[w] ? ~(unsigned)0 : 0; + p->pActiveMask[0] &= ~(unsigned)1; +} + +static void Cec_SeedSimUsePackedLanes( Cec_SeedSim_t * p ) +{ + int w; + if ( p->nEvalKeys > p->nMaxDirty ) + p->nMaxDirty = p->nEvalKeys; + for ( w = 0; w < p->nWords; w++ ) + p->pActiveMask[w] = ~(unsigned)0; + p->pActiveMask[0] &= ~(unsigned)1; + p->nEvalKeys = 0; + p->nEvalVersion++; + if ( p->nEvalVersion == 0 ) + { + size_t nKeys = (size_t)p->nFrames * p->nObjs; + memset( p->pEvalMark, 0, sizeof(int) * nKeys ); + p->nEvalVersion = 1; + } +} + +static int Cec_SeedSimComputeTfo( Cec_SeedSim_t * p, int nLimit ) +{ + if ( Vec_IntSize(p->vDirtyKeys) > nLimit ) + return 0; + while ( Vec_IntSize(p->vQueue) > 0 ) + { + int Key = Vec_IntPop( p->vQueue ); + int Frame = Key / p->nObjs; + int ObjId = Key % p->nObjs; + int FanId, i; + Gia_ObjForEachFanoutStaticId( p->pAig, ObjId, FanId, i ) + { + Gia_Obj_t * pFan = Gia_ManObj( p->pAig, FanId ); + if ( Gia_ObjIsAnd(pFan) ) + { + if ( Cec_SeedSimMark( p, Frame, FanId ) ) + { + if ( Vec_IntSize(p->vDirtyKeys) > nLimit ) + return 0; + Vec_IntPush( p->vQueue, Cec_SeedSimKey(p, Frame, FanId) ); + } + } + else if ( Gia_ObjIsRi(p->pAig, pFan) && Frame + 1 < p->nFrames ) + { + int RoId = Gia_ObjRiToRoId( p->pAig, FanId ); + if ( Cec_SeedSimMark( p, Frame + 1, RoId ) ) + { + if ( Vec_IntSize(p->vDirtyKeys) > nLimit ) + return 0; + Vec_IntPush( p->vQueue, Cec_SeedSimKey(p, Frame + 1, RoId) ); + } + } + } + } + return 1; +} + +static void Cec_SeedSimStartRootSet( Cec_SeedSim_t * p ) +{ + p->nRootVersion++; + if ( p->nRootVersion == 0 ) + { + memset( p->pRootMark, 0, sizeof(int) * p->nObjs ); + p->nRootVersion = 1; + } + Vec_IntClear( p->vDirtyRoots ); + Vec_IntClear( p->vConstRefined ); +} + +static void Cec_SeedSimAddRoot( Cec_SeedSim_t * p, int ObjId ) +{ + Gia_Man_t * pAig = p->pAig; + int iRoot; + if ( Gia_ObjIsConst(pAig, ObjId) ) + { + iRoot = ObjId; + if ( p->pRootMark[iRoot] != p->nRootVersion ) + { + p->pRootMark[iRoot] = p->nRootVersion; + Vec_IntPush( p->vConstRefined, iRoot ); + } + } + else if ( Gia_ObjIsClass(pAig, ObjId) ) + { + iRoot = Gia_ObjIsHead(pAig, ObjId) ? ObjId : Gia_ObjRepr(pAig, ObjId); + if ( p->pRootMark[iRoot] != p->nRootVersion ) + { + p->pRootMark[iRoot] = p->nRootVersion; + Vec_IntPush( p->vDirtyRoots, iRoot ); + } + } + else + return; +} + +static int Cec_SeedSimCollectEvalShape( Cec_SeedSim_t * p, + int Frame, int ObjId, int nLimit ) +{ + Gia_Obj_t * pObj; + int Key; + if ( ObjId < 0 || ObjId >= p->nObjs || Frame < 0 || Frame >= p->nFrames ) + return 0; + Key = Cec_SeedSimKey( p, Frame, ObjId ); + if ( p->pProcessMark[Key] == p->nProcessVersion ) + return 1; + p->pProcessMark[Key] = p->nProcessVersion; + Vec_IntPush( p->vDirtyKeys, Key ); + if ( Vec_IntSize(p->vDirtyKeys) > nLimit ) + return 0; + if ( ObjId == 0 ) + return 1; + pObj = Gia_ManObj( p->pAig, ObjId ); + if ( Gia_ObjIsAnd(pObj) ) + return Cec_SeedSimCollectEvalShape( p, Frame, + Gia_ObjFaninId0(pObj, ObjId), nLimit ) && + Cec_SeedSimCollectEvalShape( p, Frame, + Gia_ObjFaninId1(pObj, ObjId), nLimit ); + if ( Gia_ObjIsRo(p->pAig, pObj) && Frame > 0 ) + { + Gia_Obj_t * pRi = Gia_ObjRoToRi( p->pAig, pObj ); + int RiId = Gia_ObjId( p->pAig, pRi ); + return Cec_SeedSimCollectEvalShape( p, Frame - 1, + Gia_ObjFaninId0(pRi, RiId), nLimit ); + } + return 1; +} + +static int Cec_SeedSimDiagnosisEvalShapeSmall( Cec_SeedSim_t * p, + Vec_Int_t * vKeys, int nLimit ) +{ + int iLo = 0; + Vec_IntSort( vKeys, 0 ); + while ( iLo < Vec_IntSize(vKeys) ) + { + int Frame = Vec_IntEntry(vKeys, iLo) / p->nObjs; + int iHi = iLo, i, Key, ObjId, Ent; + while ( iHi < Vec_IntSize(vKeys) && + Vec_IntEntry(vKeys, iHi) / p->nObjs == Frame ) + iHi++; + Cec_SeedSimStartRootSet( p ); + for ( i = iLo; i < iHi; i++ ) + { + Key = Vec_IntEntry( vKeys, i ); + ObjId = Key % p->nObjs; + if ( Gia_ObjIsConst(p->pAig, ObjId) || + Gia_ObjIsClass(p->pAig, ObjId) ) + Cec_SeedSimAddRoot( p, ObjId ); + else if ( !Cec_SeedSimCollectEvalShape(p, Frame, ObjId, nLimit) ) + return 0; + } + Vec_IntForEachEntry( p->vDirtyRoots, Ent, i ) + { + int Member; + if ( !Cec_SeedSimCollectEvalShape(p, Frame, Ent, nLimit) ) + return 0; + Gia_ClassForEachObj1( p->pAig, Ent, Member ) + if ( !Cec_SeedSimCollectEvalShape(p, Frame, Member, nLimit) ) + return 0; + } + Vec_IntForEachEntry( p->vConstRefined, Ent, i ) + if ( !Cec_SeedSimCollectEvalShape(p, Frame, Ent, nLimit) ) + return 0; + iLo = iHi; + } + return 1; +} + +static void Cec_SeedSimDiffMask( Cec_SeedSim_t * p, unsigned * pValue0, + unsigned * pValue1, unsigned * pMask, unsigned * pDiff ) +{ + int fCompl = (pValue0[0] & 1) != (pValue1[0] & 1); + int w; + for ( w = 0; w < p->nWords; w++ ) + pDiff[w] = (pValue0[w] ^ (fCompl ? ~pValue1[w] : pValue1[w])) & pMask[w]; +} + +static int Cec_SeedSimMaskIsZero( unsigned * pMask, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( pMask[w] ) + return 0; + return 1; +} + +static inline unsigned Cec_SeedSimRefineMaskWord( Cec_SeedSim_t * p, int w ) +{ + return p->pRefineMask[w] | (w == 0); +} + +static int Cec_SeedSimCompareRefine( Cec_SeedSim_t * p, + unsigned * pValue0, unsigned * pValue1 ) +{ + int fCompl = (pValue0[0] & 1) != (pValue1[0] & 1); + int w; + if ( fCompl ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (pValue0[w] ^ ~pValue1[w]) & Cec_SeedSimRefineMaskWord(p, w) ) + return 0; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + if ( (pValue0[w] ^ pValue1[w]) & Cec_SeedSimRefineMaskWord(p, w) ) + return 0; + } + return 1; +} + +static int Cec_SeedSimHashRefine( Cec_SeedSim_t * p, + unsigned * pValue, int nTableSize ) +{ + static int s_Primes[16] = { + 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, + 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 + }; + unsigned uHash = 0; + int w; + if ( pValue[0] & 1 ) + for ( w = 0; w < p->nWords; w++ ) + uHash ^= (~pValue[w] & Cec_SeedSimRefineMaskWord(p, w)) * + s_Primes[w & 0xf]; + else + for ( w = 0; w < p->nWords; w++ ) + uHash ^= (pValue[w] & Cec_SeedSimRefineMaskWord(p, w)) * + s_Primes[w & 0xf]; + return (int)(uHash % nTableSize); +} + +static int Cec_SeedSimCurrentRoot( Cec_SeedSim_t * p, int ObjId ) +{ + if ( ObjId == 0 || Gia_ObjIsConst(p->pAig, ObjId) ) + return 0; + if ( Gia_ObjIsHead(p->pAig, ObjId) ) + return ObjId; + if ( Gia_ObjIsClass(p->pAig, ObjId) ) + return Gia_ObjRepr(p->pAig, ObjId); + return ObjId; +} + +static void Cec_SeedSimCheckFailedPairs( Cec_SeedSim_t * p, int Frame ) +{ + int i; + assert( Frame == p->iSeedFrame ); + for ( i = 0; i < Vec_IntSize(p->vDiagPairs); i += 3 ) + { + int Obj0 = Vec_IntEntry( p->vDiagPairs, i ); + int Obj1 = Vec_IntEntry( p->vDiagPairs, i + 1 ); + int iBit = Vec_IntEntry( p->vDiagPairs, i + 2 ); + int iWord = iBit >> 5; + unsigned Bit = (unsigned)1 << (iBit & 31); + unsigned * pValue0, * pValue1; + if ( Cec_SeedSimCurrentRoot(p, Obj0) != Cec_SeedSimCurrentRoot(p, Obj1) ) + { + p->pFoundMask[iWord] |= Bit; + continue; + } + pValue0 = Obj0 == 0 ? p->pPhase0 : Cec_SeedSimVal( p, Frame, Obj0 ); + pValue1 = Obj1 == 0 ? p->pPhase0 : Cec_SeedSimVal( p, Frame, Obj1 ); + Cec_SeedSimDiffMask( p, pValue0, pValue1, p->pActiveMask, p->pDiffMask ); + p->pFoundMask[iWord] |= p->pDiffMask[iWord] & Bit; + } +} + +static void Cec_SeedSimAddSplitKey( Cec_SeedSim_t * p, int Frame, int ObjId ) +{ + int Key = Cec_SeedSimKey( p, Frame, ObjId ); + if ( p->pSplitMark[Key] == p->nSplitVersion ) + return; + p->pSplitMark[Key] = p->nSplitVersion; + Vec_IntPush( p->vSplitKeys, Key ); +} + +static int Cec_SeedSimPrepareFrame( Cec_SeedSim_t * p, Vec_Int_t * vKeys, + int Frame, int iLo, int iHi, int nLimit, int fDiagnosis ) +{ + Gia_Man_t * pAig = p->pAig; + int i, Key, Ent; + Cec_SeedSimStartRootSet( p ); + for ( i = iLo; i < iHi; i++ ) + { + int ObjId; + Key = Vec_IntEntry( vKeys, i ); + ObjId = Key % p->nObjs; + if ( fDiagnosis ) + { + int iDiag = p->pDiagMark[Key] - 1; + unsigned * pMask; + int RootOld; + assert( iDiag >= 0 ); + pMask = (unsigned *)Vec_IntArray(p->vDiagMasks) + (size_t)iDiag * p->nWords; + RootOld = Vec_IntEntry( p->vDiagRoots, iDiag ); + int RootNew = Gia_ObjIsConst(pAig, ObjId) ? 0 : + (Gia_ObjIsHead(pAig, ObjId) ? ObjId : + (Gia_ObjIsClass(pAig, ObjId) ? Gia_ObjRepr(pAig, ObjId) : GIA_VOID)); + // Failed endpoints are diagnosis keys as well. An endpoint + // outside an equivalence class has no member-to-root assumption. + if ( RootOld == GIA_VOID ) + { + if ( !Cec_SeedSimEvalActive(p, Frame, ObjId, nLimit) ) + return 0; + continue; + } + if ( RootNew != RootOld ) + { + int w; + for ( w = 0; w < p->nWords; w++ ) + p->pFoundMask[w] |= pMask[w]; + continue; + } + } + Cec_SeedSimAddRoot( p, ObjId ); + } + Vec_IntForEachEntry( p->vDirtyRoots, Ent, i ) + { + int Member; + if ( !Cec_SeedSimEvalActive(p, Frame, Ent, nLimit) ) + return 0; + Gia_ClassForEachObj1( pAig, Ent, Member ) + { + if ( !Cec_SeedSimEvalActive(p, Frame, Member, nLimit) ) + return 0; + } + } + Vec_IntForEachEntry( p->vConstRefined, Ent, i ) + if ( !Cec_SeedSimEvalActive(p, Frame, Ent, nLimit) ) + return 0; + if ( fDiagnosis ) + { + for ( i = iLo; i < iHi; i++ ) + { + unsigned * pMask, * pValue0, * pValue1; + int ObjId, RootOld, RootNew, iDiag, w; + Key = Vec_IntEntry( vKeys, i ); + ObjId = Key % p->nObjs; + iDiag = p->pDiagMark[Key] - 1; + assert( iDiag >= 0 ); + RootOld = Vec_IntEntry( p->vDiagRoots, iDiag ); + RootNew = Gia_ObjIsConst(pAig, ObjId) ? 0 : + (Gia_ObjIsHead(pAig, ObjId) ? ObjId : + (Gia_ObjIsClass(pAig, ObjId) ? Gia_ObjRepr(pAig, ObjId) : GIA_VOID)); + pMask = (unsigned *)Vec_IntArray(p->vDiagMasks) + (size_t)iDiag * p->nWords; + if ( RootOld == GIA_VOID ) + continue; + if ( RootNew != RootOld ) + { + for ( w = 0; w < p->nWords; w++ ) + p->pFoundMask[w] |= pMask[w]; + continue; + } + if ( ObjId == RootOld ) + continue; + pValue0 = Cec_SeedSimVal( p, Frame, ObjId ); + pValue1 = RootOld == 0 ? + (Gia_ObjPhase(Gia_ManObj(pAig, ObjId)) ? p->pPhase1 : p->pPhase0) : + Cec_SeedSimVal( p, Frame, RootOld ); + Cec_SeedSimDiffMask( p, pValue0, pValue1, pMask, p->pDiffMask ); + for ( w = 0; w < p->nWords; w++ ) + p->pFoundMask[w] |= p->pDiffMask[w]; + } + if ( Frame == p->iSeedFrame ) + Cec_SeedSimCheckFailedPairs( p, Frame ); + } + return 1; +} + +static void Cec_SeedSimTxnBegin( Cec_SeedSim_t * p ) +{ + assert( !p->fTxnActive ); + assert( p->pAig->pReprs != NULL && p->pAig->pNexts != NULL ); + Vec_IntClear( p->vTxnObjs ); + Vec_IntClear( p->vTxnReprs ); + Vec_IntClear( p->vTxnNexts ); + p->nTxnVersion++; + if ( p->nTxnVersion == 0 ) + { + memset( p->pTxnMark, 0, sizeof(int) * p->nObjs ); + p->nTxnVersion = 1; + } + p->fTxnActive = 1; +} + +static void Cec_SeedSimTxnSaveObj( Cec_SeedSim_t * p, int ObjId ) +{ + assert( ObjId >= 0 && ObjId < p->nObjs ); + if ( !p->fTxnActive || p->pTxnMark[ObjId] == p->nTxnVersion ) + return; + p->pTxnMark[ObjId] = p->nTxnVersion; + Vec_IntPush( p->vTxnObjs, ObjId ); + Vec_IntPush( p->vTxnReprs, Gia_ObjRepr(p->pAig, ObjId) ); + Vec_IntPush( p->vTxnNexts, Gia_ObjNext(p->pAig, ObjId) ); +} + +static void Cec_SeedSimTxnSaveVec( Cec_SeedSim_t * p, Vec_Int_t * vObjs ) +{ + int i, ObjId; + Vec_IntForEachEntry( vObjs, ObjId, i ) + Cec_SeedSimTxnSaveObj( p, ObjId ); +} + +static void Cec_SeedSimTxnCommit( Cec_SeedSim_t * p ) +{ + assert( p->fTxnActive ); + p->fTxnActive = 0; + Vec_IntClear( p->vTxnObjs ); + Vec_IntClear( p->vTxnReprs ); + Vec_IntClear( p->vTxnNexts ); +} + +static void Cec_SeedSimTxnRollback( Cec_SeedSim_t * p ) +{ + int i, ObjId, nChanged = 0; + assert( p->fTxnActive ); + assert( Vec_IntSize(p->vTxnObjs) == Vec_IntSize(p->vTxnReprs) ); + assert( Vec_IntSize(p->vTxnObjs) == Vec_IntSize(p->vTxnNexts) ); + for ( i = Vec_IntSize(p->vTxnObjs) - 1; i >= 0; i-- ) + { + ObjId = Vec_IntEntry( p->vTxnObjs, i ); + if ( Gia_ObjRepr(p->pAig, ObjId) != Vec_IntEntry(p->vTxnReprs, i) || + Gia_ObjNext(p->pAig, ObjId) != Vec_IntEntry(p->vTxnNexts, i) ) + nChanged++; + Gia_ObjSetRepr( p->pAig, ObjId, Vec_IntEntry(p->vTxnReprs, i) ); + Gia_ObjSetNext( p->pAig, ObjId, Vec_IntEntry(p->vTxnNexts, i) ); + } + p->fTxnActive = 0; + p->nBatchRollback++; + p->nRollbackObjs += nChanged; + Vec_IntClear( p->vTxnObjs ); + Vec_IntClear( p->vTxnReprs ); + Vec_IntClear( p->vTxnNexts ); +} + +static int Cec_SeedSimRefineClass_rec( Cec_SeedSim_t * p, int Frame, int iRoot ) +{ + unsigned * pSim0; + int Ent, Count = 0; + Vec_IntClear( p->vClassOld ); + Vec_IntClear( p->vClassNew ); + Vec_IntPush( p->vClassOld, iRoot ); + pSim0 = Cec_SeedSimVal( p, Frame, iRoot ); + Gia_ClassForEachObj1( p->pAig, iRoot, Ent ) + { + unsigned * pSim1 = Cec_SeedSimVal( p, Frame, Ent ); + if ( Cec_SeedSimCompareRefine(p, pSim0, pSim1) ) + Vec_IntPush( p->vClassOld, Ent ); + else + Vec_IntPush( p->vClassNew, Ent ); + } + if ( Vec_IntSize(p->vClassNew) == 0 ) + return 0; + Cec_SeedSimTxnSaveVec( p, p->vClassOld ); + Cec_SeedSimTxnSaveVec( p, p->vClassNew ); + Cec_ManSimClassCreate( p->pAig, p->vClassOld ); + Cec_ManSimClassCreate( p->pAig, p->vClassNew ); + if ( Vec_IntSize(p->vClassNew) > 1 ) + Count += Cec_SeedSimRefineClass_rec( p, Frame, Vec_IntEntry(p->vClassNew, 0) ); + return Count + 1; +} + +static int Cec_SeedSimRefineClass( Cec_SeedSim_t * p, int Frame, int iRoot ) +{ + unsigned * pRoot = Cec_SeedSimVal( p, Frame, iRoot ); + unsigned * pDiff = p->pDiffMask; + unsigned * pTemp = p->pTempMask; + int Ent, i, w, Count; + memset( pDiff, 0, sizeof(unsigned) * p->nWords ); + Vec_IntClear( p->vClassAll ); + Gia_ClassForEachObj( p->pAig, iRoot, Ent ) + { + Vec_IntPush( p->vClassAll, Ent ); + if ( Ent == iRoot ) + continue; + Cec_SeedSimDiffMask( p, pRoot, Cec_SeedSimVal(p, Frame, Ent), + p->pRefineMask, pTemp ); + for ( w = 0; w < p->nWords; w++ ) + pDiff[w] |= pTemp[w]; + } + if ( Cec_SeedSimMaskIsZero(pDiff, p->nWords) ) + return 0; + Count = Cec_SeedSimRefineClass_rec( p, Frame, iRoot ); + assert( Count > 0 ); + Vec_IntForEachEntry( p->vClassAll, Ent, i ) + Cec_SeedSimAddSplitKey( p, Frame, Ent ); + return Count; +} + +static void Cec_SeedSimProcessRefinedConstants( Cec_SeedSim_t * p, + Cec_ManSim_t * pSim, int Frame ) +{ + Gia_Man_t * pAig = p->pAig; + int * pTable; + int i, k, Key, iPrev, nTableSize; + if ( Vec_IntSize(p->vConstRefined) == 0 ) + return; + Vec_IntForEachEntry( p->vConstRefined, i, k ) + { + unsigned * pValue = Cec_SeedSimVal( p, Frame, i ); + unsigned * pPhase = Gia_ObjPhase(Gia_ManObj(pAig, i)) ? p->pPhase1 : p->pPhase0; + unsigned * pDiff = p->pDiffMask; + Cec_SeedSimDiffMask( p, pValue, pPhase, p->pRefineMask, pDiff ); + if ( Cec_SeedSimMaskIsZero(pDiff, p->nWords) ) + { + Vec_IntDrop( p->vConstRefined, k-- ); + continue; + } + Cec_SeedSimAddSplitKey( p, Frame, i ); + } + if ( Vec_IntSize(p->vConstRefined) == 0 ) + return; + Cec_SeedSimTxnSaveVec( p, p->vConstRefined ); + if ( pSim->pPars->fConstCorr ) + { + Vec_IntForEachEntry( p->vConstRefined, i, k ) + Gia_ObjSetRepr( pAig, i, GIA_VOID ); + return; + } + nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(p->vConstRefined) / 3 ); + pTable = ABC_CALLOC( int, nTableSize ); + Vec_IntForEachEntry( p->vConstRefined, i, k ) + { + assert( Gia_ObjRepr(pAig, i) == 0 ); + assert( Gia_ObjNext(pAig, i) == 0 ); + Key = Cec_SeedSimHashRefine( p, Cec_SeedSimVal(p, Frame, i), nTableSize ); + iPrev = pTable[Key]; + if ( iPrev == 0 ) + Gia_ObjSetRepr( pAig, i, GIA_VOID ); + else + { + assert( iPrev < i ); + Gia_ObjSetNext( pAig, iPrev, i ); + Gia_ObjSetRepr( pAig, i, Gia_ObjRepr(pAig, iPrev) ); + if ( Gia_ObjRepr(pAig, i) == GIA_VOID ) + Gia_ObjSetRepr( pAig, i, iPrev ); + } + pTable[Key] = i; + } + Vec_IntForEachEntry( p->vConstRefined, i, k ) + if ( Gia_ObjIsHead(pAig, i) ) + Cec_SeedSimRefineClass_rec( p, Frame, i ); + ABC_FREE( pTable ); +} + +static void Cec_SeedSimRefineFrame( Cec_SeedSim_t * p, Cec_ManSim_t * pSim, + int Frame ) +{ + int i, Ent; + Vec_IntForEachEntry( p->vDirtyRoots, Ent, i ) + if ( Gia_ObjIsHead(p->pAig, Ent) ) + Cec_SeedSimRefineClass( p, Frame, Ent ); + Cec_SeedSimProcessRefinedConstants( p, pSim, Frame ); +} + +static int Cec_SeedSimProcessKeys( Cec_SeedSim_t * p, Cec_ManSim_t * pSim, + Vec_Int_t * vKeys, int nLimit, int fDiagnosis ) +{ + int iLo = 0; + p->pRefineMask = p->pActiveMask; + Vec_IntSort( vKeys, 0 ); + while ( iLo < Vec_IntSize(vKeys) ) + { + int Frame = Vec_IntEntry(vKeys, iLo) / p->nObjs; + int iHi = iLo; + while ( iHi < Vec_IntSize(vKeys) && + Vec_IntEntry(vKeys, iHi) / p->nObjs == Frame ) + iHi++; + if ( !Cec_SeedSimPrepareFrame(p, vKeys, Frame, iLo, iHi, nLimit, fDiagnosis) ) + return 0; + Cec_SeedSimRefineFrame( p, pSim, Frame ); + iLo = iHi; + } + return 1; +} + +static int Cec_SeedSimDiagnosisMissing( Cec_SeedSim_t * p ) +{ + int Count = 0, w; + for ( w = 0; w < p->nWords; w++ ) + { + unsigned Bits = p->pCexMask[w] & ~p->pFoundMask[w]; + while ( Bits ) + { + Bits &= Bits - 1; + Count++; + } + } + return Count; +} + +static void Cec_SeedSimRecordBatch( Cec_SeedSim_t * p, int nCex ) +{ + p->nBatchCex += nCex; + if ( nCex > p->nBatchCexMax ) + p->nBatchCexMax = nCex; +} + +static void Cec_SeedSimBuildPersistentValues( Cec_SeedSim_t * p ) +{ + Gia_Obj_t * pObj; + int Frame, i, w; + for ( Frame = 0; Frame < p->nFrames; Frame++ ) + { + memset( Cec_SeedSimVal(p, Frame, 0), 0, sizeof(unsigned) * p->nWords ); + for ( i = 0; i < p->nPis; i++ ) + { + int ObjId = Gia_ObjId( p->pAig, Gia_ManPi(p->pAig, i) ); + unsigned * pDst = Cec_SeedSimVal( p, Frame, ObjId ); + unsigned * pSrc = (unsigned *)Vec_PtrEntry( + p->vSimInfo, p->nRegs + Frame * p->nPis + i ); + memcpy( pDst, pSrc, sizeof(unsigned) * p->nWords ); + } + for ( i = 0; i < p->nRegs; i++ ) + { + int ObjId = Gia_ObjId( p->pAig, Gia_ManRo(p->pAig, i) ); + unsigned * pDst = Cec_SeedSimVal( p, Frame, ObjId ); + if ( Frame == 0 ) + { + unsigned * pSrc = (unsigned *)Vec_PtrEntry( p->vSimInfo, i ); + memcpy( pDst, pSrc, sizeof(unsigned) * p->nWords ); + } + else + { + Gia_Obj_t * pRi = Gia_ObjRoToRi( p->pAig, Gia_ManRo(p->pAig, i) ); + int RiId = Gia_ObjId( p->pAig, pRi ); + unsigned * pSrc = Cec_SeedSimVal( + p, Frame - 1, Gia_ObjFaninId0(pRi, RiId) ); + if ( Gia_ObjFaninC0(pRi) ) + for ( w = 0; w < p->nWords; w++ ) + pDst[w] = ~pSrc[w]; + else + memcpy( pDst, pSrc, sizeof(unsigned) * p->nWords ); + } + } + Gia_ManForEachAnd( p->pAig, pObj, i ) + { + unsigned * pDst = Cec_SeedSimVal( p, Frame, i ); + unsigned * pVal0 = Cec_SeedSimVal( + p, Frame, Gia_ObjFaninId0(pObj, i) ); + unsigned * pVal1 = Cec_SeedSimVal( + p, Frame, Gia_ObjFaninId1(pObj, i) ); + for ( w = 0; w < p->nWords; w++ ) + { + unsigned Val0 = Gia_ObjFaninC0(pObj) ? ~pVal0[w] : pVal0[w]; + unsigned Val1 = Gia_ObjFaninC1(pObj) ? ~pVal1[w] : pVal1[w]; + pDst[w] = Val0 & Val1; + } + } + } +} + +void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim ) +{ + int nInputs = p->nRegs + p->nPis * p->nFrames; + size_t nInputWords = (size_t)nInputs * p->nWords; + int i, w; + if ( p->vSimInfo == NULL ) + { + p->vSimInfo = Vec_PtrAllocSimInfo( nInputs, p->nWords ); + p->pPackPres = ABC_CALLOC( unsigned, nInputWords ); + p->pInputUndoMark = ABC_CALLOC( int, nInputWords ); + } + if ( p->fInitialized ) + return; + for ( i = 0; i < nInputs; i++ ) + { + unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, i ); + for ( w = 0; w < p->nWords; w++ ) + pInfo[w] = i < p->nRegs ? 0 : Gia_ManRandom( 0 ); + pInfo[0] &= ~(unsigned)1; + } + // The baseline full sweep makes every current class consistent with the + // persistent patterns. It is paid once; later fallbacks are rolled back + // to this evolving persistent state without copying the dense value cache. + Cec_ManSeqResimulateSeed( pSim, p->vSimInfo, p ); + Cec_SeedSimBuildPersistentValues( p ); + p->fInitialized = 1; +} + +static void Cec_SeedSimStartInputTxn( Cec_SeedSim_t * p ) +{ + size_t nInputWords = (size_t)Vec_PtrSize(p->vSimInfo) * p->nWords; + Vec_IntClear( p->vInputUndo ); + Vec_IntClear( p->vChangedInputs ); + p->nInputUndoVersion++; + p->nInputVarVersion++; + if ( p->nInputUndoVersion == 0 ) + { + memset( p->pInputUndoMark, 0, sizeof(int) * nInputWords ); + p->nInputUndoVersion = 1; + } + if ( p->nInputVarVersion == 0 ) + { + memset( p->pInputVarMark, 0, + sizeof(int) * Vec_PtrSize(p->vSimInfo) ); + p->nInputVarVersion = 1; + } +} + +static void Cec_SeedSimSetInputWord( Cec_SeedSim_t * p, + int iVar, int w, unsigned Value ) +{ + int Flat = iVar * p->nWords + w; + unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, iVar ); + if ( pInfo[w] == Value ) + return; + if ( p->pInputUndoMark[Flat] != p->nInputUndoVersion ) + { + p->pInputUndoMark[Flat] = p->nInputUndoVersion; + Vec_IntPush( p->vInputUndo, Flat ); + Vec_IntPush( p->vInputUndo, (int)pInfo[w] ); + } + if ( p->pInputVarMark[iVar] != p->nInputVarVersion ) + { + p->pInputVarMark[iVar] = p->nInputVarVersion; + Vec_IntPush( p->vChangedInputs, iVar ); + } + pInfo[w] = Value; +} + +static int Cec_SeedSimPackTry( Cec_SeedSim_t * p, + int iBit, int * pLits, int nLits ) +{ + int i, iVar, w = iBit >> 5; + unsigned Bit = (unsigned)1 << (iBit & 31); + for ( i = 0; i < nLits; i++ ) + { + unsigned * pInfo, * pPres; + iVar = Abc_Lit2Var( pLits[i] ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, iVar ); + pPres = p->pPackPres + (size_t)iVar * p->nWords; + if ( (pPres[w] & Bit) && + ((pInfo[w] & Bit) != (Abc_LitIsCompl(pLits[i]) ? 0 : Bit)) ) + return 0; + } + for ( i = 0; i < nLits; i++ ) + { + unsigned * pInfo, * pPres; + unsigned Value; + int Flat; + iVar = Abc_Lit2Var( pLits[i] ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, iVar ); + pPres = p->pPackPres + (size_t)iVar * p->nWords; + Flat = iVar * p->nWords + w; + if ( pPres[w] == 0 ) + Vec_IntPush( p->vPackTouched, Flat ); + pPres[w] |= Bit; + Value = Abc_LitIsCompl(pLits[i]) ? pInfo[w] & ~Bit : pInfo[w] | Bit; + Cec_SeedSimSetInputWord( p, iVar, w, Value ); + } + return 1; +} + +int Cec_SeedSimLoadPersistentBatch( Cec_SeedSim_t * p, Vec_Int_t * vCexStore, + int iStart, Vec_Int_t * vPairs, Vec_Int_t * vOutBits ) +{ + Vec_Int_t * vPat = Vec_IntAlloc( 100 ); + int nBits = 32 * p->nWords; + int i, k, nSize, Out, Flat; + Cec_SeedSimStartInputTxn( p ); + Vec_IntClear( p->vPackTouched ); + Vec_IntClear( vOutBits ); + 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_SeedSimPackTry( + p, k, Vec_IntArray(vPat), Vec_IntSize(vPat)) ) + break; + if ( k < nBits ) + { + Vec_IntPush( vOutBits, Out ); + Vec_IntPush( vOutBits, k ); + } + if ( k == nBits - 1 ) + break; + } + Vec_IntForEachEntry( p->vPackTouched, Flat, i ) + p->pPackPres[Flat] = 0; + Vec_IntClear( p->vPackTouched ); + Vec_IntForEachEntryDouble( vPairs, k, Out, i ) + { + unsigned * pSrc = (unsigned *)Vec_PtrEntry( p->vSimInfo, k ); + for ( nSize = 0; nSize < p->nWords; nSize++ ) + Cec_SeedSimSetInputWord( p, Out, nSize, pSrc[nSize] ); + } + Vec_IntFree( vPat ); + return iStart; +} + +void Cec_SeedSimRestorePersistentInputs( Cec_SeedSim_t * p ) +{ + int i, Flat; + for ( i = Vec_IntSize(p->vInputUndo) - 2; i >= 0; i -= 2 ) + { + Flat = Vec_IntEntry( p->vInputUndo, i ); + ((unsigned *)Vec_PtrEntry( + p->vSimInfo, Flat / p->nWords))[Flat % p->nWords] = + (unsigned)Vec_IntEntry( p->vInputUndo, i + 1 ); + } + Vec_IntClear( p->vInputUndo ); + Vec_IntClear( p->vChangedInputs ); +} + +static void Cec_SeedSimCommitPersistentInputs( Cec_SeedSim_t * p ) +{ + Vec_IntClear( p->vInputUndo ); + Vec_IntClear( p->vChangedInputs ); +} + +static void Cec_SeedSimEventHeapPushWord( Cec_SeedSim_t * p, int Key, int w ) +{ + unsigned * pWords = p->pEventWords + (size_t)Key * p->nEventMaskWords; + int i, Parent, fNew = 0; + if ( p->pMark[Key] != p->nMarkVersion ) + { + p->pMark[Key] = p->nMarkVersion; + memset( pWords, 0, sizeof(unsigned) * p->nEventMaskWords ); + Vec_IntPush( p->vQueue, Key ); + fNew = 1; + } + else if ( Abc_InfoHasBit(pWords, w) ) + return; + Abc_InfoSetBit( pWords, w ); + if ( !fNew ) + return; + for ( i = Vec_IntSize(p->vQueue) - 1; i > 0; i = Parent ) + { + Parent = (i - 1) >> 1; + if ( Vec_IntEntry(p->vQueue, Parent) <= Key ) + break; + Vec_IntWriteEntry( p->vQueue, i, + Vec_IntEntry(p->vQueue, Parent) ); + } + Vec_IntWriteEntry( p->vQueue, i, Key ); +} + +static int Cec_SeedSimEventHeapPop( Cec_SeedSim_t * p ) +{ + int Result = Vec_IntEntry( p->vQueue, 0 ); + int Last = Vec_IntPop( p->vQueue ); + int Size = Vec_IntSize( p->vQueue ); + int i = 0; + if ( Size == 0 ) + return Result; + while ( 2 * i + 1 < Size ) + { + int Child = 2 * i + 1; + if ( Child + 1 < Size && + Vec_IntEntry(p->vQueue, Child + 1) < + Vec_IntEntry(p->vQueue, Child) ) + Child++; + if ( Vec_IntEntry(p->vQueue, Child) >= Last ) + break; + Vec_IntWriteEntry( p->vQueue, i, + Vec_IntEntry(p->vQueue, Child) ); + i = Child; + } + Vec_IntWriteEntry( p->vQueue, i, Last ); + return Result; +} + +static void Cec_SeedSimEventRecordWord( Cec_SeedSim_t * p, + int Key, int w, unsigned OldValue ) +{ + Vec_IntPush( p->vValueUndo, Key ); + Vec_IntPush( p->vValueUndo, w ); + Vec_IntPush( p->vValueUndo, (int)OldValue ); +} + +static void Cec_SeedSimEventRecordChanged( Cec_SeedSim_t * p, int Key ) +{ + if ( p->pProcessMark[Key] == p->nProcessVersion ) + return; + p->pProcessMark[Key] = p->nProcessVersion; + Vec_IntPush( p->vChangedValues, Key ); +} + +static int Cec_SeedSimEventQueueFanouts( Cec_SeedSim_t * p, + int Frame, int ObjId, int w, int nEdgeLimit ) +{ + int FanId, i; + Gia_ObjForEachFanoutStaticId( p->pAig, ObjId, FanId, i ) + { + Gia_Obj_t * pFan = Gia_ManObj( p->pAig, FanId ); + if ( ++p->nEventEdges > nEdgeLimit ) + return 0; + if ( Gia_ObjIsAnd(pFan) ) + { + int FanKey = Cec_SeedSimKey(p, Frame, FanId); + if ( Cec_SeedSimConeHasKey(p, FanKey) ) + Cec_SeedSimEventHeapPushWord( p, FanKey, w ); + } + else if ( Gia_ObjIsRi(p->pAig, pFan) && + Frame + 1 < p->nFrames ) + { + int RoKey = Cec_SeedSimKey( + p, Frame + 1, Gia_ObjRiToRoId(p->pAig, FanId)); + if ( Cec_SeedSimConeHasKey(p, RoKey) ) + Cec_SeedSimEventHeapPushWord( p, RoKey, w ); + } + } + return 1; +} + +static int Cec_SeedSimEventUpdateInput( Cec_SeedSim_t * p, + int iVar, int nEdgeLimit ) +{ + int Frame, ObjId, w, Key, fChanged = 0; + unsigned * pInput; + if ( iVar < p->nRegs ) + { + Frame = 0; + ObjId = Gia_ObjId( p->pAig, Gia_ManRo(p->pAig, iVar) ); + } + else + { + int iPi = (iVar - p->nRegs) % p->nPis; + Frame = (iVar - p->nRegs) / p->nPis; + ObjId = Gia_ObjId( p->pAig, Gia_ManPi(p->pAig, iPi) ); + } + Key = Cec_SeedSimKey( p, Frame, ObjId ); + if ( !Cec_SeedSimConeHasKey(p, Key) ) + return 1; + pInput = (unsigned *)Vec_PtrEntry( p->vSimInfo, iVar ); + for ( w = 0; w < p->nWords; w++ ) + { + unsigned * pValue = Cec_SeedSimVal( p, Frame, ObjId ); + if ( pValue[w] == pInput[w] ) + continue; + Cec_SeedSimEventRecordWord( + p, Key, w, pValue[w] ); + pValue[w] = pInput[w]; + fChanged = 1; + if ( !Cec_SeedSimEventQueueFanouts( + p, Frame, ObjId, w, nEdgeLimit) ) + return 0; + } + if ( !fChanged ) + return 1; + Cec_SeedSimEventRecordChanged( p, Key ); + return 1; +} + +static int Cec_SeedSimEventUpdateNode( Cec_SeedSim_t * p, + int Key, int nNodeLimit, int nEdgeLimit ) +{ + int Frame = Key / p->nObjs; + int ObjId = Key % p->nObjs; + Gia_Obj_t * pObj = Gia_ManObj( p->pAig, ObjId ); + unsigned * pDst = Cec_SeedSimVal( p, Frame, ObjId ); + unsigned * pVal0, * pVal1 = NULL; + unsigned * pWords = p->pEventWords + (size_t)Key * p->nEventMaskWords; + int m, w, fChanged = 0; + if ( Gia_ObjIsRo(p->pAig, pObj) ) + { + Gia_Obj_t * pRi; + int RiId; + assert( Frame > 0 ); + pRi = Gia_ObjRoToRi( p->pAig, pObj ); + RiId = Gia_ObjId( p->pAig, pRi ); + pVal0 = Cec_SeedSimVal( + p, Frame - 1, Gia_ObjFaninId0(pRi, RiId) ); + for ( m = 0; m < p->nEventMaskWords; m++ ) + { + unsigned Bits = pWords[m]; + while ( Bits ) + { + w = 32 * m + Gia_WordFindFirstBit( Bits ); + Bits &= Bits - 1; + if ( w >= p->nWords ) + continue; + if ( ++p->nEventPops > nNodeLimit ) + return 0; + { + unsigned Value = Gia_ObjFaninC0(pRi) ? ~pVal0[w] : pVal0[w]; + if ( pDst[w] == Value ) + continue; + Cec_SeedSimEventRecordWord( p, Key, w, pDst[w] ); + pDst[w] = Value; + fChanged = 1; + if ( !Cec_SeedSimEventQueueFanouts( + p, Frame, ObjId, w, nEdgeLimit) ) + return 0; + } + } + } + } + else + { + assert( Gia_ObjIsAnd(pObj) ); + pVal0 = Cec_SeedSimVal( + p, Frame, Gia_ObjFaninId0(pObj, ObjId) ); + pVal1 = Cec_SeedSimVal( + p, Frame, Gia_ObjFaninId1(pObj, ObjId) ); + for ( m = 0; m < p->nEventMaskWords; m++ ) + { + unsigned Bits = pWords[m]; + while ( Bits ) + { + w = 32 * m + Gia_WordFindFirstBit( Bits ); + Bits &= Bits - 1; + if ( w >= p->nWords ) + continue; + if ( ++p->nEventPops > nNodeLimit ) + return 0; + { + unsigned Val0 = Gia_ObjFaninC0(pObj) ? ~pVal0[w] : pVal0[w]; + unsigned Val1 = Gia_ObjFaninC1(pObj) ? ~pVal1[w] : pVal1[w]; + unsigned Value = Val0 & Val1; + if ( pDst[w] == Value ) + continue; + Cec_SeedSimEventRecordWord( p, Key, w, pDst[w] ); + pDst[w] = Value; + fChanged = 1; + if ( !Cec_SeedSimEventQueueFanouts( + p, Frame, ObjId, w, nEdgeLimit) ) + return 0; + } + } + } + } + if ( !fChanged ) + return 1; + Cec_SeedSimEventRecordChanged( p, Key ); + return 1; +} + +static void Cec_SeedSimEventRollbackValues( Cec_SeedSim_t * p ) +{ + int i, Key, w; + for ( i = Vec_IntSize(p->vValueUndo) - 3; i >= 0; i -= 3 ) + { + Key = Vec_IntEntry( p->vValueUndo, i ); + w = Vec_IntEntry( p->vValueUndo, i + 1 ); + Cec_SeedSimVal( + p, Key / p->nObjs, Key % p->nObjs)[w] = + (unsigned)Vec_IntEntry( p->vValueUndo, i + 2 ); + } + Vec_IntClear( p->vValueUndo ); + Vec_IntClear( p->vChangedValues ); +} + +static void Cec_SeedSimEventRefine( Cec_SeedSim_t * p, Cec_ManSim_t * pSim ) +{ + int iLo = 0; + p->pRefineMask = p->pActiveMask; + // Baseline classes are value-consistent. If a pair becomes different, + // at least one member changed, so regrouping these roots is complete. + Vec_IntSort( p->vChangedValues, 0 ); + while ( iLo < Vec_IntSize(p->vChangedValues) ) + { + int Frame = Vec_IntEntry(p->vChangedValues, iLo) / p->nObjs; + int iHi = iLo, i, Key, ObjId; + while ( iHi < Vec_IntSize(p->vChangedValues) && + Vec_IntEntry(p->vChangedValues, iHi) / p->nObjs == Frame ) + iHi++; + Cec_SeedSimStartRootSet( p ); + for ( i = iLo; i < iHi; i++ ) + { + Key = Vec_IntEntry( p->vChangedValues, i ); + ObjId = Key % p->nObjs; + if ( Gia_ObjIsConst(p->pAig, ObjId) || + Gia_ObjIsClass(p->pAig, ObjId) ) + Cec_SeedSimAddRoot( p, ObjId ); + } + Cec_SeedSimRefineFrame( p, pSim, Frame ); + iLo = iHi; + } +} + +static void Cec_SeedSimQueueInitialSplits( Cec_SeedSim_t * p, int nInitialSplits ) +{ + int i, Key; + for ( i = 0; i < nInitialSplits; i++ ) + { + Key = Vec_IntEntry( p->vSplitKeys, i ); + int Frame = Key / p->nObjs; + int ObjId = Key % p->nObjs; + if ( Cec_SeedSimMark(p, Frame, ObjId) ) + Vec_IntPush( p->vQueue, Key ); + } +} + +static void Cec_SeedSimCollectWave( Cec_SeedSim_t * p ) +{ + int i, Key; + Vec_IntClear( p->vWaveKeys ); + Vec_IntForEachEntry( p->vDirtyKeys, Key, i ) + { + if ( p->pProcessMark[Key] == p->nProcessVersion ) + continue; + p->pProcessMark[Key] = p->nProcessVersion; + Vec_IntPush( p->vWaveKeys, Key ); + } +} + +static int Cec_SeedSimTryBatchLegacy( Cec_SeedSim_t * p, Cec_ManSim_t * pSim, + Vec_Ptr_t * vSimInfo, Vec_Int_t * vOutputs, Vec_Int_t * vOutBits, int nFrames ) +{ + ABC_INT64_T nKeys = (ABC_INT64_T)p->nFrames * p->nObjs; + int nLimit = (int)(nKeys * CEC_SEEDSIM_HARD_FRAC_NUM / CEC_SEEDSIM_HARD_FRAC_DEN); + int nDiagLimit = (int)(nKeys * CEC_SEEDSIM_DIAG_FRAC_NUM / CEC_SEEDSIM_DIAG_FRAC_DEN); + int nTfoLimit = (int)(nKeys * CEC_SEEDSIM_TFO_FRAC_NUM / CEC_SEEDSIM_TFO_FRAC_DEN); + int nBatchCex = Vec_IntSize(vOutBits) / 2; + int nPackedLanes = 32 * p->nWords - 1; + int nInitialSplits, nDirty; + assert( nFrames == p->nFrames ); + assert( Vec_PtrSize(vSimInfo) == p->nRegs + p->nPis * p->nFrames ); + assert( Vec_PtrReadWordsSimInfo(vSimInfo) == p->nWords ); + Cec_SeedSimRecordBatch( p, nBatchCex ); + if ( !p->fInitialized ) + { + p->nFallbackPre++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL; + } + if ( nBatchCex > CEC_SEEDSIM_CEX_LANE_FACTOR * nPackedLanes ) + { + p->nFallbackCex++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL_WIDE; + } + Cec_SeedSimReset( p ); + p->vBatchInfo = vSimInfo; + if ( !Cec_SeedSimDiagnosisShapeSmall(p, vOutputs, vOutBits, nDiagLimit) ) + { + nDirty = Vec_IntSize( p->vDirtyKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + p->vBatchInfo = NULL; + p->nFallbackPre++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL_WIDE; + } + Cec_SeedSimRestartTfoMarks( p ); + if ( !Cec_SeedSimCollectDiagnosis(p, vOutputs, vOutBits, nLimit) || + Vec_IntSize(p->vDiagKeys) > nLimit ) + { + nDirty = Abc_MaxInt( p->nSpecKeys, p->nEvalKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + p->vBatchInfo = NULL; + p->nFallbackPre++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL_WIDE; + } + if ( !Cec_SeedSimDiagnosisEvalShapeSmall(p, p->vDiagKeys, nDiagLimit) ) + { + nDirty = Vec_IntSize( p->vDirtyKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + p->vBatchInfo = NULL; + p->nFallbackPre++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL_WIDE; + } + Cec_SeedSimRestartTfoMarks( p ); + Cec_SeedSimUseCexLanes( p ); + Cec_SeedSimTxnBegin( p ); + if ( !Cec_SeedSimProcessKeys(p, pSim, p->vDiagKeys, nLimit, 1) ) + { + nDirty = Abc_MaxInt( p->nSpecKeys, p->nEvalKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + Cec_SeedSimTxnRollback( p ); + p->vBatchInfo = NULL; + p->nFallbackProcess++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL; + } + { + int nMissing; + nMissing = Cec_SeedSimDiagnosisMissing( p ); + if ( nMissing ) + { + nDirty = Abc_MaxInt( p->nSpecKeys, p->nEvalKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + Cec_SeedSimTxnRollback( p ); + p->vBatchInfo = NULL; + p->nCoverageMiss += nMissing; + p->nFallbackCoverage++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL; + } + } + Cec_SeedSimTxnCommit( p ); + Cec_SeedSimUsePackedLanes( p ); + nInitialSplits = Vec_IntSize( p->vSplitKeys ); + Cec_SeedSimQueueInitialSplits( p, nInitialSplits ); + if ( !Cec_SeedSimComputeTfo(p, nTfoLimit) ) + { + nDirty = Vec_IntSize( p->vDirtyKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + p->vBatchInfo = NULL; + p->nBatchTrunc++; + p->nTruncCone++; + p->nBatchLocal++; + return CEC_SEEDSIM_RESULT_LOCAL; + } + Cec_SeedSimCollectWave( p ); + if ( Vec_IntSize(p->vWaveKeys) && + !Cec_SeedSimProcessKeys(p, pSim, p->vWaveKeys, nTfoLimit, 0) ) + { + p->nDeferredSplits += Vec_IntSize(p->vSplitKeys) - nInitialSplits; + if ( p->nEvalKeys > p->nMaxDirty ) + p->nMaxDirty = p->nEvalKeys; + p->vBatchInfo = NULL; + p->nBatchTrunc++; + p->nTruncEval++; + p->nBatchLocal++; + return CEC_SEEDSIM_RESULT_LOCAL; + } + p->nDeferredSplits += Vec_IntSize(p->vSplitKeys) - nInitialSplits; + nDirty = Abc_MaxInt( p->nSpecKeys, Vec_IntSize(p->vDirtyKeys) ); + nDirty = Abc_MaxInt( nDirty, p->nEvalKeys ); + if ( nDirty > p->nMaxDirty ) + p->nMaxDirty = nDirty; + p->vBatchInfo = NULL; + p->nBatchLocal++; + return CEC_SEEDSIM_RESULT_LOCAL; +} + +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 ) +{ + ABC_INT64_T nKeys = (ABC_INT64_T)p->nFrames * p->nObjs; + ABC_INT64_T nWordKeys = nKeys * p->nWords; + ABC_INT64_T nNodeLimit64 = nWordKeys * + CEC_EVENT_NODE_WORD_FRAC_NUM / CEC_EVENT_NODE_WORD_FRAC_DEN; + ABC_INT64_T nEdgeLimit64 = nWordKeys * + CEC_EVENT_EDGE_WORD_FRAC_NUM / CEC_EVENT_EDGE_WORD_FRAC_DEN; + int nNodeLimit = nNodeLimit64 > 0x7fffffff ? 0x7fffffff : (int)nNodeLimit64; + int nEdgeLimit = nEdgeLimit64 > 0x7fffffff ? 0x7fffffff : (int)nEdgeLimit64; + int nInputVars = Vec_IntSize( p->vChangedInputs ); + int nInputWords = Vec_IntSize( p->vInputUndo ) / 2; + int nTotalInputs = p->nRegs + p->nPis * p->nFrames; + int i, iVar, Key; + int Status = CEC_SEEDSIM_RESULT_LOCAL; + assert( nFrames == p->nFrames ); + assert( vSimInfo == p->vSimInfo ); + Cec_SeedSimRecordBatch( p, Vec_IntSize(vOutBits) / 2 ); + p->nEventInputVarsMax = Abc_MaxInt( p->nEventInputVarsMax, nInputVars ); + p->nEventInputWordsMax = Abc_MaxInt( p->nEventInputWordsMax, nInputWords ); + if ( (ABC_INT64_T)nInputVars * CEC_EVENT_INPUT_FRAC_DEN > + (ABC_INT64_T)nTotalInputs * CEC_EVENT_INPUT_FRAC_NUM ) + { + p->nFallbackCex++; + p->nBatchFull++; + return CEC_SEEDSIM_RESULT_FULL_WIDE; + } + (void)vOutputs; + Cec_SeedSimReset( p ); + Vec_IntClear( p->vValueUndo ); + Vec_IntClear( p->vChangedValues ); + p->nEventPops = p->nEventEdges = 0; + + Vec_IntForEachEntry( p->vChangedInputs, iVar, i ) + if ( !Cec_SeedSimEventUpdateInput(p, iVar, nEdgeLimit) ) + { + Status = CEC_SEEDSIM_RESULT_FULL_WIDE; + break; + } + while ( Status == CEC_SEEDSIM_RESULT_LOCAL && + Vec_IntSize(p->vQueue) > 0 ) + { + Key = Cec_SeedSimEventHeapPop( p ); + if ( !Cec_SeedSimEventUpdateNode( + p, Key, nNodeLimit, nEdgeLimit) ) + { + Status = CEC_SEEDSIM_RESULT_FULL_WIDE; + break; + } + } + p->nEventPopsMax = Abc_MaxInt( p->nEventPopsMax, p->nEventPops ); + p->nEventEdgesMax = Abc_MaxInt( p->nEventEdgesMax, p->nEventEdges ); + p->nMaxDirty = Abc_MaxInt( + p->nMaxDirty, Vec_IntSize(p->vChangedValues) ); + if ( Status != CEC_SEEDSIM_RESULT_LOCAL ) + { + Cec_SeedSimEventRollbackValues( p ); + p->nEventFallback++; + p->nEventFallbackWork++; + p->nFallbackPre++; + p->nBatchFull++; + return Status; + } + Cec_SeedSimTxnBegin( p ); + Cec_SeedSimEventRefine( p, pSim ); + Cec_SeedSimTxnCommit( p ); + Vec_IntClear( p->vValueUndo ); + Vec_IntClear( p->vChangedValues ); + Cec_SeedSimCommitPersistentInputs( p ); + p->nEventLocal++; + p->nBatchLocal++; + return CEC_SEEDSIM_RESULT_LOCAL; +} + +void Cec_SeedSimSaveFrameInputs( Cec_SeedSim_t * p, Vec_Ptr_t * vInfoCis, int Frame ) +{ + Gia_Obj_t * pObj; + int i; + assert( Frame >= 0 && Frame < p->nFrames ); + assert( Vec_PtrSize(vInfoCis) == p->nPis + p->nRegs ); + assert( Vec_PtrReadWordsSimInfo(vInfoCis) == p->nWords ); + Cec_SeedSimSetPhase( p, Frame, 0, 0 ); + Gia_ManForEachCi( p->pAig, pObj, i ) + Cec_SeedSimSetPhase( p, Frame, Gia_ObjId(p->pAig, pObj), 0 ); +} + +void Cec_SeedSimSaveFrameOutputs( Cec_SeedSim_t * p, Vec_Ptr_t * vInfoCos, int Frame ) +{ + Gia_Obj_t * pObj; + int i; + assert( Frame >= 0 && Frame < p->nFrames ); + assert( Vec_PtrSize(vInfoCos) == Gia_ManCoNum(p->pAig) ); + assert( Vec_PtrReadWordsSimInfo(vInfoCos) == p->nWords ); + Gia_ManForEachCo( p->pAig, pObj, i ) + Cec_SeedSimSetPhase( p, Frame, Gia_ObjId(p->pAig, pObj), + ((unsigned *)Vec_PtrEntry(vInfoCos, i))[0] & 1 ); +} + +void Cec_SeedSimFinishFull( Cec_SeedSim_t * p ) +{ + p->fInitialized = 1; +} + +void Cec_SeedSimBeginCall( Cec_SeedSim_t * p ) +{ + assert( !p->fTxnActive ); + p->nBatchLocal = p->nBatchFull = p->nBatchTrunc = p->nMaxDirty = 0; + p->nBatchRollback = p->nRollbackObjs = p->nCoverageMiss = 0; + p->nFallbackPre = p->nFallbackProcess = p->nFallbackCoverage = 0; + p->nFallbackCex = p->nFallbackBypass = 0; + p->nTruncCone = p->nTruncEval = 0; + p->nBatchCex = p->nBatchCexMax = p->nDeferredSplits = 0; + p->nEventLocal = p->nEventFallback = 0; + p->nEventPopsMax = p->nEventEdgesMax = 0; + p->nEventInputVarsMax = p->nEventInputWordsMax = 0; + p->nEventFallbackWork = 0; +} + +void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex ) +{ + Cec_SeedSimRecordBatch( p, nCex ); + p->nFallbackBypass++; + p->nBatchFull++; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index f732565672..f2f608fa83 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -174,14 +174,183 @@ struct Cec_IncrMgr_t_ int nObjs; // cached Gia_ManObjNum(pAig) Vec_Int_t * vReprPrev; // snapshot of pReprs 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) 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 * vBfsNext; // BFS frontier carried to next frame 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 /// //////////////////////////////////////////////////////////////////////// @@ -192,8 +361,13 @@ struct Cec_IncrMgr_t_ /*=== cecCorr.c ============================================================*/ 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 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 ============================================================*/ extern Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames ); 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 void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive ); 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 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 ============================================================*/ 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_ManSimClassesRefine( Cec_ManSim_t * p ); 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 ============================================================*/ extern int * Cec_ManDetectIsomorphism( Gia_Man_t * p ); /*=== 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 ); /*=== cecSeq.c ============================================================*/ 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 void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ); 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 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_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_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 ); diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c index 81420e032e..629941b74e 100644 --- a/src/proof/cec/cecSeq.c +++ b/src/proof/cec/cecSeq.c @@ -170,6 +170,53 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) 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************************************************************* Synopsis [Resimulates information to refine equivalence classes.] diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index f8342859ab..a3518e76b7 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -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) ); } +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************************************************************* 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 [] ***********************************************************************/ -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; Vec_Int_t * vCexStore; + Vec_Int_t * vOutVals = NULL; Vec_Str_t * vStatus; Cec_ManSat_t * p; 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 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); vCexStore = Vec_IntAlloc( 10000 ); + if ( pvOutVals ) + { + *pvOutVals = NULL; + if ( vOutLits ) + vOutVals = Vec_IntStartFull( 2 * Gia_ManPoNum(pAig) ); + } // perform solving p = Cec_ManSatCreate( pAig, pPars ); 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 ) continue; assert( status == 0 ); + Cec_ManSatSaveOutVals( p, vOutLits, vOutVals, i ); // save the pattern // Gia_ManIncrementTravId( pAig ); // 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_ManSatStop( p ); *pvStatus = vStatus; + if ( pvOutVals ) + *pvOutVals = vOutVals; + else + Vec_IntFreeP( &vOutVals ); 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 /// diff --git a/src/proof/cec/module.make b/src/proof/cec/module.make index d9d921e2d2..a009e3b714 100644 --- a/src/proof/cec/module.make +++ b/src/proof/cec/module.make @@ -3,7 +3,9 @@ SRC += src/proof/cec/cecCec.c \ src/proof/cec/cecClass.c \ src/proof/cec/cecCore.c \ src/proof/cec/cecCorr.c \ + src/proof/cec/cecCorrDyn.c \ src/proof/cec/cecCorrIncr.c \ + src/proof/cec/cecCorrIncrSim.c \ src/proof/cec/cecIso.c \ src/proof/cec/cecMan.c \ src/proof/cec/cecPat.c \