diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-20 12:51:04 -0800 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-20 12:51:04 -0800 |
commit | 9f43c84501cf8c5a8ae74cc5bebea63dafc3a714 (patch) | |
tree | 413cd6e1f956e848770bf95cc422d43ab180519b /src | |
parent | 19510bd38e46fd913bf6dc29393938e50fd717ee (diff) | |
download | abc-9f43c84501cf8c5a8ae74cc5bebea63dafc3a714.tar.gz abc-9f43c84501cf8c5a8ae74cc5bebea63dafc3a714.tar.bz2 abc-9f43c84501cf8c5a8ae74cc5bebea63dafc3a714.zip |
added options of checking and pushing to %pdra
Diffstat (limited to 'src')
-rw-r--r-- | src/base/wlc/wlc.h | 2 | ||||
-rw-r--r-- | src/base/wlc/wlcAbs.c | 10 | ||||
-rw-r--r-- | src/base/wlc/wlcCom.c | 12 | ||||
-rw-r--r-- | src/proof/pdr/pdrIncr.c | 37 |
4 files changed, 51 insertions, 10 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index cf8bdab4..9cb34bf3 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -184,6 +184,8 @@ struct WlcPdr_Par_t_ int nBitsFlop; // flop bit-width int nIterMax; // the max number of iterations 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 fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 8fde7f56..fbaa1b8a 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -32,7 +32,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 ); -extern int IPdr_ManSolveInt( Pdr_Man_t * p ); +extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -59,6 +59,8 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) pPars->nBitsFlop = ABC_INFINITY; // flop bit-width pPars->nIterMax = 1000; // the max number of iterations pPars->fXorOutput = 1; // XOR outputs of word-level miter + pPars->fCheckClauses = 1; // Check clauses in the reloaded trace + pPars->fPushClauses = 0; // Push clauses in the reloaded trace pPars->fVerbose = 0; // verbose output pPars->fPdrVerbose = 0; // show verbose PDR output } @@ -76,7 +78,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) +static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); Wlc_Obj_t * pObj; int i, Count[4] = {0}; @@ -197,7 +199,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * SeeAlso [] ***********************************************************************/ -static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) +static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) { Wlc_Ntk_t * pNtkNew = NULL; Vec_Int_t * vPisOld = Vec_IntAlloc( 100 ); @@ -401,7 +403,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ) IPdr_ManRestore( pPdr, vClauses ); } - RetValue = IPdr_ManSolveInt( pPdr ); + RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses ); pPdr->tTotal += Abc_Clock() - pdrClk; pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index d30b376e..7801abc6 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; WlcPdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) { switch ( c ) { @@ -524,6 +524,12 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'x': pPars->fXorOutput ^= 1; break; + case 'c': + pPars->fCheckClauses ^= 1; + break; + case 'p': + pPars->fPushClauses ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -544,7 +550,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] [-xvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\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 ); @@ -552,6 +558,8 @@ 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-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-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 09a06a27..85403a7d 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -68,7 +68,9 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) /**Function************************************************************* - Synopsis [] + Synopsis [ Check if each cube c_k in frame k satisfies the query + R_{k-1} && T && !c_k && c_k' (must be UNSAT). + Return True if all cubes pass the check. ] Description [] @@ -214,7 +216,7 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) SeeAlso [] ***********************************************************************/ -int IPdr_ManSolveInt( Pdr_Man_t * p ) +int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) { int fPrintClauses = 0; Pdr_Set_t * pCube = NULL; @@ -242,7 +244,34 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManCreateSolver( p, (iFrame = 0) ); else { iFrame = Vec_VecSize(p->vClauses) - 1; - IPdr_ManCheckClauses( p ); + + if ( fCheckClauses ) + { + if ( p->pPars->fVerbose ) + Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ; + IPdr_ManCheckClauses( p ); + if ( p->pPars->fVerbose ) + Abc_Print( 1, " Passed!\n" ) ; + } + + if ( fPushClauses ) + { + p->iUseFrame = Abc_MaxInt(iFrame, 1); + + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" ); + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + } + + RetValue = Pdr_ManPushClauses( p ); + + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "IPDR: Finished pushing. After:\n" ); + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + } + } } while ( 1 ) { @@ -602,7 +631,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) p = Pdr_ManStart( pAig, pPars, NULL ); while ( 1 ) { - RetValue = IPdr_ManSolveInt( p ); + RetValue = IPdr_ManSolveInt( p, 1, 0 ); if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) { vClausesSaved = IPdr_ManSaveClauses( p, 1 ); |