diff options
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/wlc.h | 1 | ||||
-rw-r--r-- | src/base/wlc/wlcAbs.c | 48 | ||||
-rw-r--r-- | src/base/wlc/wlcCom.c | 8 | ||||
-rw-r--r-- | src/base/wlc/wlcNtk.c | 1 |
4 files changed, 43 insertions, 15 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 028a4f1d..eb8f4aa4 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -182,6 +182,7 @@ struct Wlc_Par_t_ int fProofUsePPI; // Use PPI values in PBR int fUseBmc3; // Run BMC3 in parallel int fShrinkAbs; // Shrink Abs with BMC + int fShrinkScratch; // Restart pdr from scratch after shrinking int fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index b3ac623e..e355c313 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -558,19 +558,24 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_ return pNew; } -static int Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex ) +static Abc_Cex_t * Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex ) { Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0, 0 ); int f, i; Gia_Obj_t * pObj, * pObjRi; + Abc_Cex_t * pCexReal = Abc_CexAlloc( Gia_ManRegNum(pGiaOrig), Gia_ManPiNum(pGiaOrig), pCex->iFrame + 1 ); Gia_ManConst0(pGiaOrig)->Value = 0; Gia_ManForEachRi( pGiaOrig, pObj, i ) pObj->Value = 0; for ( f = 0; f <= pCex->iFrame; f++ ) { - for( i = 0; i < Gia_ManPiNum( pGiaOrig ); i++ ) + for( i = 0; i < Gia_ManPiNum( pGiaOrig ); i++ ) + { Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i); + if ( Gia_ManPi(pGiaOrig, i)->Value ) + Abc_InfoSetBit(pCexReal->pData, pCexReal->nRegs + pCexReal->nPis*f + i); + } Gia_ManForEachRiRo( pGiaOrig, pObjRi, pObj, i ) pObj->Value = pObjRi->Value; Gia_ManForEachAnd( pGiaOrig, pObj, i ) @@ -582,14 +587,15 @@ static int Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex ) if (pObj->Value==1) { Abc_Print( 1, "CEX is real on the original model.\n" ); Gia_ManStop(pGiaOrig); - return 1; + return pCexReal; } } } // Abc_Print( 1, "CEX is spurious.\n" ); Gia_ManStop(pGiaOrig); - return 0; + Abc_CexFree(pCexReal); + return NULL; } static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops ) @@ -1472,12 +1478,13 @@ int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) return RetValue; } -int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) +int Wla_ManSolveInt( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; Pdr_Man_t * pPdr; Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars; Abc_Cex_t * pBmcCex = NULL; + Abc_Cex_t * pCexReal = NULL; int RetValue = -1; int RunId = Wla_GetGlobalRunId(); @@ -1511,7 +1518,7 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) assert( Vec_VecSize( pWla->vClauses) >= 2 ); if ( pWla->fNewAbs ) - IPdr_ManRebuildClauses( pPdr, pWla->vClauses ); + IPdr_ManRebuildClauses( pPdr, pWla->pPars->fShrinkScratch ? NULL : pWla->vClauses ); else IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL ); @@ -1546,8 +1553,13 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) } // verify CEX - if ( Wlc_NtkCexIsReal( pWla->p, pWla->pCex ) ) + pCexReal = Wlc_NtkCexIsReal( pWla->p, pWla->pCex ); + if ( pCexReal ) + { + Abc_CexFree( pWla->pCex ); + pWla->pCex = pCexReal; return 0; + } return -1; } @@ -1678,17 +1690,14 @@ void Wla_ManStop( Wla_Man_t * p ) ABC_FREE( p ); } -int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +int Wla_ManSolve( Wla_Man_t * pWla, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); abctime tTotal; - Wla_Man_t * pWla = NULL; Wlc_Ntk_t * pAbs = NULL; Aig_Man_t * pAig = NULL; - - int RetValue = -1; - pWla = Wla_ManStart( p, pPars ); + int RetValue = -1; // perform refinement iterations for ( pWla->nIters = 1; pWla->nIters < pPars->nIterMax; ++pWla->nIters ) @@ -1701,7 +1710,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAig = Wla_ManBitBlast( pWla, pAbs ); Wlc_NtkFree( pAbs ); - RetValue = Wla_ManSolve( pWla, pAig ); + RetValue = Wla_ManSolveInt( pWla, pAig ); Aig_ManStop( pAig ); if ( RetValue != -1 ) @@ -1735,6 +1744,19 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ABC_PRTP( "Total ", tTotal, tTotal ); } + return RetValue; +} + +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + Wla_Man_t * pWla = NULL; + + int RetValue = -1; + + pWla = Wla_ManStart( p, pPars ); + + RetValue = Wla_ManSolve( pWla, pPars ); + Wla_ManStop( pWla ); return RetValue; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index dbbf060e..4e6fbd18 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -464,7 +464,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, "AMXFILabrcdipqmsuxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmstuxvwh" ) ) != EOF ) { switch ( c ) { @@ -567,6 +567,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': pPars->fShrinkAbs ^= 1; break; + case 't': + pPars->fShrinkScratch ^= 1; + break; case 'u': pPars->fCheckCombUnsat ^= 1; break; @@ -590,7 +593,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] [-abrcdipqmxsuvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxstuvwh]\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 ); @@ -606,6 +609,7 @@ usage: Abc_Print( -2, "\t-d : toggle using another way of creating abstractions [default = %s]\n", pPars->fAbs2? "yes": "no" ); Abc_Print( -2, "\t-i : toggle using PPI values in proof-based refinement [default = %s]\n", pPars->fProofUsePPI? "yes": "no" ); Abc_Print( -2, "\t-s : toggle shrinking abstractions with BMC [default = %s]\n", pPars->fShrinkAbs? "yes": "no" ); + Abc_Print( -2, "\t-t : toggle restarting pdr from scratch after shrinking abstractions with BMC [default = %s]\n", pPars->fShrinkScratch? "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-q : toggle running bmc3 in parallel for CEX [default = %s]\n", pPars->fUseBmc3? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 43b98d9a..6efa0f6b 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -126,6 +126,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->fProofUsePPI = 0; // Use PPI values in PBR pPars->fUseBmc3 = 0; // Run BMC3 in parallel pPars->fShrinkAbs = 0; // Shrink Abs with BMC + pPars->fShrinkScratch= 0; // Restart pdr from scratch after shrinking pPars->fVerbose = 0; // verbose output` pPars->fPdrVerbose = 0; // show verbose PDR output } |