diff options
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/wlcAbs.c | 48 |
1 files changed, 36 insertions, 12 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 390770ea..82de4284 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(); @@ -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 ) @@ -1715,7 +1724,9 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) printf( "\n" ); printf( "Abstraction " ); if ( RetValue == 0 ) + { printf( "resulted in a real CEX" ); + } else if ( RetValue == 1 ) printf( "is successfully proved" ); else @@ -1735,6 +1746,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; |