mainInt.h File Reference

#include "main.h"
#include "misc/tim/tim.h"
#include "map/if/if.h"
#include "aig/aig/aig.h"
#include "aig/gia/gia.h"
#include "proof/ssw/ssw.h"
#include "proof/fra/fra.h"
#include "misc/vec/vecHsh.h"

Include dependency graph for mainInt.h:

Go to the source code of this file.

Classes
struct	Abc_Frame_t_
struct	Abc_FrameInitializer_t_

Macros
#define	ABC_VERSION   "UC Berkeley, ABC 1.01"
	INCLUDES ///.
#define	ABC_MAX_STR   (1<<15)

Typedefs
typedef void(*	Abc_Frame_Callback_BmcFrameDone_Func) (int frame, int po, int status)
	STRUCTURE DEFINITIONS ///.
typedef void(*	Abc_Frame_Initialization_Func) (Abc_Frame_t *pAbc)
typedef struct Abc_FrameInitializer_t_	Abc_FrameInitializer_t

Functions
ABC_DLL int	main (int argc, char *argv[])
	GLOBAL VARIABLES ///.
ABC_DLL void	Abc_FrameInit (Abc_Frame_t *pAbc)
	FUNCTION DEFINITIONS ///.
ABC_DLL void	Abc_FrameEnd (Abc_Frame_t *pAbc)
ABC_DLL void	Abc_FrameAddInitializer (Abc_FrameInitializer_t *p)
ABC_DLL Abc_Frame_t *	Abc_FrameAllocate ()
ABC_DLL void	Abc_FrameDeallocate (Abc_Frame_t *p)
ABC_DLL char *	Abc_UtilsGetVersion (Abc_Frame_t *pAbc)
	FUNCTION DEFINITIONS ///.
ABC_DLL char *	Abc_UtilsGetUsersInput (Abc_Frame_t *pAbc)
ABC_DLL void	Abc_UtilsPrintHello (Abc_Frame_t *pAbc)
ABC_DLL void	Abc_UtilsPrintUsage (Abc_Frame_t *pAbc, char *ProgName)
ABC_DLL void	Abc_UtilsSource (Abc_Frame_t *pAbc)
ABC_DLL void	Abc_FrameStoreStart (Abc_Frame_t *pAbc)
ABC_DLL void	Abc_FrameStoreStop (Abc_Frame_t *pAbc)
ABC_DLL void	Abc_FrameStoreAdd (Abc_Frame_t *pAbc, Gia_Man_t *p)
ABC_DLL void	Abc_FrameStorePrint (Abc_Frame_t *pAbc)

Macro Definition Documentation

ABC_MAX_STR

#define ABC_MAX_STR   (1<<15)

Definition at line 52 of file mainInt.h.

ABC_VERSION

#define ABC_VERSION   "UC Berkeley, ABC 1.01"

INCLUDES ///.

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

FileName [mainInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The main package.]

Synopsis [Internal declarations of the main package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp

] PARAMETERS ///

Definition at line 49 of file mainInt.h.

Typedef Documentation

Abc_Frame_Callback_BmcFrameDone_Func

typedef void(* Abc_Frame_Callback_BmcFrameDone_Func) (int frame, int po, int status)

STRUCTURE DEFINITIONS ///.

Definition at line 58 of file mainInt.h.

Abc_Frame_Initialization_Func

typedef void(* Abc_Frame_Initialization_Func) (Abc_Frame_t *pAbc)

Definition at line 173 of file mainInt.h.

Abc_FrameInitializer_t

typedef struct Abc_FrameInitializer_t_ Abc_FrameInitializer_t

Definition at line 176 of file mainInt.h.

Function Documentation

Abc_FrameAddInitializer()

ABC_DLL void Abc_FrameAddInitializer ( Abc_FrameInitializer_t * p )

extern

Definition at line 76 of file mainInit.c.

{
    if( ! s_InitializerStart )
        s_InitializerStart = p;
 
    p->next = NULL;
    p->prev = s_InitializerEnd;
 
    if ( s_InitializerEnd )
        s_InitializerEnd->next = p;
 
    s_InitializerEnd = p;
 
}

Abc_FrameAllocate()

ABC_DLL Abc_Frame_t * Abc_FrameAllocate ( )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file mainFrame.c.

{
    Abc_Frame_t * p;
    extern void define_cube_size( int n );
    extern void set_espresso_flags();
    // allocate and clean
    p = ABC_CALLOC( Abc_Frame_t, 1 );
    // get version
    p->sVersion = Abc_UtilsGetVersion( p );
    // set streams
    p->Err = stderr;
    p->Out = stdout;
    p->Hst = NULL;
    p->Status     = -1;
    p->nFrames    = -1;
    // set the starting step
    p->nSteps     =  1;
    p->fBatchMode =  0;
    // networks to be used by choice
    p->vStore = Vec_PtrAlloc( 16 );
    p->vAbcObjIds = Vec_IntAlloc( 0 );
    // initialize decomposition manager
//    define_cube_size(20);
//    set_espresso_flags();
    // initialize the trace manager
//    Abc_HManStart();
    p->vPlugInComBinPairs = Vec_PtrAlloc( 100 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameDeallocate()

ABC_DLL void Abc_FrameDeallocate ( Abc_Frame_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file mainFrame.c.

{
    extern void Rwt_ManGlobalStop();
    extern void undefine_cube_size();
//    extern void Ivy_TruthManStop();
//    Abc_HManStop();
//    undefine_cube_size();
    Rwt_ManGlobalStop();
//    Ivy_TruthManStop();
    if ( p->vAbcObjIds)  Vec_IntFree( p->vAbcObjIds );
    if ( p->vCexVec   )  Vec_PtrFreeFree( p->vCexVec );
    if ( p->vPoEquivs )  Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
    if ( p->vStatuses )  Vec_IntFree( p->vStatuses );
    if ( p->pManDec   )  Dec_ManStop( (Dec_Man_t *)p->pManDec );
#ifdef ABC_USE_CUDD
    if ( p->dd        )  Extra_StopManager( p->dd );
#endif
    if ( p->vStore    )  Vec_PtrFree( p->vStore );
    if ( p->pSave1    )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );
    if ( p->pSave2    )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );
    if ( p->pSave3    )  Aig_ManStop( (Aig_Man_t *)p->pSave3 );
    if ( p->pSave4    )  Aig_ManStop( (Aig_Man_t *)p->pSave4 );
    if ( p->pManDsd   )  If_DsdManFree( (If_DsdMan_t *)p->pManDsd, 0 );
    if ( p->pManDsd2  )  If_DsdManFree( (If_DsdMan_t *)p->pManDsd2, 0 );
    if ( p->pNtkBackup)  Abc_NtkDelete( p->pNtkBackup );
    if ( p->vPlugInComBinPairs ) 
    {
        char * pTemp;
        int i;
        Vec_PtrForEachEntry( char *, p->vPlugInComBinPairs, pTemp, i )
            ABC_FREE( pTemp );
        Vec_PtrFree( p->vPlugInComBinPairs );
    }
    Vec_IntFreeP( &p->vIndFlops );
    Vec_PtrFreeP( &p->vLTLProperties_global );
    if ( p->vSignalNames )
    Vec_PtrFreeFree( p->vSignalNames );
    ABC_FREE( p->pSpecName );
    Abc_FrameDeleteAllNetworks( p );
    ABC_FREE( p->pDrivingCell );
    ABC_FREE( p->pCex2 );
    ABC_FREE( p->pCex );
    Vec_IntFreeP( &p->pAbcWlcInv );
    Abc_NamDeref( s_GlobalFrame->pJsonStrs );
    Vec_WecFreeP( &s_GlobalFrame->vJsonObjs );  
    Ndr_Delete( s_GlobalFrame->pNdr );
    ABC_FREE( s_GlobalFrame->pNdrArray );
    Abc_FrameStoreStop( s_GlobalFrame );
 
    Gia_ManStopP( &p->pGiaMiniAig );
    Gia_ManStopP( &p->pGiaMiniLut );
    Vec_IntFreeP( &p->vCopyMiniAig );
    Vec_IntFreeP( &p->vCopyMiniLut );
    ABC_FREE( p->pArray );
    ABC_FREE( p->pBoxes );
    
 
    ABC_FREE( p );
    s_GlobalFrame = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameEnd()

ABC_DLL void Abc_FrameEnd ( Abc_Frame_t * pAbc )

extern

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

Synopsis [Stops all the packages.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file mainInit.c.

{
    Abc_FrameInitializer_t* p;
    for( p = s_InitializerEnd ; p ; p = p->prev )
        if ( p->destroy )
            p->destroy(pAbc);
    Abc_End( pAbc );
    Io_End( pAbc );
    Cmd_End( pAbc );
    If_End( pAbc );
    Map_End( pAbc );
    Mio_End( pAbc );
    Super_End( pAbc );
    Libs_End( pAbc );
    Load_End( pAbc );
    Scl_End( pAbc );
    Wlc_End( pAbc );
    Wln_End( pAbc );
    Bac_End( pAbc );
    Cba_End( pAbc );
    Pla_End( pAbc );
    Test_End( pAbc );
    Glucose_End( pAbc );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameInit()

ABC_DLL void Abc_FrameInit ( Abc_Frame_t * pAbc )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts all the packages.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file mainInit.c.

{
    Abc_FrameInitializer_t* p;
    Cmd_Init( pAbc );
    Cmd_CommandExecute( pAbc, "set checkread" ); 
    Io_Init( pAbc );
    Abc_Init( pAbc );
    If_Init( pAbc );
    Map_Init( pAbc );
    Mio_Init( pAbc );
    Super_Init( pAbc );
    Libs_Init( pAbc );
    Load_Init( pAbc );
    Scl_Init( pAbc );
    Wlc_Init( pAbc );
    Wln_Init( pAbc );
    Bac_Init( pAbc );
    Cba_Init( pAbc );
    Pla_Init( pAbc );
    Test_Init( pAbc );
    Glucose_Init( pAbc );
    Glucose2_Init( pAbc );
    for( p = s_InitializerStart ; p ; p = p->next )
        if(p->init)
            p->init(pAbc);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameStoreAdd()

ABC_DLL void Abc_FrameStoreAdd ( Abc_Frame_t * pAbc, Gia_Man_t * p )

extern

Definition at line 316 of file mainUtils.c.

{
    if ( pAbc->pHash == NULL )
        Abc_FrameStoreStart( pAbc );
    Gia_Man_t * p = Gia_ManIsoCanonicize( pGia, 0 );
    Vec_IntClear( pAbc->pHash->vEntry );
    Vec_IntPush( pAbc->pHash->vEntry, 0 );
    Vec_IntPush( pAbc->pHash->vEntry, Gia_ManPiNum(p) );
    Vec_IntPush( pAbc->pHash->vEntry, Gia_ManPoNum(p) );
    Vec_IntPush( pAbc->pHash->vEntry, Gia_ManRegNum(p) );
    Gia_Obj_t * pObj; int i;
    Gia_ManForEachAnd( p, pObj, i )
        Vec_IntPushTwo( pAbc->pHash->vEntry, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
    int iEntry = Hsh_VecManAdd( pAbc->pHash, pAbc->pHash->vEntry );
    if ( Vec_IntSize(pAbc->pHash->vValue) == iEntry )
        Vec_IntPush( pAbc->pHash->vValue, 0 );
    Vec_IntAddToEntry( pAbc->pHash->vValue, iEntry, 1 );
    assert( Vec_IntSize(pAbc->pHash->vValue) == Hsh_VecSize(pAbc->pHash) );
    Gia_ManStop( p );
}

Here is the call graph for this function:

Abc_FrameStorePrint()

ABC_DLL void Abc_FrameStorePrint ( Abc_Frame_t * pAbc )

extern

Definition at line 336 of file mainUtils.c.

{
    if ( pAbc->pHash == NULL )
        Abc_FrameStoreStart( pAbc );
    int i, Entry, nAll = 0, Max = Vec_IntFindMax( pAbc->pHash->vValue );
    Vec_Int_t * vCounts = Vec_IntStart( Max+1 );
    Vec_IntForEachEntry( pAbc->pHash->vValue, Entry, i )
        Vec_IntAddToEntry( vCounts, Entry, 1 );
    printf( "Distribution of %d stored items by reference count (<ref_count>=<num_items>): ", Hsh_VecSize(pAbc->pHash) );
    Vec_IntForEachEntry( vCounts, Entry, i )
        if ( Entry )
            printf( "%d=%d ", i, Entry ), nAll += i * Entry;
    printf( "ALL=%d\n", nAll );
    Vec_IntFree( vCounts );
}

Here is the call graph for this function:

Abc_FrameStoreStart()

ABC_DLL void Abc_FrameStoreStart ( Abc_Frame_t * pAbc )

extern

Definition at line 309 of file mainUtils.c.

{
    Abc_FrameStoreStop( pAbc );
    pAbc->pHash = Hsh_VecManStart( 1000 );
    pAbc->pHash->vEntry = Vec_IntAlloc( 1000 );
    pAbc->pHash->vValue = Vec_IntAlloc( 1000 );    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameStoreStop()

ABC_DLL void Abc_FrameStoreStop ( Abc_Frame_t * pAbc )

extern

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

Synopsis []

Description []

SideEffects []

Definition at line 303 of file mainUtils.c.

{
    if ( pAbc->pHash ) 
        Hsh_VecManStop( pAbc->pHash );
    pAbc->pHash = NULL;
}

Here is the caller graph for this function:

Abc_UtilsGetUsersInput()

ABC_DLL char * Abc_UtilsGetUsersInput ( Abc_Frame_t * pAbc )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file mainUtils.c.

{
    static char Prompt[5000];
    sprintf( Prompt, "abc %02d> ", pAbc->nSteps );
#ifdef ABC_USE_READLINE
    {
    static char * line = NULL;
    if (line != NULL) ABC_FREE(line);
    line = readline(Prompt);  
    if (line == NULL){ printf("***EOF***\n"); exit(0); }
    add_history(line);
    return line;
    }
#else
    {
    char * pRetValue;
    fprintf( pAbc->Out, "%s", Prompt );
    pRetValue = fgets( Prompt, 5000, stdin );
    return Prompt;
    }
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_UtilsGetVersion()

ABC_DLL char * Abc_UtilsGetVersion ( Abc_Frame_t * pAbc )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file mainUtils.c.

{
    static char Version[1000];
#if __GNUC__
    #pragma GCC diagnostic push
    #pragma GCC diagnostic ignored "-Wdate-time"
#endif
    sprintf(Version, "%s (compiled %s %s)", ABC_VERSION, __DATE__, __TIME__);
#if __GNUC__
    #pragma GCC diagnostic pop
#endif
    return Version;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_UtilsPrintHello()

ABC_DLL void Abc_UtilsPrintHello ( Abc_Frame_t * pAbc )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file mainUtils.c.

{
    fprintf( pAbc->Out, "%s\n", pAbc->sVersion );
}

Here is the caller graph for this function:

Abc_UtilsPrintUsage()

ABC_DLL void Abc_UtilsPrintUsage ( Abc_Frame_t * pAbc, char * ProgName )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file mainUtils.c.

{
    fprintf( pAbc->Err, "\n" );
    fprintf( pAbc->Err,
             "usage: %s [-c cmd] [-q cmd] [-C cmd] [-Q cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [-b] [file]\n",
             ProgName);
    fprintf( pAbc->Err, "    -c cmd\texecute commands `cmd'\n");
    fprintf( pAbc->Err, "    -q cmd\texecute commands `cmd' quietly\n");
    fprintf( pAbc->Err, "    -C cmd\texecute commands `cmd', then continue in interactive mode\n");
    fprintf( pAbc->Err, "    -Q cmd\texecute commands `cmd' quietly, then continue in interactive mode\n");
    fprintf( pAbc->Err, "    -F script\texecute commands from a script file and echo commands\n");
    fprintf( pAbc->Err, "    -f script\texecute commands from a script file\n");
    fprintf( pAbc->Err, "    -h\t\tprint the command usage\n");
    fprintf( pAbc->Err, "    -o file\tspecify output filename to store the result\n");
    fprintf( pAbc->Err, "    -s\t\tdo not read any initialization file\n");
    fprintf( pAbc->Err, "    -t type\tspecify input type (blif_mv (default), blif_mvs, blif, or none)\n");
    fprintf( pAbc->Err, "    -T type\tspecify output type (blif_mv (default), blif_mvs, blif, or none)\n");
    fprintf( pAbc->Err, "    -x\t\tequivalent to '-t none -T none'\n");
    fprintf( pAbc->Err, "    -b\t\trunning in bridge mode\n");
    fprintf( pAbc->Err, "\n" );
}

Here is the caller graph for this function:

Abc_UtilsSource()

ABC_DLL void Abc_UtilsSource ( Abc_Frame_t * pAbc )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file mainUtils.c.

{  
#ifdef WIN32
    if ( Cmd_CommandExecute(pAbc, "source abc.rc") )
    {
        if ( Cmd_CommandExecute(pAbc, "source ..\\abc.rc") == 0 )
            printf( "Loaded \"abc.rc\" from the parent directory.\n" );
        else if ( Cmd_CommandExecute(pAbc, "source ..\\..\\abc.rc") == 0 )
            printf( "Loaded \"abc.rc\" from the grandparent directory.\n" );
    }
#else
 
#if 0
    {
        char * sPath1, * sPath2;
 
         // If .rc is present in both the home and current directories, then read
         // it from the home directory.  Otherwise, read it from wherever it's located.
        sPath1 = Extra_UtilFileSearch(".rc", "~/", "r");
        sPath2 = Extra_UtilFileSearch(".rc", ".",  "r");
  
        if ( sPath1 && sPath2 ) {
            /* ~/.rc == .rc : Source the file only once */
            (void) Cmd_CommandExecute(pAbc, "source -s ~/.rc");
        }
        else {
            if (sPath1) {
                (void) Cmd_CommandExecute(pAbc, "source -s ~/.rc");
            }
            if (sPath2) {
                (void) Cmd_CommandExecute(pAbc, "source -s .rc");
            }
        }
        if ( sPath1 ) ABC_FREE(sPath1);
        if ( sPath2 ) ABC_FREE(sPath2);
    
        /* execute the abc script which can be open with the "open_path" */
        Cmd_CommandExecute( pAbc, "source -s abc.rc" );
    }
#endif
 
    {
        char * sPath1, * sPath2;
        char * home;
 
         // If .rc is present in both the home and current directories, then read
         // it from the home directory.  Otherwise, read it from wherever it's located.
        home = getenv("HOME");
        if (home){
            char * sPath3 = ABC_ALLOC(char, strlen(home) + 2);
            (void) sprintf(sPath3, "%s/", home);
            sPath1 = Extra_UtilFileSearch(".abc.rc", sPath3, "r");
            ABC_FREE(sPath3);
        }else
            sPath1 = NULL;
 
        sPath2 = Extra_UtilFileSearch(".abc.rc", ".",  "r");
 
        if ( sPath1 && sPath2 ) {
            /* ~/.rc == .rc : Source the file only once */
            char *tmp_cmd = ABC_ALLOC(char, strlen(sPath1)+12);
            (void) sprintf(tmp_cmd, "source -s %s", sPath1);
            // (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc");
            (void) Cmd_CommandExecute(pAbc, tmp_cmd);
            ABC_FREE(tmp_cmd);
        }
        else {
            if (sPath1) {
                char *tmp_cmd = ABC_ALLOC(char, strlen(sPath1)+12);
                (void) sprintf(tmp_cmd, "source -s %s", sPath1);
                // (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc");
                (void) Cmd_CommandExecute(pAbc, tmp_cmd);
                ABC_FREE(tmp_cmd);
            }
            if (sPath2) {
                char *tmp_cmd = ABC_ALLOC(char, strlen(sPath2)+12);
                (void) sprintf(tmp_cmd, "source -s %s", sPath2);
                // (void) Cmd_CommandExecute(pAbc, "source -s .abc.rc");
                (void) Cmd_CommandExecute(pAbc, tmp_cmd);
                ABC_FREE(tmp_cmd);
            }
        }
        if ( sPath1 ) ABC_FREE(sPath1);
        if ( sPath2 ) ABC_FREE(sPath2);
 
        /* execute the abc script which can be open with the "open_path" */
        Cmd_CommandExecute( pAbc, "source -s abc.rc" );
    }
    
#endif //WIN32
}

Here is the call graph for this function:

Here is the caller graph for this function:

main()

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

extern

GLOBAL VARIABLES ///.

MACRO DEFINITIONS /// FUNCTION DEFINITIONS ///

GLOBAL VARIABLES ///.

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

FileName [mainMC.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The main package.]

Synopsis [The main file for the model checker.]

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 [The main() procedure.]

Description []

SideEffects []

SeeAlso []

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 []

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

Synopsis [Takes file with commands to be executed and the number of CPUs.]

Description []

SideEffects []

SeeAlso []

Definition at line 9 of file main.c.

{
   return ABC_NAMESPACE_PREFIX Abc_RealMain(argc, argv);
}

Here is the call graph for this function: