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

Uncommenting handling of initial values of the flops.

This commit is contained in:
Alan Mishchenko 2017-09-19 17:29:03 -07:00
parent 5585ce8aa6
commit 1e0bbef1ef
3 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -5255,6 +5255,10 @@ SOURCE=.\src\proof\cec\cecSat.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\proof\cec\cecSatG.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSeq.c SOURCE=.\src\proof\cec\cecSeq.c
# End Source File # End Source File
# Begin Source File # Begin Source File

4
src/aig/gia/giaCex.c
View File

@ -90,8 +90,8 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
int RetValue, i, k, iBit = 0; int RetValue, i, k, iBit = 0;
assert( Gia_ManPiNum(pAig) == p->nPis ); assert( Gia_ManPiNum(pAig) == p->nPis );
Gia_ManCleanMark0(pAig); Gia_ManCleanMark0(pAig);
// Gia_ManForEachRo( pAig, pObj, i ) Gia_ManForEachRo( pAig, pObj, i )
// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
iBit = p->nRegs; iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ ) for ( i = 0; i <= p->iFrame; i++ )
{ {

4
src/base/abc/abcLatch.c
View File

@ -738,8 +738,8 @@ int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p )
Abc_NtkCleanMarkC( pNtk ); Abc_NtkCleanMarkC( pNtk );
Abc_AigConst1(pNtk)->fMarkC = 1; Abc_AigConst1(pNtk)->fMarkC = 1;
// initialize flops // initialize flops
// Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
// Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++); Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
// simulate timeframes // simulate timeframes
iBit = p->nRegs; iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ ) for ( i = 0; i <= p->iFrame; i++ )