diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 53 | ||||
-rw-r--r-- | src/base/abci/abc.c | 99 | ||||
-rw-r--r-- | src/misc/util/utilCex.c | 58 | ||||
-rw-r--r-- | src/misc/util/utilCex.h | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcCexCut.c | 104 |
6 files changed, 312 insertions, 4 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e24c9c2c..93387a05 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -767,6 +767,7 @@ extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut ); extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 ); +extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ); extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 378193b2..b0c5ca21 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1216,6 +1216,59 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 ) /**Function************************************************************* + Synopsis [Duplicates transition relation from p1 and property from p2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) +{ + Gia_Man_t * pTemp, * pNew; + Gia_Obj_t * pObj; + int i; + // there is no flops in 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) ); + + // start new AIG + pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) ); + pNew->pName = Abc_UtilStrsav( p1->pName ); + pNew->pSpec = Abc_UtilStrsav( p1->pSpec ); + Gia_ManHashAlloc( pNew ); + // dup first AIG + Gia_ManConst0(p1)->Value = 0; + Gia_ManForEachCi( p1, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p1, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // dup second AIG + Gia_ManConst0(p2)->Value = 0; + Gia_ManForEachPi( p2, pObj, i ) + pObj->Value = Gia_ManRo(p1, i)->Value; + Gia_ManForEachAnd( p2, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // add property output + pObj = Gia_ManPo( p2, 0 ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + // add flop inputs + Gia_ManForEachRi( p1, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); +// Gia_ManPrintStats( pGiaNew, 0 ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Print representatives.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 09e1c94e..7618c164 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -365,6 +365,7 @@ static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, cha 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_CommandAbc9CexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -820,6 +821,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) 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", "&cexmin", Abc_CommandAbc9CexMin, 0 ); Cmd_CommandAdd( pAbc, "Abstraction", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 ); @@ -28661,7 +28663,7 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) { - Abc_Print( 1, "Current counter-example is not a valid counter-example for &-space AIG \"%s\".\n", Gia_ManName(pAbc->pGia) ); + Abc_Print( 1, "Current CEX does not fail AIG \"%s\" in the &-space.\n", Gia_ManName(pAbc->pGia) ); return 0; } if ( iFrStop == ABC_INFINITY ) @@ -28681,7 +28683,100 @@ usage: Abc_Print( -2, "\t extract logic representation of bad states\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 optimization summary [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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9CexMerge( 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; } diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 80d8e141..16dbb076 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -172,6 +172,64 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i /**Function************************************************************* + Synopsis [Derives CEX from comb model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd ) +{ + Abc_Cex_t * pNew; + int nFramesGain; + int i, f, iBit; + + if ( iFrBeg < 0 ) + { printf( "Starting frame is less than 0.\n" ); return NULL; } + if ( iFrEnd < 0 ) + { printf( "Stopping frame is less than 0.\n" ); return NULL; } + if ( iFrBeg > pCex->iFrame ) + { 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 ) + { 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( pCex->nPis == pPart->nPis ); + assert( iFrEnd - iFrBeg > pPart->iFrame ); + + nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame; + pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain ); + pNew->iPo = pCex->iPo; + pNew->iFrame = pCex->iFrame - nFramesGain; + + for ( iBit = 0; iBit < pCex->nRegs; iBit++ ) + if ( Abc_InfoHasBit(pCex->pData, iBit) ) + Abc_InfoSetBit( pNew->pData, iBit++ ); + for ( f = 0; f < iFrBeg; f++ ) + for ( i = 0; i < pCex->nPis; i++ ) + if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) + Abc_InfoSetBit( pNew->pData, iBit++ ); + for ( f = 0; f < pPart->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 ( 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++ ); + assert( iBit == pNew->nBits ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Prints out the counter-example.] Description [] diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h index b45cd27b..1fd06f96 100644 --- a/src/misc/util/utilCex.h +++ b/src/misc/util/utilCex.h @@ -61,6 +61,7 @@ extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs ); extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ); extern Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo ); +extern Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd ); extern void Abc_CexPrintStats( Abc_Cex_t * p ); extern void Abc_CexPrint( Abc_Cex_t * p ); extern void Abc_CexFreeP( Abc_Cex_t ** p ); diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index 79944097..96d46fb3 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -42,9 +42,109 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd ) +Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) { - return NULL; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + Vec_Bit_t * vInitNew; + int i, k, iBit = 0; + + if ( iFrBeg < 0 ) + { printf( "Starting frame is less than 0.\n" ); return NULL; } + if ( iFrEnd < 0 ) + { printf( "Stopping frame is less than 0.\n" ); return NULL; } + if ( iFrBeg > pCex->iFrame ) + { 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 ) + { 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 ); + + // skip trough the first iFrEnd frames + Gia_ManCleanMark0(p); + Gia_ManForEachRo( p, pObj, i ) + pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + vInitNew = Vec_BitStart( Gia_ManRegNum(p) ); + for ( i = 0; i < iFrEnd; i++ ) + { + // remember values in frame iFrBeg + if ( i == iFrBeg ) + Gia_ManForEachRo( p, pObjRo, k ) + if ( pObjRo->fMark0 ) + Vec_BitWriteEntry( vInitNew, k, 1 ); + // simulate other values + 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)); + Gia_ManForEachCo( p, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( i == iFrEnd ); + + // create new AIG manager + pNew = Gia_ManStart( 10000 ); + 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 ); + 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)); + 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_ObjFanin0(pObj)->Value; + else if ( !Gia_ObjFanin1(pObj)->fMark0 ) + pObj->Value = Gia_ObjFanin1(pObj)->Value; + else assert( 0 ); + } + Gia_ManForEachCo( p, pObj, k ) + { + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + pObj->Value = Gia_ObjFanin0(pObj)->Value; + } + if ( i == pCex->iFrame ) + break; + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + pObjRo->Value = pObjRi->Value; + } + } + Gia_ManHashStop( p ); + assert( iBit == pCex->nBits ); + + // create PO + Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value ); + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + // create new GIA + pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); + Gia_ManStop( pTemp ); + + // create new initial state + pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); + Gia_ManStop( pTemp ); + Vec_BitFree( vInitNew ); + return pNew; } //////////////////////////////////////////////////////////////////////// |