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

Adding switch to stop scorr if refinement is too slow.

This commit is contained in:
Alan Mishchenko 2022-04-24 08:53:57 -07:00
parent b79f37ae57
commit 8e13245ed0
6 changed files with 121 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -21552,15 +21552,14 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
Ssw_Pars_t Pars, * pPars = &Pars;
int nConstrs = 0;
int c;
int c, nConstrs = 0;
extern Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplkodsefqvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNXcmplkodsefqvwh" ) ) != EOF )
{
switch ( c )
{
@ -21674,6 +21673,17 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConstrs < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLimitMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLimitMax < 0 )
goto usage;
break;
case 'c':
pPars->fConstrs ^= 1;
break;
@ -21795,7 +21805,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: scorr [-PQFCLSIVMN <num>] [-cmplkodsefqvwh]\n" );
Abc_Print( -2, "usage: scorr [-PQFCLSIVMNX <num>] [-cmplkodsefqvwh]\n" );
Abc_Print( -2, "\t performs sequential sweep using K-step induction\n" );
Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@ -21808,6 +21818,7 @@ usage:
Abc_Print( -2, "\t-V num : min var num needed to recycle the SAT solver [default = %d]\n", pPars->nSatVarMax2 );
Abc_Print( -2, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
Abc_Print( -2, "\t-N num : set last <num> POs to be constraints (use with -c) [default = %d]\n", nConstrs );
Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
Abc_Print( -2, "\t-c : toggle using explicit constraints [default = %s]\n", pPars->fConstrs? "yes": "no" );
Abc_Print( -2, "\t-m : toggle full merge if constraints are present [default = %s]\n", pPars->fMergeFull? "yes": "no" );
Abc_Print( -2, "\t-p : toggle aligning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
@ -22118,10 +22129,11 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFramesP;
int nConfMax;
int nVarsMax;
int nLimitMax;
int fNewAlgor;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int nLimitMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@ -22131,10 +22143,11 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
nFramesP = 0;
nConfMax = 1000;
nVarsMax = 1000;
nLimitMax = 0;
fNewAlgor = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PCSXnvh" ) ) != EOF )
{
switch ( c )
{
@ -22171,6 +22184,17 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nVarsMax < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
nLimitMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLimitMax < 0 )
goto usage;
break;
case 'n':
fNewAlgor ^= 1;
break;
@ -22204,7 +22228,7 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( fNewAlgor )
pNtkRes = Abc_NtkDarLcorrNew( pNtk, nVarsMax, nConfMax, fVerbose );
pNtkRes = Abc_NtkDarLcorrNew( pNtk, nVarsMax, nConfMax, nLimitMax, fVerbose );
else
pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
if ( pNtkRes == NULL )
@ -22217,11 +22241,12 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lcorr [-PCS num] [-nvh]\n" );
Abc_Print( -2, "usage: lcorr [-PCSX num] [-nvh]\n" );
Abc_Print( -2, "\t computes latch correspondence using 1-step induction\n" );
Abc_Print( -2, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfMax );
Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", nVarsMax );
Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", nLimitMax );
Abc_Print( -2, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgor? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -36411,7 +36436,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManCorSetDefaultParams( pPars );
pPars->fLatchCorr = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrcvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXrcvwh" ) ) != EOF )
{
switch ( c )
{
@ -36448,6 +36473,17 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nPrefix < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLimitMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLimitMax < 0 )
goto usage;
break;
case 'r':
pPars->fUseRings ^= 1;
break;
@ -36490,11 +36526,12 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &lcorr [-FCP num] [-rcvwh]\n" );
Abc_Print( -2, "usage: &lcorr [-FCPX num] [-rcvwh]\n" );
Abc_Print( -2, "\t performs latch 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 );
Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
@ -36523,7 +36560,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Cec_ManCorSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPpkrecqwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXpkrecqwvh" ) ) != EOF )
{
switch ( c )
{
@ -36560,6 +36597,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nPrefix < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLimitMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLimitMax < 0 )
goto usage;
break;
case 'p':
fPartition ^= 1;
break;
@ -36617,11 +36665,12 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &scorr [-FCP num] [-pkrecqwvh]\n" );
Abc_Print( -2, "usage: &scorr [-FCPX num] [-pkrecqwvh]\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 );
Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
Abc_Print( -2, "\t-p : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );

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

@ -2302,7 +2302,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int nLimitMax, int fVerbose )
{
Ssw_Pars_t Pars, * pPars = &Pars;
Aig_Man_t * pMan, * pTemp;
@ -2314,6 +2314,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
pPars->fLatchCorrOpt = 1;
pPars->nBTLimit = nConfMax;
pPars->nSatVarMax = nVarsMax;
pPars->nLimitMax = nLimitMax;
pPars->fVerbose = fVerbose;
pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
Aig_ManStop( pTemp );

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

@ -149,6 +149,7 @@ struct Cec_ParCor_t_
int nBTLimit; // conflict limit at a node
int nLevelMax; // (scorr only) the max number of levels
int nStepsMax; // (scorr only) the max number of induction steps
int nLimitMax; // (scorr only) stop after this many iterations if little or no improvement
int fLatchCorr; // consider only latch outputs
int fConstCorr; // consider only constants
int fUseRings; // use rings

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

@ -756,6 +756,21 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
Abc_Print( 1, "%c ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
Abc_PrintTime( 1, "T", Time );
}
int Cec_ManCountLits( Gia_Man_t * p )
{
int i, CounterX = 0, Counter0 = 0, Counter = 0;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjIsNone(p, i) )
CounterX++;
else if ( Gia_ObjIsConst(p, i) )
Counter0++;
else if ( Gia_ObjIsHead(p, i) )
Counter++;
}
CounterX -= Gia_ManCoNum(p);
return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
}
/**Function*************************************************************
@ -777,7 +792,7 @@ 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;
int fChanges, RetValue, i;
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
@ -791,7 +806,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
fChanges = 1;
while ( fChanges )
for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
{
abctime clkBmc = Abc_Clock();
fChanges = 0;
@ -918,7 +933,7 @@ 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;
int r, RetValue, nPrev[4] = {0};
abctime clkTotal = Abc_Clock();
abctime clkSat = 0, clkSim = 0, clkSrm = 0;
abctime clk2, clk = Abc_Clock();
@ -1031,6 +1046,21 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ManSimStop( pSim );
return 0;
}
if ( pPars->nLimitMax )
{
int nCur = Cec_ManCountLits(pAig);
if ( r > 4 && nPrev[0] - nCur <= 4*pPars->nLimitMax )
{
printf( "Iterative refinement is stopped after iteration %d\n", r );
printf( "because refinement does not proceed quickly.\n" );
Cec_ManSimStop( pSim );
return 0;
}
nPrev[0] = nPrev[1];
nPrev[1] = nPrev[2];
nPrev[2] = nPrev[3];
nPrev[3] = nCur;
}
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );

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

@ -55,6 +55,7 @@ struct Ssw_Pars_t_
int nResimDelta; // the number of nodes to resimulate
int nStepsMax; // (scorr only) the max number of induction steps
int TimeLimit; // time out in seconds
int nLimitMax; // the limit on the number of iterations
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
int fConstCorr; // perform constant correspondence

25
src/proof/ssw/sswCore.c
View File

@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
{
int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
Aig_Man_t * pAigNew;
int RetValue, nIter = -1;
int RetValue, nIter = -1, nPrev[4] = {0};
abctime clk, clkTotal = Abc_Clock();
// get the starting stats
p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
@ -352,7 +352,7 @@ clk = Abc_Clock();
{
printf( "Iterative refinement is stopped after iteration %d\n", nIter );
printf( "because the property output is no longer a candidate constant.\n" );
// prepare to quite
// prepare to quit
p->nLitsEnd = p->nLitsBeg;
p->nNodesEnd = p->nNodesBeg;
p->nRegsEnd = p->nRegsBeg;
@ -381,6 +381,27 @@ clk = Abc_Clock();
break;
if ( p->pPars->pFunc )
((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
if ( p->pPars->nLimitMax )
{
int nCur = Ssw_ClassesCand1Num(p->ppClasses);
if ( nIter > 4 && nPrev[0] - nCur <= 4*p->pPars->nLimitMax )
{
printf( "Iterative refinement is stopped after iteration %d\n", nIter );
printf( "because the refinment is very slow.\n" );
// prepare to quit
p->nLitsEnd = p->nLitsBeg;
p->nNodesEnd = p->nNodesBeg;
p->nRegsEnd = p->nRegsBeg;
// cleanup
Aig_ManSetPhase( p->pAig );
Aig_ManCleanMarkB( p->pAig );
return Aig_ManDupSimple( p->pAig );
}
nPrev[0] = nPrev[1];
nPrev[1] = nPrev[2];
nPrev[2] = nPrev[3];
nPrev[3] = nCur;
}
}
finalize: