diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2019-01-16 17:57:40 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2019-01-16 17:57:40 -0800 |
| commit | d05f89d9977f5cb27d25ad5ae167ff5a311ea7e2 (patch) | |
| tree | 2a4edab672c35929007f30b331006530a0de1f88 /src/base/io/io.c | |
| parent | 7f778ff805c6b0b2911f7ab64b4e263a719b81e7 (diff) | |
| download | abc-d05f89d9977f5cb27d25ad5ae167ff5a311ea7e2.tar.gz abc-d05f89d9977f5cb27d25ad5ae167ff5a311ea7e2.tar.bz2 abc-d05f89d9977f5cb27d25ad5ae167ff5a311ea7e2.zip | |
Fixing the problem with outputting word-level CEXes.
Diffstat (limited to 'src/base/io/io.c')
| -rw-r--r-- | src/base/io/io.c | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index a85d64ef..e68985f3 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2446,12 +2446,35 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); // output flop values (unaffected by the minimization) Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + { + char * pObjName = Abc_ObjName(Abc_ObjFanout0(pObj)); + int ii, NameLen = strlen(pObjName); + // check if there is a PI with a matching name + Abc_Obj_t * pObjPi; + Abc_NtkForEachPi( pNtk, pObjPi, ii ) + if ( !strncmp(Abc_ObjName(pObjPi), pObjName, NameLen) && !strncmp(Abc_ObjName(pObjPi)+NameLen, "_init", 5) ) + { + if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+ii) ) + fprintf( pFile, "%s@%d=%c\n", pObjName, 0, '0'+Abc_InfoHasBit(pCex->pData, pCare->nRegs+ii) ); + break; + } + if ( ii != Abc_NtkPiNum(pNtk) ) + continue; + if ( !strncmp(pObjName, "abc_reset_flop", 14) ) + continue; + fprintf( pFile, "%s@0=%c\n", pObjName, '0'+!Abc_LatchIsInit0(pObj) ); + } // 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 |