luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #14 from YosysHQ/micko/read_cex_fix 

Make read_cex able to append if some latches are missing
This commit is contained in:
Miodrag Milanović 2022-04-18 09:24:59 +02:00 committed by GitHub
parent 00b674d5b3 43a15df951
commit 3da935785f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 13 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/base/io/io.c
View File

@ -705,11 +705,14 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
nFrames = -1;
int status = 0;
int i;
int nRegsNtk = 0;
Abc_Obj_t * pObj;
Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
Buffer = ABC_ALLOC( char, MaxLine );
while ( fgets( Buffer, MaxLine, pFile ) != NULL )
{
if ( Buffer[0] == '#' )
if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' )
continue;
Buffer[strlen(Buffer) - 1] = '\0';
if (state==0 && strlen(Buffer)>1) {
@ -719,7 +722,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
iPo = 0;
status = 1;
}
if (state==1 && Buffer[0]!='b' && Buffer[0]!='c') {
if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') {
// old format detected, first line was actually register
*fOldFormat = 1;
state = 3;
@ -766,6 +769,14 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
}
}
nRegs = Vec_IntSize(vNums);
if ( nRegs < nRegsNtk )
{
printf( "WARNING: Register number is smaller then in Ntk. Appending.\n" );
for (i=0; i<nRegsNtk-nRegs;i++) {
Vec_IntPush( vNums, 0 );
}
nRegs = Vec_IntSize(vNums);
}
state = 3;
break;
default:
@ -786,12 +797,9 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
if (usedX)
printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
Abc_Obj_t * pObj;
int iFrameCex = nFrames;
int nRegsNtk = 0;
int nPiNtk = 0;
int nPoNtk = 0;
Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
Abc_NtkForEachPi(pNtk, pObj, i ) nPiNtk++;
Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++;
if ( nRegs < 0 )