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

added %pdra -a: run with pdr -nct

This commit is contained in:
Yen-Sheng Ho 2017-02-23 08:48:53 -08:00
parent f01c63f712
commit d5bbf9188c
5 changed files with 42 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/base/wlc/wlc.h
View File

@ -173,6 +173,7 @@ struct Wlc_Par_t_
int fCheckClauses; // Check clauses in the reloaded trace
int fPushClauses; // Push clauses in the reloaded trace
int fMFFC; // Refine the entire MFFC of a PPI
int fPdra; // Use pdr -nct
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};

8
src/base/wlc/wlcAbs.c
View File

@ -390,6 +390,14 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
pPdrPars->fVerbose = pPars->fPdrVerbose;
pPdrPars->fVeryVerbose = 0;
if ( pPars->fPdra )
{
pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
}
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{

8
src/base/wlc/wlcCom.c
View File

@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpmxvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIacpmxvwh" ) ) != EOF )
{
switch ( c )
{
@ -521,6 +521,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nIterMax < 0 )
goto usage;
break;
case 'a':
pPars->fPdra ^= 1;
break;
case 'x':
pPars->fXorOutput ^= 1;
break;
@ -553,7 +556,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpmxvwh]\n" );
Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-acpmxvwh]\n" );
Abc_Print( -2, "\t abstraction for word-level networks\n" );
Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
@ -561,6 +564,7 @@ usage:
Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" );
Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" );

1
src/base/wlc/wlcNtk.c
View File

@ -117,6 +117,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
pPars->fPushClauses = 0; // Push clauses in the reloaded trace
pPars->fMFFC = 1; // Refine the entire MFFC of a PPI
pPars->fPdra = 0; // Use pdr -nct
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}

26
src/proof/pdr/pdrIncr.c
View File

@ -190,6 +190,21 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal )
SeeAlso []
***********************************************************************/
int IPdr_ManRestoreAbsFlops( Pdr_Man_t * p )
{
Pdr_Set_t * pSet; int i, j, k;
Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
{
for ( k = 0; k < pSet->nLits; k++ )
{
Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
}
}
return 0;
}
int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap )
{
int i;
@ -288,6 +303,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
return 1;
}
}
if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame >= 1 )
{
assert( p->vAbsFlops == NULL );
p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
p->vMapPpi2Ff = Vec_IntAlloc( 100 );
IPdr_ManRestoreAbsFlops( p );
}
}
while ( 1 )
{