Undoing previous change in 'resim' (do not initialize flops using their values in the CEX because the number of flops in the CEX can be different).

This commit is contained in:
Alan Mishchenko 2011-08-01 11:25:46 +07:00
parent 88251e97e3
commit ab3c537072
1 changed files with 12 additions and 2 deletions

View File

@ -49,20 +49,30 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t
assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
nWords = Vec_PtrReadWordsSimInfo( vInfo );
/*
// user register values
assert( pCex->nRegs == Gia_ManRegNum(pAig) );
for ( k = 0; k < pCex->nRegs; k++ )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0;
}
/*
*/
// print warning about register values
for ( k = 0; k < pCex->nRegs; k++ )
if ( Gia_InfoHasBit( pCex->pData, k ) )
break;
if ( k < pCex->nRegs )
Abc_Print( 0, "The CEX has flop values different from 0, but they are currently not used by \"resim\".\n" );
// assign zero register values
for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
*/
for ( i = pCex->nRegs; i < pCex->nBits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ );