From ab3c537072854a95c7da6e1dcc7f155c808fb837 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Aug 2011 11:25:46 +0700 Subject: 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). --- src/aig/cec/cecSeq.c | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'src/aig/cec') diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 7e7549c0..dd561971 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -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++ ); -- cgit v1.2.3