demo.c File Reference

#include <stdio.h>
#include <time.h>

Include dependency graph for demo.c:

Go to the source code of this file.

Typedefs
typedef struct Abc_Frame_t_	Abc_Frame_t

Functions
void	Abc_Start ()
	DECLARATIONS ///.
void	Abc_Stop ()
Abc_Frame_t *	Abc_FrameGetGlobalFrame ()
int	Cmd_CommandExecute (Abc_Frame_t *pAbc, const char *sCommand)
int	main (int argc, char *argv[])
	FUNCTION DEFINITIONS ///.

Typedef Documentation

Abc_Frame_t

typedef struct Abc_Frame_t_ Abc_Frame_t

Definition at line 42 of file demo.c.

Function Documentation

Abc_FrameGetGlobalFrame()

Abc_Frame_t * Abc_FrameGetGlobalFrame

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 643 of file mainFrame.c.

{
    if ( s_GlobalFrame == 0 )
    {
        // start the framework
        s_GlobalFrame = Abc_FrameAllocate();
        // perform initializations
        Abc_FrameInit( s_GlobalFrame );
    }
    return s_GlobalFrame;
}

Here is the caller graph for this function:

Abc_Start()

void Abc_Start

(

)

DECLARATIONS ///.

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

FileName [demo.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [ABC as a static library.]

Synopsis [A demo program illustrating the use of ABC as a static library.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

demo.c,v 1.00 2005/11/14 00:00:00 alanmi Exp

]

INCLUDES ///.

FUNCTION DECLARATIONS ///.

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

FileName [main.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The main package.]

Synopsis [Here everything starts.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Initialization procedure for the library project.]

Description [Note that when Abc_Start() is run in a static library project, it does not load the resource file by default. As a result, ABC is not set up the same way, as when it is run on a command line. For example, some error messages while parsing files will not be produced, and intermediate networks will not be checked for consistancy. One possibility is to load the resource file after Abc_Start() as follows: Abc_UtilsSource( Abc_FrameGetGlobalFrame() );]

SideEffects []

SeeAlso []

Definition at line 52 of file mainLib.c.

{
    Abc_Frame_t * pAbc;
    // added to detect memory leaks:
#if defined(_DEBUG) && defined(_MSC_VER) 
    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif
    // start the glocal frame
    pAbc = Abc_FrameGetGlobalFrame();
    // source the resource file
//    Abc_UtilsSource( pAbc );
}

Here is the caller graph for this function:

Abc_Stop()

void Abc_Stop

(

)

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

Synopsis [Deallocation procedure for the library project.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file mainLib.c.

{
    Abc_Frame_t * pAbc;
    pAbc = Abc_FrameGetGlobalFrame();
    // perform uninitializations
    Abc_FrameEnd( pAbc );
    // stop the framework
    Abc_FrameDeallocate( pAbc );
}

Here is the caller graph for this function:

Cmd_CommandExecute()

int Cmd_CommandExecute	(	Abc_Frame_t *	pAbc,
		const char *	sCommand )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file cmdApi.c.

{
    int fStatus = 0, argc, loop;
    const char * sCommandNext;
    char **argv;
 
    if ( !pAbc->fAutoexac && !pAbc->fSource ) 
        Cmd_HistoryAddCommand(pAbc, sCommand);
    sCommandNext = sCommand;
    do 
    {
        if ( sCommandNext[0] == '#' && Cmd_CommandHandleSpecial( pAbc, sCommandNext ) )
            break;
        sCommandNext = CmdSplitLine( pAbc, sCommandNext, &argc, &argv );
        loop = 0;
        fStatus = CmdApplyAlias( pAbc, &argc, &argv, &loop );
        if ( fStatus == 0 ) 
            fStatus = CmdCommandDispatch( pAbc, &argc, &argv );
        CmdFreeArgv( argc, argv );
    } 
    while ( fStatus == 0 && *sCommandNext != '\0' );
    return fStatus;
}

Here is the caller graph for this function:

main()

int main	(	int	argc,
		char *	argv[] )

FUNCTION DEFINITIONS ///.

GLOBAL VARIABLES ///.

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

Synopsis [The main() procedure.]

Description [This procedure compiles into a stand-alone program for DAG-aware rewriting of the AIGs. A BLIF or PLA file to be considered for rewriting should be given as a command-line argument. Implementation of the rewriting is inspired by the paper: Per Bjesse, Arne Boralv, "DAG-aware circuit compression for formal verification", Proc. ICCAD 2004.]

SideEffects []

SeeAlso []

Definition at line 73 of file demo.c.

{
    // parameters
    int fUseResyn2  = 0;
    int fPrintStats = 1;
    int fVerify     = 1;
    // variables
    Abc_Frame_t * pAbc;
    char * pFileName;
    char Command[1000];
    clock_t clkRead, clkResyn, clkVer, clk;

    // get the input file name
    if ( argc != 2 )
    {
        printf( "Wrong number of command-line arguments.\n" );
        return 1;
    }
    pFileName = argv[1];

    // start the ABC framework
    Abc_Start();
    pAbc = Abc_FrameGetGlobalFrame();
 
clk = clock();
    // read the file
    sprintf( Command, "read %s", pFileName );
    if ( Cmd_CommandExecute( pAbc, Command ) )
    {
        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
        return 1;
    }

    // balance
    sprintf( Command, "balance" );
    if ( Cmd_CommandExecute( pAbc, Command ) )
    {
        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
        return 1;
    }
clkRead = clock() - clk;

    // print stats
    if ( fPrintStats )
    {
        sprintf( Command, "print_stats" );
        if ( Cmd_CommandExecute( pAbc, Command ) )
        {
            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
            return 1;
        }
    }
 
clk = clock();
    // synthesize
    if ( fUseResyn2 )
    {
        sprintf( Command, "balance; rewrite -l; refactor -l; balance; rewrite -l; rewrite -lz; balance; refactor -lz; rewrite -lz; balance" );
        if ( Cmd_CommandExecute( pAbc, Command ) )
        {
            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
            return 1;
        }
    }
    else
    {
        sprintf( Command, "balance; rewrite -l; rewrite -lz; balance; rewrite -lz; balance" );
        if ( Cmd_CommandExecute( pAbc, Command ) )
        {
            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
            return 1;
        }
    }
clkResyn = clock() - clk;

    // print stats
    if ( fPrintStats )
    {
        sprintf( Command, "print_stats" );
        if ( Cmd_CommandExecute( pAbc, Command ) )
        {
            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
            return 1;
        }
    }

    // write the result in blif
    sprintf( Command, "write_blif result.blif" );
    if ( Cmd_CommandExecute( pAbc, Command ) )
    {
        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
        return 1;
    }

    // perform verification
clk = clock();
    if ( fVerify )
    {
        sprintf( Command, "cec %s result.blif", pFileName );
        if ( Cmd_CommandExecute( pAbc, Command ) )
        {
            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
            return 1;
        }
    }
clkVer = clock() - clk;
 
    printf( "Reading = %6.2f sec   ",     (float)(clkRead)/(float)(CLOCKS_PER_SEC) );
    printf( "Rewriting = %6.2f sec   ",   (float)(clkResyn)/(float)(CLOCKS_PER_SEC) );
    printf( "Verification = %6.2f sec\n", (float)(clkVer)/(float)(CLOCKS_PER_SEC) );

    // stop the ABC framework
    Abc_Stop();
    return 0;
}

Here is the call graph for this function: