summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/wlc/wlc.h1
-rw-r--r--src/base/wlc/wlcAbs.c48
-rw-r--r--src/base/wlc/wlcCom.c8
-rw-r--r--src/base/wlc/wlcNtk.c1
-rw-r--r--src/proof/pdr/pdrIncr.c3
5 files changed, 46 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
}
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index c59bfe1c..7bb3319d 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -261,6 +261,9 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
int RetValue = -1;
int nCubes = 0;
+ if ( vClauses == NULL )
+ return RetValue;
+
assert( Vec_VecSize(vClauses) >= 2 );
assert( Vec_VecSize(p->vClauses) == 0 );
Vec_VecExpand( p->vClauses, 1 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-25 16:49:49 +0000