From f6ae0e41f338a109ad2c973ace13b728f4947e14 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 4 Apr 2014 13:14:16 -0700 Subject: Better CEX minimization and renaming of write_counter into write_cex. --- abclib.dsp | 4 + src/base/io/io.c | 39 ++++-- src/misc/util/utilCex.c | 27 +++++ src/misc/util/utilCex.h | 1 + src/sat/bmc/bmc.h | 6 + src/sat/bmc/bmcCexCare.c | 298 ++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bmc/bmcCexTools.c | 4 +- src/sat/bmc/module.make | 1 + 8 files changed, 366 insertions(+), 14 deletions(-) create mode 100644 src/sat/bmc/bmcCexCare.c diff --git a/abclib.dsp b/abclib.dsp index 555e24cf..18348add 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -1423,6 +1423,10 @@ SOURCE=.\src\sat\bmc\bmcBmci.c # End Source File # Begin Source File +SOURCE=.\src\sat\bmc\bmcCexCare.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bmc\bmcCexCut.c # End Source File # Begin Source File diff --git a/src/base/io/io.c b/src/base/io/io.c index ef17c8fd..3e969915 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -22,6 +22,7 @@ #include "base/main/mainInt.h" #include "aig/saig/saig.h" #include "proof/abs/abs.h" +#include "sat/bmc/bmc.h" ABC_NAMESPACE_IMPL_START @@ -60,7 +61,7 @@ static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf2 ( Abc_Frame_t * pAbc, int argc, char **argv ); -static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteCex ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -124,7 +125,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_book", IoCommandWriteBook, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 ); - Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_cex", IoCommandWriteCex, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); Cmd_CommandAdd( pAbc, "I/O", "&write_cnf", IoCommandWriteCnf2, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 ); @@ -2171,18 +2172,20 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) +int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) { Abc_Ntk_t * pNtk; char * pFileName; int c, fNames = 0; int fMinimize = 0; + int fUseOldMin = 0; + int fCheckCex = 0; int forceSeq = 0; int fPrintFull = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "snmfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snmocfvh" ) ) != EOF ) { switch ( c ) { @@ -2195,6 +2198,12 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) case 'm': fMinimize ^= 1; break; + case 'o': + fUseOldMin ^= 1; + break; + case 'c': + fCheckCex ^= 1; + break; case 'f': fPrintFull ^= 1; break; @@ -2236,7 +2245,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) Abc_NtkForEachLatch( pNtk, pObj, i ) if ( !Abc_LatchIsInit0(pObj) ) { - fprintf( stdout, "IoCommandWriteCounter(): The init-state should be all-0 for counter-example to work.\n" ); + fprintf( stdout, "IoCommandWriteCex(): The init-state should be all-0 for counter-example to work.\n" ); fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" ); return 1; } @@ -2244,7 +2253,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) { - fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName ); + fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName ); return 1; } if ( fPrintFull ) @@ -2267,9 +2276,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose ); - if ( pCare == NULL ) - printf( "Counter-example minimization has failed.\n" ); + if ( fUseOldMin ) + { + pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose ); + if ( fCheckCex ) + Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose ); + } + else + pCare = Bmc_CexCareMinimize( pAig, pCex, fCheckCex, fVerbose ); Aig_ManStop( pAig ); } // output flop values (unaffected by the minimization) @@ -2299,7 +2313,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) int i; if ( pFile == NULL ) { - fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName ); + fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName ); return 1; } if ( fNames ) @@ -2321,12 +2335,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: write_counter [-snmfvh] \n" ); + fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] \n" ); fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" ); fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" ); fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" ); fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" ); fprintf( pAbc->Err, "\t-m : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" ); + fprintf( pAbc->Err, "\t-o : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" ); + fprintf( pAbc->Err, "\t-c : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" ); fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" ); fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); @@ -2334,7 +2350,6 @@ usage: return 1; } - /**Function************************************************************* Synopsis [] diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 1399f55d..2f2901e0 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -488,6 +488,33 @@ Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * return pCex; } +/**Function************************************************************* + + Synopsis [Count the number of 1s in the CEX.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_CexOnes32( unsigned i ) +{ + i = i - ((i >> 1) & 0x55555555); + i = (i & 0x33333333) + ((i >> 2) & 0x33333333); + i = ((i + (i >> 4)) & 0x0F0F0F0F); + return (i*(0x01010101))>>24; +} +int Abc_CexCountOnes( Abc_Cex_t * p ) +{ + int nWords = Abc_BitWordNum( p->nBits ); + int i, Count = 0; + for ( i = 0; i < nWords; i++ ) + Count += Abc_CexOnes32( p->pData[i] ); + return Count; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h index 98463410..c6904a60 100644 --- a/src/misc/util/utilCex.h +++ b/src/misc/util/utilCex.h @@ -72,6 +72,7 @@ extern Abc_Cex_t * Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPos extern Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld ); extern Abc_Cex_t * Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New ); extern Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew ); +extern int Abc_CexCountOnes( Abc_Cex_t * p ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 0bc7bb3f..3eeeb7b5 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -126,11 +126,17 @@ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); /*=== bmcBmcAnd.c ==========================================================*/ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars ); +/*=== bmcCexCare.c ==========================================================*/ +extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose ); +extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); /*=== bmcCexCut.c ==========================================================*/ extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose ); extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose ); /*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); +/*=== bmcCexTool.c ==========================================================*/ +extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose ); +extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); /*=== bmcICheck.c ==========================================================*/ extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose ); extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose ); diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c new file mode 100644 index 00000000..addb89fd --- /dev/null +++ b/src/sat/bmc/bmcCexCare.c @@ -0,0 +1,298 @@ +/**CFile**************************************************************** + + FileName [bmcCexCare.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Computing care set of the counter-example.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcCexCare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "aig/gia/giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Backward propagation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_CexCarePropagateFwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, int fGrow ) +{ + Gia_Obj_t * pObj; + int Prio, Prio0, Prio1; + int i, Phase0, Phase1; + if ( (fGrow & 2) ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Abc_Var2Lit( f * pCex->nPis + (pCex->nPis-1-i) + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ); + } + else + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Abc_Var2Lit( f * pCex->nPis + i + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ); + } + Gia_ManForEachAnd( p, pObj, i ) + { + Prio0 = Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value); + Prio1 = Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value); + Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj); + Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj); + if ( Phase0 && Phase1 ) + Prio = (fGrow & 1) ? Abc_MinInt(Prio0, Prio1) : Abc_MaxInt(Prio0, Prio1); + else if ( Phase0 && !Phase1 ) + Prio = Prio1; + else if ( !Phase0 && Phase1 ) + Prio = Prio0; + else // if ( !Phase0 && !Phase1 ) + Prio = (fGrow & 1) ? Abc_MaxInt(Prio0, Prio1) : Abc_MinInt(Prio0, Prio1); + pObj->Value = Abc_Var2Lit( Prio, Phase0 & Phase1 ); + } + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); +} +void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, int fGrow, Vec_Int_t * vPrios ) +{ + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int f, i; + Gia_ManConst0( p )->Value = 0; + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = 0; + Vec_IntClear( vPrios ); + for ( f = 0; f <= pCex->iFrame; f++ ) + { + Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) + Vec_IntPush( vPrios, (pObjRo->Value = pObjRi->Value) ); + Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow ); + } +} + +/**Function************************************************************* + + Synopsis [Forward propagation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin ) +{ + Gia_Obj_t * pObj; + int i, Phase0, Phase1; + Gia_ManForEachCand( p, pObj, i ) + pObj->fPhase = 0; + Gia_ManForEachCo( p, pObj, i ) + if ( pObj->fPhase ) + Gia_ObjFanin0(pObj)->fPhase = 1; + Gia_ManForEachAndReverse( p, pObj, i ) + { + if ( !pObj->fPhase ) + continue; + Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj); + Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj); + if ( Phase0 && Phase1 ) + { + Gia_ObjFanin0(pObj)->fPhase = 1; + Gia_ObjFanin1(pObj)->fPhase = 1; + } + else if ( Phase0 && !Phase1 ) + Gia_ObjFanin1(pObj)->fPhase = 1; + else if ( !Phase0 && Phase1 ) + Gia_ObjFanin0(pObj)->fPhase = 1; + else // if ( !Phase0 && !Phase1 ) + { + if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) <= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) ) + Gia_ObjFanin0(pObj)->fPhase = 1; + else + Gia_ObjFanin1(pObj)->fPhase = 1; + } + } + Gia_ManForEachPi( p, pObj, i ) + if ( pObj->fPhase ) + Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + pCexMin->nPis * f + i ); +} +Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPrios, int fGrow ) +{ + Abc_Cex_t * pCexMin; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int f, i; + pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 ); + pCexMin->iPo = pCex->iPo; + pCexMin->iFrame = pCex->iFrame; + Gia_ManForEachCo( p, pObj, i ) + pObj->fPhase = 0; + for ( f = pCex->iFrame; f >= 0; f-- ) + { + Gia_ManPo(p, pCex->iPo)->fPhase = (int)(f == pCex->iFrame); + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Vec_IntEntry( vPrios, f * pCex->nRegs + i ); + Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow ); + Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin ); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) + pObjRi->fPhase = pObjRo->fPhase; + } + return pCexMin; +} + +/**Function************************************************************* + + Synopsis [Computes the care set of the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose ) +{ + int nTryCexes = 4; // belongs to range [1;4] + Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL}; + int k, nOnesBest, nOnesCur; + Vec_Int_t * vPrios; + if ( pCex->nPis != Gia_ManPiNum(p) ) + { + printf( "Given CEX does to have same number of inputs as the AIG.\n" ); + return NULL; + } + if ( pCex->nRegs != Gia_ManRegNum(p) ) + { + printf( "Given CEX does to have same number of flops as the AIG.\n" ); + return NULL; + } + if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) ) + { + printf( "Given CEX has PO whose index is out of range for the AIG.\n" ); + return NULL; + } + assert( pCex->nPis == Gia_ManPiNum(p) ); + assert( pCex->nRegs == Gia_ManRegNum(p) ); + assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) ); + if ( fVerbose ) + { + printf( "Original : " ); + Bmc_CexPrint( pCex, Gia_ManPiNum(p), 0 ); + } + vPrios = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) ); + for ( k = 0; k < nTryCexes; k++ ) + { + Bmc_CexCarePropagateFwd(p, pCex, k, vPrios ); + assert( Vec_IntSize(vPrios) == pCex->nRegs * (pCex->iFrame + 1) ); + if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) ) + { + printf( "Counter-example is invalid.\n" ); + Vec_IntFree( vPrios ); + return NULL; + } + pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPrios, k ); + if ( fVerbose ) + { + if ( (k & 1) ) + printf( "Decrease : " ); + else + printf( "Increase : " ); + Bmc_CexPrint( pCexMin[k], Gia_ManPiNum(p), 0 ); + } + } + Vec_IntFree( vPrios ); + // select the best one + pCexBest = pCexMin[0]; + nOnesBest = Abc_CexCountOnes(pCexMin[0]); + for ( k = 1; k < nTryCexes; k++ ) + { + nOnesCur = Abc_CexCountOnes(pCexMin[k]); + if ( nOnesBest > nOnesCur ) + { + nOnesBest = nOnesCur; + pCexBest = pCexMin[k]; + } + } + for ( k = 0; k < nTryCexes; k++ ) + if ( pCexBest != pCexMin[k] ) + Abc_CexFreeP( &pCexMin[k] ); + // verify and return + if ( fVerbose ) + { + printf( "Final : " ); + Bmc_CexPrint( pCexBest, Gia_ManPiNum(p), 0 ); + } + if ( !Bmc_CexVerify( p, pCex, pCexBest ) ) + printf( "Counter-example verification has failed.\n" ); + else if ( fCheck ) + printf( "Counter-example verification succeeded.\n" ); + return pCexBest; +} +Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose ) +{ + Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); + Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, pCex, fCheck, fVerbose ); + Gia_ManStop( pGia ); + return pCexMin; +} + +/**Function************************************************************* + + Synopsis [Verifies the care set of the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +{ + Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); + if ( fVerbose ) + { + printf( "Original : " ); + Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 ); + printf( "Minimized: " ); + Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); + } + if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) ) + printf( "Counter-example verification has failed.\n" ); + else + printf( "Counter-example verification succeeded.\n" ); + Gia_ManStop( pGia ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c index 811a90b7..05dade97 100644 --- a/src/sat/bmc/bmcCexTools.c +++ b/src/sat/bmc/bmcCexTools.c @@ -348,7 +348,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) Gia_Obj_t * pObj; int i, k; assert( pCex->nRegs > 0 ); - assert( pCexCare->nRegs == 0 ); +// assert( pCexCare->nRegs == 0 ); Gia_ObjTerSimSet0( Gia_ManConst0(p) ); Gia_ManForEachRi( p, pObj, k ) Gia_ObjTerSimSet0( pObj ); @@ -356,7 +356,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) { Gia_ManForEachPi( p, pObj, k ) { - if ( !Abc_InfoHasBit( pCexCare->pData, i * pCexCare->nPis + k ) ) + if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) ) Gia_ObjTerSimSetX( pObj ); else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) ) Gia_ObjTerSimSet1( pObj ); diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index 3ff4b100..6deb9eb1 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -3,6 +3,7 @@ SRC += src/sat/bmc/bmcBmc.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcBmcAnd.c \ src/sat/bmc/bmcBmci.c \ + src/sat/bmc/bmcCexCare.c \ src/sat/bmc/bmcCexCut.c \ src/sat/bmc/bmcCexDepth.c \ src/sat/bmc/bmcCexMin1.c \ -- cgit v1.2.3