abcBmc.c File Reference

#include "base/abc/abc.h"
#include "aig/ivy/ivy.h"

Include dependency graph for abcBmc.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Ivy_Man_t *	Abc_NtkIvyBefore (Abc_Ntk_t *pNtk, int fSeq, int fUseDc)
	DECLARATIONS ///.
void	Abc_NtkBmc (Abc_Ntk_t *pNtk, int nFrames, int fInit, int fVerbose)
	FUNCTION DEFINITIONS ///.

Function Documentation

Abc_NtkBmc()

void Abc_NtkBmc	(	Abc_Ntk_t *	pNtk,
		int	nFrames,
		int	fInit,
		int	fVerbose )

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file abcBmc.c.

{
    Ivy_FraigParams_t Params, * pParams = &Params; 
    Ivy_Man_t * pMan, * pFrames, * pFraig;
    Vec_Ptr_t * vMapping;
    // convert to IVY manager
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    // generate timeframes
    pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping );
    // fraig the timeframes
    Ivy_FraigParamsDefault( pParams );
    pParams->nBTLimitNode = ABC_INFINITY;
    pParams->fVerbose = 0;
    pParams->fProve = 0;
    pFraig = Ivy_FraigPerform( pFrames, pParams );
printf( "Frames have %6d nodes.  ", Ivy_ManNodeNum(pFrames) );
printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
    // report the classes
//    if ( fVerbose )
//        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
    // free stuff
    Vec_PtrFree( vMapping );
    Ivy_ManStop( pFraig );
    Ivy_ManStop( pFrames );
    Ivy_ManStop( pMan );
}

Here is the call graph for this function:

Abc_NtkIvyBefore()

ABC_NAMESPACE_IMPL_START Ivy_Man_t * Abc_NtkIvyBefore ( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )

extern

DECLARATIONS ///.

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

FileName [abcBmc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Performs bounded model check.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

DECLARATIONS ///.

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

Synopsis [Prepares the IVY package.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file abcIvy.c.

{
    Ivy_Man_t * pMan;
//timeRetime = Abc_Clock();
    assert( !Abc_NtkIsNetlist(pNtk) );
    if ( Abc_NtkIsBddLogic(pNtk) )
    {
        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
        {
            printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
            return NULL;
        }
    }
    if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
    {
        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
//        return NULL;
    }
    // print warning about choice nodes
    if ( Abc_NtkGetChoiceNum( pNtk ) )
        printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
    // convert to the AIG manager
    pMan = Abc_NtkToIvy( pNtk );
    if ( !Ivy_ManCheck( pMan ) )
    {
        printf( "AIG check has failed.\n" );
        Ivy_ManStop( pMan );
        return NULL;
    }
//    Ivy_ManPrintStats( pMan );
    if ( fSeq )
    {
        int nLatches = Abc_NtkLatchNum(pNtk);
        Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
        Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
        Vec_IntFree( vInit );
//        Ivy_ManPrintStats( pMan );
    }
//timeRetime = Abc_Clock() - timeRetime;
    return pMan;
}

Here is the call graph for this function:

Here is the caller graph for this function: