summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/wlc/wlc.h1
-rw-r--r--src/base/wlc/wlcAbs.c117
-rw-r--r--src/base/wlc/wlcCom.c8
-rw-r--r--src/base/wlc/wlcNtk.c1
-rw-r--r--src/proof/pdr/pdrIncr.c120
5 files changed, 240 insertions, 7 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index f5dbba42..699d2d9b 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -177,6 +177,7 @@ struct Wlc_Par_t_
int fPdra; // Use pdr -nct
int fProofRefine; // Use proof-based refinement
int fHybrid; // Use a hybrid of CBR and PBR
+ int fCheckCombUnsat; // Check if ABS becomes comb. unsat
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index ad6c6642..79da6235 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -21,6 +21,7 @@
#include "wlc.h"
#include "proof/pdr/pdr.h"
#include "proof/pdr/pdrInt.h"
+#include "proof/ssw/ssw.h"
#include "aig/gia/giaAig.h"
#include "sat/bmc/bmc.h"
@@ -33,6 +34,9 @@ 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_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 );
+extern void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs );
typedef struct Int_Pair_t_ Int_Pair_t;
struct Int_Pair_t_
@@ -302,6 +306,40 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
return pNew;
}
+static int Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex )
+{
+ Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0 );
+ int f, i;
+ Gia_Obj_t * pObj, * pObjRi;
+
+ 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++ )
+ Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
+ Gia_ManForEachRiRo( pGiaOrig, pObjRi, pObj, i )
+ pObj->Value = pObjRi->Value;
+ Gia_ManForEachAnd( pGiaOrig, pObj, i )
+ pObj->Value = Gia_ObjFanin0Copy(pObj) & Gia_ObjFanin1Copy(pObj);
+ Gia_ManForEachCo( pGiaOrig, pObj, i )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ManForEachPo( pGiaOrig, pObj, i )
+ {
+ if (pObj->Value==1) {
+ Abc_Print( 1, "CEX is real on the original model.\n" );
+ Gia_ManStop(pGiaOrig);
+ return 1;
+ }
+ }
+ }
+
+ // Abc_Print( 1, "CEX is spurious.\n" );
+ Gia_ManStop(pGiaOrig);
+ return 0;
+}
+
static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops )
{
Vec_Int_t * vFlops = Vec_IntAlloc( 100 );
@@ -1077,20 +1115,83 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Gia_ManPrintStats( pGia, NULL );
}
Wlc_NtkFree( pAbs );
+ // Gia_AigerWrite( pGia, "abs.aig", 0, 0 );
// try to prove abstracted GIA by converting it to AIG and calling PDR
pAig = Gia_ManToAigSimple( pGia );
- pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
- clk2 = Abc_Clock();
+ if ( vClauses && pPars->fCheckCombUnsat )
+ {
+ Pdr_Man_t * pPdr2;
+
+ if ( Aig_ManAndNum( pAig ) <= 20000 )
+ {
+ Aig_Man_t * pAigScorr;
+ Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
+ int nAnds;
+
+ clk2 = Abc_Clock();
+
+ Ssw_ManSetDefaultParams( pScorrPars );
+ pScorrPars->fStopWhenGone = 1;
+ pScorrPars->nFramesK = 1;
+ pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
+ assert ( pAigScorr );
+ nAnds = Aig_ManAndNum( pAigScorr);
+ Aig_ManStop( pAigScorr );
+
+ if ( nAnds == 0 )
+ {
+ if ( pPars->fVerbose )
+ Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 );
+ RetValue = 1;
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ Aig_ManStop( pAig );
+ break;
+ }
+ else if ( pPars->fVerbose )
+ {
+ Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+ }
+ }
+
+ clk2 = Abc_Clock();
+
+ pPdrPars->fVerbose = 0;
+ pPdr2 = Pdr_ManStart( pAig, pPdrPars, NULL );
+ RetValue = IPdr_ManCheckCombUnsat( pPdr2 );
+ Pdr_ManStop( pPdr2 );
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+
+ tPdr += Abc_Clock() - clk2;
+
+ if ( RetValue == 1 )
+ {
+ if ( pPars->fVerbose )
+ Abc_PrintTime( 1, "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk2 );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ Aig_ManStop( pAig );
+ break;
+ }
+
+ if ( pPars->fVerbose )
+ Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk2 );
+ }
+
+ clk2 = Abc_Clock();
+ pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
if ( vClauses ) {
assert( Vec_VecSize( vClauses) >= 2 );
IPdr_ManRestore( pPdr, vClauses, vMap );
}
Vec_IntFreeP( &vMap );
- RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
+ if ( !vClauses || RetValue != 1 )
+ RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
pPdr->tTotal += Abc_Clock() - clk2;
tPdr += pPdr->tTotal;
@@ -1107,6 +1208,16 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
break;
}
+ // verify CEX
+ if ( Wlc_NtkCexIsReal( p, pCex ) )
+ {
+ vRefine = NULL;
+ Abc_CexFree( pCex ); // return CEX in the future
+ Pdr_ManStop( pPdr );
+ Aig_ManStop( pAig );
+ break;
+ }
+
// perform refinement
if ( pPars->fHybrid || !pPars->fProofRefine )
{
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 38f919d4..a10310d4 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;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmuxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -553,6 +553,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fMFFC ^= 1;
break;
+ case 'u':
+ pPars->fCheckCombUnsat ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -573,7 +576,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] [-abrcpmxvwh]\n" );
+ Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxuvwh]\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 );
@@ -586,6 +589,7 @@ usage:
Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using both cex-based and proof-based refinement [default = %s]\n", pPars->fHybrid? "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-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-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 89699949..e6f25f1e 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -121,6 +121,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fPdra = 0; // Use pdr -nct
pPars->fProofRefine = 0; // Use proof-based refinement
pPars->fHybrid = 1; // Use a hybrid of CBR and PBR
+ pPars->fCheckCombUnsat = 0; // Check if ABS becomes comb. unsat
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 8ca8e29e..fa5d11b4 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -59,8 +59,9 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
- Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
- Pdr_SetPrint( stdout, pCube, nRegs, NULL );
+ Abc_Print( 1, "Frame[%4d]Cube[%4d] = ", k, Counter++ );
+ // Pdr_SetPrint( stdout, pCube, nRegs, NULL );
+ ZPdr_SetPrint( pCube );
Abc_Print( 1, "\n" );
}
}
@@ -738,6 +739,121 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
return RetValue;
}
+int IPdr_ManCheckCombUnsat( Pdr_Man_t * p )
+{
+ int iFrame, RetValue = -1;
+
+ Pdr_ManCreateSolver( p, (iFrame = 0) );
+ Pdr_ManCreateSolver( p, (iFrame = 1) );
+
+ p->nFrames = iFrame;
+ p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+ RetValue = Pdr_ManCheckCube( p, iFrame, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
+ return RetValue;
+}
+
+int IPdr_ManCheckCubeReduce( Pdr_Man_t * p, Vec_Ptr_t * vClauses, Pdr_Set_t * pCube, int nConfLimit )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vLits, * vLitsA;
+ int Lit, RetValue = l_True;
+ int i;
+ Pdr_Set_t * pCla;
+ int iActVar = 0;
+ abctime clk = Abc_Clock();
+
+ pSat = Pdr_ManSolver( p, 1 );
+
+ if ( pCube == NULL ) // solve the property
+ {
+ Lit = toLit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+ RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 );
+ assert( RetValue == 1 );
+
+ vLitsA = Vec_IntStart( Vec_PtrSize( vClauses ) );
+ iActVar = Pdr_ManFreeVar( p, 1 );
+ for ( i = 1; i < Vec_PtrSize( vClauses ); ++i )
+ Pdr_ManFreeVar( p, 1 );
+ Vec_PtrForEachEntry( Pdr_Set_t *, vClauses, pCla, i )
+ {
+ vLits = Pdr_ManCubeToLits( p, 1, pCla, 1, 0 );
+ Lit = Abc_Var2Lit( iActVar + i, 1 );
+ Vec_IntPush( vLits, Lit );
+
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ assert( RetValue == 1 );
+ Vec_IntWriteEntry( vLitsA, i, Abc_Var2Lit( iActVar + i, 0 ) );
+ }
+ sat_solver_compress( pSat );
+
+ // solve
+ RetValue = sat_solver_solve( pSat, Vec_IntArray(vLitsA), Vec_IntArray(vLitsA) + Vec_IntSize(vLitsA), nConfLimit, 0, 0, 0 );
+ Vec_IntFree( vLitsA );
+
+ if ( RetValue == l_Undef )
+ return -1;
+ }
+
+ assert( RetValue != l_Undef );
+ if ( RetValue == l_False ) // UNSAT
+ {
+ int ncorelits, *pcorelits;
+ Vec_Ptr_t * vTemp = NULL;
+ Vec_Bit_t * vMark = NULL;
+
+ ncorelits = sat_solver_final(pSat, &pcorelits);
+ Abc_Print( 1, "UNSAT at the last frame. nCores = %d (out of %d).", ncorelits, Vec_PtrSize( vClauses ) );
+ Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
+
+ vTemp = Vec_PtrDup( vClauses );
+ vMark = Vec_BitStart( Vec_PtrSize( vClauses) );
+ Vec_PtrClear( vClauses );
+ for ( i = 0; i < ncorelits; ++i )
+ {
+ //Abc_Print( 1, "Core[%d] = lit(%d) = var(%d) = %d-th set\n", i, pcorelits[i], Abc_Lit2Var(pcorelits[i]), Abc_Lit2Var(pcorelits[i]) - iActVar );
+ Vec_BitWriteEntry( vMark, Abc_Lit2Var( pcorelits[i] ) - iActVar, 1 );
+ }
+
+ Vec_PtrForEachEntry( Pdr_Set_t *, vTemp, pCla, i )
+ {
+ if ( Vec_BitEntry( vMark, i ) )
+ {
+ Vec_PtrPush( vClauses, pCla );
+ continue;
+ }
+ Pdr_SetDeref( pCla );
+ }
+
+ Vec_PtrFree( vTemp );
+ Vec_BitFree( vMark );
+ RetValue = 1;
+ }
+ else // SAT
+ {
+ Abc_Print( 1, "SAT at the last frame." );
+ Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
+ RetValue = 0;
+ }
+
+ return RetValue;
+}
+
+int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
+{
+ int iFrame, RetValue = -1;
+ Vec_Ptr_t * vLast = NULL;
+
+ Pdr_ManCreateSolver( p, (iFrame = 0) );
+ Pdr_ManCreateSolver( p, (iFrame = 1) );
+
+ p->nFrames = iFrame;
+ p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+ vLast = Vec_VecEntry( vClauses, Vec_VecSize( vClauses ) - 1 );
+ RetValue = IPdr_ManCheckCubeReduce( p, vLast, NULL, p->pPars->nConfLimit );
+ return RetValue;
+}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 22:58:17 +0000