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

Experiment with "scorr".

This commit is contained in:
Alan Mishchenko 2024-11-17 15:44:32 -08:00
parent 3aff0af0c5
commit 1f3cf0aad9
3 changed files with 22 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -23148,7 +23148,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNXcmplkodsefqvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNXRcmplkodsefqvwh" ) ) != EOF )
{
switch ( c )
{
@ -23273,6 +23273,18 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nLimitMax < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nSkip = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nSkip < 0 )
goto usage;
break;
case 'c':
pPars->fConstrs ^= 1;
break;
@ -23394,7 +23406,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: scorr [-PQFCLSIVMNX <num>] [-cmplkodsefqvwh]\n" );
Abc_Print( -2, "usage: scorr [-PQFCLSIVMNXR <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 );
@ -23408,6 +23420,7 @@ usage:
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-R num : the number used to skip some constraints [default = %d]\n", pPars->nSkip );
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" );

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

@ -74,6 +74,7 @@ struct Ssw_Pars_t_
int fEquivDump; // enables dumping equivalences
int fEquivDump2; // enables dumping equivalences
int fStopWhenGone; // stop when PO output is not a candidate constant
int nSkip;
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)

8
src/proof/ssw/sswAig.c
View File

@ -120,8 +120,10 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
// add the constraint
if ( fTwoPos )
{
Aig_ObjCreateCo( pFrames, pObjNew2 );
Aig_ObjCreateCo( pFrames, pObjNew );
if ( p->pPars->nSkip == 0 ||rand() % p->pPars->nSkip == 0 ) {
Aig_ObjCreateCo( pFrames, pObjNew2 );
Aig_ObjCreateCo( pFrames, pObjNew );
}
}
else
{
@ -158,6 +160,8 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
// add timeframes
iLits = 0;
if ( p->pPars->nSkip )
srand(1);
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs