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

%pdra: added an option -u for checking comb. unsat

This commit is contained in:
Yen-Sheng Ho 2017-03-01 14:57:43 -08:00
parent da0f4ef33b
commit 18b47dfbd5
5 changed files with 54 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -177,6 +177,7 @@ struct Wlc_Par_t_
int fPdra; // Use pdr -nct
int fProofRefine; // Use proof-based refinement
int fHybrid; // Use a hybrid of CBR and PBR
int fCheckCombUnsat; // Check if ABS becomes comb. unsat
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};

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

@ -33,6 +33,7 @@ ABC_NAMESPACE_IMPL_START
extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p );
typedef struct Int_Pair_t_ Int_Pair_t;
struct Int_Pair_t_
@ -1111,20 +1112,49 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Gia_ManPrintStats( pGia, NULL );
}
Wlc_NtkFree( pAbs );
// Gia_AigerWrite( pGia, "abs.aig", 0, 0 );
// try to prove abstracted GIA by converting it to AIG and calling PDR
pAig = Gia_ManToAigSimple( pGia );
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
clk2 = Abc_Clock();
if ( vClauses && pPars->fCheckCombUnsat )
{
clk2 = Abc_Clock();
Pdr_Man_t * pPdr2;
pPdrPars->fVerbose = 0;
pPdr2 = Pdr_ManStart( pAig, pPdrPars, NULL );
RetValue = IPdr_ManCheckCombUnsat( pPdr2 );
Pdr_ManStop( pPdr2 );
pPdrPars->fVerbose = pPars->fPdrVerbose;
tPdr += Abc_Clock() - clk2;
if ( RetValue == 1 )
{
if ( pPars->fVerbose )
Abc_PrintTime( 1, "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk2 );
Gia_ManStop( pGia );
Vec_IntFree( vPisNew );
Aig_ManStop( pAig );
break;
}
if ( pPars->fVerbose )
Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk2 );
}
clk2 = Abc_Clock();
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
if ( vClauses ) {
assert( Vec_VecSize( vClauses) >= 2 );
IPdr_ManRestore( pPdr, vClauses, vMap );
}
Vec_IntFreeP( &vMap );
RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
if ( !vClauses || RetValue != 1 )
RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
pPdr->tTotal += Abc_Clock() - clk2;
tPdr += pPdr->tTotal;

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, "AMXFILabrcpmxvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmuxvwh" ) ) != EOF )
{
switch ( c )
{
@ -553,6 +553,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fMFFC ^= 1;
break;
case 'u':
pPars->fCheckCombUnsat ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -573,7 +576,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\n" );
Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxuvwh]\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 );
@ -586,6 +589,7 @@ usage:
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-u : toggle checking combinationally unsat [default = %s]\n", pPars->fCheckCombUnsat? "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" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );

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

@ -121,6 +121,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fPdra = 0; // Use pdr -nct
pPars->fProofRefine = 0; // Use proof-based refinement
pPars->fHybrid = 1; // Use a hybrid of CBR and PBR
pPars->fCheckCombUnsat = 0; // Check if ABS becomes comb. unsat
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}

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

@ -738,6 +738,19 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
return RetValue;
}
int IPdr_ManCheckCombUnsat( Pdr_Man_t * p )
{
int iFrame, RetValue = -1;
Pdr_ManCreateSolver( p, (iFrame = 0) );
Pdr_ManCreateSolver( p, (iFrame = 1) );
p->nFrames = iFrame;
p->iUseFrame = Abc_MaxInt(iFrame, 1);
RetValue = Pdr_ManCheckCube( p, iFrame, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
return RetValue;
}
/**Function*************************************************************