cecProve.c File Reference

#include <math.h>
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "sat/bmc/bmc.h"
#include "proof/pdr/pdr.h"
#include "proof/cec/cec.h"
#include "proof/ssw/ssw.h"

Include dependency graph for cecProve.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Ssw_RarSimulateGia (Gia_Man_t *p, Ssw_RarPars_t *pPars)
	DECLARATIONS ///.
int	Bmcg_ManPerform (Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
int	Cec_GiaProveTest (Gia_Man_t *p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent)

Function Documentation

Bmcg_ManPerform()

int Bmcg_ManPerform ( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 445 of file bmcBmcG.c.

{ 
    pPars->nProcs = 1;
    return Bmcg_ManPerformOne( pGia, pPars );
}

Here is the call graph for this function:

Cec_GiaProveTest()

int Cec_GiaProveTest	(	Gia_Man_t *	p,
		int	nProcs,
		int	nTimeOut,
		int	nTimeOut2,
		int	nTimeOut3,
		int	fVerbose,
		int	fVeryVerbose,
		int	fSilent )

Definition at line 54 of file cecProve.c.

{ return -1; }

Ssw_RarSimulateGia()

ABC_NAMESPACE_IMPL_START int Ssw_RarSimulateGia ( Gia_Man_t * p, Ssw_RarPars_t * pPars )

extern

DECLARATIONS ///.

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

FileName [cecSplit.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Cofactoring for combinational miters.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

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

Synopsis [Perform sequential simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1188 of file sswRarity.c.

{
    Aig_Man_t * pAig;
    int RetValue;
    if ( pPars->fUseFfGrouping )
    {
        Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p), 10 );
        Gia_Man_t * pTemp = Gia_ManDupPermFlopGap( p, vPerm );
        Vec_IntFree( vPerm );
        pAig = Gia_ManToAigSimple( pTemp );
        Gia_ManStop( pTemp );
    }
    else
        pAig = Gia_ManToAigSimple( p );
    RetValue = Ssw_RarSimulate( pAig, pPars );
    // save counter-example
    Abc_CexFree( p->pCexSeq );
    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
    Aig_ManStop( pAig );
    return RetValue;
}

Here is the call graph for this function: