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

Enabled detecting CEXes in multiple POs without stopping (sim3 -a).

This commit is contained in:
Alan Mishchenko 2013-01-23 16:50:45 +07:00
parent dfd871c24d
commit 4efc89d342
2 changed files with 26 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
src/proof/ssw/sswRarity.c
View File

@ -549,44 +549,40 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
{
Aig_Obj_t * pObj;
int i;
int i, RetValue = 0;
p->iFailPo = -1;
p->iFailPat = -1;
Saig_ManForEachPo( p->pAig, pObj, i )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
return 0;
break;
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
if ( !Ssw_RarManObjIsConst(p, pObj) )
if ( Ssw_RarManObjIsConst(p, pObj) )
continue;
RetValue = 1;
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
if ( pnSolvedNow == NULL )
break;
// remember the one solved
(*pnSolvedNow)++;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
// print final report
if ( !fNotVerbose )
{
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
// remember the one solved
if ( pnSolvedNow )
{
(*pnSolvedNow)++;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
// print final report
if ( !fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
nOutDigits, p->iFailPo, iFrame,
nOutDigits, *pnSolvedNow,
nOutDigits, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Time );
}
continue;
}
return 1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
nOutDigits, p->iFailPo, iFrame,
nOutDigits, *pnSolvedNow,
nOutDigits, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Time );
}
}
return 0;
return RetValue;
}
/**Function*************************************************************

2
src/python/pyabc.i
View File

@ -238,6 +238,8 @@ Abc_Cex_t* _cex_get_vec(int i)
return NULL;
}
if ( pCex == (Abc_Cex_t *)1 )
return pCex;
return Abc_CexDup( pCex, -1 );
}