bmcMulti.c File Reference

#include "bmc.h"
#include "proof/ssw/ssw.h"
#include "misc/extra/extra.h"
#include "aig/gia/giaAig.h"
#include "aig/ioa/ioa.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Vec_Int_t *	Gia_ManProcessOutputs (Vec_Ptr_t *vCexesIn, Vec_Ptr_t *vCexesOut, Vec_Int_t *vOutMap)
	DECLARATIONS ///. More...
int	Gia_ManCountConst0PosGia (Gia_Man_t *p)
int	Gia_ManCountConst0Pos (Aig_Man_t *p)
void	Gia_ManMultiReport (Aig_Man_t *p, char *pStr, int nTotalPo, int nTotalSize, abctime clkStart)
Aig_Man_t *	Gia_ManMultiProveSyn (Aig_Man_t *p, int fVerbose, int fVeryVerbose)
Vec_Ptr_t *	Gia_ManMultiProveAig (Aig_Man_t *p, Bmc_MulPar_t *pPars)
int	Gia_ManMultiProve (Gia_Man_t *p, Bmc_MulPar_t *pPars)

Function Documentation

int Gia_ManCountConst0Pos

(

Aig_Man_t *

p

)

Definition at line 95 of file bmcMulti.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Saig_ManForEachPo( p, pObj, i )
        Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p));
    return Counter;
}

int Gia_ManCountConst0PosGia

(

Gia_Man_t *

p

)

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

Synopsis [Counts the number of constant 0 POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file bmcMulti.c.

{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    Gia_ManForEachPo( p, pObj, i )
        Counter += (Gia_ObjFaninLit0p(p, pObj) == 0);
    return Counter;
}

int Gia_ManMultiProve	(	Gia_Man_t *	p,
		Bmc_MulPar_t *	pPars
	)

Definition at line 279 of file bmcMulti.c.

{
    Aig_Man_t * pAig;
    if ( p->vSeqModelVec )
        Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
    pAig = Gia_ManToAig( p, 0 );
    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, pPars ); // deletes pAig
    assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
    return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
}

Vec_Ptr_t* Gia_ManMultiProveAig	(	Aig_Man_t *	p,
		Bmc_MulPar_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file bmcMulti.c.

{
    Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
    Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
    Vec_Int_t * vOutMap, * vLeftOver;
    Vec_Ptr_t * vCexes;
    Aig_Man_t * pTemp;
    abctime clkStart = Abc_Clock();
    abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0;
    int nTotalPo     = Saig_ManPoNum(p);
    int nTotalSize   = Aig_ManObjNum(p);
    int TimeOutLoc   = pPars->TimeOutLoc;
    int i, RetValue  = -1;
    if ( pPars->fVerbose )
        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", 
            pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
    if ( pPars->fVerbose )
        printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", 
            pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
    // create output map
    vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
    vCexes  = Vec_PtrStart( Saig_ManPoNum(p) );        // maps solved outputs into their CEXes (or markers)
    for ( i = 0; i < 1000; i++ )
    {
        int nSolved = Vec_PtrCountZero(vCexes);
        // perform SIM3
        Ssw_RarSetDefaultParams( pParsSim );
        pParsSim->fSolveAll = 1;
        pParsSim->fNotVerbose = 1;
        pParsSim->fSilent = !pPars->fVeryVerbose;
        pParsSim->TimeOut = TimeOutLoc;
        pParsSim->nRandSeed = (i * 17) % 500;
        pParsSim->nWords = 5;
        RetValue *= Ssw_RarSimulate( p, pParsSim );
        // sort outputs
        if ( p->vSeqModelVec )
        {
            vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
            if ( Vec_IntSize(vLeftOver) == 0 )
                break;
            // remove solved        
            p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
            Vec_IntFree( vLeftOver );
            Aig_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
            Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );

        // check timeout
        if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
        {
            printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
            break;
        }

        // perform BMC
        Saig_ParBmcSetDefaultParams( pParsBmc );
        pParsBmc->fSolveAll = 1;
        pParsBmc->fNotVerbose = 1;
        pParsBmc->fSilent = !pPars->fVeryVerbose;
        pParsBmc->nTimeOut = TimeOutLoc;
        pParsBmc->nTimeOutOne = pPars->TimePerOut;
        RetValue *= Saig_ManBmcScalable( p, pParsBmc );
        if ( pPars->fVeryVerbose )
            Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", 
                Saig_ManPoNum(p) - Vec_PtrCountZero(p->vSeqModelVec), Saig_ManPoNum(p), pParsBmc->iFrame );
        // sort outputs
        if ( p->vSeqModelVec )
        {
            vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
            if ( Vec_IntSize(vLeftOver) == 0 )
                break;
            // remove solved        
            p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
            Vec_IntFree( vLeftOver );
            Aig_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
            Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );

        // check timeout
        if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
        {
            printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
            break;
        }

        // check gap timeout
        if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) )
        {
            printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap );
            break;
        }

        // synthesize
        if ( pPars->fUseSyn )
        {
            p = Gia_ManMultiProveSyn( pTemp = p, pPars->fVerbose, pPars->fVeryVerbose );
            Aig_ManStop( pTemp );
            if ( pPars->fVerbose )
                Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
        }

        // increase timeout
        TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
    }
    Vec_IntFree( vOutMap );
    if ( pPars->fVerbose )
        printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) );
    if ( pPars->fDumpFinal )
    {
        char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
        Ioa_WriteAiger( p, pFileName, 0, 0 );
        printf( "Final AIG was dumped into file \"%s\".\n", pFileName );
    }
    Aig_ManStop( p );
    return vCexes;
}

Aig_Man_t* Gia_ManMultiProveSyn	(	Aig_Man_t *	p,
		int	fVerbose,
		int	fVeryVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file bmcMulti.c.

{
    Aig_Man_t * pAig;
    Gia_Man_t * pGia, * pTemp;
    pGia = Gia_ManFromAig( p );
    pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0, 0 );
    Gia_ManStop( pTemp );
    pAig = Gia_ManToAig( pGia, 0 );
    Gia_ManStop( pGia );
    return pAig;
}

void Gia_ManMultiReport	(	Aig_Man_t *	p,
		char *	pStr,
		int	nTotalPo,
		int	nTotalSize,
		abctime	clkStart
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file bmcMulti.c.

{
    printf( "%3s : ", pStr );
    printf( "PI =%6d  ", Saig_ManPiNum(p) );
    printf( "PO =%6d  ", Saig_ManPoNum(p) );
    printf( "FF =%7d  ", Saig_ManRegNum(p) );
    printf( "ND =%7d  ", Aig_ManNodeNum(p) );
    printf( "Solved =%7d (%5.1f %%)  ", nTotalPo-Saig_ManPoNum(p), 100.0*(nTotalPo-Saig_ManPoNum(p))/Abc_MaxInt(1, nTotalPo) );
    printf( "Size   =%7d (%5.1f %%)  ", Aig_ManObjNum(p),          100.0*Aig_ManObjNum(p)/Abc_MaxInt(1, nTotalSize) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
}

ABC_NAMESPACE_IMPL_START Vec_Int_t* Gia_ManProcessOutputs	(	Vec_Ptr_t *	vCexesIn,
		Vec_Ptr_t *	vCexesOut,
		Vec_Int_t *	vOutMap
	)

DECLARATIONS ///.

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

FileName [bmcMulti.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Proving multi-output properties.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Divides outputs into solved and unsolved.]

Description [Return array of unsolved outputs to extract into a new AIG. Updates the resulting CEXes (vCexesOut) and current output map (vOutMap).]

SideEffects []

SeeAlso []

Definition at line 50 of file bmcMulti.c.

{
    Abc_Cex_t * pCex; 
    Vec_Int_t * vLeftOver;
    int i, iOut;
    assert( Vec_PtrSize(vCexesIn) == Vec_IntSize(vOutMap) );
    vLeftOver = Vec_IntAlloc( Vec_PtrSize(vCexesIn) );
    Vec_IntForEachEntry( vOutMap, iOut, i )
    {
        assert( Vec_PtrEntry(vCexesOut, iOut) == NULL );
        pCex = (Abc_Cex_t *)Vec_PtrEntry( vCexesIn, i );
        if ( pCex ) // found a CEX for output iOut
        {
            Vec_PtrWriteEntry( vCexesIn, i, NULL );
            Vec_PtrWriteEntry( vCexesOut, iOut, pCex );
        }
        else // still unsolved
        {
            Vec_IntWriteEntry( vOutMap, Vec_IntSize(vLeftOver), iOut );
            Vec_IntPush( vLeftOver, i );
        }
    }
    Vec_IntShrink( vOutMap, Vec_IntSize(vLeftOver) );
    return vLeftOver;
}