bmc.h File Reference

#include "aig/saig/saig.h"
#include "aig/gia/gia.h"

Include dependency graph for bmc.h:

Go to the source code of this file.

Classes
struct	Bmc_EsPar_t_
struct	Saig_ParBmc_t_
struct	Bmc_AndPar_t_
struct	Bmc_BCorePar_t_
struct	Bmc_MulPar_t_
struct	Bmc_ParFf_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Bmc_EsPar_t_	Bmc_EsPar_t
	INCLUDES ///.
typedef struct Unr_Man_t_	Unr_Man_t
typedef struct Saig_ParBmc_t_	Saig_ParBmc_t
typedef struct Bmc_AndPar_t_	Bmc_AndPar_t
typedef struct Bmc_BCorePar_t_	Bmc_BCorePar_t
typedef struct Bmc_MulPar_t_	Bmc_MulPar_t
typedef struct Bmc_ParFf_t_	Bmc_ParFf_t

Functions
void	Bmc_ManBCorePerform (Gia_Man_t *pGia, Bmc_BCorePar_t *pPars)
	MACRO DEFINITIONS ///.
int	Saig_ManBmcSimple (Aig_Man_t *pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int *piFrame, int nCofFanLit, int fUseSatoko)
int	Saig_BmcPerform (Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent, int fUseSatoko)
void	Saig_ParBmcSetDefaultParams (Saig_ParBmc_t *p)
int	Saig_ManBmcScalable (Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
int	Gia_ManBmcPerform (Gia_Man_t *p, Bmc_AndPar_t *pPars)
Abc_Cex_t *	Bmc_CexCareExtendToObjects (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
	DECLARATIONS ///.
Abc_Cex_t *	Bmc_CexCareMinimize (Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
Abc_Cex_t *	Bmc_CexCareMinimizeAig (Gia_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
int	Bmc_CexCareVerify (Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
int	Bmc_CexCareVerifyAnyPo (Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Abc_Cex_t *	Bmc_CexCareSatBasedMinimize (Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int fHighEffort, int fCheck, int fVerbose)
Abc_Cex_t *	Bmc_CexCareSatBasedMinimizeAig (Gia_Man_t *p, Abc_Cex_t *pCex, int fHighEffort, int fVerbose)
Gia_Man_t *	Bmc_GiaTargetStates (Gia_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose)
Aig_Man_t *	Bmc_AigTargetStates (Aig_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose)
Abc_Cex_t *	Saig_ManCexMinPerform (Aig_Man_t *pAig, Abc_Cex_t *pCex)
void	Bmc_CexPrint (Abc_Cex_t *pCex, int nRealPis, int fVerbose)
int	Bmc_CexVerify (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
int	Bmc_CexVerifyAnyPo (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
void	Bmc_PerformICheck (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose)
Vec_Int_t *	Bmc_PerformISearch (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose)
Unr_Man_t *	Unr_ManUnrollStart (Gia_Man_t *pGia, int fVerbose)
Gia_Man_t *	Unr_ManUnrollFrame (Unr_Man_t *p, int f)
void	Unr_ManFree (Unr_Man_t *p)

Typedef Documentation

Bmc_AndPar_t

typedef struct Bmc_AndPar_t_ Bmc_AndPar_t

Definition at line 143 of file bmc.h.

Bmc_BCorePar_t

typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t

Definition at line 169 of file bmc.h.

Bmc_EsPar_t

typedef typedefABC_NAMESPACE_HEADER_START struct Bmc_EsPar_t_ Bmc_EsPar_t

INCLUDES ///.

CFile****************************************************************

FileName [bmc.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

bmc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 47 of file bmc.h.

Bmc_MulPar_t

typedef struct Bmc_MulPar_t_ Bmc_MulPar_t

Definition at line 180 of file bmc.h.

Bmc_ParFf_t

typedef struct Bmc_ParFf_t_ Bmc_ParFf_t

Definition at line 194 of file bmc.h.

Saig_ParBmc_t

typedef struct Saig_ParBmc_t_ Saig_ParBmc_t

Definition at line 105 of file bmc.h.

Unr_Man_t

typedef struct Unr_Man_t_ Unr_Man_t

Definition at line 103 of file bmc.h.

Function Documentation

Bmc_AigTargetStates()

Aig_Man_t * Bmc_AigTargetStates ( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose )

extern

Function*************************************************************

Synopsis [Generate AIG for target bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file bmcCexCut.c.

{
    Aig_Man_t * pAig;
    Gia_Man_t * pGia, * pRes;
    pGia = Gia_ManFromAigSimple( p );
    if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) )
    {
        Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); 
        Gia_ManStop( pGia );
        return NULL;
    }
    pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose );
    Gia_ManStop( pGia );
    pAig = Gia_ManToAigSimple( pRes );
    Gia_ManStop( pRes );
    return pAig;
}

Here is the call graph for this function:

Bmc_CexCareExtendToObjects()

Abc_Cex_t * Bmc_CexCareExtendToObjects ( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcCexCare.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Computing care set of the counter-example.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

bmcCexCare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Takes CEX and its care-set. Returns care-set of all objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file bmcCexCare.c.

{
    Abc_Cex_t * pNew;
    Gia_Obj_t * pObj;
    int i, k;
    assert( pCex->nPis == pCexCare->nPis );
    assert( pCex->nRegs == pCexCare->nRegs );
    assert( pCex->nBits == pCexCare->nBits );
    // start the counter-example
    pNew = Abc_CexAlloc( pCex->nRegs, Gia_ManObjNum(p), pCex->iFrame + 1 );
    pNew->iFrame = pCex->iFrame;
    pNew->iPo    = pCex->iPo;
    // initialize terminary simulation
    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
    Gia_ManForEachRi( p, pObj, k )
        Gia_ObjTerSimSet0( pObj );
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Gia_ManForEachPi( p, pObj, k )
        {
            if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
                Gia_ObjTerSimSetX( pObj );
            else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
                Gia_ObjTerSimSet1( pObj );
            else
                Gia_ObjTerSimSet0( pObj );
        }
        Gia_ManForEachRo( p, pObj, k )
            Gia_ObjTerSimRo( p, pObj );
        Gia_ManForEachAnd( p, pObj, k )
            Gia_ObjTerSimAnd( pObj );
        Gia_ManForEachCo( p, pObj, k )
            Gia_ObjTerSimCo( pObj );
        // add cares to the exdended counter-example
        Gia_ManForEachObj( p, pObj, k )
            if ( !Gia_ObjTerSimGetX(pObj) )
                Abc_InfoSetBit( pNew->pData, pNew->nRegs + pNew->nPis * i + k );
    }
    pObj = Gia_ManPo( p, pCex->iPo );
    assert( Gia_ObjTerSimGet1(pObj) );
    return pNew;
}

Here is the call graph for this function:

Bmc_CexCareMinimize()

Abc_Cex_t * Bmc_CexCareMinimize ( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )

extern

Definition at line 426 of file bmcCexCare.c.

{
    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
    Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, nTryCexes, fCheck, fVerbose );
    Gia_ManStop( pGia );
    return pCexMin;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexCareMinimizeAig()

Abc_Cex_t * Bmc_CexCareMinimizeAig ( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )

extern

Definition at line 254 of file bmcCexCare.c.

{
    //int nTryCexes = 4; // belongs to range [1;4]
    Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
    int k, f, i, nOnesBest, nOnesCur, Counter = 0;
    Vec_Int_t * vPriosIn, * vPriosFf;
    if ( pCex->nPis != Gia_ManPiNum(p) )
    {
        printf( "Given CEX does to have same number of inputs as the AIG.\n" );
        return NULL;
    }
    if ( pCex->nRegs != Gia_ManRegNum(p) )
    {
        printf( "Given CEX does to have same number of flops as the AIG.\n" );
        return NULL;
    }
    if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) )
    {
        printf( "Given CEX has PO whose index is out of range for the AIG.\n" );
        return NULL;
    }
    assert( pCex->nPis == Gia_ManPiNum(p) );
    assert( pCex->nRegs == Gia_ManRegNum(p) );
    assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) );
    if ( fVerbose )
    {
        printf( "Original :    " );
        Bmc_CexPrint( pCex, nRealPis, 0 );
    }
    vPriosIn = Vec_IntAlloc( pCex->nPis  * (pCex->iFrame + 1) );
    vPriosFf = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
    for ( k = 0; k < nTryCexes; k++ )
    {
        Counter = 0;
        Vec_IntFill( vPriosIn, pCex->nPis * (pCex->iFrame + 1), 0 );
/*
        if ( k == 0 )
        {
            for ( f = 0; f <= pCex->iFrame; f++ )
                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = 0; f <= pCex->iFrame; f++ )
                for ( i = 0; i < nRealPis; i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else if ( k == 1 )
        {
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = 0; i < nRealPis; i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else if ( k == 2 )
        {
            for ( f = 0; f <= pCex->iFrame; f++ )
                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = 0; f <= pCex->iFrame; f++ )
                for ( i = nRealPis - 1; i >= 0; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else if ( k == 3 )
        {
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = nRealPis - 1; i >= 0; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else assert( 0 );
*/
        if ( k == 0 )
        {
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = nRealPis - 1; i >= 0; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else if ( k == 1 )
        {
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = 0; i < nRealPis; i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else if ( k == 2 )
        {
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = nRealPis - 1; i >= 0; i-- )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else if ( k == 3 )
        {
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
            for ( f = pCex->iFrame; f >= 0; f-- )
                for ( i = 0; i < nRealPis; i++ )
                    Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
        }
        else assert( 0 );
 
        assert( Counter == pCex->nPis * (pCex->iFrame + 1) );
        Bmc_CexCarePropagateFwd( p, pCex, vPriosIn, vPriosFf );
        assert( Vec_IntSize(vPriosFf) == pCex->nRegs * (pCex->iFrame + 1) );
        if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) )
        {
            printf( "Counter-example is invalid.\n" );
            Vec_IntFree( vPriosIn );
            Vec_IntFree( vPriosFf );
            return NULL;
        }
        pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPriosIn, vPriosFf );
        if ( fVerbose )
        {
            if ( k == 0 )
                printf( "PI-  PPI-:    " );
            else if ( k == 1 )
                printf( "PI+  PPI-:    " );
            else if ( k == 2 )
                printf( "PI-  PPI+:    " );
            else if ( k == 3 )
                printf( "PI+  PPI+:    " );
            else assert( 0 );
            Bmc_CexPrint( pCexMin[k], nRealPis, 0 );
        }
    }
    Vec_IntFree( vPriosIn );
    Vec_IntFree( vPriosFf );
    // select the best one
    pCexBest  = pCexMin[0];
    nOnesBest = Abc_CexCountOnes(pCexMin[0]);
    for ( k = 1; k < nTryCexes; k++ )
    {
        if ( pCexMin[k] == NULL )
            continue;
        nOnesCur = Abc_CexCountOnes(pCexMin[k]);
        if ( nOnesBest > nOnesCur )
        {
            nOnesBest = nOnesCur;
            pCexBest  = pCexMin[k];
        }
    }
    if ( fVerbose )
    {
        //Abc_Cex_t * pTotal = Bmc_CexCareTotal( pCexMin, nTryCexes );
        printf( "Final    :    " );
        Bmc_CexPrint( pCexBest, nRealPis, 0 );
        //printf( "Total    :    " );
        //Bmc_CexPrint( pTotal, nRealPis, 0 );
        //Abc_CexFreeP( &pTotal );
    }
    for ( k = 0; k < nTryCexes; k++ )
        if ( pCexMin[k] && pCexBest != pCexMin[k] )
            Abc_CexFreeP( &pCexMin[k] );
    // verify and return
    if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
        printf( "Counter-example verification has failed.\n" );
    else if ( fCheck ) 
        printf( "Counter-example verification succeeded.\n" );
    return pCexBest;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexCareSatBasedMinimize()

Abc_Cex_t * Bmc_CexCareSatBasedMinimize ( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose )

extern

Definition at line 433 of file bmcCexCare.c.

{
    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
    Abc_Cex_t * pCexMin = Bmc_CexCareSatBasedMinimizeAig( pGia, pCex, fHighEffort, fVerbose );
    if ( pCexMin == NULL )
    {
        Gia_ManStop( pGia );
        return NULL;
    }
    // unfortunately, cannot verify - ternary simulation does not work
    Gia_ManStop( pGia );
    return pCexMin;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexCareSatBasedMinimizeAig()

Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig ( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose )

extern

Definition at line 517 of file giaCex.c.

{
    abctime clk = Abc_Clock();
    int n, i, iFirstVar, iLit, status;
    Vec_Int_t * vLits = NULL, * vTemp;
    sat_solver * pSat;
    Cnf_Dat_t * pCnf;
    int nFinal, * pFinal;
    Abc_Cex_t * pCexBest = NULL; 
    int CountBest = 0;
    Gia_Man_t * pFrames;
 
    // CEX minimization
    clk = Abc_Clock();
    pCexBest = Bmc_CexCareMinimizeAig( p, Gia_ManPiNum(p), pCex, 1, 1, fVerbose );
    for ( i = pCexBest->nRegs; i < pCexBest->nBits; i++ )
        CountBest += Abc_InfoHasBit(pCexBest->pData, i);
    if ( fVerbose )
    {
        printf( "Care bits = %d. ", CountBest );
        Abc_PrintTime( 1, "Non-SAT-based CEX minimization", Abc_Clock() - clk );
    }
 
    // SAT instance
    clk = Abc_Clock();
    pFrames = Gia_ManFramesForCexMin( p, pCex->iFrame + 1 );
    pCnf = (Cnf_Dat_t*)Mf_ManGenerateCnf( pFrames, 8, 0, 0, 0, 0 );
    iFirstVar = pCnf->nVars - (pCex->iFrame+1) * pCex->nPis;
    pSat = (sat_solver*)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    iLit = Abc_Var2Lit( 1, 1 );
    status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
    assert( status );
    // create literals
    vTemp = Vec_IntAlloc( 100 );
    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
        Vec_IntPush( vTemp, Abc_Var2Lit(iFirstVar + i - pCex->nRegs, !Abc_InfoHasBit(pCex->pData, i)) );
    if ( fVerbose )
    Abc_PrintTime( 1, "Constructing SAT solver", Abc_Clock() - clk );
 
    for ( n = 0; n < 2; n++ )
    {
        Vec_IntFreeP( &vLits );
 
        vLits = Vec_IntDup( vTemp );
        if ( n ) Vec_IntReverseOrder( vLits );
 
        // SAT-based minimization
        clk = Abc_Clock();
        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
        nFinal = sat_solver_final( pSat, &pFinal );
        if ( fVerbose )
        {
            printf( "Status %s   Selected %5d assumptions out of %5d.  ", status == l_False ? "OK ":"BUG", nFinal, Vec_IntSize(vLits) );
            Abc_PrintTime( 1, "Analyze_final", Abc_Clock() - clk );
        }
        if ( CountBest > nFinal )
        {
            CountBest = nFinal;
            ABC_FREE( pCexBest );
            pCexBest = Bmc_CexCareDeriveCex( pCex, iFirstVar, pFinal, nFinal );
        }
        if ( !fHighEffort )
            continue;
 
        // SAT-based minimization
        clk = Abc_Clock();
        nFinal = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits), 0 );
        if ( fVerbose )
        {
            printf( "Status %s   Selected %5d assumptions out of %5d.  ", status == l_False ? "OK ":"BUG", nFinal, Vec_IntSize(vLits) );
            Abc_PrintTime( 1, "LEXUNSAT     ", Abc_Clock() - clk );
        }
        if ( CountBest > nFinal )
        {
            CountBest = nFinal;
            ABC_FREE( pCexBest );
            pCexBest = Bmc_CexCareDeriveCex( pCex, iFirstVar, Vec_IntArray(vLits), nFinal );
        }
    }
    if ( fVerbose )
    {
        printf( "Final    :    " );
        Bmc_CexPrint( pCexBest, pCexBest->nPis, 0 );
    }
    // cleanup
    Vec_IntFreeP( &vLits );
    Vec_IntFreeP( &vTemp );
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Gia_ManStop( pFrames );
    return pCexBest;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexCareVerify()

int Bmc_CexCareVerify ( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )

extern

Function*************************************************************

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 458 of file bmcCexCare.c.

{
    int result;
    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
    if ( fVerbose )
    {
        printf( "Original :    " );
        Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
        printf( "Minimized:    " );
        Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
    }
    result = Bmc_CexVerify( pGia, pCex, pCexMin );
    if ( !result )
        printf( "Counter-example verification has failed.\n" );
    else 
        printf( "Counter-example verification succeeded.\n" );
    Gia_ManStop( pGia );
    return result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexCareVerifyAnyPo()

int Bmc_CexCareVerifyAnyPo ( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )

extern

Function*************************************************************

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 497 of file bmcCexCare.c.

{
    int iPo;
    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
    if ( fVerbose )
    {
        printf( "Original :    " );
        Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
        printf( "Minimized:    " );
        Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
    }
    iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin );
    if ( iPo < 0 )
        printf( "Counter-example verification has failed.\n" );
    else
        printf( "Counter-example verification succeeded.\n" );
    Gia_ManStop( pGia );
    return iPo;
}

Here is the call graph for this function:

Bmc_CexPrint()

void Bmc_CexPrint ( Abc_Cex_t * pCex, int nRealPis, int fVerbose )

extern

Function*************************************************************

Synopsis [Prints one counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file bmcCexTools.c.

{
    int i, k, Count, iBit = pCex->nRegs;
    Abc_CexPrintStatsInputs( pCex, nRealPis );
    if ( !fVerbose )
        return;
 
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Count = 0;
        printf( "%3d : ", i );
        for ( k = 0; k < nRealPis; k++ )
        {
            Count += Abc_InfoHasBit(pCex->pData, iBit);
            printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
        }
        printf( " %3d ", Count );
        Count = 0;
        for (      ; k < pCex->nPis; k++ )
        {
            Count += Abc_InfoHasBit(pCex->pData, iBit);
            printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
        }
        printf( " %3d\n", Count );
    }
    assert( iBit == pCex->nBits );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexVerify()

int Bmc_CexVerify ( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )

extern

Function*************************************************************

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file bmcCexTools.c.

{
    Gia_Obj_t * pObj;
    int i, k;
//    assert( pCex->nRegs > 0 );
//    assert( pCexCare->nRegs == 0 );
    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
    Gia_ManForEachRi( p, pObj, k )
        Gia_ObjTerSimSet0( pObj );
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Gia_ManForEachPi( p, pObj, k )
        {
            if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
                Gia_ObjTerSimSetX( pObj );
            else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
                Gia_ObjTerSimSet1( pObj );
            else
                Gia_ObjTerSimSet0( pObj );
        }
        Gia_ManForEachRo( p, pObj, k )
            Gia_ObjTerSimRo( p, pObj );
        Gia_ManForEachAnd( p, pObj, k )
            Gia_ObjTerSimAnd( pObj );
        Gia_ManForEachCo( p, pObj, k )
            Gia_ObjTerSimCo( pObj );
    }
    pObj = Gia_ManPo( p, pCex->iPo );
    return Gia_ObjTerSimGet1(pObj);
}

Here is the caller graph for this function:

Bmc_CexVerifyAnyPo()

int Bmc_CexVerifyAnyPo ( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )

extern

Function*************************************************************

Synopsis [Verifies the care set of the counter-example for an arbitrary PO.]

Description []

SideEffects []

SeeAlso []

Definition at line 388 of file bmcCexTools.c.

{
    Gia_Obj_t * pObj;
    int i, k;
//    assert( pCex->nRegs > 0 );
//    assert( pCexCare->nRegs == 0 );
    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
    Gia_ManForEachRi( p, pObj, k )
        Gia_ObjTerSimSet0( pObj );
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Gia_ManForEachPi( p, pObj, k )
        {
            if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
                Gia_ObjTerSimSetX( pObj );
            else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
                Gia_ObjTerSimSet1( pObj );
            else
                Gia_ObjTerSimSet0( pObj );
        }
        Gia_ManForEachRo( p, pObj, k )
            Gia_ObjTerSimRo( p, pObj );
        Gia_ManForEachAnd( p, pObj, k )
            Gia_ObjTerSimAnd( pObj );
        Gia_ManForEachCo( p, pObj, k )
            Gia_ObjTerSimCo( pObj );
    }
    for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++)
    {
        pObj = Gia_ManPo( p, i );
        if (Gia_ObjTerSimGet1(pObj))
            return i;
    }
    return -1;
}

Here is the caller graph for this function:

Bmc_GiaTargetStates()

Gia_Man_t * Bmc_GiaTargetStates ( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose )

extern

Function*************************************************************

Synopsis [Generate GIA for target bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 461 of file bmcCexCut.c.

{
    Gia_Man_t * pNew, * pTemp;
    Vec_Bit_t * vInitNew;
 
    if ( iFrBeg < 0 )
        { printf( "Starting frame is less than 0.\n" ); return NULL; }
    if ( iFrEnd < 0 )
        { printf( "Stopping frame is less than 0.\n" ); return NULL; }
    if ( iFrBeg > pCex->iFrame )
        { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
    if ( iFrEnd > pCex->iFrame )
        { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
    if ( iFrBeg > iFrEnd )
        { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
    assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
    assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
    assert( iFrBeg < iFrEnd );
 
    if ( fUseOne )
        pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
    else if ( fAllFrames )
        pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd );
    else 
        pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
 
    if ( !fCombOnly )
    {
        // create new GIA
        pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); 
        Gia_ManStop( pTemp );
 
        // create new initial state
        pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
        Gia_ManStop( pTemp );
    }
 
    Vec_BitFree( vInitNew );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_ManBCorePerform()

void Bmc_ManBCorePerform ( Gia_Man_t * p, Bmc_BCorePar_t * pPars )

extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file bmcBCore.c.

{
    clock_t clk = clock();
    Intp_Man_t * pManProof;
    Vec_Int_t * vVarMap, * vCore;
    sat_solver * pSat;
    FILE * pFile;
    void * pSatCnf; 
    int RetValue;
    // create SAT solver
    pSat = sat_solver_new();
    sat_solver_store_alloc( pSat ); 
    sat_solver_setnvars( pSat, 1000 );
    sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
    vVarMap = Bmc_ManBCoreCollect( p, pPars->iFrame, pPars->iOutput, pSat );
    sat_solver_store_mark_roots( pSat ); 
    // create pivot variables
    if ( pPars->pFilePivots )
    {
        Vec_Int_t * vPivots = Bmc_ManBCoreCollectPivots(p, pPars->pFilePivots, vVarMap);
        sat_solver_set_pivot_variables( pSat, Vec_IntArray(vPivots), Vec_IntSize(vPivots) );
        Vec_IntReleaseArray( vPivots );
        Vec_IntFree( vPivots );
    }
    // solve the problem
    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( RetValue == l_Undef )
    {
        Vec_IntFree( vVarMap );
        sat_solver_delete( pSat );
        printf( "Timeout of conflict limit is reached.\n" );
        return;
    }
    if ( RetValue == l_True )
    {
        Vec_IntFree( vVarMap );
        sat_solver_delete( pSat );
        printf( "The BMC problem is SAT.\n" );
        return;
    }
    if ( pPars->fVerbose )
    {
        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
        Abc_PrintTime( 1, "Time", clock() - clk );
    }
    assert( RetValue == l_False );
    pSatCnf = sat_solver_store_release( pSat ); 
//    Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" );
    // derive the UNSAT core
    clk = clock();
    pManProof = Intp_ManAlloc();
    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 1, pPars->fVerbose );
    Intp_ManFree( pManProof );
    if ( pPars->fVerbose )
    {
        printf( "UNSAT core contains %d (out of %d) learned clauses.   ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) );
        Abc_PrintTime( 1, "Time", clock() - clk );
    }
    // write the problem
    Vec_IntSort( vCore, 0 );
    pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout;
    Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap );
    if ( pFile != stdout )
        fclose( pFile );
    // cleanup
    Sto_ManFree( (Sto_Man_t *)pSatCnf );
    Vec_IntFree( vVarMap );
    Vec_IntFree( vCore );
    sat_solver_delete( pSat );
}

Here is the call graph for this function:

Bmc_PerformICheck()

void Bmc_PerformICheck ( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file bmcICheck.c.

{
    int fUseOldCnf = 0;
    Gia_Man_t * pMiter, * pTemp;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Vec_Int_t * vLits, * vUsed;
    int i, status, Lit;
    int nLitsUsed, nLits, * pLits;
    abctime clkStart = Abc_Clock();
    assert( nFramesMax > 0 );
    assert( Gia_ManRegNum(p) > 0 );
 
    if ( fVerbose )
    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
 
    // create miter
    pTemp = Gia_ManDup( p );
    pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
    Gia_ManStop( pTemp );
    assert( Gia_ManPoNum(pMiter)  == 2 * Gia_ManPoNum(p) );
    assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
    // derive CNF
    if ( fUseOldCnf )
        pCnf = Cnf_DeriveGiaRemapped( pMiter );
    else
    {
        pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
        Gia_ManStop( pTemp );
        pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
    }
 
    // collect positive literals
    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
    for ( i = 0; i < Gia_ManRegNum(p); i++ )
        Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) );
 
    // iteratively compute a minimal M-inductive set of next-state functions
    nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits);
    vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
    while ( 1 )
    {
        int fChanges = 0;
        // derive SAT solver        
        pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
//        sat_solver_bookmark( pSat );
        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_Undef )
        {
            printf( "Timeout reached after %d seconds.\n", nTimeOut );
            break;
        }
        if ( status == l_True )
        {
            printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
            break;
        }
        assert( status == l_False );
        // call analize_final
        nLits = sat_solver_final( pSat, &pLits );
        // mark used literals
        Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
        for ( i = 0; i < nLits; i++ )
            Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );
 
        // check if there are any positive unused
        Vec_IntForEachEntry( vLits, Lit, i )
        {
            assert( i == Abc_Lit2Var(Lit) );
            if ( Abc_LitIsCompl(Lit) )
                continue;
            if ( Vec_IntEntry(vUsed, i) )
                continue;
            // positive literal became unused
            Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
            nLitsUsed--;
            fChanges = 1;
        }
        // report the results
        if ( fVerbose )
        printf( "M =%4d :  AIG =%8d.  SAT vars =%8d.  SAT conf =%8d.  S =%6d. (%6.2f %%)  ",
            nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), 
            Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), 
            sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
        if ( fVerbose )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
        // count the number of negative literals
        sat_solver_delete( pSat );
        if ( !fChanges || fEmpty )
            break;
//        break;
//        sat_solver_rollback( pSat );
    }
    Cnf_DataFree( pCnf );
    Gia_ManStop( pMiter );
    Vec_IntFree( vLits );
    Vec_IntFree( vUsed );
}

Here is the call graph for this function:

Bmc_PerformISearch()

Vec_Int_t * Bmc_PerformISearch ( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose )

extern

Definition at line 489 of file bmcICheck.c.

{
    Vec_Int_t * vLits, * vFlops;
    int i, f;
    if ( fVerbose )
    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops with %s %s flop order:\n",
        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p), fReverse ? "reverse":"direct", fBackTopo ? "backward":"natural" );
    fflush( stdout );
 
    // collect positive literals
    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
    for ( i = 0; i < Gia_ManRegNum(p); i++ )
        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
 
    for ( f = 1; f <= nFramesMax; f++ )
        if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fBackTopo, fVerbose, vLits ) )
        {
            Vec_IntFree( vLits );
            return NULL;
        }
 
    // dump the numbers of the flops
    if ( fDump )
    {
        int nLitsUsed = 0;
        for ( i = 0; i < Gia_ManRegNum(p); i++ )
            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
                nLitsUsed++;
        printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
        for ( i = 0; i < Gia_ManRegNum(p); i++ )
            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
                printf( "%d ", i );
        printf( "\n" );
    }       
    // save flop indexes
    vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
    for ( i = 0; i < Gia_ManRegNum(p); i++ )
        if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
            Vec_IntPush( vFlops, 1 );
        else
            Vec_IntPush( vFlops, 0 );
    Vec_IntFree( vLits );
    return vFlops;
}

Here is the call graph for this function:

Gia_ManBmcPerform()

int Gia_ManBmcPerform ( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1066 of file bmcBmcAnd.c.

{
    abctime TimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
    if ( pPars->nFramesAdd == 0 )
        return Gia_ManBmcPerformInt( pGia, pPars );
    // iterate over the engine until we read the global timeout
    assert( pPars->nTimeOut >= 0 );
    while ( 1 )
    {
        if ( TimeToStop && TimeToStop < Abc_Clock() )
            return -1;
        if ( Gia_ManBmcPerformInt( pGia, pPars ) == 0 )
            return 0;
        // set the new runtime limit
        if ( pPars->nTimeOut )
        {
            pPars->nTimeOut = Abc_MinInt( pPars->nTimeOut-1, (int)((TimeToStop - Abc_Clock()) / CLOCKS_PER_SEC) );
            if ( pPars->nTimeOut <= 0 )
                return -1;
        }
        else
            return -1;
        // set the new frames limit
        pPars->nFramesAdd *= 2;
    }
    return -1;
}

Here is the call graph for this function:

Saig_BmcPerform()

int Saig_BmcPerform ( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent, int fUseSatoko )

extern

Function*************************************************************

Synopsis [Performs BMC with the given parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 811 of file bmcBmc2.c.

{
    Saig_Bmc_t * p;
    Aig_Man_t * pNew;
    Cnf_Dat_t * pCnf;
    int nOutsSolved = 0;
    int Iter, RetValue = -1;
    abctime nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    abctime clk = Abc_Clock(), clk2, clkTotal = Abc_Clock();
    int Status = -1;
/*
    Vec_Ptr_t * vSimInfo;
    vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
    Abs_ManFreeAray( vSimInfo );
*/
    if ( fVerbose )
    {
        printf( "Running \"bmc2\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
            nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
    } 
    nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose, fUseSatoko );
    // set runtime limit
    if ( nTimeOut )
    {
        if ( p->pSat2 )
            satoko_set_runtime_limit( p->pSat2, nTimeToStop );
        else
            sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
    }
    for ( Iter = 0; ; Iter++ )
    {
        clk2 = Abc_Clock();
        // add new logic interval to frames
        Saig_BmcInterval( p );
//        Saig_BmcAddTargetsAsPos( p );
        if ( Vec_PtrSize(p->vTargets) == 0 )
            break;
        // convert logic slice into new AIG
        pNew = Saig_BmcIntervalToAig( p );
//printf( "StitchVars = %d.\n", p->nStitchVars );
        // derive CNF for the new AIG
        pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) );
        Cnf_DataLift( pCnf, p->nSatVars );
        p->nSatVars += pCnf->nVars;
        // add this CNF to the solver
        Saig_BmcLoadCnf( p, pCnf );
        Cnf_DataFree( pCnf );
        Aig_ManStop( pNew );
        // solve the targets
        RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
        if ( fVerbose )
        {
            printf( "%4d : F =%5d. O =%4d.  And =%8d. Var =%8d. Conf =%7d. ", 
                Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, 
                p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2) );   
            printf( "%4.0f MB",     4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
            printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
            printf( "\n" );
            fflush( stdout );
        }
        if ( RetValue != l_False )
            break;
        // check the timeout
        if ( nTimeOut && Abc_Clock() > nTimeToStop )
        {
            if ( !fSilent )
                printf( "Reached timeout (%d seconds).\n",  nTimeOut );
            if ( piFrames )
                *piFrames = p->iFrameLast-1;
            Saig_BmcManStop( p );
            return Status;
        }
    }
    if ( RetValue == l_True )
    {
        assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
        if ( !fSilent )
            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", 
                p->iOutputFail, p->pAig->pName, p->iFrameFail );
        Status = 0;
        if ( piFrames )
            *piFrames = p->iFrameFail - 1;
    }
    else // if ( RetValue == l_False || RetValue == l_Undef )
    {
        if ( !fSilent )
            Abc_Print( 1, "No output failed in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
        if ( piFrames )
        {
            if ( p->iOutputLast > 0 )
                *piFrames = p->iFramePrev - 2;
            else
                *piFrames = p->iFramePrev - 1;
        }
    }
    if ( !fSilent )
    {
        if ( fVerbOverwrite )
        {
            ABC_PRTr( "Time", Abc_Clock() - clk );
        }
        else
        {
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( RetValue != l_True )
        {
            if ( p->iFrameLast >= p->nFramesMax )
                printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
            else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
                printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
            else if ( nTimeOut && Abc_Clock() > nTimeToStop )
                printf( "Reached timeout (%d seconds).\n", nTimeOut );
            else
                printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
        }
    }
    Saig_BmcManStop( p );
    fflush( stdout );
    return Status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcScalable()

int Saig_ManBmcScalable ( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )

extern

Function*************************************************************

Synopsis [Bounded model checking engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 1461 of file bmcBmc3.c.

{
    Gia_ManBmc_t * p;
    Aig_Obj_t * pObj;
    Abc_Cex_t * pCexNew, * pCexNew0;
    FILE * pLogFile = NULL;
    unsigned * pInfo;
    int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
    int i, f, k, Lit, status;
    abctime clk, clk2, clkSatRun, clkOther = 0, clkTotal = Abc_Clock();
    abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
    abctime nTimeToStopNG, nTimeToStop;
    if ( pPars->pLogFileName )
        pLogFile = fopen( pPars->pLogFileName, "wb" );
    if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
        pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
    if ( pPars->nTimeOutOne && !pPars->fSolveAll )
        pPars->nTimeOutOne = 0;
    nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    nTimeToStop   = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
    // create BMC manager
    p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose );
    p->pPars = pPars;
    if ( p->pSat )
    {
        p->pSat->nLearntStart = p->pPars->nLearnedStart;
        p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
        p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
        p->pSat->nLearntMax   = p->pSat->nLearntStart;
        p->pSat->fNoRestarts  = p->pPars->fNoRestarts;
        p->pSat->RunId        = p->pPars->RunId;
        p->pSat->pFuncStop    = p->pPars->pFuncStop;
    }
    else if ( p->pSat3 )
    {
//        satoko_set_runid(p->pSat3, p->pPars->RunId);
//        satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop);
    }
    else
    {
        satoko_set_runid(p->pSat2, p->pPars->RunId);
        satoko_set_stop_func(p->pSat2, p->pPars->pFuncStop);
    }
    if ( pPars->fSolveAll && p->vCexes == NULL )
        p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d.\n",// Sect =%3d.\n", 
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums );//, Vec_VecSize(p->vSects) );
        Abc_Print( 1, "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
            pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
    } 
    pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
    // set runtime limit
    if ( nTimeToStop )
    {
        if ( p->pSat2 )
            satoko_set_runtime_limit( p->pSat2, nTimeToStop );
        else if ( p->pSat3 )
            bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
        else
            sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
    }
    // perform frames
    Aig_ManRandom( 1 );
    pPars->timeLastSolved = Abc_Clock();
    for ( f = 0; f < pPars->nFramesMax; f++ )
    {
        // stop BMC after exploring all reachable states
        if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
        {
            Abc_Print( 1, "Stopping BMC because all 2^%d reachable states are visited.\n", Aig_ManRegNum(pAig) );
            if ( p->pPars->fUseBridge )
                Saig_ManForEachPo( pAig, pObj, i )
                    if ( !(p->vCexes && Vec_PtrEntry(p->vCexes, i)) && !(p->pTime4Outs && p->pTime4Outs[i] == 0) ) // not SAT and not timed out
                        Gia_ManToBridgeResult( stdout, 1, NULL, i );
            RetValue = pPars->nFailOuts ? 0 : 1;
            goto finish;
        }
        // stop BMC if all targets are solved
        if ( pPars->fSolveAll && pPars->nFailOuts + pPars->nDropOuts >= Saig_ManPoNum(pAig) )
        {
            Abc_Print( 1, "Stopping BMC because all targets are disproved or timed out.\n" );
            RetValue = pPars->nFailOuts ? 0 : 1;
            goto finish;
        }
        // consider the next timeframe
        if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
            pPars->iFrame = f-1;
        // map nodes of this section
        Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
        Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
/*
        // cannot remove mapping of frame values for any timeframes
        // because with constant propagation they may be needed arbitrarily far
        if ( f > 2*Vec_VecSize(p->vSects) )
        {
            int iFrameOld = f - 2*Vec_VecSize( p->vSects );
            void * pMemory = Vec_IntReleaseArray( Vec_PtrEntry(p->vId2Var, iFrameOld) );
            ABC_FREE( pMemory );
        } 
*/
        // prepare some nodes
        Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
        Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
        Saig_ManForEachPi( pAig, pObj, i )
            Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
        if ( f == 0 )
        {
            Saig_ManForEachLo( p->pAig, pObj, i )
            {
                Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
                Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
            }
        }
        if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
            continue;
        // create CNF upfront
        if ( pPars->fSolveAll )
        {
            Saig_ManForEachPo( pAig, pObj, i )
            {
                if ( i >= Saig_ManPoNum(pAig) )
                    break;
                // check for timeout
                if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
                {
                    Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  pPars->nTimeOutGap );
                    goto finish;
                }
                if ( nTimeToStop && Abc_Clock() > nTimeToStop )
                {
                    if ( !pPars->fSilent )
                        Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                    goto finish;
                }
                // skip solved outputs
                if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
                    continue;
                // skip output whose time has run out
                if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
                    continue;
                // add constraints for this output
clk2 = Abc_Clock();
                Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2;
            }
        }
        // solve SAT
        clk = Abc_Clock(); 
        Saig_ManForEachPo( pAig, pObj, i )
        {
            if ( i >= Saig_ManPoNum(pAig) )
                break;
            // check for timeout
            if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
            {
                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  pPars->nTimeOutGap );
                goto finish;
            }
            if ( nTimeToStop && Abc_Clock() > nTimeToStop )
            {
                if ( !pPars->fSilent )
                    Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                goto finish;
            }
            if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
            {
                if ( !pPars->fSilent )
                    Abc_Print( 1, "Bmc3 got callbacks.\n" );
                goto finish;
            }
            // skip solved outputs
            if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
                continue;
            // skip output whose time has run out
            if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
                continue;
            // add constraints for this output
clk2 = Abc_Clock();
            Lit = Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2;
            // solve this output
            fUnfinished = 0;
            if ( p->pSat ) sat_solver_compress( p->pSat );
            if ( p->pTime4Outs )
            {
                assert( p->pTime4Outs[i] > 0 );
                clkOne = Abc_Clock();
                if ( p->pSat2 )
                    satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
                else if ( p->pSat3 )
                    bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() );
                else
                    sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
            }
clk2 = Abc_Clock();
            status = Saig_ManCallSolver( p, Lit );
clkSatRun = Abc_Clock() - clk2;
            if ( pLogFile )
                fprintf( pLogFile, "Frame %5d  Output %5d  Time(ms) %8d %8d\n", f, i, 
                    Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC),
                    Lit < 2 ? 0 : Abc_MaxInt(0, Abc_MinInt(pPars->nTimeOutOne, pPars->nTimeOutOne - (int)((p->pTime4Outs[i] - clkSatRun) * 1000 / CLOCKS_PER_SEC))) );
            if ( p->pTime4Outs )
            {
                abctime timeSince = Abc_Clock() - clkOne;
                assert( p->pTime4Outs[i] > 0 );
                p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
                if ( p->pTime4Outs[i] == 0 && status != l_True )
                    pPars->nDropOuts++;
            }
            if ( status == l_False )
            {
nTimeUnsat += clkSatRun;
                if ( Lit != 0 )
                {
                    // add final unit clause
                    Lit = lit_neg( Lit );
                    if ( p->pSat2 )
                        status = satoko_add_clause( p->pSat2, &Lit, 1 );
                    else if ( p->pSat3 )
                        status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 );
                    else
                        status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                    assert( status );
                    // add learned units
                    if ( p->pSat )
                    {
                        for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
                        {
                            Lit = veci_begin(&p->pSat->unit_lits)[k];
                            status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                            assert( status );
                        }
                        veci_resize(&p->pSat->unit_lits, 0);
                        // propagate units
                        sat_solver_compress( p->pSat );
                    }
                }
                if ( p->pPars->fUseBridge )
                    Gia_ManReportProgress( stdout, i, f );
            }
            else if ( status == l_True )
            {
nTimeSat += clkSatRun;
                RetValue = 0;
                fFirst = 0;
                if ( !pPars->fSolveAll )
                {
                    if ( pPars->fVerbose )
                    {
                        Abc_Print( 1, "%4d %s : ", f,  fUnfinished ? "-" : "+" );
                        Abc_Print( 1, "Var =%8.0f. ",  (double)p->nSatVars );
                        Abc_Print( 1, "Cla =%9.0f. ",  (double)(p->pSat ? p->pSat->stats.clauses   : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3)   : satoko_clausenum(p->pSat2)) );
                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
//                        Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
//                        Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
//                        ABC_PRT( "Time", Abc_Clock() - clk );
                        Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
                        Abc_Print( 1, "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
                        Abc_Print( 1, "%4.0f MB",      1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
                        Abc_Print( 1, "%9.2f sec  ",   (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
//                        Abc_Print( 1, "\n" );
//                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
//                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
//                        Abc_Print( 1, "S =%6d. ", p->nBufNum );
//                        Abc_Print( 1, "D =%6d. ", p->nDupNum );
                        Abc_Print( 1, "\n" );
                        fflush( stdout );
                    }
                    ABC_FREE( pAig->pSeqModel );
                    pAig->pSeqModel = Saig_ManGenerateCex( p, f, i );
                    goto finish;
                }
                pPars->nFailOuts++;
                if ( !pPars->fNotVerbose )
                    Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                        nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                if ( p->vCexes == NULL )
                    p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                pCexNew0 = NULL;
                if ( p->pPars->fUseBridge )
                {
                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                    //Abc_CexFree( pCexNew );
                    pCexNew0 = pCexNew; 
                    pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
                }
                Vec_PtrWriteEntry( p->vCexes, i, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); 
                if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
                {
                    Abc_CexFreeP( &pCexNew0 );
                    Abc_Print( 1, "Quitting due to callback on fail.\n" );
                    goto finish;
                }
                // reset the timeout
                pPars->timeLastSolved = Abc_Clock();
                nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
                if ( nTimeToStop )
                {
                    if ( p->pSat2 )
                        satoko_set_runtime_limit( p->pSat2, nTimeToStop );
                    else if ( p->pSat3 )
                        bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
                    else
                        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
                }
 
                // check if other outputs failed under the same counter-example
                Saig_ManForEachPo( pAig, pObj, k )
                {
                    Abc_Cex_t * pCexDup;
                    if ( k >= Saig_ManPoNum(pAig) )
                        break;
                    // skip solved outputs
                    if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) )
                        continue;
                    // check if this output is solved
                    Lit = Saig_ManBmcCreateCnf( p, pObj, f );
                    if ( p->pSat2 )
                    {
                        if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                            continue;
                    }
                    else if ( p->pSat3 )
                    {
                        if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                            continue;
                    }
                    else
                    {
                        if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                            continue;
                    }
                    // write entry
                    pPars->nFailOuts++;
                    if ( !pPars->fNotVerbose )
                        Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                            nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                    // report to the bridge
                    if ( p->pPars->fUseBridge )
                    {
                        // set the output number
                        pCexNew0->iPo = k;
                        Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
                    }
                    // remember solved output
                    //Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
                    pCexDup = Abc_CexDup(pCexNew, Saig_ManRegNum(pAig));
                    pCexDup->iPo = k;
                    Vec_PtrWriteEntry( p->vCexes, k, pCexDup );
                }
                Abc_CexFreeP( &pCexNew0 );
                Abc_CexFree( pCexNew );
            }
            else 
            {
nTimeUndec += clkSatRun;
                assert( status == l_Undef );
                if ( pPars->nFramesJump )
                {
                    pPars->nConfLimit = pPars->nConfLimitJump;
                    nJumpFrame = f + pPars->nFramesJump;
                    fUnfinished = 1;
                    break;
                }
                if ( p->pTime4Outs == NULL )
                    goto finish;
            }
        }
        if ( pPars->fVerbose ) 
        {
            if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
            {
                fFirst = 0;
//                Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
            }
            Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
            Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
//            Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
            Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses   : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3)   : satoko_clausenum(p->pSat2))   );
            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
//            Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
//            Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
            Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
            if ( pPars->fSolveAll )
                Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
            if ( pPars->nTimeOutOne )
                Abc_Print( 1, "T/O =%4d. ", pPars->nDropOuts );
//            ABC_PRT( "Time", Abc_Clock() - clk );
//            Abc_Print( 1, "%4.0f MB",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
            Abc_Print( 1, "%4.0f MB",     4.0*(f+1)*p->nObjNums /(1<<20) );
            Abc_Print( 1, "%4.0f MB",     1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
//            Abc_Print( 1, " %6d %6d ",   p->nLitUsed, p->nLitUseless );
            Abc_Print( 1, "%9.2f sec ",   1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
//            Abc_Print( 1, "\n" );
//            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
//            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
//            Abc_Print( 1, "Simples = %6d. ", p->nBufNum );
//            Abc_Print( 1, "Dups = %6d. ", p->nDupNum );
            Abc_Print( 1, "\n" );
            fflush( stdout );
        }
    }
    // consider the next timeframe
    if ( nJumpFrame && pPars->nStart == 0 )
        pPars->iFrame = nJumpFrame - pPars->nFramesJump;
    else if ( RetValue == -1 && pPars->nStart == 0 )
        pPars->iFrame = f-1;
//ABC_PRT( "CNF generation runtime", clkOther );
finish:
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Runtime:  " );
        Abc_Print( 1, "CNF = %.1f sec (%.1f %%)  ",   1.0*clkOther/CLOCKS_PER_SEC,   100.0*clkOther/(Abc_Clock() - clkTotal)   );
        Abc_Print( 1, "UNSAT = %.1f sec (%.1f %%)  ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
        Abc_Print( 1, "SAT = %.1f sec (%.1f %%)  ",   1.0*nTimeSat/CLOCKS_PER_SEC,   100.0*nTimeSat/(Abc_Clock() - clkTotal)   );
        Abc_Print( 1, "UNDEC = %.1f sec (%.1f %%)",   1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
        Abc_Print( 1, "\n" );
    }
    Saig_Bmc3ManStop( p );
    fflush( stdout );
    if ( pLogFile )
        fclose( pLogFile );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManBmcSimple()

int Saig_ManBmcSimple ( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit, int fUseSatoko )

extern

Function*************************************************************

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file bmcBmc.c.

{
    extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit );
    sat_solver * pSat = NULL;
    satoko_t * pSat2 = NULL;
    Cnf_Dat_t * pCnf;
    Aig_Man_t * pFrames, * pAigTemp;
    Aig_Obj_t * pObj;
    int status, Lit, i, RetValue = -1;
    abctime clk;
 
    // derive the timeframes
    clk = Abc_Clock();
    if ( nCofFanLit )
    {
        pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
        if ( pFrames == NULL )
            return -1;
    }
    else if ( nSizeMax > 0 )
    {
        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
        nFrames = Aig_ManCoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManCoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
    }
    else
        pFrames = Saig_ManFramesBmc( pAig, nFrames );
    if ( piFrame )
        *piFrame = nFrames;
    if ( fVerbose )
    {
        printf( "Running \"bmc\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
            nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames), 
            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
        ABC_PRT( "Time", Abc_Clock() - clk );
        fflush( stdout );
    }
    // rewrite the timeframes
    if ( fRewrite )
    {
        clk = Abc_Clock();
//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
        Aig_ManStop( pAigTemp );
        if ( fVerbose )
        {
            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
            ABC_PRT( "Time", Abc_Clock() - clk );
            fflush( stdout );
        }
    }
    // create the SAT solver
    clk = Abc_Clock();
    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );  
//if ( s_fInterrupt )
//return -1;
    if ( fUseSatoko )
    {
        satoko_opts_t opts;
        satoko_default_opts(&opts);
        opts.conf_limit = nConfLimit;
        pSat2 = satoko_create();  
        satoko_configure(pSat2, &opts);
        satoko_setnvars(pSat2, pCnf->nVars);
        for ( i = 0; i < pCnf->nClauses; i++ )
            if ( !satoko_add_clause( pSat2, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
                assert( 0 );
    }
    else
    {
        pSat = sat_solver_new();
        sat_solver_setnvars( pSat, pCnf->nVars );
        for ( i = 0; i < pCnf->nClauses; i++ )
            if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
                assert( 0 );
    }
    if ( fVerbose )
    {
        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
        ABC_PRT( "Time", Abc_Clock() - clk );
        fflush( stdout );
    }
    status = pSat ? sat_solver_simplify(pSat) : 1;
    if ( status == 0 )
    {
        if ( fVerbose )
        {
            printf( "The BMC problem is trivially UNSAT\n" );
            fflush( stdout );
        }
    }
    else
    {
        abctime clkPart = Abc_Clock();
        Aig_ManForEachCo( pFrames, pObj, i )
        {
            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
            if ( fVerbose )
            {
                printf( "Solving output %2d of frame %3d ... \r", 
                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
            }
            clk = Abc_Clock();
            if ( pSat2 )
                status = satoko_solve_assumptions_limit( pSat2, &Lit, 1, nConfLimit );
            else
                status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
            {
                printf( "Solved %2d outputs of frame %3d.  ", 
                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                printf( "Conf =%8.0f. Imp =%11.0f. ", 
                    (double)(pSat ? pSat->stats.conflicts    : satoko_conflictnum(pSat2)), 
                    (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2)->n_propagations) );
                ABC_PRT( "T", Abc_Clock() - clkPart );
                clkPart = Abc_Clock();
                fflush( stdout );
            }
            if ( status == l_False )
            {
/*
                Lit = lit_neg( Lit );
                RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
                assert( RetValue );
                if ( pSat->qtail != pSat->qhead )
                {
                    RetValue = sat_solver_simplify(pSat);
                    assert( RetValue );
                }
*/
            }
            else if ( status == l_True )
            {
                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
                int * pModel = pSat2 ? Sat2_SolverGetModel(pSat2, vCiIds->pArray, vCiIds->nSize) : Sat_SolverGetModel(pSat, vCiIds->pArray, vCiIds->nSize);
                pModel[Aig_ManCiNum(pFrames)] = pObj->Id;
                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
                ABC_FREE( pModel );
                Vec_IntFree( vCiIds );
 
                if ( piFrame )
                    *piFrame = i / Saig_ManPoNum(pAig);
                RetValue = 0;
                break;
            }
            else
            {
                if ( piFrame )
                    *piFrame = i / Saig_ManPoNum(pAig);
                RetValue = -1;
                break;
            }
        }
    }
    if ( pSat )  sat_solver_delete( pSat );
    if ( pSat2 ) satoko_destroy( pSat2 );
    Cnf_DataFree( pCnf );
    Aig_ManStop( pFrames );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManCexMinPerform()

Abc_Cex_t * Saig_ManCexMinPerform ( Aig_Man_t * pAig, Abc_Cex_t * pCex )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 547 of file bmcCexMin1.c.

{
    int fReasonPi = 0;
 
    Abc_Cex_t * pCexMin = NULL;
    Aig_Man_t * pManNew = NULL;
    Vec_Vec_t * vFrameReas;
    vFrameReas = Saig_ManCexMinComputeReason( pAig, pCex, fReasonPi );
    printf( "Reason size = %d.  Ave = %d.\n", Vec_VecSizeSize(vFrameReas), Vec_VecSizeSize(vFrameReas)/(pCex->iFrame + 1) );
 
    // try reducing the frames
    if ( !fReasonPi )
    {
        char * pFileName = "aigcube.aig";
        pManNew = Saig_ManCexMinDupWithCubes( pAig, vFrameReas );
        Ioa_WriteAiger( pManNew, pFileName, 0, 0 );
        Aig_ManStop( pManNew );
        printf( "Intermediate AIG is written into file \"%s\".\n", pFileName );
    }
 
    // find reduced counter-example
    Vec_VecFree( vFrameReas );
    return pCexMin;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ParBmcSetDefaultParams()

void Saig_ParBmcSetDefaultParams ( Saig_ParBmc_t * p )

extern

Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 1334 of file bmcBmc3.c.

{
    memset( p, 0, sizeof(Saig_ParBmc_t) );
    p->nStart         =     0;    // maximum number of timeframes 
    p->nFramesMax     =     0;    // maximum number of timeframes 
    p->nConfLimit     =     0;    // maximum number of conflicts at a node
    p->nConfLimitJump =     0;    // maximum number of conflicts after jumping
    p->nFramesJump    =     0;    // the number of tiemframes to jump
    p->nTimeOut       =     0;    // approximate timeout in seconds
    p->nTimeOutGap    =     0;    // time since the last CEX found
    p->nPisAbstract   =     0;    // the number of PIs to abstract
    p->fSolveAll      =     0;    // stops on the first SAT instance
    p->fDropSatOuts   =     0;    // replace sat outputs by constant 0
    p->nLearnedStart  = 10000;    // starting learned clause limit
    p->nLearnedDelta  =  2000;    // delta of learned clause limit
    p->nLearnedPerce  =    80;    // ratio of learned clause limit
    p->fVerbose       =     0;    // verbose 
    p->fNotVerbose    =     0;    // skip line-by-line print-out 
    p->iFrame         =    -1;    // explored up to this frame
    p->nFailOuts      =     0;    // the number of failed outputs
    p->nDropOuts      =     0;    // the number of timed out outputs
    p->timeLastSolved =     0;    // time when the last one was solved
}

Here is the call graph for this function:

Here is the caller graph for this function:

Unr_ManFree()

void Unr_ManFree ( Unr_Man_t * p )

extern

Definition at line 340 of file bmcUnroll.c.

{
    Gia_ManStop( p->pFrames );
    // intermediate data
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vOrderLim );
    Vec_IntFreeP( &p->vTents );
    Vec_IntFreeP( &p->vRanks );
    // unrolling data
    Vec_IntFreeP( &p->vObjLim );
    Vec_IntFreeP( &p->vCiMap );
    Vec_IntFreeP( &p->vCoMap );
    Vec_IntFreeP( &p->vPiLits );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Unr_ManUnrollFrame()

Gia_Man_t * Unr_ManUnrollFrame ( Unr_Man_t * p, int f )

extern

Definition at line 379 of file bmcUnroll.c.

{
    int i, iLit, iLit0, iLit1, hStart;
    for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
        Vec_IntPush( p->vPiLits, Gia_ManAppendCi(p->pFrames) );
    hStart = Vec_IntEntry( p->vObjLim, Abc_MaxInt(0, Vec_IntSize(p->vObjLim)-1-f) );
    while ( p->pObjs + hStart < p->pEnd )
    {
        Unr_Obj_t * pUnrObj = Unr_ManObj( p, hStart );
        if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 != UNR_DIFF_NULL ) // AND node
        {
            iLit0 = Unr_ManFanin0Value( p, pUnrObj );
            iLit1 = Unr_ManFanin1Value( p, pUnrObj );
            iLit  = Gia_ManHashAnd( p->pFrames, iLit0, iLit1 );
            Unr_ManObjSetValue( pUnrObj, iLit );
        }
        else if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 == UNR_DIFF_NULL ) // PO/RI/RO
        {
            iLit  = Unr_ManFanin0Value( p, pUnrObj );
            Unr_ManObjSetValue( pUnrObj, iLit );
            if ( pUnrObj->fItIsPo )
                Gia_ManAppendCo( p->pFrames, iLit );
        }
        else // PI  (pUnrObj->hFan0 is CioId; pUnrObj->hFan1 is tent)
        {
            assert( pUnrObj->fItIsPi && f >= (int)pUnrObj->hFan1 );
            iLit = Vec_IntEntry( p->vPiLits, Gia_ManPiNum(p->pGia) * (f - pUnrObj->hFan1) + pUnrObj->hFan0 );
            Unr_ManObjSetValue( pUnrObj, iLit );
        }
        hStart += Unr_ObjSize( pUnrObj );
    }
    assert( p->pObjs + hStart == p->pEnd );
    assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(p->pGia) );
    return p->pFrames;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Unr_ManUnrollStart()

Unr_Man_t * Unr_ManUnrollStart ( Gia_Man_t * pGia, int fVerbose )

extern

Function*************************************************************

Synopsis [Perform smart unrolling.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file bmcUnroll.c.

{
    int i, iHandle;
    Unr_Man_t * p;
    p = Unr_ManAlloc( pGia );
    Unr_ManSetup( p, fVerbose );
    for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ )
        if ( (iHandle = Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i)) != -1 )
            Unr_ManObjSetValue( Unr_ManObj(p, iHandle), 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function: