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

Trying to fix a false-positive due to incorrect inductive termination check in 'int' when K is more than 1 (not fixed yet).

This commit is contained in:
Alan Mishchenko 2012-02-01 14:54:32 -08:00
parent 61211df4ff
commit 16fd67f0ab
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/proof/int/intCore.c
View File

@ -169,14 +169,16 @@ p->timeCnf += clock() - clk;
//////////////////////////////////////////
// start containment checking
if ( !(pPars->fTransLoop || pPars->fUseBackward) )
if ( !(pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1) )
{
pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
// try new containment check for the initial state
clk = clock();
pCnfInter2 = Cnf_Derive( p->pInter, 1 );
p->timeCnf += clock() - clk;
clk = clock();
RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
p->timeEqu += clock() - clk;
// assert( RetValue == 0 );
Cnf_DataFree( pCnfInter2 );
if ( p->vInters )
@ -296,8 +298,12 @@ clk = clock();
{
if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
{
if ( pPars->fTransLoop || pPars->fUseBackward )
Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
{
clk2 = clock();
Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, Abc_MinInt(i + 1, pPars->nFramesK), pPars->fUseBackward );
timeTemp = clock() - clk2;
}
else
{ // new containment check
clk2 = clock();