diff options
Diffstat (limited to 'src/proof/pdr/pdrMan.c')
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 341 |
1 files changed, 333 insertions, 8 deletions
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index b58c479b..a076223b 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "pdrInt.h" +#include "sat/bmc/bmc.h" ABC_NAMESPACE_IMPL_START @@ -33,6 +34,208 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* + Synopsis [Structural analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManDeriveFlopPriorities3( Gia_Man_t * p, int fMuxCtrls ) +{ + int fDiscount = 0; + Vec_Wec_t * vLevels; + Vec_Int_t * vRes, * vLevel, * vCosts; + Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1; + int i, k, Entry, MaxEntry = 0; + Gia_ManCreateRefs(p); + // discount references + if ( fDiscount ) + { + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0)); + pData0 = Gia_Regular(pData0); + pData1 = Gia_Regular(pData1); + p->pRefs[Gia_ObjId(p, pCtrl)]--; + if ( pData0 == pData1 ) + p->pRefs[Gia_ObjId(p, pData0)]--; + } + } + // create flop costs + vCosts = Vec_IntAlloc( Gia_ManRegNum(p) ); + Gia_ManForEachRo( p, pObj, i ) + { + Vec_IntPush( vCosts, Gia_ObjRefNum(p, pObj) ); + MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) ); + //printf( "%d(%d) ", i, Gia_ObjRefNum(p, pObj) ); + } + //printf( "\n" ); + MaxEntry++; + // add costs due to MUX inputs + if ( fMuxCtrls ) + { + int fVerbose = 0; + Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pCtrl, * pData1, * pData0; + int nCtrls = 0, nDatas = 0, nBoth = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 ); + pCtrl = Gia_Regular(pCtrl); + pData1 = Gia_Regular(pData1); + pData0 = Gia_Regular(pData0); + Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 ); + Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 ); + Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 ); + } + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) ) + Vec_IntAddToEntry( vCosts, i, MaxEntry ); + //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + // Vec_IntAddToEntry( vCosts, i, MaxEntry ); + MaxEntry = 2*MaxEntry + 1; + // print out + if ( fVerbose ) + { + Gia_ManForEachRo( p, pObj, i ) + { + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) ) + nCtrls++; + if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + nDatas++; + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + nBoth++; + } + printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth ); + } + Vec_BitFree( vCtrls ); + Vec_BitFree( vDatas ); + } + // create levelized structure + vLevels = Vec_WecStart( MaxEntry ); + Vec_IntForEachEntry( vCosts, Entry, i ) + Vec_WecPush( vLevels, Entry, i ); + // collect in this order + MaxEntry = 0; + vRes = Vec_IntStart( Gia_ManRegNum(p) ); + Vec_WecForEachLevel( vLevels, vLevel, i ) + Vec_IntForEachEntry( vLevel, Entry, k ) + Vec_IntWriteEntry( vRes, Entry, MaxEntry++ ); + //printf( "%d ", Gia_ObjRefNum(p, Gia_ManCi(p, Gia_ManPiNum(p)+Entry)) ); + //printf( "\n" ); + assert( MaxEntry == Gia_ManRegNum(p) ); + Vec_WecFree( vLevels ); + Vec_IntFree( vCosts ); + ABC_FREE( p->pRefs ); +//Vec_IntPrint( vRes ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Structural analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls ) +{ + int fDiscount = 0; + Vec_Int_t * vRes = NULL; + Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1; + int MaxEntry = 0; + int i, * pPerm; + // create flop costs + Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) ); + Gia_ManCreateRefs(p); + // discount references + if ( fDiscount ) + { + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0)); + pData0 = Gia_Regular(pData0); + pData1 = Gia_Regular(pData1); + p->pRefs[Gia_ObjId(p, pCtrl)]--; + if ( pData0 == pData1 ) + p->pRefs[Gia_ObjId(p, pData0)]--; + } + } + Gia_ManForEachRo( p, pObj, i ) + { + Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) ); + MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) ); + } + MaxEntry++; + ABC_FREE( p->pRefs ); + // add costs due to MUX inputs + if ( fMuxCtrls ) + { + int fVerbose = 0; + Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pCtrl, * pData1, * pData0; + int nCtrls = 0, nDatas = 0, nBoth = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 ); + pCtrl = Gia_Regular(pCtrl); + pData1 = Gia_Regular(pData1); + pData0 = Gia_Regular(pData0); + Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 ); + Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 ); + Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 ); + } + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) ) + Vec_IntAddToEntry( vCosts, i, MaxEntry ); + //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + // Vec_IntAddToEntry( vCosts, i, MaxEntry ); + // print out + if ( fVerbose ) + { + Gia_ManForEachRo( p, pObj, i ) + { + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) ) + nCtrls++; + if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + nDatas++; + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + nBoth++; + } + printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth ); + } + Vec_BitFree( vCtrls ); + Vec_BitFree( vDatas ); + } + // create ordering based on costs + pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) ); + vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) ); + Vec_IntFree( vCosts ); + vCosts = Vec_IntInvert( vRes, -1 ); + Vec_IntFree( vRes ); +//Vec_IntPrint( vCosts ); + return vCosts; +} + +/**Function************************************************************* + Synopsis [Creates manager.] Description [] @@ -48,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; @@ -56,7 +260,15 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio if ( !p->pPars->fMonoCnf ) p->vVLits = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) ); // internal use - p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops + p->nPrioShift = Abc_Base2Log(Aig_ManRegNum(pAig)); + if ( vPrioInit ) + p->vPrio = vPrioInit; + else if ( pPars->fFlopPrio ) + p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1); + else if ( p->pPars->fNewXSim ) + p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) ); + else + p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) ); p->vLits = Vec_IntAlloc( 100 ); // array of literals p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots @@ -67,9 +279,9 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vVisits = Vec_IntAlloc( 100 ); // intermediate p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed p->vRes = Vec_IntAlloc( 100 ); // final result - p->vSuppLits= Vec_IntAlloc( 100 ); // support literals - p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) ); p->pCnfMan = Cnf_ManStart(); + // ternary simulation + p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL; // additional AIG data-members if ( pAig->pFanData == NULL ) Aig_ManFanoutStart( pAig ); @@ -108,11 +320,12 @@ 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 ) { - Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n", - p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts ); + Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Cex =%4d Start =%4d\n", + p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts ); ABC_PRTP( "SAT solving", p->tSat, p->tTotal ); ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal ); ABC_PRTP( " sat ", p->tSatSat, p->tTotal ); @@ -121,6 +334,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal ); ABC_PRTP( "Containment", p->tContain, p->tTotal ); ABC_PRTP( "CNF compute", p->tCnf, p->tTotal ); + ABC_PRTP( "Refinement ", p->tAbs, p->tTotal ); ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal ); fflush( stdout ); } @@ -150,6 +364,12 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_WecFreeP( &p->vVLits ); // CNF manager Cnf_ManStop( p->pCnfMan ); + Vec_IntFreeP( &p->vAbsFlops ); + Vec_IntFreeP( &p->vMapFf2Ppi ); + Vec_IntFreeP( &p->vMapPpi2Ff ); + // terminary simulation + if ( p->pPars->fNewXSim ) + Txs_ManStop( p->pTxs ); // internal use Vec_IntFreeP( &p->vPrio ); // priority flops Vec_IntFree( p->vLits ); // array of literals @@ -162,9 +382,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_IntFree( p->vVisits ); // intermediate Vec_IntFree( p->vCi2Rem ); // CIs to be removed Vec_IntFree( p->vRes ); // final result - Vec_IntFree( p->vSuppLits ); // support literals Vec_PtrFreeP( &p->vInfCubes ); - ABC_FREE( p->pCubeJust ); ABC_FREE( p->pTime4Outs ); if ( p->vCexes ) Vec_PtrFreeFree( p->vCexes ); @@ -197,7 +415,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++ ) @@ -206,6 +423,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) ); } @@ -215,6 +434,112 @@ 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 || !p->vMapPpi2Ff ) + 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); + if ( p->pPars->fUseSimpleRef ) + { + // rely on ternary simulation to perform refinement + Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i ) + { + assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 ); + Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 ); + nFfRefined++; + } + } + else + { + // 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, 0, 0 ); + 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 ); + p->nCexesTotal++; + p->nCexes++; + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |