diff options
Diffstat (limited to 'src/aig/gia/giaUtil.c')
| -rw-r--r-- | src/aig/gia/giaUtil.c | 57 |
1 files changed, 55 insertions, 2 deletions
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index cc1a3861..822f1e64 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -580,6 +580,29 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob /**Function************************************************************* + Synopsis [Allocates a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ) +{ + Gia_Cex_t * pCex; + int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); + pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); + pCex->nRegs = nRegs; + pCex->nPis = nRealPis; + pCex->nBits = nRegs + nRealPis * nFrames; + return pCex; +} + +/**Function************************************************************* + Synopsis [Resimulates the counter-example.] Description [] @@ -589,7 +612,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob SeeAlso [] ***********************************************************************/ -int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts ) +int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; @@ -608,7 +631,7 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut pObjRo->fMark0 = pObjRi->fMark0; } assert( iBit == p->nBits ); - if ( fDoubleOuts ) + 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; @@ -616,6 +639,36 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut return RetValue; } +/**Function************************************************************* + + Synopsis [Prints out the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintCounterExample( Gia_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", Aig_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", Aig_InfoHasBit(p->pData, k++) ); + printf( "\n" ); + } + assert( k == p->nBits ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |