pdrMan.c

Go to the documentation of this file.

 
#include "pdrInt.h"
#include "sat/bmc/bmc.h"
 
ABC_NAMESPACE_IMPL_START
 



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;
}

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;
}

Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
{
    Pdr_Man_t * p;
    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;
    p->pOrder   = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
    p->vActVars = Vec_IntAlloc( 256 );
    if ( !p->pPars->fMonoCnf )
        p->vVLits   = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
    // internal use
    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
    p->vCiVals  = Vec_IntAlloc( 100 );  // cone leaf values
    p->vCoVals  = Vec_IntAlloc( 100 );  // cone root values
    p->vNodes   = Vec_IntAlloc( 100 );  // cone nodes
    p->vUndo    = Vec_IntAlloc( 100 );  // cone undos
    p->vVisits  = Vec_IntAlloc( 100 );  // intermediate
    p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
    p->vRes     = Vec_IntAlloc( 100 );  // final result
    p->pCnfMan  = Cnf_ManStart();
    // ternary simulation
    p->pTxs3    = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
    // additional AIG data-members
    if ( pAig->pFanData == NULL )
        Aig_ManFanoutStart( pAig );
    if ( pAig->pTerSimData == NULL )
        pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
    // time spent on each outputs
    if ( pPars->nTimeOutOne )
    {
        int i;
        p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
        for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
            p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
    }
    if ( pPars->fSolveAll )
    {
        p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
        p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
        Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
    }
    return p;
}

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%%)  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 );
        ABC_PRTP( "Generalize ", p->tGeneral,   p->tTotal );
        ABC_PRTP( "Push clause", p->tPush,      p->tTotal );
        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 );
    }
//    Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
    Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
        sat_solver_delete( pSat );
    Vec_PtrFree( p->vSolvers );
    Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
        Pdr_SetDeref( pCla );
    Vec_VecFree( p->vClauses );
    Pdr_QueueStop( p );
    ABC_FREE( p->pOrder );
    Vec_IntFree( p->vActVars );
    // static CNF
    Cnf_DataFree( p->pCnf1 );
    Vec_IntFreeP( &p->vVar2Reg );
    // dynamic CNF
    Cnf_DataFree( p->pCnf2 );
    if ( p->pvId2Vars )
    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
        ABC_FREE( p->pvId2Vars[i].pArray );
    ABC_FREE( p->pvId2Vars );
//    Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
    for ( i = 0; i < Vec_PtrSize(&p->vVar2Ids); i++ )
        Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, i) );
    ABC_FREE( p->vVar2Ids.pArray );
    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 )
        Txs3_ManStop( p->pTxs3 );
    // internal use
    Vec_IntFreeP( &p->vPrio   );  // priority flops
    Vec_IntFree( p->vLits     );  // array of literals
    Vec_IntFree( p->vCiObjs   );  // cone leaves
    Vec_IntFree( p->vCoObjs   );  // cone roots
    Vec_IntFree( p->vCiVals   );  // cone leaf values
    Vec_IntFree( p->vCoVals   );  // cone root values
    Vec_IntFree( p->vNodes    );  // cone nodes
    Vec_IntFree( p->vUndo     );  // cone undos
    Vec_IntFree( p->vVisits   );  // intermediate
    Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
    Vec_IntFree( p->vRes      );  // final result
    Vec_PtrFreeP( &p->vInfCubes );
    ABC_FREE( p->pTime4Outs );
    if ( p->vCexes )
        Vec_PtrFreeFree( p->vCexes );
    // additional AIG data-members
    if ( p->pAig->pFanData != NULL )
        Aig_ManFanoutStop( p->pAig );
    if ( p->pAig->pTerSimData != NULL )
        ABC_FREE( p->pAig->pTerSimData );
    ABC_FREE( p );
}

Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
{
    Abc_Cex_t * pCex;
    Pdr_Obl_t * pObl;
    int i, f, Lit, nFrames = 0;
    // count the number of frames
    for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
        nFrames++;
    // create the counter-example
    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), 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 ( Abc_LitIsCompl(Lit) )
                continue;
            if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
                continue;
            assert( Abc_Lit2Var(Lit) < pCex->nPis );
            Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
        }
    assert( f == nFrames );
    if ( !Saig_ManVerifyCex(p->pAig, pCex) )
        printf( "CEX for output %d is not valid.\n", p->iOutCur );
    return pCex;
}

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 ( Abc_Lit2Var(Lit) < nPis ) // PI literal
                continue;
            Flop = Abc_Lit2Var(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 ( Abc_LitIsCompl(Lit) )
                    continue;
                if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
                else
                {
                    int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(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;
}

 
 
ABC_NAMESPACE_IMPL_END