diff options
| -rw-r--r-- | src/aig/gia/giaDup.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 218 | ||||
| -rw-r--r-- | src/misc/util/utilCex.c | 23 | ||||
| -rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcCexCut.c | 67 |
5 files changed, 275 insertions, 40 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index b0c5ca21..eddbd320 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1234,8 +1234,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) assert( Gia_ManRegNum(p2) == 0 ); // there is only one PO in p2 assert( Gia_ManPoNum(p2) == 1 ); - // flop count of p1 is equal to input count of p2 - assert( Gia_ManRegNum(p1) == Gia_ManPiNum(p2) ); + // input count of p2 is equal to flop count of p1 + assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) ); // start new AIG pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) ); @@ -1261,7 +1261,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) Gia_ManForEachRi( p1, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); -// Gia_ManPrintStats( pGiaNew, 0 ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p1) ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7618c164..678589e2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -296,6 +296,8 @@ static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCexSave ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCexLoad ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDualRail ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBlockPo ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -364,8 +366,8 @@ static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -755,6 +757,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); Cmd_CommandAdd( pAbc, "Verification", "cexsave", Abc_CommandCexSave, 0 ); Cmd_CommandAdd( pAbc, "Verification", "cexload", Abc_CommandCexLoad, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "cexcut", Abc_CommandCexCut, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "cexmerge", Abc_CommandCexMerge, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dualrail", Abc_CommandDualRail, 1 ); Cmd_CommandAdd( pAbc, "Verification", "blockpo", Abc_CommandBlockPo, 1 ); @@ -820,8 +824,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); +// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); +// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmin", Abc_CommandAbc9CexMin, 0 ); Cmd_CommandAdd( pAbc, "Abstraction", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 ); @@ -22516,7 +22520,7 @@ int Abc_CommandCexSave( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pCex == NULL ) { - Abc_Print( -1, "Empty network.\n" ); + Abc_Print( -1, "Current CEX is not available..\n" ); return 1; } ABC_FREE( pAbc->pCex2 ); @@ -22555,9 +22559,9 @@ int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pAbc->pCex == NULL ) + if ( pAbc->pCex2 == NULL ) { - Abc_Print( -1, "Empty network.\n" ); + Abc_Print( -1, "Saved CEX is not available.\n" ); return 1; } ABC_FREE( pAbc->pCex ); @@ -22583,6 +22587,200 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c; + int iFrStart = 0; + int iFrStop = ABC_INFINITY; + int fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + iFrStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrStart < 0 ) + goto usage; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + iFrStop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrStop < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + if ( pAbc->pCex == NULL ) + { + Abc_Print( 1, "There is no current cex.\n"); + return 0; + } + if ( pAbc->pNtkCur == NULL ) + { + Abc_Print( 1, "There is no AIG in the &-space.\n"); + return 0; + } + if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) + { + Abc_Print( 1, "Current network is not an AIG.\n"); + return 0; + } + if ( iFrStop == ABC_INFINITY ) + iFrStop = pAbc->pCex->iFrame; + + { + Abc_Ntk_t * pNtkNew; + Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); + Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fVerbose ); + Aig_ManStop( pAig ); + if ( pAigNew == NULL ) + { + Abc_Print( 1, "Command has failed.\n"); + return 0; + } + pNtkNew = Abc_NtkFromAigPhase( pAigNew ); + pNtkNew->pName = Extra_UtilStrsav( pAbc->pNtkCur->pName ); + Aig_ManStop( pAigNew ); + // update the network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); + } + return 0; + +usage: + Abc_Print( -2, "usage: cexcut [-FG num] [-vh]\n" ); + Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" ); + Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart ); + Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandCexMerge( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Cex_t * pCexNew; + int c; + int iFrStart = 0; + int iFrStop = ABC_INFINITY; + int fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + iFrStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrStart < 0 ) + goto usage; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + iFrStop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrStop < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + if ( pAbc->pCex == NULL ) + { + Abc_Print( 1, "There is no current cex.\n"); + return 0; + } + if ( pAbc->pCex2 == NULL ) + { + Abc_Print( 1, "There is no saved cex.\n"); + return 0; + } + if ( iFrStop - iFrStart < pAbc->pCex->iFrame ) + { + Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n"); + return 0; + } + pCexNew = Abc_CexMerge( pAbc->pCex2, pAbc->pCex, iFrStart, iFrStop ); + if ( pCexNew == NULL ) + { + Abc_Print( 1, "Merging CEXes has failed.\n"); + return 0; + } + // replace the saved CEX + ABC_FREE( pAbc->pCex2 ); + pAbc->pCex2 = pCexNew; + return 0; + +usage: + Abc_Print( -2, "usage: cexmerge [-FG num] [-vh]\n" ); + Abc_Print( -2, "\t merges the current CEX into the saved one\n" ); + Abc_Print( -2, "\t and sets the resulting CEX as the saved one\n" ); + Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart ); + Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandCexMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; @@ -28680,10 +28878,10 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &cexcut [-FG num] [-vh]\n" ); - Abc_Print( -2, "\t extract logic representation of bad states\n" ); + Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" ); Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart ); Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -28754,7 +28952,7 @@ int Abc_CommandAbc9CexMerge( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "There is no saved cex.\n"); return 0; } - if ( iFrStop - iFrStart > pAbc->pCex->iFrame ) + if ( iFrStop - iFrStart < pAbc->pCex->iFrame ) { Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n"); return 0; diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 16dbb076..edb246b9 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -195,14 +195,14 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrEnd > pCex->iFrame ) { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } - if ( iFrBeg >= iFrEnd ) + if ( iFrBeg > iFrEnd ) { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; } assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame ); assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame ); - assert( iFrBeg < iFrEnd ); + assert( iFrBeg <= iFrEnd ); assert( pCex->nPis == pPart->nPis ); - assert( iFrEnd - iFrBeg > pPart->iFrame ); + assert( iFrEnd - iFrBeg >= pPart->iFrame ); nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame; pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain ); @@ -211,20 +211,21 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i for ( iBit = 0; iBit < pCex->nRegs; iBit++ ) if ( Abc_InfoHasBit(pCex->pData, iBit) ) - Abc_InfoSetBit( pNew->pData, iBit++ ); + Abc_InfoSetBit( pNew->pData, iBit ); for ( f = 0; f < iFrBeg; f++ ) - for ( i = 0; i < pCex->nPis; i++ ) + for ( i = 0; i < pCex->nPis; i++, iBit++ ) if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) - Abc_InfoSetBit( pNew->pData, iBit++ ); + Abc_InfoSetBit( pNew->pData, iBit ); for ( f = 0; f < pPart->iFrame; f++ ) - for ( i = 0; i < pCex->nPis; i++ ) + for ( i = 0; i < pCex->nPis; i++, iBit++ ) if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) ) - Abc_InfoSetBit( pNew->pData, iBit++ ); + Abc_InfoSetBit( pNew->pData, iBit ); for ( f = iFrEnd; f <= pCex->iFrame; f++ ) - for ( i = 0; i < pCex->nPis; i++ ) - if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) ) - Abc_InfoSetBit( pNew->pData, iBit++ ); + for ( i = 0; i < pCex->nPis; i++, iBit++ ) + if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) + Abc_InfoSetBit( pNew->pData, iBit ); assert( iBit == pNew->nBits ); + return pNew; } diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index e1841bbc..5d789dcb 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -76,6 +76,7 @@ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); /*=== bmcCexCut.c ==========================================================*/ extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); +extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); /*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index 96d46fb3..bbb1bc73 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -6,7 +6,7 @@ PackageName [SAT-based bounded model checking.] - Synopsis [] + Synopsis [Derives characterization of bad states.] Author [Alan Mishchenko] @@ -19,6 +19,7 @@ ***********************************************************************/ #include "bmc.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START @@ -47,7 +48,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pObjRo, * pObjRi; Vec_Bit_t * vInitNew; - int i, k, iBit = 0; + int i, k, iBit = 0, fCompl0, fCompl1; if ( iFrBeg < 0 ) { printf( "Starting frame is less than 0.\n" ); return NULL; } @@ -57,7 +58,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrEnd > pCex->iFrame ) { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } - if ( iFrBeg >= iFrEnd ) + if ( iFrBeg > iFrEnd ) { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; } assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame ); assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame ); @@ -65,7 +66,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in // skip trough the first iFrEnd frames Gia_ManCleanMark0(p); - Gia_ManForEachRo( p, pObj, i ) + Gia_ManForEachRo( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); vInitNew = Vec_BitStart( Gia_ManRegNum(p) ); for ( i = 0; i < iFrEnd; i++ ) @@ -90,35 +91,39 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in // create new AIG manager pNew = Gia_ManStart( 10000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 1; Gia_ManForEachPi( p, pObj, k ) pObj->Value = 1; - Gia_ManForEachRo( p, pObjRo, i ) - pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 ); - Gia_ManHashStart( p ); + Gia_ManForEachRo( p, pObjRo, k ) + pObjRo->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 ); + Gia_ManHashStart( pNew ); for ( i = iFrEnd; i <= pCex->iFrame; i++ ) { Gia_ManForEachPi( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); Gia_ManForEachAnd( p, pObj, k ) { - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = fCompl0 & fCompl1; if ( pObj->fMark0 ) - pObj->Value = Gia_ManHashAnd( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); - else if ( !Gia_ObjFanin0(pObj)->fMark0 && !Gia_ObjFanin1(pObj)->fMark0 ) - pObj->Value = Gia_ManHashOr( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); - else if ( !Gia_ObjFanin0(pObj)->fMark0 ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 && !fCompl1 ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 ) pObj->Value = Gia_ObjFanin0(pObj)->Value; - else if ( !Gia_ObjFanin1(pObj)->fMark0 ) + else if ( !fCompl1 ) pObj->Value = Gia_ObjFanin1(pObj)->Value; else assert( 0 ); + assert( pObj->Value > 0 ); } Gia_ManForEachCo( p, pObj, k ) { pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); pObj->Value = Gia_ObjFanin0(pObj)->Value; - } + assert( pObj->Value > 0 ); + } if ( i == pCex->iFrame ) break; Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) @@ -127,7 +132,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in pObjRo->Value = pObjRi->Value; } } - Gia_ManHashStop( p ); + Gia_ManHashStop( pNew ); assert( iBit == pCex->nBits ); // create PO @@ -143,10 +148,40 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in // create new initial state pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); Gia_ManStop( pTemp ); + Vec_BitFree( vInitNew ); return pNew; } +/**Function************************************************************* + + Synopsis [Generate AIG for target bad states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) +{ + Aig_Man_t * pAig; + Gia_Man_t * pGia, * pRes; + pGia = Gia_ManFromAigSimple( p ); + if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) ) + { + Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); + Gia_ManStop( pGia ); + return NULL; + } + pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fVerbose ); + pAig = Gia_ManToAigSimple( pRes ); + Gia_ManStop( pGia ); + Gia_ManStop( pRes ); + return pAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |