diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2019-01-18 12:34:59 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2019-01-18 12:34:59 -0800 |
| commit | 81b263e35aacc6a15a9da9c553262cacf946b8cd (patch) | |
| tree | 701ebc71d0d1c35144a5a16e62ceaa3b599967b2 | |
| parent | 4d8c72d0e923fe4e052cac4a3ef1b6138ecb3f1e (diff) | |
| download | abc-81b263e35aacc6a15a9da9c553262cacf946b8cd.tar.gz abc-81b263e35aacc6a15a9da9c553262cacf946b8cd.tar.bz2 abc-81b263e35aacc6a15a9da9c553262cacf946b8cd.zip | |
Fixing the problem with outputting word-level CEXes after retiming.
| -rw-r--r-- | src/base/io/io.c | 40 |
1 files changed, 28 insertions, 12 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index 0703d775..e7de926a 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2475,24 +2475,40 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) } fprintf( pFile, "\n"); fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); - // output flop values (unaffected by the minimization) if ( (vNamesIn = Abc_FrameReadCexCiNames(pAbc)) != NULL ) + { + // output flop values (unaffected by the minimization) Vec_PtrForEachEntryStart( char *, vNamesIn, pObjName, i, Abc_NtkPiNum(pNtk) ) IoCommandPrintLatchName( pFile, pNtk, NULL, pObjName, pCex, pCare ); + // output PI values (while skipping the minimized ones) + for ( f = 0; f <= pCex->iFrame; f++ ) + Vec_PtrForEachEntryStop( char *, vNamesIn, pObjName, i, Abc_NtkPiNum(pNtk) ) + { + // skip names with "_init" in the end + int NameLen = strlen(pObjName); + if ( NameLen > 5 && !strncmp(pObjName+NameLen-5, "_init", 5) ) + continue; + if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) ) + fprintf( pFile, "%s@%d=%c\n", pObjName, f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + } + } else + { + // output flop values (unaffected by the minimization) Abc_NtkForEachLatch( pNtk, pObj, i ) IoCommandPrintLatchName( pFile, pNtk, pObj, Abc_ObjName(Abc_ObjFanout0(pObj)), pCex, pCare ); - // output PI values (while skipping the minimized ones) - for ( f = 0; f <= pCex->iFrame; f++ ) - Abc_NtkForEachPi( pNtk, pObj, i ) - { - // skip names with "_init" in the end - int NameLen = strlen(Abc_ObjName(pObj)); - if ( NameLen > 5 && !strncmp(Abc_ObjName(pObj)+NameLen-5, "_init", 5) ) - continue; - if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) ) - fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); - } + // output PI values (while skipping the minimized ones) + for ( f = 0; f <= pCex->iFrame; f++ ) + Abc_NtkForEachPi( pNtk, pObj, i ) + { + // skip names with "_init" in the end + int NameLen = strlen(Abc_ObjName(pObj)); + if ( NameLen > 5 && !strncmp(Abc_ObjName(pObj)+NameLen-5, "_init", 5) ) + continue; + if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) ) + fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + } + } Abc_CexFreeP( &pCare ); } else |