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

added an option -r to %pdra: proof-based refinement only

This commit is contained in:
Yen-Sheng Ho 2017-02-28 18:05:58 -08:00
parent d95d51c474
commit 902a78eeb8
4 changed files with 21 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -171,11 +171,12 @@ struct Wlc_Par_t_
int nIterMax; // the max number of iterations
int nLimit; // the max number of signals
int fXorOutput; // XOR outputs of word-level miter
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 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 fProofRefine; // Use proof-based refinement
int fHybrid; // Use a hybrid of CBR and PBR
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};

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

@ -1107,9 +1107,16 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
}
// perform refinement
clk2 = Abc_Clock();
vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
tCbr += Abc_Clock() - clk2;
if ( pPars->fHybrid || !pPars->fProofRefine )
{
clk2 = Abc_Clock();
vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
tCbr += Abc_Clock() - clk2;
}
else // proof-based only
{
vRefine = Vec_IntDup( vPisNew );
}
if ( pPars->fProofRefine )
{
clk2 = Abc_Clock();

6
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, "AMXFILabcpmxvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
{
switch ( c )
{
@ -538,6 +538,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
pPars->fProofRefine ^= 1;
break;
case 'r':
pPars->fHybrid ^= 1;
break;
case 'x':
pPars->fXorOutput ^= 1;
break;
@ -581,6 +584,7 @@ usage:
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-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using both cex-based and proof-based refinement [default = %s]\n", pPars->fHybrid? "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

@ -120,6 +120,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fMFFC = 1; // Refine the entire MFFC of a PPI
pPars->fPdra = 0; // Use pdr -nct
pPars->fProofRefine = 0; // Use proof-based refinement
pPars->fHybrid = 1; // Use a hybrid of CBR and PBR
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}