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

Fixing the problem with outputting word-level CEXes.

This commit is contained in:
Alan Mishchenko 2019-01-16 17:57:40 -08:00
parent 7f778ff805
commit d05f89d997
2 changed files with 48 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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

25
src/base/wlc/wlcBlast.c
View File

@ -1150,6 +1150,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
int i, k, b, iFanin, iLit, nAndPrev, * pFans0, * pFans1, * pFans2, * pFans3;
int nFFins = 0, nFFouts = 0, curPi = 0, curPo = 0, nFf2Regs = 0;
int nBitCis = 0, nBitCos = 0, fAdded = 0;
int iFirstAddPi = -1; // remembers the first additional PI that stands for DC-flop output
Wlc_BstPar_t Par, * pPar = &Par;
Wlc_BstParDefault( pPar );
pPar = pParIn ? pParIn : pPar;
@ -2122,9 +2123,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
{
char Buffer[100];
sprintf( Buffer, "%s%d", "init", i );
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
//Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
// save NULL at this time - to be overwritten later
//printf( "Adding NULL in position %d\n", Vec_PtrSize(pNew->vNamesIn) );
Vec_PtrPush( pNew->vNamesIn, NULL );
fAdded = 1;
}
// remember the place in the array where the first real flop is
iFirstAddPi = Vec_PtrSize(pNew->vNamesIn);
}
Wlc_NtkForEachCi( p, pObj, i )
if ( !Wlc_ObjIsPi(pObj) )
@ -2141,6 +2147,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
}
}
/*
Wlc_NtkForEachFf2( p, pObj, i )
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
@ -2159,6 +2166,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
}
}
*/
Wlc_NtkForEachFf2( p, pObj, i )
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
@ -2191,6 +2199,21 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
}
}
assert( Vec_PtrSize(pNew->vNamesIn) == Gia_ManCiNum(pNew) );
// finish creating names of additional primary inputs
if ( p->pInits )
{
int Length = strlen(p->pInits);
assert( iFirstAddPi >= 0 );
for ( i = 0; i < Length; i++ )
if ( p->pInits[i] == 'x' || p->pInits[i] == 'X' )
{
char Buffer[1000];
sprintf( Buffer, "%s_init", (char *)Vec_PtrEntry(pNew->vNamesIn, iFirstAddPi+i) );
assert( Vec_PtrEntry(pNew->vNamesIn, iFirstAddPi-Length+i) == NULL );
Vec_PtrWriteEntry( pNew->vNamesIn, iFirstAddPi-Length+i, Abc_UtilStrsav(Buffer) );
//printf( "Replacing NULL in position %d\n", iFirstAddPi-Length+i );
}
}
// create output names
pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
Wlc_NtkForEachFf2( p, pObj, i )