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

Updated 'iprove' to generate seq CEX when CEC fails.

This commit is contained in:
Alan Mishchenko 2011-06-25 09:23:44 -07:00
parent 4669839b24
commit 15cc374fe3
4 changed files with 34 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/base/abci/abc.c
View File

@ -10633,6 +10633,13 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_PrintTime( 1, "Time", clock() - clk );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
// update counter example
if ( RetValue == 0 && Abc_NtkLatchNum(pNtkTemp) == 0 )
{
Abc_Cex_t * pCex = Abc_CexDeriveFromCombModel( pNtkTemp->pModel, Abc_NtkPiNum(pNtkTemp), 0, iOut );
Abc_FrameReplaceCex( pAbc, &pCex );
}
return 0;
usage:

3
src/base/abci/abcIvy.c
View File

@ -520,8 +520,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
pFanin = Abc_ObjFanin0(pObj);
if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
{
pNtk->pModel = ABC_ALLOC( int, Abc_NtkPiNum(pNtk) );
memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) );
pNtk->pModel = ABC_CALLOC( int, Abc_NtkCiNum(pNtk) );
return 0;
}

25
src/misc/util/utilCex.c
View File

@ -150,6 +150,30 @@ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew )
return pCex;
}
/**Function*************************************************************
Synopsis [Derives CEX from comb model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo )
{
Abc_Cex_t * pCex;
int i;
pCex = Abc_CexAlloc( nRegs, nPis, 1 );
pCex->iPo = iPo;
pCex->iFrame = 0;
for ( i = 0; i < nPis; i++ )
if ( pModel[i] )
pCex->pData[i>>5] |= (1<<(i & 31));
return pCex;
}
/**Function*************************************************************
Synopsis [Prints out the counter-example.]
@ -196,6 +220,7 @@ void Abc_CexFree( Abc_Cex_t * p )
ABC_FREE( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/misc/util/utilCex.h
View File

@ -60,6 +60,7 @@ extern Abc_Cex_t * Abc_CexAlloc( int nRegs, int nTruePis, int nFrames );
extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut );
extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew );
extern Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo );
extern void Abc_CexPrint( Abc_Cex_t * p );
extern void Abc_CexFree( Abc_Cex_t * p );