From 8bff9aa1cd118028db47d886254dc4c76c516166 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Feb 2017 17:36:20 -0800 Subject: Adding PDR with abstraction. --- src/proof/pdr/pdrCore.c | 132 +++++++++++++++++++++++++++++------------------- src/proof/pdr/pdrInt.h | 10 ++-- src/proof/pdr/pdrInv.c | 1 + src/proof/pdr/pdrMan.c | 113 ++++++++++++++++++++++++++++++++++++----- src/proof/pdr/pdrTsim.c | 36 ++++++++++++- 5 files changed, 221 insertions(+), 71 deletions(-) (limited to 'src/proof') diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 74a15e40..47f0ac8b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -420,6 +420,8 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, { assert( pCubeMin->Lits[i] >= 0 ); assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); + if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 ) + p->nAbsFlops++; Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } @@ -778,6 +780,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) { assert( pCubeMin->Lits[i] >= 0 ); assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); + if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 ) + p->nAbsFlops++; Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref @@ -837,29 +841,43 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_Set_t * pCube = NULL; Aig_Obj_t * pObj; Abc_Cex_t * pCexNew; - int k, RetValue = -1; + int iFrame, RetValue = -1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved if ( p->pPars->fSolveAll ) - Saig_ManForEachPo( p->pAig, pObj, k ) + Saig_ManForEachPo( p->pAig, pObj, iFrame ) if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) { - Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat p->pPars->nProveOuts++; if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, k ); + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); } // create the first timeframe p->pPars->timeLastSolved = Abc_Clock(); - Pdr_ManCreateSolver( p, (k = 0) ); + Pdr_ManCreateSolver( p, (iFrame = 0) ); while ( 1 ) { - p->nFrames = k; - assert( k == Vec_PtrSize(p->vSolvers)-1 ); - p->iUseFrame = Abc_MaxInt(k, 1); + if ( p->pPars->fUseAbs && iFrame == 2 ) + { + int i, Prio, Num = Saig_ManPiNum(p->pAig); + assert( p->vAbsFlops == NULL ); + p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) ); + p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) ); + p->vMapPpi2Ff = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( p->vPrio, Prio, i ) + if ( Prio >> p->nPrioShift ) + Vec_IntWriteEntry( p->vAbsFlops, i, 1 ); + } + if ( p->pPars->fUseAbs && p->vAbsFlops ) + printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) ); + + p->nFrames = iFrame; + assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); + p->iUseFrame = Abc_MaxInt(iFrame, 1); Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { // skip disproved outputs @@ -876,16 +894,16 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( !p->pPars->fSolveAll ) { - pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ); + pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ); p->pAig->pSeqModel = pCexNew; return 0; // SAT } - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; p->pPars->nFailOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( !p->pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n", - nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); @@ -895,8 +913,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Quitting due to callback on fail.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) ) @@ -918,11 +936,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); - p->pPars->iFrame = k; + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + p->pPars->iFrame = iFrame; return -1; } - RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 ); + RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0 ); if ( RetValue == 1 ) break; if ( RetValue == -1 ) @@ -930,9 +948,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( p->timeToStop && Abc_Clock() > p->timeToStop ) - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) { Pdr_QueueClean( p ); @@ -940,10 +958,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) break; // keep solving } else if ( p->pPars->nConfLimit ) - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); else if ( p->pPars->fVerbose ) - Abc_Print( 1, "Computation cancelled by the callback.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( RetValue == 0 ) @@ -954,9 +972,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( p->timeToStop && Abc_Clock() > p->timeToStop ) - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) { Pdr_QueueClean( p ); @@ -964,25 +982,33 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) break; // keep solving } else if ( p->pPars->nConfLimit ) - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); else if ( p->pPars->fVerbose ) - Abc_Print( 1, "Computation cancelled by the callback.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( RetValue == 0 ) { if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; if ( !p->pPars->fSolveAll ) { - p->pAig->pSeqModel = Pdr_ManDeriveCex(p); + Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p); + if ( pCex == NULL ) + { + assert( p->pPars->fUseAbs ); + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving + } + p->pAig->pSeqModel = pCex; return 0; // SAT } p->pPars->nFailOuts++; @@ -997,13 +1023,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Quitting due to callback on fail.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( !p->pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", - nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT Pdr_QueueClean( p ); @@ -1025,7 +1051,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); if ( !p->pPars->fNotVerbose ) - Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur ); + Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); } p->timeToStopOne = 0; } @@ -1036,11 +1062,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); - Pdr_ManSetPropertyOutput( p, k ); - Pdr_ManCreateSolver( p, ++k ); + Pdr_ManSetPropertyOutput( p, iFrame ); + Pdr_ManCreateSolver( p, ++iFrame ); if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } // push clauses into this timeframe @@ -1052,11 +1078,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( !p->pPars->fSilent ) { if ( p->timeToStop && Abc_Clock() > p->timeToStop ) - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); else - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame ); } - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; return -1; } if ( RetValue ) @@ -1067,17 +1093,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManReportInvariant( p ); if ( !p->pPars->fSilent ) Pdr_ManVerifyInvariant( p ); - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; // count the number of UNSAT outputs p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; // convert previously 'unknown' into 'unsat' if ( p->pPars->vOutMap ) - for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ ) - if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown + for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ ) + if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown { - Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, k ); + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); } if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) ) return 1; // UNSAT @@ -1091,44 +1117,44 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // check termination if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) { - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; return -1; } if ( p->timeToStop && Abc_Clock() > p->timeToStop ) { if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); - p->pPars->iFrame = k; + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) { if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); - p->pPars->iFrame = k; + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + p->pPars->iFrame = iFrame; return -1; } - if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax ) + if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; return -1; } } diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index fb671700..2ee4ae09 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -31,6 +31,7 @@ #include "sat/bsat/satSolver.h" #include "pdr.h" #include "misc/hash/hashInt.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_HEADER_START @@ -71,6 +72,7 @@ struct Pdr_Man_t_ // input problem Pdr_Par_t * pPars; // parameters Aig_Man_t * pAig; // user's AIG + Gia_Man_t * pGia; // user's AIG // static CNF representation Cnf_Man_t * pCnfMan; // CNF manager Cnf_Dat_t * pCnf1; // CNF for this AIG @@ -90,7 +92,10 @@ struct Pdr_Man_t_ int * pOrder; // ordering of the lits Vec_Int_t * vActVars; // the counter of activation variables int iUseFrame; // the first used frame - Vec_Int_t * vAbs; // abstraction (mapping abstracted flop ID into its PPIs number) + int nAbsFlops; // the number of flops used + Vec_Int_t * vAbsFlops; // flops currently used + Vec_Int_t * vMapFf2Ppi; + Vec_Int_t * vMapPpi2Ff; // terminary simulation Txs_Man_t * pTxs; // internal use @@ -161,8 +166,6 @@ static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p ) /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== pdrCex.c ==========================================================*/ -extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); /*=== pdrCnf.c ==========================================================*/ extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj ); extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ); @@ -183,6 +186,7 @@ extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ); extern void Pdr_ManStop( Pdr_Man_t * p ); extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); +extern Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ); /*=== pdrSat.c ==========================================================*/ extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ); extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index fe759fff..7a8a66d6 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -81,6 +81,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%6d", p->nQueMax ); + Abc_Print( 1, "%6d", p->nAbsFlops ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index b2df5e01..e2807c92 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "pdrInt.h" -#include "aig/gia/giaAig.h" +#include "sat/bmc/bmc.h" ABC_NAMESPACE_IMPL_START @@ -233,13 +233,6 @@ Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls ) //Vec_IntPrint( vCosts ); return vCosts; } -Vec_Int_t * Pdr_ManDeriveFlopPriorities( Aig_Man_t * pAig, int fMuxCtrls ) -{ - Gia_Man_t * pGia = Gia_ManFromAigSimple(pAig); - Vec_Int_t * vRes = Pdr_ManDeriveFlopPriorities2(pGia, fMuxCtrls); - Gia_ManStop( pGia ); - return vRes; -} /**Function************************************************************* @@ -258,6 +251,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p = ABC_CALLOC( Pdr_Man_t, 1 ); p->pPars = pPars; p->pAig = pAig; + p->pGia = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL; p->vSolvers = Vec_PtrAlloc( 0 ); p->vClauses = Vec_VecAlloc( 0 ); p->pQueue = NULL; @@ -270,7 +264,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio if ( vPrioInit ) p->vPrio = vPrioInit; else if ( pPars->fFlopPrio ) - p->vPrio = Pdr_ManDeriveFlopPriorities(pAig, 1); + p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1); else if ( p->pPars->fNewXSim ) p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) ); else @@ -286,8 +280,6 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed p->vRes = Vec_IntAlloc( 100 ); // final result p->pCnfMan = Cnf_ManStart(); - if ( p->vAbs ) - p->vAbs = Vec_IntStart( Aig_ManRegNum(pAig) ); // ternary simulation p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL; // additional AIG data-members @@ -328,6 +320,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Pdr_Set_t * pCla; sat_solver * pSat; int i, k; + Gia_ManStopP( &p->pGia ); Aig_ManCleanMarkAB( p->pAig ); if ( p->pPars->fVerbose ) { @@ -370,7 +363,9 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_WecFreeP( &p->vVLits ); // CNF manager Cnf_ManStop( p->pCnfMan ); - Vec_IntFreeP( &p->vAbs ); + Vec_IntFreeP( &p->vAbsFlops ); + Vec_IntFreeP( &p->vMapFf2Ppi ); + Vec_IntFreeP( &p->vMapPpi2Ff ); // terminary simulation if ( p->pPars->fNewXSim ) Txs_ManStop( p->pTxs ); @@ -419,7 +414,6 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) nFrames++; // create the counter-example pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); -// pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; pCex->iPo = p->iOutCur; pCex->iFrame = nFrames-1; for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) @@ -428,6 +422,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) Lit = pObl->pState->Lits[i]; if ( lit_sign(Lit) ) continue; + if ( lit_var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away + continue; assert( lit_var(Lit) < pCex->nPis ); Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) ); } @@ -437,6 +433,97 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) return pCex; } +/**Function************************************************************* + + Synopsis [Derives counter-example when abstraction is used.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ) +{ + extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi ); + + Gia_Man_t * pAbs; + Abc_Cex_t * pCex, * pCexCare; + Pdr_Obl_t * pObl; + int i, f, Lit, Flop, nFrames = 0; + int nPis = Saig_ManPiNum(p->pAig); + int nFfRefined = 0; + if ( !p->pPars->fUseAbs ) + return Pdr_ManDeriveCex(p); + // restore previous map + Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i ) + { + assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i ); + Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 ); + } + Vec_IntClear( p->vMapPpi2Ff ); + // count the number of frames + for ( pObl = p->pQueue; pObl; pObl = pObl->pNext ) + { + for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) + { + Lit = pObl->pState->Lits[i]; + if ( lit_var(Lit) < nPis ) // PI literal + continue; + Flop = lit_var(Lit) - nPis; + if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal + continue; + Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) ); + Vec_IntPush( p->vMapPpi2Ff, Flop ); + } + nFrames++; + } + if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX + return Pdr_ManDeriveCex(p); + // create the counter-example + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames ); + pCex->iPo = p->iOutCur; + pCex->iFrame = nFrames-1; + for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) + for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) + { + Lit = pObl->pState->Lits[i]; + if ( lit_sign(Lit) ) + continue; + if ( lit_var(Lit) < nPis ) // PI literal + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) ); + else + { + int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis); + assert( iPPI < pCex->nPis ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI ); + } + } + assert( f == nFrames ); + // perform CEX minimization + pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi ); + pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 1, 1 ); + Gia_ManStop( pAbs ); + assert( pCexCare->nPis == pCex->nPis ); + Abc_CexFree( pCex ); + // detect care PPIs + for ( f = 0; f < nFrames; f++ ) + { + for ( i = nPis; i < pCexCare->nPis; i++ ) + if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) ) + { + if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted + Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++; + } + } + Abc_CexFree( pCexCare ); + if ( nFfRefined == 0 ) // no refinement -- this is a real CEX + return Pdr_ManDeriveCex(p); + printf( "CEX-based refinement refined %d flops.\n", nFfRefined ); + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 0bcb6e0c..1cff03c7 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -440,7 +440,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) + if ( Vec_IntEntry(vPrio, Entry) ) continue; Vec_IntClear( vUndo ); if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) @@ -454,7 +454,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) + if ( !Vec_IntEntry(vPrio, Entry) ) continue; Vec_IntClear( vUndo ); if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) @@ -473,7 +473,39 @@ 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, k = 0, fAllNegs = 1; + 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; + } + } + } + } 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) ); -- cgit v1.2.3