Bug fix in 'testcex' when flop count in the CEX is different from the network (say, after seq synthesis).

This commit is contained in:
Alan Mishchenko 2014-12-19 18:34:29 -08:00
parent dd912b5c61
commit d5a952c462
1 changed files with 3 additions and 2 deletions

View File

@ -733,9 +733,10 @@ int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p )
Abc_NtkCleanMarkC( pNtk );
Abc_AigConst1(pNtk)->fMarkC = 1;
// initialize flops
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
// Abc_NtkForEachLatch( pNtk, pObj, i )
// Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
// simulate timeframes
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
{
Abc_NtkForEachPi( pNtk, pObj, k )