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

Adding PDR with abstraction.

This commit is contained in:
Alan Mishchenko 2017-02-11 21:00:37 -08:00
parent 2a5fa67d36
commit ae521b6601
3 changed files with 11 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/proof/pdr/pdrCore.c
View File

@ -706,7 +706,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
{
Counter++;
pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 )
if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
return 0; // SAT
if ( pThis->iFrame > kMax ) // finished this level
return 1;
@ -862,7 +862,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
while ( 1 )
{
int fRefined = 0;
if ( p->pPars->fUseAbs && iFrame == 3 )
if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 2 )
{
int i, Prio;
assert( p->vAbsFlops == NULL );
@ -995,7 +995,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
p->pPars->iFrame = iFrame;
if ( !p->pPars->fSolveAll )
@ -1043,6 +1043,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
}
}
if ( fRefined )
break;
if ( p->pTime4Outs )
{
abctime timeSince = Abc_Clock() - clkOne;
@ -1059,9 +1061,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->timeToStopOne = 0;
}
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
if ( fRefined )
continue;
// open a new timeframe
p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL );

4
src/proof/pdr/pdrInv.c
View File

@ -470,8 +470,8 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p )
Vec_Ptr_t * vCubes;
int kStart = Pdr_ManFindInvariantStart( p );
vCubes = Pdr_ManCollectCubes( p, kStart );
Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n",
kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns );
Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n",
kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns );
// Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
// kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
Vec_PtrFree( vCubes );

37
src/proof/pdr/pdrTsim.c
View File

@ -473,54 +473,21 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
assert( Vec_IntSize(vRes) > 0 );
//p->tTsim += Abc_Clock() - clk;
// move abstracted literals from flops to inputs
if ( p->pPars->fUseAbs && p->vAbsFlops )
{
int i, iLit, Used, k = 0, fAllNegs = 1;
int i, iLit, k = 0;
Vec_IntForEachEntry( vRes, iLit, i )
{
if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
{
Vec_IntWriteEntry( vRes, k++, iLit );
fAllNegs &= Abc_LitIsCompl(iLit);
}
else
Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
}
Vec_IntShrink( vRes, k );
if ( fAllNegs ) // insert any positive literal
{
Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
{
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue;
if ( Vec_IntEntry(vCiVals, i) )
{
Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
Vec_IntPush( vRes, Abc_Var2Lit(Entry, 0) );
break;
}
}
// add any flop that is not in the cone
if ( i == Vec_IntSize(vCiObjs) )
{
Vec_IntForEachEntry( p->vAbsFlops, Used, i )
{
if ( !Used )
continue;
if ( Vec_IntFind( vRes, Abc_Var2Lit(i, 1) ) >= 0 )
continue;
Vec_IntPush( vRes, Abc_Var2Lit(i, 0) );
//Vec_IntPrint( vRes );
break;
}
assert( i < Vec_IntSize(p->vAbsFlops) );
}
}
}
pRes = Pdr_SetCreate( vRes, vPiLits );
assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
//ZH: Disabled assertion because this invariant doesn't hold with down
//because of the join operation which can bring in initial states
//assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );