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

Merge pull request #506 from zxxr1113/incremental_scorr_clean 

New feature: Add incremental refinement to &scorr command
This commit is contained in:
alanminko 2026-05-11 14:36:23 -07:00 committed by GitHub
parent 8c9e66205e 97b15a29a0
commit 9d410e8163
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 809 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -6681,6 +6681,10 @@ SOURCE=.\src\proof\cec\cecCorr.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecCorrIncr.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecInt.h
# End Source File
# Begin Source File

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

@ -41167,7 +41167,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManCorSetDefaultParams( pPars );
pPars->nProcs = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqiowvh" ) ) != EOF )
{
switch ( c )
{
@ -41266,6 +41266,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'q':
pPars->fStopWhenGone ^= 1;
break;
case 'i':
pPars->fIncremental ^= 1;
break;
case 'o':
fUseOld ^= 1;
break;
@ -41339,7 +41342,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqowvh]\n" );
Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqiowvh]\n" );
Abc_Print( -2, "\t performs signal correpondence computation\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@ -41354,6 +41357,7 @@ usage:
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-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" );

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

@ -167,6 +167,7 @@ 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 fVerboseFlops; // verbose stats
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats

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

@ -34,7 +34,10 @@ static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
// Shared with cecCorrIncr.c (declared in cecInt.h).
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 ///
@ -45,13 +48,13 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
Synopsis [Computes the real value of the literal w/o spec reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
if ( Gia_ObjIsAnd(pObj) )
{
@ -792,7 +795,7 @@ int Cec_ManCountLits( Gia_Man_t * p )
***********************************************************************/
void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
{
{
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Vec_Str_t * vStatus;
@ -801,6 +804,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
int fChanges, RetValue, i;
Cec_IncrMgr_t * pBmcMgr = NULL;
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
@ -813,20 +817,44 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fIncremental )
{
pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs );
Cec_IncrMgrSnapshotClasses( pBmcMgr );
}
fChanges = 1;
for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
{
int * pTfoMask = NULL;
int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0, fConverged = 0;
if ( Cec_ParCorShouldStop( pPars ) )
break;
abctime clkBmc = Abc_Clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
// BMC SRM is non-ring (Gia_ManCorrSpecReduceInit ignores fRings);
// 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 )
break;
}
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 );
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) );
if ( pBmcMgr )
Cec_IncrMgrSnapshotClasses( pBmcMgr );
if ( Gia_ManPoNum(pSrm) == 0 )
{
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
break;
}
}
pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat )
vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
@ -849,6 +877,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
if ( Cec_ParCorShouldStop( pPars ) )
break;
}
Cec_IncrMgrFree( pBmcMgr );
Cec_ManSimStop( pSim );
}
@ -949,6 +978,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
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)
abctime clkIncr = 0;
int nIncrSkipped = 0, nIncrFallback = 0;
if ( Gia_ManRegNum(pAig) == 0 )
{
Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
@ -999,25 +1031,65 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ManSimStop( pSim );
return 1;
}
if ( pPars->fIncremental )
{
pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames );
Cec_IncrMgrSnapshotClasses( pMgr );
}
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
{
if ( Cec_ParCorShouldStop( pPars ) )
{
Cec_ManSimStop( pSim );
Cec_IncrMgrFree( pMgr );
return 1;
}
if ( pPars->nStepsMax == r )
{
Cec_ManSimStop( pSim );
Cec_IncrMgrFree( pMgr );
Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
fflush( stdout );
return 1;
}
clk = Abc_Clock();
// perform speculative reduction
// perform speculative reduction (with optional active-list filter)
clk2 = Abc_Clock();
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
{
int * pTfoMask = NULL;
int nReprSeeds = 0, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0;
int fConverged = 0;
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 )
{
clkSrm += Abc_Clock() - clk2;
break;
}
if ( pTfoMask == NULL )
nIncrFallback++;
else
nIncrSkipped += nTotalPairs - nActivePairs;
}
if ( pTfoMask )
pSrm = Gia_ManCorrSpecReduce_Active( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr );
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.
if ( pMgr )
Cec_IncrMgrSnapshotClasses( pMgr );
}
assert( 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 )
@ -1058,6 +1130,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
if ( Cec_ParCorShouldStop( pPars ) )
{
Cec_ManSimStop( pSim );
Cec_IncrMgrFree( pMgr );
return 1;
}
// quit if const is no longer there
@ -1067,6 +1140,7 @@ 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_IncrMgrFree( pMgr );
return 0;
}
if ( pPars->nLimitMax )
@ -1078,6 +1152,7 @@ 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_IncrMgrFree( pMgr );
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
return 0;
@ -1105,11 +1180,17 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
if ( pMgr )
{
ABC_PRTP( "Incr ", clkIncr, clkTotal );
Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped );
}
Abc_PrintTime( 1, "TOTAL", clkTotal );
fflush( stdout );
}
Cec_IncrMgrFree( pMgr );
return 1;
}
}
/**Function*************************************************************

674
src/proof/cec/cecCorrIncr.c Normal file
View File

@ -0,0 +1,674 @@
/**CFile****************************************************************
FileName [cecCorrIncr.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Incremental active-list / TFO filter for &scorr.]
Author [Xiran Zhao]
Affiliation [University of Chinese Academy of Sciences]
Date [Ver. 1.0. Started - May 2026.]
***********************************************************************/
#include "cecInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates the incremental active-list manager.]
Description [The manager owns one snapshot of pReprs/pNexts plus the
TFO bookkeeping arrays. pAig must outlive the manager; the manager
never duplicates the AIG, only references it. If the host AIG does
not yet carry a static fanout, this routine builds it and remembers
to tear it down on Free.]
SideEffects [Builds static fanout on pAig if not already present.]
SeeAlso []
***********************************************************************/
Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames )
{
Cec_IncrMgr_t * p = ABC_CALLOC( Cec_IncrMgr_t, 1 );
p->pAig = pAig;
p->nFrames = nFrames;
p->nObjs = Gia_ManObjNum(pAig);
p->vReprPrev = Vec_IntStartFull( p->nObjs );
p->vNextPrev = Vec_IntStart( p->nObjs );
p->vSeeds = Vec_IntAlloc( 64 );
p->vTfoNodes = Vec_IntAlloc( 1024 );
p->pTfoMark = ABC_CALLOC( int, p->nObjs );
p->vBfsCur = Vec_IntAlloc( 1024 );
p->vBfsNext = Vec_IntAlloc( 1024 );
if ( pAig->vFanout == NULL )
{
Gia_ManStaticFanoutStart( pAig );
p->fOwnsFanout = 1;
}
return p;
}
/**Function*************************************************************
Synopsis [Frees the incremental manager.]
Description [Releases all internal vectors and the TFO mark array.
If the manager built the static fanout on Alloc, it is also torn
down here. Safe to call with a NULL pointer.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_IncrMgrFree( Cec_IncrMgr_t * p )
{
if ( p == NULL ) return;
if ( p->fOwnsFanout )
Gia_ManStaticFanoutStop( p->pAig );
Vec_IntFree( p->vReprPrev );
Vec_IntFree( p->vNextPrev );
Vec_IntFree( p->vSeeds );
Vec_IntFree( p->vTfoNodes );
Vec_IntFree( p->vBfsCur );
Vec_IntFree( p->vBfsNext );
ABC_FREE( p->pTfoMark );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Snapshots the current equivalence-class state.]
Description [Copies the per-node pReprs and pNexts arrays into the
manager so the next iteration can diff against the class state whose
pairs were just emitted into the SRM. Should be called after SRM
construction and before SAT/sim refinement: the snapshot then reflects
exactly the pairs the SAT solver was asked to prove. O(N).]
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p )
{
Gia_Man_t * pAig = p->pAig;
int i;
assert( pAig->pReprs != NULL );
for ( i = 0; i < p->nObjs; i++ )
{
Vec_IntWriteEntry( p->vReprPrev, i, Gia_ObjRepr(pAig, i) );
Vec_IntWriteEntry( p->vNextPrev, i, pAig->pNexts ? Gia_ObjNext(pAig, i) : 0 );
}
}
/**Function*************************************************************
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.]
SideEffects []
SeeAlso [Cec_IncrMgrComputeTfo Cec_IncrMgrRingEdgeChanged]
***********************************************************************/
int Cec_IncrMgrComputeSeeds( Cec_IncrMgr_t * p )
{
Gia_Man_t * pAig = p->pAig;
int i, reprNew, reprOld;
Vec_IntClear( p->vSeeds );
for ( i = 1; i < p->nObjs; i++ )
{
reprNew = Gia_ObjRepr( pAig, i );
reprOld = Vec_IntEntry( p->vReprPrev, i );
if ( reprNew != reprOld )
Vec_IntPush( p->vSeeds, i );
}
return Vec_IntSize( p->vSeeds );
}
/**Function*************************************************************
Synopsis [Counts nodes whose ring-list successor changed.]
Description [Used only for convergence and fallback decisions. These
nodes are NOT TFO seeds, because a pNexts-only change creates a new
ring edge (proved edge-locally by the active SRM builder) rather than
a new fanout cone to re-prove. Returns 0 when pNexts is unallocated,
i.e. when ring mode is off.]
SideEffects []
SeeAlso [Cec_IncrMgrComputeSeeds]
***********************************************************************/
int Cec_IncrMgrCountNextChanges( Cec_IncrMgr_t * p )
{
Gia_Man_t * pAig = p->pAig;
int i, nChanges = 0;
if ( pAig->pNexts == NULL )
return 0;
for ( i = 1; i < p->nObjs; i++ )
nChanges += Gia_ObjNext( pAig, i ) != Vec_IntEntry( p->vNextPrev, i );
return nChanges;
}
/**Function*************************************************************
Synopsis [Detects whether a ring edge is new since the last snapshot.]
Description [Ring classes store list edges explicitly in pNexts, but
the SRM also proves the implicit closing edge tail -> head. For an
explicit edge, the edge is unchanged iff the predecessor's pNexts slot
still names the same successor. For the closing edge there is no
pNexts slot to compare, so we reconstruct whether the same tail/head
pair already existed in the previous snapshot: the tail must have been
pointing to the head (closing the ring) and the head must still have
been a class root. Returns 1 to mean "must be re-proved". Passing a
NULL manager or a non-ring AIG returns 0 (no edge work needed).]
SideEffects []
SeeAlso [Cec_IncrMgrCountActivePairs]
***********************************************************************/
int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj )
{
Gia_Man_t * pAig;
int iNextCur, iNextOld;
if ( p == NULL )
return 0;
pAig = p->pAig;
if ( pAig->pNexts == NULL )
return 0;
iNextCur = Gia_ObjNext( pAig, iPrev );
iNextOld = Vec_IntEntry( p->vNextPrev, iPrev );
if ( iNextCur == iObj )
return iNextOld != iObj;
if ( iNextCur > 0 )
return 1; // conservative: should not happen for callers below
// Closing edge: prove if the previous snapshot did not already contain
// exactly this tail/head pair as a ring's closing edge.
return iNextOld > 0 ||
Vec_IntEntry( p->vReprPrev, iPrev ) != iObj ||
Vec_IntEntry( p->vReprPrev, iObj ) != GIA_VOID ||
Vec_IntEntry( p->vNextPrev, iObj ) <= 0;
}
/**Function*************************************************************
Synopsis [Counts total and active candidate pairs before SRM build.]
Description [Mirrors the PO-emission loops in the active SRM builders
but stops before constructing the unrolled network: it walks every
candidate pair the SRM would emit and tallies how many would survive
the active filter (pTfoMark plus the ring-edge override). The count
is approximate because SRM construction can still simplify a pair
away after the literal it represents collapses; it is used only to
decide whether the active filter saves enough work to be worth the
bookkeeping (the main loop falls back to the full SRM above ~70%
active pairs). When pTfoMark is NULL every pair is counted active.]
SideEffects []
SeeAlso [Gia_ManCorrSpecReduce_Active]
***********************************************************************/
void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_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) += pTfoMark == NULL || pTfoMark[i];
}
else if ( Gia_ObjIsHead( pAig, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( pAig, i, iObj )
{
(*pnTotal)++;
(*pnActive) += pTfoMark == NULL || pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( p, iPrev, iObj );
iPrev = iObj;
}
iObj = i; // closing edge tail -> head
(*pnTotal)++;
(*pnActive) += pTfoMark == NULL || pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( p, 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) += pTfoMark == NULL || pTfoMark[i] || pTfoMark[idR];
}
}
}
/**Function*************************************************************
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.
RI nodes themselves are intentionally not marked: SRM emission is
keyed on AIG candidate nodes (ANDs and CIs) and never on COs, so
marking RIs would only inflate the active set without enabling any
additional pair.
Mark clearing is amortised: vTfoNodes records every id touched in
the previous round and is iterated to zero only those entries, so
the routine never sweeps the full N-sized array. Cost per call is
O(|TFO_k| * avg_fanout).]
SideEffects []
SeeAlso [Cec_IncrMgrComputeSeeds]
***********************************************************************/
void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p )
{
Gia_Man_t * pAig = p->pAig;
int * pMark = p->pTfoMark;
int f, i, k, Id, FanId, RoId;
Vec_IntForEachEntry( p->vTfoNodes, Id, i )
pMark[Id] = 0;
Vec_IntClear( p->vTfoNodes );
Vec_IntClear( p->vBfsCur );
Vec_IntClear( p->vBfsNext );
Vec_IntForEachEntry( p->vSeeds, Id, i )
{
if ( !pMark[Id] )
{
pMark[Id] = 1;
Vec_IntPush( p->vTfoNodes, Id );
Vec_IntPush( p->vBfsCur, Id );
}
}
for ( f = 0; f <= p->nFrames; f++ )
{
int head = 0;
while ( head < Vec_IntSize(p->vBfsCur) )
{
Gia_Obj_t * pFan;
Id = Vec_IntEntry( p->vBfsCur, head++ );
int nFan = Gia_ObjFanoutNumId( pAig, Id );
for ( k = 0; k < nFan; k++ )
{
FanId = Gia_ObjFanoutId( pAig, Id, k );
pFan = Gia_ManObj( pAig, FanId );
if ( Gia_ObjIsRi(pAig, pFan) )
{
if ( f < p->nFrames )
{
RoId = Gia_ObjRiToRoId( pAig, FanId );
if ( !pMark[RoId] )
{
pMark[RoId] = 1;
Vec_IntPush( p->vTfoNodes, RoId );
Vec_IntPush( p->vBfsNext, RoId );
}
}
}
else if ( Gia_ObjIsCo(pFan) )
{
// PO: not a candidate, skip
}
else
{
if ( !pMark[FanId] )
{
pMark[FanId] = 1;
Vec_IntPush( p->vTfoNodes, FanId );
Vec_IntPush( p->vBfsCur, FanId );
}
}
}
}
Vec_IntClear( p->vBfsCur );
Vec_IntAppend( p->vBfsCur, p->vBfsNext );
Vec_IntClear( p->vBfsNext );
if ( Vec_IntSize(p->vBfsCur) == 0 )
break;
}
}
/**Function*************************************************************
Synopsis [Active-filter 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.
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.]
SideEffects []
SeeAlso [Gia_ManCorrSpecReduce]
***********************************************************************/
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 * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrev, iObj, iPrevNew, iObjNew;
assert( nFrames > 0 );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManHashAlloc( pNew );
Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
Gia_ManForEachRo( p, pObj, i )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
for ( f = 0; f < nFrames+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
if ( fRings )
{
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsConst( p, i ) )
{
if ( pTfoMark && !pTfoMark[i] )
continue;
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
{
Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i );
Vec_IntPush( vXorLits, iObjNew );
}
}
else if ( Gia_ObjIsHead( p, i ) )
{
// Walk every ring edge so iPrev stays aligned with the class
// order; emit only when an endpoint is in TFO or the edge is
// new/rewired since the last snapshot.
iPrev = i;
Gia_ClassForEachObj1( p, i, iObj )
{
int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj );
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)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
}
}
iPrev = iObj;
}
// Closing edge tail -> head
iObj = i;
{
int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] ||
Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj );
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)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
}
}
}
}
}
}
else
{
Gia_ManForEachObj1( p, pObj, i )
{
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] )
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) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
Vec_IntErase( &p->vCopies );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Active-filter variant of Gia_ManCorrSpecReduceInit (BMC SRM).]
Description [Mirrors Gia_ManCorrSpecReduceInit but emits a candidate
PO (pRepr, pObj) only when at least one of the two endpoints lies in
pTfoMark. The baseline BMC SRM accepts an fRings flag for symmetry
with the inductive builder but never inspects it -- its topology is
always (head, member) pairs derived from pReprs alone, with no ring
edges to close. Therefore this active variant only needs pReprs-
driven seeds: pNexts changes cannot affect this SRM and there is no
closing edge to reprove. Passing pTfoMark == NULL falls back to the
unfiltered baseline behaviour.]
SideEffects []
SeeAlso [Gia_ManCorrSpecReduceInit]
***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr,
Vec_Int_t ** pvOutputs, int * pTfoMark )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrevNew, iObjNew;
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
Vec_IntFill( &p->vCopies, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p), -1 );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
{
Gia_ManAppendCi(pNew);
Gia_ObjSetCopyF( p, 0, pObj, 0 );
}
for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
for ( f = nPrefix; f < nFrames+nPrefix; f++ )
{
Gia_ManForEachObj1( p, pObj, i )
{
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] )
continue;
}
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
Vec_IntErase( &p->vCopies );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
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
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -149,7 +149,7 @@ struct Cec_ManFra_t_
{
// parameters
Gia_Man_t * pAig; // the AIG to be used for simulation
Cec_ParFra_t * pPars; // SAT sweeping parameters
Cec_ParFra_t * pPars; // SAT sweeping parameters
// simulation patterns
Vec_Int_t * vXorNodes; // nodes used in speculative reduction
int nAllProved; // total number of proved nodes
@ -165,6 +165,23 @@ struct Cec_ManFra_t_
abctime timeTotal; // total runtime
};
// incremental active-list manager for &scorr -i
typedef struct Cec_IncrMgr_t_ Cec_IncrMgr_t;
struct Cec_IncrMgr_t_
{
Gia_Man_t * pAig; // host AIG (immutable across iterations)
int nFrames; // unrolling depth used by the SRM builder
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 * vTfoNodes; // ids currently in TFO (for fast clearing)
int * pTfoMark; // dense mark array, size = nObjs
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)
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -175,6 +192,20 @@ struct Cec_ManFra_t_
/*=== cecCorr.c ============================================================*/
extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time );
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 );
/*=== cecCorrIncr.c ============================================================*/
extern Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames );
extern void Cec_IncrMgrFree( Cec_IncrMgr_t * p );
extern void Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p );
extern int Cec_IncrMgrComputeSeeds( Cec_IncrMgr_t * p );
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_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 );
/*=== cecClass.c ============================================================*/
extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );

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

@ -3,6 +3,7 @@ SRC += src/proof/cec/cecCec.c \
src/proof/cec/cecClass.c \
src/proof/cec/cecCore.c \
src/proof/cec/cecCorr.c \
src/proof/cec/cecCorrIncr.c \
src/proof/cec/cecIso.c \
src/proof/cec/cecMan.c \
src/proof/cec/cecPat.c \