Skip to content

Commit 9d410e8

Browse files
alanminkoalanminko
authored
Merge pull request #506 from zxxr1113/incremental_scorr_clean
New feature: Add incremental refinement to &scorr command
2 parents 8c9e662 + 97b15a2 commit 9d410e8

7 files changed

Lines changed: 809 additions & 13 deletions

File tree

‎abclib.dsp‎

Lines changed: 4 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎src/base/abci/abc.c‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41167,7 +41167,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
4116741167
Cec_ManCorSetDefaultParams( pPars );
4116841168
pPars->nProcs = 1;
4116941169
Extra_UtilGetoptReset();
41170-
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
41170+
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqiowvh" ) ) != EOF )
4117141171
{
4117241172
switch ( c )
4117341173
{
@@ -41266,6 +41266,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
4126641266
case 'q':
4126741267
pPars->fStopWhenGone ^= 1;
4126841268
break;
41269+
case 'i':
41270+
pPars->fIncremental ^= 1;
41271+
break;
4126941272
case 'o':
4127041273
fUseOld ^= 1;
4127141274
break;
@@ -41339,7 +41342,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
4133941342
return 0;
4134041343

4134141344
usage:
41342-
Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqowvh]\n" );
41345+
Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqiowvh]\n" );
4134341346
Abc_Print( -2, "\t performs signal correpondence computation\n" );
4134441347
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
4134541348
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@@ -41354,6 +41357,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
4135441357
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
4135541358
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
4135641359
Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
41360+
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" );
4135741361
Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
4135841362
Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
4135941363
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );

‎src/proof/cec/cec.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -167,6 +167,7 @@ struct Cec_ParCor_t_
167167
// int fFirstStop; // stop on the first sat output
168168
int fUseSmartCnf; // use smart CNF computation
169169
int fStopWhenGone; // quit when PO is not a candidate constant
170+
int fIncremental; // active-list/TFO-triggered reproof in main loop
170171
int fVerboseFlops; // verbose stats
171172
int fVeryVerbose; // verbose stats
172173
int fVerbose; // verbose stats

‎src/proof/cec/cecCorr.c‎

Lines changed: 91 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,10 @@ static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
3434
/// DECLARATIONS ///
3535
////////////////////////////////////////////////////////////////////////
3636

37-
static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
37+
// Shared with cecCorrIncr.c (declared in cecInt.h).
38+
extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
39+
extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
40+
3841

3942
////////////////////////////////////////////////////////////////////////
4043
/// FUNCTION DEFINITIONS ///
@@ -45,13 +48,13 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
4548
Synopsis [Computes the real value of the literal w/o spec reduction.]
4649
4750
Description []
48-
51+
4952
SideEffects []
5053
5154
SeeAlso []
5255
5356
***********************************************************************/
54-
static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
57+
int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
5558
{
5659
if ( Gia_ObjIsAnd(pObj) )
5760
{
@@ -792,7 +795,7 @@ int Cec_ManCountLits( Gia_Man_t * p )
792795
793796
***********************************************************************/
794797
void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
795-
{
798+
{
796799
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
797800
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
798801
Vec_Str_t * vStatus;
@@ -801,6 +804,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
801804
Cec_ManSim_t * pSim;
802805
Gia_Man_t * pSrm;
803806
int fChanges, RetValue, i;
807+
Cec_IncrMgr_t * pBmcMgr = NULL;
804808
// prepare simulation manager
805809
Cec_ManSimSetDefaultParams( pParsSim );
806810
pParsSim->nWords = pPars->nWords;
@@ -813,20 +817,44 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
813817
Cec_ManSatSetDefaultParams( pParsSat );
814818
pParsSat->nBTLimit = pPars->nBTLimit;
815819
pParsSat->fVerbose = pPars->fVerbose;
820+
if ( pPars->fIncremental )
821+
{
822+
pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs );
823+
Cec_IncrMgrSnapshotClasses( pBmcMgr );
824+
}
816825
fChanges = 1;
817826
for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
818827
{
828+
int * pTfoMask = NULL;
829+
int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0, fConverged = 0;
819830
if ( Cec_ParCorShouldStop( pPars ) )
820831
break;
821832
abctime clkBmc = Abc_Clock();
822833
fChanges = 0;
823-
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
834+
// BMC SRM is non-ring (Gia_ManCorrSpecReduceInit ignores fRings);
835+
// the incremental mask filters on pReprs-derived endpoints only.
836+
if ( pBmcMgr && i > 0 )
837+
{
838+
pTfoMask = Cec_IncrMgrDecideMask( pBmcMgr, 0, &fConverged,
839+
&nReprSeeds, NULL, &nTotalPairs, &nActivePairs );
840+
if ( fConverged )
841+
break;
842+
}
843+
if ( pTfoMask )
844+
pSrm = Gia_ManCorrSpecReduceInit_Active( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask );
845+
else
846+
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
847+
if ( pTfoMask && pPars->fVeryVerbose )
848+
Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n",
849+
i, nReprSeeds, nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) );
850+
if ( pBmcMgr )
851+
Cec_IncrMgrSnapshotClasses( pBmcMgr );
824852
if ( Gia_ManPoNum(pSrm) == 0 )
825853
{
826854
Gia_ManStop( pSrm );
827855
Vec_IntFree( vOutputs );
828856
break;
829-
}
857+
}
830858
pParsSat->nBTLimit *= 10;
831859
if ( pPars->fUseCSat )
832860
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
849877
if ( Cec_ParCorShouldStop( pPars ) )
850878
break;
851879
}
880+
Cec_IncrMgrFree( pBmcMgr );
852881
Cec_ManSimStop( pSim );
853882
}
854883

@@ -949,6 +978,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
949978
abctime clkTotal = Abc_Clock();
950979
abctime clkSat = 0, clkSim = 0, clkSrm = 0;
951980
abctime clk2, clk = Abc_Clock();
981+
Cec_IncrMgr_t * pMgr = NULL; // incremental manager (NULL when -i is off)
982+
abctime clkIncr = 0;
983+
int nIncrSkipped = 0, nIncrFallback = 0;
952984
if ( Gia_ManRegNum(pAig) == 0 )
953985
{
954986
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 )
9991031
Cec_ManSimStop( pSim );
10001032
return 1;
10011033
}
1034+
if ( pPars->fIncremental )
1035+
{
1036+
pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames );
1037+
Cec_IncrMgrSnapshotClasses( pMgr );
1038+
}
10021039
// perform refinement of equivalence classes
10031040
for ( r = 0; r < nIterMax; r++ )
1004-
{
1041+
{
10051042
if ( Cec_ParCorShouldStop( pPars ) )
10061043
{
10071044
Cec_ManSimStop( pSim );
1045+
Cec_IncrMgrFree( pMgr );
10081046
return 1;
10091047
}
10101048
if ( pPars->nStepsMax == r )
10111049
{
10121050
Cec_ManSimStop( pSim );
1051+
Cec_IncrMgrFree( pMgr );
10131052
Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
10141053
fflush( stdout );
10151054
return 1;
10161055
}
10171056
clk = Abc_Clock();
1018-
// perform speculative reduction
1057+
// perform speculative reduction (with optional active-list filter)
10191058
clk2 = Abc_Clock();
1020-
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
1059+
{
1060+
int * pTfoMask = NULL;
1061+
int nReprSeeds = 0, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0;
1062+
int fConverged = 0;
1063+
if ( pMgr && r > 0 )
1064+
{
1065+
abctime clkI = Abc_Clock();
1066+
pTfoMask = Cec_IncrMgrDecideMask( pMgr, pPars->fUseRings, &fConverged,
1067+
&nReprSeeds, &nNextChanges,
1068+
&nTotalPairs, &nActivePairs );
1069+
clkIncr += Abc_Clock() - clkI;
1070+
if ( fConverged )
1071+
{
1072+
clkSrm += Abc_Clock() - clk2;
1073+
break;
1074+
}
1075+
if ( pTfoMask == NULL )
1076+
nIncrFallback++;
1077+
else
1078+
nIncrSkipped += nTotalPairs - nActivePairs;
1079+
}
1080+
if ( pTfoMask )
1081+
pSrm = Gia_ManCorrSpecReduce_Active( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr );
1082+
else
1083+
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
1084+
if ( pTfoMask && pPars->fVeryVerbose )
1085+
Abc_Print( 1, " [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n",
1086+
r, nReprSeeds, nNextChanges, Vec_IntSize(pMgr->vTfoNodes),
1087+
nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) );
1088+
// Snapshot AFTER SRM build: the active builder still reads the
1089+
// previous pNexts to recognise newly-created ring edges.
1090+
if ( pMgr )
1091+
Cec_IncrMgrSnapshotClasses( pMgr );
1092+
}
10211093
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
10221094
clkSrm += Abc_Clock() - clk2;
10231095
if ( Gia_ManCoNum(pSrm) == 0 )
@@ -1058,6 +1130,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
10581130
if ( Cec_ParCorShouldStop( pPars ) )
10591131
{
10601132
Cec_ManSimStop( pSim );
1133+
Cec_IncrMgrFree( pMgr );
10611134
return 1;
10621135
}
10631136
// quit if const is no longer there
@@ -1067,6 +1140,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
10671140
printf( "because the property output is no longer a candidate constant.\n" );
10681141
fflush( stdout );
10691142
Cec_ManSimStop( pSim );
1143+
Cec_IncrMgrFree( pMgr );
10701144
return 0;
10711145
}
10721146
if ( pPars->nLimitMax )
@@ -1078,6 +1152,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
10781152
printf( "because refinement does not proceed quickly.\n" );
10791153
fflush( stdout );
10801154
Cec_ManSimStop( pSim );
1155+
Cec_IncrMgrFree( pMgr );
10811156
ABC_FREE( pAig->pReprs );
10821157
ABC_FREE( pAig->pNexts );
10831158
return 0;
@@ -1105,11 +1180,17 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
11051180
ABC_PRTP( "Sat ", clkSat, clkTotal );
11061181
ABC_PRTP( "Sim ", clkSim, clkTotal );
11071182
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
1183+
if ( pMgr )
1184+
{
1185+
ABC_PRTP( "Incr ", clkIncr, clkTotal );
1186+
Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped );
1187+
}
11081188
Abc_PrintTime( 1, "TOTAL", clkTotal );
11091189
fflush( stdout );
11101190
}
1191+
Cec_IncrMgrFree( pMgr );
11111192
return 1;
1112-
}
1193+
}
11131194

11141195
/**Function*************************************************************
11151196

0 commit comments

Comments
 (0)