diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 17:46:48 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 17:46:48 -0800 |
commit | 71cbf17e7f0352556af12ccccf9051e02c773e58 (patch) | |
tree | 002afb74b25be94e512e4869d328959046529766 /src/aig/saig/saigDup.c | |
parent | 686d38d66754027cd29c64f1dc2975248eab7796 (diff) | |
download | abc-71cbf17e7f0352556af12ccccf9051e02c773e58.tar.gz abc-71cbf17e7f0352556af12ccccf9051e02c773e58.tar.bz2 abc-71cbf17e7f0352556af12ccccf9051e02c773e58.zip |
Unified the use of counter-examples in three packages.
Diffstat (limited to 'src/aig/saig/saigDup.c')
-rw-r--r-- | src/aig/saig/saigDup.c | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index f4e557f8..b2b33bdb 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -265,6 +265,91 @@ Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) return pNew; } +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB; + Aig_ManCleanMarkB(pAig); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + // remember the number of failed output + RetValue = -1; + Saig_ManForEachPo( pAig, pObj, i ) + if ( pObj->fMarkB ) + { + RetValue = i; + break; + } + Aig_ManCleanMarkB(pAig); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |