diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 11 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaEra2.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaSim.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaSim2.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 323 |
7 files changed, 98 insertions, 256 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e3546686..b2f039a7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -33,6 +33,7 @@ #include <time.h> #include "vec.h" +#include "utilCex.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -788,17 +789,13 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); -extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ); -extern Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame ); -extern Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel ); -extern Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew ); -extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); -extern void Gia_ManPrintCounterExample( Abc_Cex_t * p ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); +extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); +extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); @@ -808,8 +805,6 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); - - ABC_NAMESPACE_HEADER_END diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 38e010f1..607e5ac6 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -530,8 +530,8 @@ void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) { printf( "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 ); Abc_PrintTime( 1, "Time", clk ); - pGia->pCexSeq = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 ); - if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) ) + pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 ); + if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) ) Abc_Print( 1, "Generated counter-example is INVALID.\n" ); pPars->Status = 0; } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4ded9a78..71204548 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -416,7 +416,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) } Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); if ( p->pCexSeq ) - pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) ); + pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; } @@ -764,7 +764,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); if ( p->pCexSeq ) - pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) ); + pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; } diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c index 64464832..dedbc032 100644 --- a/src/aig/gia/giaEra2.c +++ b/src/aig/gia/giaEra2.c @@ -1758,7 +1758,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos // verify if ( pAig->pCexSeq ) { - if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) printf( "Generated counter-example is INVALID. \n" ); else printf( "Generated counter-example verified correctly. \n" ); @@ -1922,7 +1922,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast ) Vec_PtrPush( vStates, pSta ); assert( Vec_PtrSize(vStates) >= 1 ); // start the counter-example - pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) ); + pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) ); pCex->iFrame = Vec_PtrSize(vStates)-1; pCex->iPo = p->iOutFail; // compute states diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 1de1a2d4..18e02d81 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -436,7 +436,7 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, iPioId, Counter; - p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data @@ -513,7 +513,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) pPars->iOutFail = iOut; pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); - if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) { // Abc_Print( 1, "\n" ); Abc_Print( 1, "\nGenerated counter-example is INVALID. " ); diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c index 4131f942..e1a5aa07 100644 --- a/src/aig/gia/giaSim2.c +++ b/src/aig/gia/giaSim2.c @@ -606,7 +606,7 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, Counter; - p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data @@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) pPars->iOutFail = iOut; pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); - if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) { // Abc_Print( 1, "\n" ); Abc_Print( 1, "\nGenerated counter-example is INVALID. " ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 82bdb367..2794956a 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -829,244 +829,6 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob /**Function************************************************************* - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ) -{ - Abc_Cex_t * pCex; - int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - pCex->nRegs = nRegs; - pCex->nPis = nRealPis; - pCex->nBits = nRegs + nRealPis * nFrames; - return pCex; -} - - -/**Function************************************************************* - - Synopsis [Prints the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintCex( Abc_Cex_t * p ) -{ - int i, f, k; - for ( k = 0; k < p->nRegs; k++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k) ); - printf( "\n" ); - for ( f = 0; f <= p->iFrame; f++ ) - { - for ( i = 0; i < p->nPis; i++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k++) ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Derives the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); - assert( Vec_IntSize(vValues) == nSkip + pCex->nBits ); - pCex->iPo = 0; - pCex->iFrame = iFrame; - for ( i = 0; i < pCex->nBits; i++ ) - if ( Vec_IntEntry(vValues, nSkip + i) ) - Gia_InfoSetBit( pCex->pData, i ); - return pCex; -} - -/**Function************************************************************* - - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Gia_ManAllocCounterExample( nRegs, nRealPis, 1 ); - pCex->iPo = iPo; - pCex->iFrame = 0; - for ( i = pCex->nRegs; i < pCex->nBits; i++ ) - if ( pModel[i-pCex->nRegs] ) - Gia_InfoSetBit( pCex->pData, i ); - return pCex; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) -{ - Gia_Obj_t * pObj, * pObjRi, * pObjRo; - int RetValue, i, k, iBit = 0; - Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - for ( i = 0; i <= p->iFrame; i++ ) - { - Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - Gia_ManForEachAnd( pAig, pObj, k ) - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachCo( pAig, pObj, k ) - pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); - if ( i == p->iFrame ) - break; - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) - { - pObjRo->fMark0 = pObjRi->fMark0; - } - } - assert( iBit == p->nBits ); - if ( fDualOut ) - RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0; - else - RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; - Gia_ManCleanMark0(pAig); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p ) -{ - Gia_Obj_t * pObj, * pObjRi, * pObjRo; - int RetValue, i, k, iBit = 0; - Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - for ( i = 0; i <= p->iFrame; i++ ) - { - Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - Gia_ManForEachAnd( pAig, pObj, k ) - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachCo( pAig, pObj, k ) - pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) - pObjRo->fMark0 = pObjRi->fMark0; - } - assert( iBit == p->nBits ); - // remember the number of failed output - RetValue = -1; - Gia_ManForEachPo( pAig, pObj, i ) - if ( Gia_ManPo(pAig, i)->fMark0 ) - { - RetValue = i; - break; - } - Gia_ManCleanMark0(pAig); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Gia_ManAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 ); - pCex->iPo = p->iPo; - pCex->iFrame = p->iFrame; - for ( i = p->nRegs; i < p->nBits; i++ ) - if ( Gia_InfoHasBit(p->pData, i) ) - Gia_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs ); - return pCex; -} - -/**Function************************************************************* - - Synopsis [Prints out the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintCounterExample( Abc_Cex_t * p ) -{ - int i, f, k; - printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n", - p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits ); - printf( "State : " ); - for ( k = 0; k < p->nRegs; k++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k) ); - printf( "\n" ); - for ( f = 0; f <= p->iFrame; f++ ) - { - printf( "Frame %2d : ", f ); - for ( i = 0; i < p->nPis; i++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k++) ); - printf( "\n" ); - } - assert( k == p->nBits ); -} - -/**Function************************************************************* - Synopsis [Dereferences the node's MFFC.] Description [] @@ -1371,6 +1133,91 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ) */ } +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Gia_ManCleanMark0(pAig); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + } + } + assert( iBit == p->nBits ); + if ( fDualOut ) + RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0; + else + RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; + Gia_ManCleanMark0(pAig); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Gia_ManCleanMark0(pAig); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( iBit == p->nBits ); + // remember the number of failed output + RetValue = -1; + Gia_ManForEachPo( pAig, pObj, i ) + if ( Gia_ManPo(pAig, i)->fMark0 ) + { + RetValue = i; + break; + } + Gia_ManCleanMark0(pAig); + return RetValue; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |