summaryrefslogtreecommitdiffstats
path: root/src/base/wlc
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/wlc')
-rw-r--r--src/base/wlc/wlc.h5
-rw-r--r--src/base/wlc/wlcAbs.c289
-rw-r--r--src/base/wlc/wlcCom.c8
-rw-r--r--src/base/wlc/wlcNtk.c1
-rw-r--r--src/base/wlc/wlcPth.c25
5 files changed, 291 insertions, 37 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 5d4f374e..028a4f1d 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -181,6 +181,7 @@ struct Wlc_Par_t_
int fAbs2; // Use UFAR style createAbs
int fProofUsePPI; // Use PPI values in PBR
int fUseBmc3; // Run BMC3 in parallel
+ int fShrinkAbs; // Shrink Abs with BMC
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
@@ -192,12 +193,16 @@ struct Wla_Man_t_
Wlc_Par_t * pPars;
Vec_Vec_t * vClauses;
Vec_Int_t * vBlacks;
+ Vec_Int_t * vSignals;
Abc_Cex_t * pCex;
Gia_Man_t * pGia;
Vec_Bit_t * vUnmark;
void * pPdrPars;
void * pThread;
+ int iCexFrame;
+ int fNewAbs;
+
int nIters;
int nTotalCla;
int nDisj;
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index f069c95f..b3ac623e 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -32,7 +32,8 @@ 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_ManRestoreClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
+extern int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses );
extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p );
extern int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses );
@@ -212,7 +213,7 @@ void Wlc_NtkAbsAnalyzeRefine( Wlc_Ntk_t * p, Vec_Int_t * vBlacks, Vec_Bit_t * vU
Vec_IntFree( vSuppRefs );
}
-static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars )
+static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int first_sel_pi, int num_sel_pis, Vec_Bit_t * vMark, int nConfLimit, Wlc_Par_t * pPars, int fSetPO, int RunId )
{
Vec_Int_t * vCores = NULL;
Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames );
@@ -221,6 +222,11 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num
int i;
sat_solver_setnvars(pSat, pCnf->nVars);
+ if ( RunId >= 0 )
+ {
+ pSat->RunId = RunId;
+ pSat->pFuncStop = Wla_CallBackToStop;
+ }
for (i = 0; i < pCnf->nClauses; i++)
{
@@ -237,18 +243,35 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num
assert(pCnf->pVarNums[pObj->Id] >= 0);
Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0));
}
- ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits));
- if (!ret)
- Abc_Print( 1, "UNSAT after adding PO clauses.\n" );
+ if ( !fSetPO )
+ {
+ ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits));
+ if (!ret)
+ Abc_Print( 1, "UNSAT after adding PO clauses.\n" );
+ }
+ else
+ {
+ int Lit;
+ for ( i = 0; i < Vec_IntSize(vLits); ++i )
+ {
+ if ( i == Vec_IntSize(vLits) - 1 )
+ Lit = Vec_IntEntry( vLits, i );
+ else
+ Lit = lit_neg(Vec_IntEntry( vLits, i ));
+ ret = sat_solver_addclause(pSat, &Lit, &Lit + 1);
+ if (!ret)
+ Abc_Print( 1, "UNSAT after adding PO clauses.\n" );
+ }
+ }
Vec_IntFree(vLits);
}
+
// main procedure
{
int status;
Vec_Int_t* vLits = Vec_IntAlloc(100);
Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars );
- int first_sel_pi = sel_pi_first ? 0 : num_other_pis;
for ( i = 0; i < num_sel_pis; ++i )
{
int cur_pi = first_sel_pi + i;
@@ -295,6 +318,52 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num
return vCores;
}
+static Gia_Man_t * Wlc_NtkUnrollWoCex(Wlc_Ntk_t * pChoice, int nFrames, int first_sel_pi, int num_sel_pis)
+{
+ Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0 );
+ Gia_Man_t * pFrames = NULL, * pGia;
+ Gia_Obj_t * pObj, * pObjRi;
+ int f, i;
+
+ pFrames = Gia_ManStart( 10000 );
+ pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName );
+ Gia_ManHashAlloc( pFrames );
+ Gia_ManConst0(pGiaChoice)->Value = 0;
+ Gia_ManForEachRi( pGiaChoice, pObj, i )
+ pObj->Value = 0;
+
+ for ( f = 0; f < nFrames; f++ )
+ {
+ for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ )
+ {
+ if ( i >= first_sel_pi && i < first_sel_pi + num_sel_pis )
+ {
+ if( f == 0 )
+ Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+ }
+ else
+ {
+ Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+ }
+ }
+ Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i )
+ pObj->Value = pObjRi->Value;
+ Gia_ManForEachAnd( pGiaChoice, pObj, i )
+ pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj));
+ Gia_ManForEachCo( pGiaChoice, pObj, i )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ManForEachPo( pGiaChoice, pObj, i )
+ Gia_ManAppendCo(pFrames, pObj->Value);
+ }
+ Gia_ManHashStop (pFrames);
+ Gia_ManSetRegNum(pFrames, 0);
+ pFrames = Gia_ManCleanup(pGia = pFrames);
+ Gia_ManStop(pGia);
+ Gia_ManStop(pGiaChoice);
+
+ return pFrames;
+}
+
static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first, int fUsePPI)
{
Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0 );
@@ -363,7 +432,7 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i
return pFrames;
}
-Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
+Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t * vPPIs )
{
//if ( vBlacks== NULL ) return NULL;
Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
@@ -375,6 +444,7 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
+ Vec_Bit_t * vPPIMark = NULL;
Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
{
@@ -382,6 +452,16 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
}
+ if ( vPPIs )
+ {
+ vPPIMark = Vec_BitStart( Wlc_NtkObjNumMax(pNtk) );
+ Wlc_NtkForEachObjVec( vPPIs, pNtk, pObj, i )
+ {
+ Vec_IntWriteEntry(vPPIs, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
+ Vec_BitWriteEntry( vPPIMark, Vec_IntEntry(vPPIs, i), 1 );
+ }
+ }
+
// Vec_IntPrint(vNodes);
Wlc_NtkCleanCopy( p );
@@ -394,6 +474,17 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
}
+ if ( vPPIs )
+ {
+ Wlc_NtkForEachObjVec( vPPIs, p, pObj, i )
+ {
+ iObj = Wlc_ObjId(p, pObj);
+ pObj->Mark = 1;
+ // add fresh PI with the same number of bits
+ Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
+ }
+ }
+
// add sel PI
Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
{
@@ -410,27 +501,32 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
// cout << "break at " << i << endl;
break;
}
+
+ // update fanins
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+ // node to remain
+ iObj = i;
+
if ( pObj->Mark )
{
// clean
pObj->Mark = 0;
- isSigned = Wlc_ObjIsSigned(pObj);
- range = Wlc_ObjRange(pObj);
- Vec_IntClear(vFanins);
- Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
- Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
- Vec_IntPush(vFanins, i);
- iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
- }
- else
- {
- // update fanins
- Wlc_ObjForEachFanin( pObj, iFanin, k )
- Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
- // node to remain
- iObj = i;
+ if ( vPPIMark && Vec_BitEntry(vPPIMark, i) )
+ iObj = Vec_IntEntry( vMapNode2Pi, i );
+ else
+ {
+ isSigned = Wlc_ObjIsSigned(pObj);
+ range = Wlc_ObjRange(pObj);
+ Vec_IntClear(vFanins);
+ Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
+ Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
+ Vec_IntPush(vFanins, i);
+ iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
+ }
}
+
Wlc_ObjSetCopy( p, i, iObj );
}
@@ -451,6 +547,8 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
// DumpWlcNtk(p);
pNew = Wlc_NtkDupDfsSimple( p );
+ if ( vPPIMark )
+ Vec_BitFree( vPPIMark );
Vec_IntFree( vFanins );
Vec_IntFree( vMapNode2Pi );
Vec_IntFree( vMapNode2Sel );
@@ -573,6 +671,42 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t
return pNew;
}
+static Vec_Bit_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFrames, Vec_Int_t * vWhites, Vec_Int_t * vBlacks, int RunId )
+{
+ Gia_Man_t * pGiaFrames;
+ Wlc_Ntk_t * pNtkWithChoices = NULL;
+ Vec_Int_t * vCoreSels;
+ Vec_Bit_t * vChoiceMark;
+ int first_sel_pi;
+ int i, Entry;
+ abctime clk = Abc_Clock();
+
+ assert( vWhites && Vec_IntSize(vWhites) );
+ pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vWhites, vBlacks );
+
+ first_sel_pi = Wlc_NtkNumPiBits( pNtkWithChoices ) - Vec_IntSize( vWhites );
+ pGiaFrames = Wlc_NtkUnrollWoCex( pNtkWithChoices, nFrames, first_sel_pi, Vec_IntSize( vWhites ) );
+
+ vChoiceMark = Vec_BitStartFull( Vec_IntSize( vWhites ) );
+ vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, nFrames, first_sel_pi, Vec_IntSize( vWhites ), vChoiceMark, 0, pPars, 0, RunId );
+
+ Wlc_NtkFree( pNtkWithChoices );
+ Gia_ManStop( pGiaFrames );
+
+ if ( vCoreSels == NULL )
+ return NULL;
+
+ Vec_BitReset( vChoiceMark );
+ Vec_IntForEachEntry( vCoreSels, Entry, i )
+ Vec_BitWriteEntry( vChoiceMark, Entry, 1 );
+
+ Abc_Print( 1, "ProofReduce: remove %d out of %d white boxes.", Vec_IntSize(vWhites) - Vec_BitCount(vChoiceMark), Vec_IntSize(vWhites) );
+ Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
+
+ Vec_IntFree( vCoreSels );
+ return vChoiceMark;
+}
+
static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine )
{
Gia_Man_t * pGiaFrames;
@@ -599,13 +733,13 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe
Vec_BitWriteEntry( vChoiceMark, i, 1 );
}
- pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL;
+ pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks, NULL ) : NULL;
pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0, pPars->fProofUsePPI );
if ( !pPars->fProofUsePPI )
- vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars );
+ vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, num_ppis, Vec_IntSize( vBlacks ), vChoiceMark, 0, pPars, 0, -1 );
else
- vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), 0, vChoiceMark, 0, 0, pPars );
+ vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, 0, Vec_IntSize( vBlacks ), vChoiceMark, 0, pPars, 0, -1 );
Wlc_NtkFree( pNtkWithChoices );
Gia_ManStop( pGiaFrames );
@@ -629,15 +763,18 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe
return 0;
}
-static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark )
+static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark, Vec_Int_t * vSignals )
{
int Entry, i;
Wlc_Obj_t * pObj; int Count[4] = {0};
Vec_Int_t * vBlacks = Vec_IntAlloc( 100 );
+ Vec_Int_t * vVec;
assert( *pvBlacks );
- Vec_IntForEachEntry( *pvBlacks, Entry, i )
+ vVec = vSignals ? vSignals : *pvBlacks;
+
+ Vec_IntForEachEntry( vVec, Entry, i )
{
if ( Vec_BitEntry( vUnmark, Entry) )
continue;
@@ -1182,6 +1319,54 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
+Vec_Int_t * Wla_ManCollectNodes( Wla_Man_t * pWla, int fBlack )
+{
+ Vec_Int_t * vNodes = NULL;
+ int i, Entry;
+
+ assert( pWla->vSignals );
+
+ vNodes = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntry( pWla->vSignals, Entry, i )
+ {
+ if ( !fBlack && Vec_BitEntry(pWla->vUnmark, Entry) )
+ Vec_IntPush( vNodes, Entry );
+
+ if ( fBlack && !Vec_BitEntry(pWla->vUnmark, Entry) )
+ Vec_IntPush( vNodes, Entry );
+ }
+
+ return vNodes;
+}
+
+int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames, int RunId )
+{
+ int i, Entry;
+ int RetValue = 0;
+
+ Vec_Int_t * vWhites = Wla_ManCollectNodes( pWla, 0 );
+ Vec_Int_t * vBlacks = Wla_ManCollectNodes( pWla, 1 );
+ Vec_Bit_t * vCoreMarks = Wlc_NtkProofReduce( pWla->p, pWla->pPars, nFrames, vWhites, vBlacks, RunId );
+
+ if ( vCoreMarks == NULL )
+ {
+ Vec_IntFree( vWhites );
+ Vec_IntFree( vBlacks );
+ return -1;
+ }
+
+ RetValue = Vec_IntSize( vWhites ) != Vec_BitCount( vCoreMarks );
+
+ Vec_IntForEachEntry( vWhites, Entry, i )
+ if ( !Vec_BitEntry( vCoreMarks, i ) )
+ Vec_BitWriteEntry( pWla->vUnmark, Entry, 0 );
+
+ Vec_IntFree( vWhites );
+ Vec_IntFree( vBlacks );
+ Vec_BitFree( vCoreMarks );
+
+ return RetValue;
+}
Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
{
@@ -1189,9 +1374,14 @@ Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
// get abstracted GIA and the set of pseudo-PIs (vBlacks)
if ( pWla->vBlacks == NULL )
+ {
pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars );
+ pWla->vSignals = Vec_IntDup( pWla->vBlacks );
+ }
else
- Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark );
+ {
+ Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark, pWla->vSignals );
+ }
pAbs = Wlc_NtkAbs2( pWla->p, pWla->vBlacks, NULL );
return pAbs;
@@ -1319,7 +1509,13 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
if ( pWla->vClauses ) {
assert( Vec_VecSize( pWla->vClauses) >= 2 );
- IPdr_ManRestore( pPdr, pWla->vClauses, NULL );
+
+ if ( pWla->fNewAbs )
+ IPdr_ManRebuildClauses( pPdr, pWla->vClauses );
+ else
+ IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
+
+ pWla->fNewAbs = 0;
}
RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses );
@@ -1361,6 +1557,16 @@ void Wla_ManRefine( Wla_Man_t * pWla )
abctime clk;
int nNodes;
Vec_Int_t * vRefine = NULL;
+
+ if ( pWla->fNewAbs )
+ {
+ if ( pWla->pCex )
+ Abc_CexFree( pWla->pCex );
+ pWla->pCex = NULL;
+ Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
+ return;
+ }
+
// perform refinement
if ( pWla->pPars->fHybrid || !pWla->pPars->fProofRefine )
{
@@ -1410,6 +1616,19 @@ void Wla_ManRefine( Wla_Man_t * pWla )
}
*/
pWla->tCbr += Abc_Clock() - clk;
+
+ // Experimental
+ /*
+ if ( pWla->pCex->iFrame > 0 )
+ {
+ Vec_Int_t * vWhites = Wla_ManCollectWhites( pWla );
+ Vec_Bit_t * vCore = Wlc_NtkProofReduce( pWla->p, pWla->pPars, pWla->pCex->iFrame, vWhites );
+ Vec_IntFree( vWhites );
+ Vec_BitFree( vCore );
+ }
+ */
+
+ pWla->iCexFrame = pWla->pCex->iFrame;
Vec_IntFree( vRefine );
Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
@@ -1437,10 +1656,13 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars )
}
p->pPdrPars = (void *)pPdrPars;
- p->nIters = 1;
+ p->iCexFrame = 0;
+ p->fNewAbs = 0;
+
+ p->nIters = 1;
p->nTotalCla = 0;
- p->nDisj = 0;
- p->nNDisj = 0;
+ p->nDisj = 0;
+ p->nNDisj = 0;
return p;
}
@@ -1448,6 +1670,7 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars )
void Wla_ManStop( Wla_Man_t * p )
{
if ( p->vBlacks ) Vec_IntFree( p->vBlacks );
+ if ( p->vSignals ) Vec_IntFree( p->vSignals );
if ( p->pGia ) Gia_ManStop( p->pGia );
if ( p->pCex ) Abc_CexFree( p->pCex );
Vec_BitFree( p->vUnmark );
@@ -1568,7 +1791,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
if ( vBlacks == NULL )
vBlacks = Wlc_NtkGetBlacks( p, pPars );
else
- Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
+ Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark, NULL );
pAbs = Wlc_NtkAbs2( p, vBlacks, NULL );
vPisNew = Vec_IntDup( vBlacks );
}
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 871b3e5d..dbbf060e 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, "AMXFILabrcdipqmuxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmsuxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -564,6 +564,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fMFFC ^= 1;
break;
+ case 's':
+ pPars->fShrinkAbs ^= 1;
+ break;
case 'u':
pPars->fCheckCombUnsat ^= 1;
break;
@@ -587,7 +590,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] [-abrcdipqmxuvwh]\n" );
+ Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxsuvwh]\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 );
@@ -602,6 +605,7 @@ usage:
Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
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-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 d1eaf7c5..43b98d9a 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -125,6 +125,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fAbs2 = 0; // Use UFAR style createAbs
pPars->fProofUsePPI = 0; // Use PPI values in PBR
pPars->fUseBmc3 = 0; // Run BMC3 in parallel
+ pPars->fShrinkAbs = 0; // Shrink Abs with BMC
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}
diff --git a/src/base/wlc/wlcPth.c b/src/base/wlc/wlcPth.c
index 783dbe6f..7b8e1942 100644
--- a/src/base/wlc/wlcPth.c
+++ b/src/base/wlc/wlcPth.c
@@ -40,6 +40,7 @@ ABC_NAMESPACE_IMPL_START
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig );
extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp );
+extern int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames );
static volatile int g_nRunIds = 0; // the number of the last prover instance
int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
@@ -55,6 +56,7 @@ void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppC
// information given to the thread
typedef struct Bmc3_ThData_t_
{
+ Wla_Man_t * pWla;
Aig_Man_t * pAig;
Abc_Cex_t ** ppCex;
int RunId;
@@ -84,6 +86,7 @@ void * Wla_Bmc3Thread ( void * pArg )
{
int status;
int RetValue = -1;
+ int nFramesNoChangeLim = 10;
Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
@@ -91,6 +94,9 @@ void * Wla_Bmc3Thread ( void * pArg )
pBmcPars->pFuncStop = Wla_CallBackToStop;
pBmcPars->RunId = pData->RunId;
+ if ( pData->pWla->pPars->fShrinkAbs )
+ pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim;
+
RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
if ( RetValue == 0 )
@@ -106,10 +112,24 @@ void * Wla_Bmc3Thread ( void * pArg )
++g_nRunIds;
status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
}
- else
+ else if ( RetValue == -1 )
{
- if ( pData->fVerbose )
+ if ( pData->RunId < g_nRunIds && pData->fVerbose )
Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
+
+ if ( pData->pWla->nIters > 1 && pData->RunId == g_nRunIds )
+ {
+ RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim );
+ pData->pWla->iCexFrame += nFramesNoChangeLim;
+
+ if ( RetValue == 1 )
+ {
+ pData->pWla->fNewAbs = 1;
+ status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
+ ++g_nRunIds;
+ status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
+ }
+ }
}
// free memory
@@ -132,6 +152,7 @@ void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppC
pWla->pThread = (void *)ABC_CALLOC( pthread_t, 1 );
pData = ABC_CALLOC( Bmc3_ThData_t, 1 );
+ pData->pWla = pWla;
pData->pAig = pAig;
pData->ppCex = ppCex;
pData->RunId = g_nRunIds;
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-31 00:06:59 +0000