ioAbc.h File Reference

#include "base/abc/abc.h"
#include "misc/extra/extra.h"

Go to the source code of this file.

Macros
#define	IO_WRITE_LINE_LENGTH   78
	MACRO DEFINITIONS ///. More...

Enumerations
enum	Io_FileType_t {   IO_FILE_NONE = 0, IO_FILE_AIGER, IO_FILE_BAF, IO_FILE_BBLIF,   IO_FILE_BLIF, IO_FILE_BLIFMV, IO_FILE_BENCH, IO_FILE_BOOK,   IO_FILE_CNF, IO_FILE_DOT, IO_FILE_EDIF, IO_FILE_EQN,   IO_FILE_GML, IO_FILE_LIST, IO_FILE_PLA, IO_FILE_SMV,   IO_FILE_VERILOG, IO_FILE_UNKNOWN }
	INCLUDES ///. More...

Functions
Abc_Ntk_t *	Io_ReadAiger (char *pFileName, int fCheck)
	FUNCTION DECLARATIONS ///. More...
Abc_Ntk_t *	Io_ReadBaf (char *pFileName, int fCheck)
	DECLARATIONS ///. More...
Abc_Ntk_t *	Io_ReadBblif (char *pFileName, int fCheck)
Abc_Ntk_t *	Io_ReadBlif (char *pFileName, int fCheck)
	FUNCTION DEFINITIONS ///. More...
Abc_Ntk_t *	Io_ReadBlifMv (char *pFileName, int fBlifMv, int fCheck)
	FUNCTION DEFINITIONS ///. More...
Abc_Ntk_t *	Io_ReadBench (char *pFileName, int fCheck)
	FUNCTION DEFINITIONS ///. More...
void	Io_ReadBenchInit (Abc_Ntk_t *pNtk, char *pFileName)
Abc_Ntk_t *	Io_ReadEdif (char *pFileName, int fCheck)
	FUNCTION DEFINITIONS ///. More...
Abc_Ntk_t *	Io_ReadEqn (char *pFileName, int fCheck)
	FUNCTION DEFINITIONS ///. More...
Abc_Ntk_t *	Io_ReadPla (char *pFileName, int fZeros, int fCheck)
	FUNCTION DEFINITIONS ///. More...
Abc_Ntk_t *	Io_ReadVerilog (char *pFileName, int fCheck)
	DECLARATIONS ///. More...
void	Io_WriteAiger (Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact, int fUnique)
void	Io_WriteAigerCex (Abc_Cex_t *pCex, Abc_Ntk_t *pNtk, void *pG, char *pFileName)
void	Io_WriteBaf (Abc_Ntk_t *pNtk, char *pFileName)
	DECLARATIONS ///. More...
void	Io_WriteBblif (Abc_Ntk_t *pNtk, char *pFileName)
void	Io_WriteBlifLogic (Abc_Ntk_t *pNtk, char *pFileName, int fWriteLatches)
	FUNCTION DEFINITIONS ///. More...
void	Io_WriteBlif (Abc_Ntk_t *pNtk, char *pFileName, int fWriteLatches, int fBb2Wb, int fSeq)
void	Io_WriteTimingInfo (FILE *pFile, Abc_Ntk_t *pNtk)
void	Io_WriteBlifSpecial (Abc_Ntk_t *pNtk, char *FileName, char *pLutStruct, int fUseHie)
void	Io_WriteBlifMv (Abc_Ntk_t *pNtk, char *FileName)
	FUNCTION DEFINITIONS ///. More...
int	Io_WriteBench (Abc_Ntk_t *pNtk, const char *FileName)
	FUNCTION DEFINITIONS ///. More...
int	Io_WriteBenchLut (Abc_Ntk_t *pNtk, char *FileName)
void	Io_WriteBook (Abc_Ntk_t *pNtk, char *FileName)
int	Io_WriteCnf (Abc_Ntk_t *pNtk, char *FileName, int fAllPrimes)
	FUNCTION DEFINITIONS ///. More...
void	Io_WriteDot (Abc_Ntk_t *pNtk, char *FileName)
	FUNCTION DEFINITIONS ///. More...
void	Io_WriteDotNtk (Abc_Ntk_t *pNtk, Vec_Ptr_t *vNodes, Vec_Ptr_t *vNodesShow, char *pFileName, int fGateNames, int fUseReverse)
void	Io_WriteDotSeq (Abc_Ntk_t *pNtk, Vec_Ptr_t *vNodes, Vec_Ptr_t *vNodesShow, char *pFileName, int fGateNames, int fUseReverse)
void	Io_WriteEqn (Abc_Ntk_t *pNtk, char *pFileName)
	FUNCTION DEFINITIONS ///. More...
void	Io_WriteGml (Abc_Ntk_t *pNtk, char *pFileName)
	DECLARATIONS ///. More...
void	Io_WriteList (Abc_Ntk_t *pNtk, char *pFileName, int fUseHost)
	FUNCTION DEFINITIONS ///. More...
int	Io_WritePla (Abc_Ntk_t *pNtk, char *FileName)
	FUNCTION DEFINITIONS ///. More...
int	Io_WriteSmv (Abc_Ntk_t *pNtk, char *FileName)
void	Io_WriteVerilog (Abc_Ntk_t *pNtk, char *FileName)
	FUNCTION DEFINITIONS ///. More...
Io_FileType_t	Io_ReadFileType (char *pFileName)
	DECLARATIONS ///. More...
Io_FileType_t	Io_ReadLibType (char *pFileName)
Abc_Ntk_t *	Io_ReadNetlist (char *pFileName, Io_FileType_t FileType, int fCheck)
Abc_Ntk_t *	Io_Read (char *pFileName, Io_FileType_t FileType, int fCheck, int fBarBufs)
void	Io_Write (Abc_Ntk_t *pNtk, char *pFileName, Io_FileType_t FileType)
void	Io_WriteHie (Abc_Ntk_t *pNtk, char *pBaseName, char *pFileName)
Abc_Obj_t *	Io_ReadCreatePi (Abc_Ntk_t *pNtk, char *pName)
Abc_Obj_t *	Io_ReadCreatePo (Abc_Ntk_t *pNtk, char *pName)
Abc_Obj_t *	Io_ReadCreateLatch (Abc_Ntk_t *pNtk, char *pNetLI, char *pNetLO)
Abc_Obj_t *	Io_ReadCreateResetLatch (Abc_Ntk_t *pNtk, int fBlifMv)
Abc_Obj_t *	Io_ReadCreateResetMux (Abc_Ntk_t *pNtk, char *pResetLO, char *pDataLI, int fBlifMv)
Abc_Obj_t *	Io_ReadCreateNode (Abc_Ntk_t *pNtk, char *pNameOut, char *pNamesIn[], int nInputs)
Abc_Obj_t *	Io_ReadCreateConst (Abc_Ntk_t *pNtk, char *pName, int fConst1)
Abc_Obj_t *	Io_ReadCreateInv (Abc_Ntk_t *pNtk, char *pNameIn, char *pNameOut)
Abc_Obj_t *	Io_ReadCreateBuf (Abc_Ntk_t *pNtk, char *pNameIn, char *pNameOut)
FILE *	Io_FileOpen (const char *FileName, const char *PathVar, const char *Mode, int fVerbose)

Macro Definition Documentation

#define IO_WRITE_LINE_LENGTH   78

MACRO DEFINITIONS ///.

Definition at line 71 of file ioAbc.h.

Enumeration Type Documentation

enum Io_FileType_t

INCLUDES ///.

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

FileName [ioAbc.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

ioAbc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Enumerator
IO_FILE_NONE
IO_FILE_AIGER
IO_FILE_BAF
IO_FILE_BBLIF
IO_FILE_BLIF
IO_FILE_BLIFMV
IO_FILE_BENCH
IO_FILE_BOOK
IO_FILE_CNF
IO_FILE_DOT
IO_FILE_EDIF
IO_FILE_EQN
IO_FILE_GML
IO_FILE_LIST
IO_FILE_PLA
IO_FILE_SMV
IO_FILE_VERILOG
IO_FILE_UNKNOWN

Definition at line 46 of file ioAbc.h.

             { 
    IO_FILE_NONE = 0, 
    IO_FILE_AIGER,      
    IO_FILE_BAF,      
    IO_FILE_BBLIF,      
    IO_FILE_BLIF,      
    IO_FILE_BLIFMV,      
    IO_FILE_BENCH,      
    IO_FILE_BOOK,
    IO_FILE_CNF,      
    IO_FILE_DOT,      
    IO_FILE_EDIF,      
    IO_FILE_EQN,      
    IO_FILE_GML,      
    IO_FILE_LIST,      
    IO_FILE_PLA,      
    IO_FILE_SMV,      
    IO_FILE_VERILOG,    
    IO_FILE_UNKNOWN       
} Io_FileType_t;

Function Documentation

FILE* Io_FileOpen	(	const char *	FileName,
		const char *	PathVar,
		const char *	Mode,
		int	fVerbose
	)

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

Synopsis [Provide an fopen replacement with path lookup]

Description [Provide an fopen replacement where the path stored in pathvar MVSIS variable is used to look up the path for name. Returns NULL if file cannot be opened.]

SideEffects []

SeeAlso []

Definition at line 819 of file ioUtil.c.

{
    char * t = 0, * c = 0, * i;

    if ( PathVar == 0 )
    {
        return fopen( FileName, Mode );
    }
    else
    {
        if ( (c = Abc_FrameReadFlag( (char*)PathVar )) )
        {
            char ActualFileName[4096];
            FILE * fp = 0;
            t = Extra_UtilStrsav( c );
            for (i = strtok( t, ":" ); i != 0; i = strtok( 0, ":") )
            {
#ifdef WIN32
                _snprintf ( ActualFileName, 4096, "%s/%s", i, FileName );
#else
                snprintf ( ActualFileName, 4096, "%s/%s", i, FileName );
#endif
                if ( ( fp = fopen ( ActualFileName, Mode ) ) )
                {
                    if ( fVerbose )
                    fprintf ( stdout, "Using file %s\n", ActualFileName );
                    ABC_FREE( t );
                    return fp;
                }
            }
            ABC_FREE( t );
            return 0;
        }
        else
        {
            return fopen( FileName, Mode );
        }
    }
}

Abc_Ntk_t* Io_Read	(	char *	pFileName,
		Io_FileType_t	FileType,
		int	fCheck,
		int	fBarBufs
	)

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

Synopsis [Read the network from a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file ioUtil.c.

{
    Abc_Ntk_t * pNtk, * pTemp;
    Vec_Ptr_t * vLtl;
    // get the netlist
    pNtk = Io_ReadNetlist( pFileName, FileType, fCheck );
    if ( pNtk == NULL )
        return NULL;
    vLtl = temporaryLtlStore( pNtk );
    if ( !Abc_NtkIsNetlist(pNtk) )
        return pNtk;
    // derive barbufs
    if ( fBarBufs )
    {
        pNtk = Abc_NtkToBarBufs( pTemp = pNtk );
        Abc_NtkDelete( pTemp );
        assert( Abc_NtkIsLogic(pNtk) );
        return pNtk;
    }
    // flatten logic hierarchy
    assert( Abc_NtkIsNetlist(pNtk) );
    if ( Abc_NtkWhiteboxNum(pNtk) > 0 )
    {
        pNtk = Abc_NtkFlattenLogicHierarchy( pTemp = pNtk );
        Abc_NtkDelete( pTemp );
        if ( pNtk == NULL )
        {
            fprintf( stdout, "Flattening logic hierarchy has failed.\n" );
            return NULL;
        }
    }
    // convert blackboxes
    if ( Abc_NtkBlackboxNum(pNtk) > 0 )
    {
        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
        pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
        Abc_NtkDelete( pTemp );
        if ( pNtk == NULL )
        {
            fprintf( stdout, "Converting blackboxes has failed.\n" );
            return NULL;
        }
    }
    // consider the case of BLIF-MV
    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
    {
        pNtk = Abc_NtkStrashBlifMv( pTemp = pNtk );
        Abc_NtkDelete( pTemp );
        if ( pNtk == NULL )
        {
            fprintf( stdout, "Converting BLIF-MV to AIG has failed.\n" );
            return NULL;
        }
        return pNtk;
    }
    // convert the netlist into the logic network
    pNtk = Abc_NtkToLogic( pTemp = pNtk );
    if( vLtl )
        updateLtlStoreOfNtk( pNtk, vLtl );
    Abc_NtkDelete( pTemp );
    if ( pNtk == NULL )
    {
        fprintf( stdout, "Converting netlist to logic network after reading has failed.\n" );
        return NULL;
    }
    return pNtk;
}

Abc_Ntk_t* Io_ReadAiger	(	char *	pFileName,
		int	fCheck
	)

FUNCTION DECLARATIONS ///.

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

Synopsis [Reads the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file ioReadAiger.c.

{
    ProgressBar * pProgress;
    FILE * pFile;
    Vec_Ptr_t * vNodes, * vTerms;
    Vec_Int_t * vLits = NULL;
    Abc_Obj_t * pObj, * pNode0, * pNode1;
    Abc_Ntk_t * pNtkNew;
    int nTotal, nInputs, nOutputs, nLatches, nAnds;
    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
    int nFileSize = -1, iTerm, nDigits, i;
    char * pContents, * pDrivers = NULL, * pSymbols, * pCur, * pName, * pType;
    unsigned uLit0, uLit1, uLit;
    int RetValue;

    // read the file into the buffer
    if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
        pContents = Ioa_ReadLoadFileBz2Aig( pFileName, &nFileSize );
    else if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
        pContents = Ioa_ReadLoadFileGzAig( pFileName, &nFileSize );
    else
    {
//        pContents = Ioa_ReadLoadFile( pFileName );
        nFileSize = Extra_FileSize( pFileName );
        pFile = fopen( pFileName, "rb" );
        pContents = ABC_ALLOC( char, nFileSize );
        RetValue = fread( pContents, nFileSize, 1, pFile );
        fclose( pFile );
    }


    // check if the input file format is correct
    if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
    {
        fprintf( stdout, "Wrong input file format.\n" );
        ABC_FREE( pContents );
        return NULL;
    }

    // read the parameters (M I L O A + B C J F)
    pCur = pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
    // read the number of objects
    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
    // read the number of inputs
    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
    // read the number of latches
    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
    // read the number of outputs
    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
    // read the number of nodes
    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
    if ( *pCur == ' ' )
    {
//        assert( nOutputs == 0 );
        // read the number of properties
        pCur++;
        nBad = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nBad;
    }
    if ( *pCur == ' ' )
    {
        // read the number of properties
        pCur++;
        nConstr = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nConstr;
    }
    if ( *pCur == ' ' )
    {
        // read the number of properties
        pCur++;
        nJust = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nJust;
    }
    if ( *pCur == ' ' )
    {
        // read the number of properties
        pCur++;
        nFair = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nFair;
    }
    if ( *pCur != '\n' )
    {
        fprintf( stdout, "The parameter line is in a wrong format.\n" );
        ABC_FREE( pContents );
        return NULL;
    }
    pCur++;

    // check the parameters
    if ( nTotal != nInputs + nLatches + nAnds )
    {
        fprintf( stdout, "The number of objects does not match.\n" );
        ABC_FREE( pContents );
        return NULL;
    }
    if ( nJust || nFair )
    {
        fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
        ABC_FREE( pContents );
        return NULL;
    }

    if ( nConstr )
    {
        if ( nConstr == 1 )
            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
        else
            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
    }

    // allocate the empty AIG
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pName = Extra_FileNameGeneric( pFileName );
    pNtkNew->pName = Extra_UtilStrsav( pName );
    pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
    ABC_FREE( pName );
    pNtkNew->nConstrs = nConstr;

    // prepare the array of nodes
    vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
    Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );

    // create the PIs
    for ( i = 0; i < nInputs; i++ )
    {
        pObj = Abc_NtkCreatePi(pNtkNew);    
        Vec_PtrPush( vNodes, pObj );
    }
    // create the POs
    for ( i = 0; i < nOutputs; i++ )
    {
        pObj = Abc_NtkCreatePo(pNtkNew);   
    }
    // create the latches
    nDigits = Abc_Base10Log( nLatches );
    for ( i = 0; i < nLatches; i++ )
    {
        pObj = Abc_NtkCreateLatch(pNtkNew);
        Abc_LatchSetInit0( pObj );
        pNode0 = Abc_NtkCreateBi(pNtkNew);
        pNode1 = Abc_NtkCreateBo(pNtkNew);
        Abc_ObjAddFanin( pObj, pNode0 );
        Abc_ObjAddFanin( pNode1, pObj );
        Vec_PtrPush( vNodes, pNode1 );
        // assign names to latch and its input
//        Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
//        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
    } 
    

    if ( pContents[3] == ' ' ) // standard AIGER
    {
        // remember the beginning of latch/PO literals
        pDrivers = pCur;
        // scroll to the beginning of the binary data
        for ( i = 0; i < nLatches + nOutputs; )
            if ( *pCur++ == '\n' )
                i++;
    }
    else // modified AIGER
    { 
        vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
    }

    // create the AND gates
    pProgress = Extra_ProgressBarStart( stdout, nAnds );
    for ( i = 0; i < nAnds; i++ )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        uLit = ((i + 1 + nInputs + nLatches) << 1);
        uLit1 = uLit  - Io_ReadAigerDecode( &pCur );
        uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
//        assert( uLit1 > uLit0 );
        pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
        pNode1 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
        assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
        Vec_PtrPush( vNodes, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pNode0, pNode1) );
    }
    Extra_ProgressBarStop( pProgress );

    // remember the place where symbols begin
    pSymbols = pCur;

    // read the latch driver literals
    pCur = pDrivers;
    if ( pContents[3] == ' ' ) // standard AIGER
    {
        Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
        {
            uLit0 = atoi( pCur );  while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
            if ( *pCur == ' ' ) // read initial value
            {
                int Init;
                pCur++;
                Init = atoi( pCur );
                if ( Init == 0 )
                    Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) );
                else if ( Init == 1 )
                    Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
                else 
                {
                    assert( Init == Abc_Var2Lit(1+Abc_NtkPiNum(pNtkNew)+i, 0) ); 
                    // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf
                    Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) );
                }
                while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
            }
            if ( *pCur != '\n' )
            {
                fprintf( stdout, "The initial value of latch number %d is not recongnized.\n", i );
                return NULL;
            }
            pCur++;

            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
            Abc_ObjAddFanin( pObj, pNode0 );
        }
        // read the PO driver literals
        Abc_NtkForEachPo( pNtkNew, pObj, i )
        {
            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
            Abc_ObjAddFanin( pObj, pNode0 );
        }
    }
    else
    {
        // read the latch driver literals
        Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
        {
            uLit0 = Vec_IntEntry( vLits, i );
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
            Abc_ObjAddFanin( pObj, pNode0 );
        }
        // read the PO driver literals
        Abc_NtkForEachPo( pNtkNew, pObj, i )
        {
            uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
            Abc_ObjAddFanin( pObj, pNode0 );
        }
        Vec_IntFree( vLits );
    }
 
    // read the names if present
    pCur = pSymbols;
    if ( pCur < pContents + nFileSize && *pCur != 'c' )
    {
        int Counter = 0;
        while ( pCur < pContents + nFileSize && *pCur != 'c' )
        {
            // get the terminal type
            pType = pCur;
            if ( *pCur == 'i' )
                vTerms = pNtkNew->vPis;
            else if ( *pCur == 'l' )
                vTerms = pNtkNew->vBoxes;
            else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
                vTerms = pNtkNew->vPos;
            else
            {
//                fprintf( stdout, "Wrong terminal type.\n" );
                return NULL;
            }
            // get the terminal number
            iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
            // get the node
            if ( iTerm >= Vec_PtrSize(vTerms) )
            {
                fprintf( stdout, "The number of terminal is out of bound.\n" );
                return NULL;
            }
            pObj = (Abc_Obj_t *)Vec_PtrEntry( vTerms, iTerm );
            if ( *pType == 'l' )
                pObj = Abc_ObjFanout0(pObj);
            // assign the name
            pName = pCur;          while ( *pCur++ != '\n' );
            // assign this name 
            *(pCur-1) = 0;
            Abc_ObjAssignName( pObj, pName, NULL );
            if ( *pType == 'l' )
            {
                Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
                Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
            }
            // mark the node as named
            pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
        } 

        // assign the remaining names
        Abc_NtkForEachPi( pNtkNew, pObj, i )
        {
            if ( pObj->pCopy ) continue;
            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
            Counter++;
        }
        Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
        {
            if ( pObj->pCopy ) continue;
            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
            Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
            Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
            Counter++;
        }
        Abc_NtkForEachPo( pNtkNew, pObj, i )
        {
            if ( pObj->pCopy ) continue;
            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
            Counter++;
        }
//        if ( Counter )
//            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
    }
    else
    {
//        printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
        Abc_NtkShortNames( pNtkNew );
    }

    // read the name of the model if given
    pCur = pSymbols;
    if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
    {
        pCur++;
        if ( *pCur == 'n' )
        {
            pCur++;
            // read model name
            if ( strlen(pCur) > 0 )
            {
                ABC_FREE( pNtkNew->pName );
                pNtkNew->pName = Extra_UtilStrsav( pCur );
            }
        }
    }

    // skipping the comments
    ABC_FREE( pContents );
    Vec_PtrFree( vNodes );

    // remove the extra nodes
    Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );

    // update polarity of the additional outputs
    if ( nBad || nConstr || nJust || nFair )
        Abc_NtkInvertConstraints( pNtkNew );

    // check the result
    if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
    {
        printf( "Io_ReadAiger: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

Abc_Ntk_t* Io_ReadBaf	(	char *	pFileName,
		int	fCheck
	)

DECLARATIONS ///.

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

FileName [ioReadBaf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedures to read AIG in the binary format.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Reads the AIG in the binary format.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ioReadBaf.c.

{
    ProgressBar * pProgress;
    FILE * pFile;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pObj, * pNode0, * pNode1;
    Abc_Ntk_t * pNtkNew;
    int nInputs, nOutputs, nLatches, nAnds, nFileSize, Num, i;
    char * pContents, * pName, * pCur;
    unsigned * pBufferNode;
    int RetValue;

    // read the file into the buffer
    nFileSize = Extra_FileSize( pFileName );
    pFile = fopen( pFileName, "rb" );
    pContents = ABC_ALLOC( char, nFileSize );
    RetValue = fread( pContents, nFileSize, 1, pFile );
    fclose( pFile );

    // skip the comments (comment lines begin with '#' and end with '\n')
    for ( pCur = pContents; *pCur == '#'; )
        while ( *pCur++ != '\n' );

    // read the name
    pName = pCur;             while ( *pCur++ );
    // read the number of inputs
    nInputs = atoi( pCur );   while ( *pCur++ );
    // read the number of outputs
    nOutputs = atoi( pCur );  while ( *pCur++ );
    // read the number of latches
    nLatches = atoi( pCur );  while ( *pCur++ );
    // read the number of nodes
    nAnds = atoi( pCur );     while ( *pCur++ );

    // allocate the empty AIG
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pNtkNew->pName = Extra_UtilStrsav( pName );
    pNtkNew->pSpec = Extra_UtilStrsav( pFileName );

    // prepare the array of nodes
    vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
    Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );

    // create the PIs
    for ( i = 0; i < nInputs; i++ )
    {
        pObj = Abc_NtkCreatePi(pNtkNew);    
        Abc_ObjAssignName( pObj, pCur, NULL );  while ( *pCur++ );
        Vec_PtrPush( vNodes, pObj );
    }
    // create the POs
    for ( i = 0; i < nOutputs; i++ )
    {
        pObj = Abc_NtkCreatePo(pNtkNew);   
        Abc_ObjAssignName( pObj, pCur, NULL );  while ( *pCur++ ); 
    }
    // create the latches
    for ( i = 0; i < nLatches; i++ )
    {
        pObj = Abc_NtkCreateLatch(pNtkNew);
        Abc_ObjAssignName( pObj, pCur, NULL );  while ( *pCur++ ); 

        pNode0 = Abc_NtkCreateBi(pNtkNew);
        Abc_ObjAssignName( pNode0, pCur, NULL );  while ( *pCur++ ); 

        pNode1 = Abc_NtkCreateBo(pNtkNew);
        Abc_ObjAssignName( pNode1, pCur, NULL );  while ( *pCur++ ); 
        Vec_PtrPush( vNodes, pNode1 );

        Abc_ObjAddFanin( pObj, pNode0 );
        Abc_ObjAddFanin( pNode1, pObj );
    }

    // get the pointer to the beginning of the node array
    pBufferNode = (unsigned *)(pContents + (nFileSize - (2 * nAnds + nOutputs + nLatches) * sizeof(int)) );
    // make sure we are at the place where the nodes begin
    if ( pBufferNode != (unsigned *)pCur )
    {
        ABC_FREE( pContents );
        Vec_PtrFree( vNodes );
        Abc_NtkDelete( pNtkNew );
        printf( "Warning: Internal reader error.\n" );
        return NULL;
    }

    // create the AND gates
    pProgress = Extra_ProgressBarStart( stdout, nAnds );
    for ( i = 0; i < nAnds; i++ )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, pBufferNode[2*i+0] >> 1), pBufferNode[2*i+0] & 1 );
        pNode1 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, pBufferNode[2*i+1] >> 1), pBufferNode[2*i+1] & 1 );
        Vec_PtrPush( vNodes, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pNode0, pNode1) );
    }
    Extra_ProgressBarStop( pProgress );

    // read the POs
    Abc_NtkForEachCo( pNtkNew, pObj, i )
    {
        Num = pBufferNode[2*nAnds+i];
        if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) )
        {
            Abc_ObjSetData( Abc_ObjFanout0(pObj), (void *)(ABC_PTRINT_T)(Num & 3) );
            Num >>= 2;
        }
        pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, Num >> 1), Num & 1 );
        Abc_ObjAddFanin( pObj, pNode0 );
    }
    ABC_FREE( pContents );
    Vec_PtrFree( vNodes );

    // remove the extra nodes
//    Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );

    // check the result
    if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
    {
        printf( "Io_ReadBaf: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;

}

Abc_Ntk_t* Io_ReadBblif	(	char *	pFileName,
		int	fCheck
	)

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

Synopsis [Reads the AIG in the binary format.]

Description []

SideEffects []

SeeAlso []

Definition at line 324 of file ioReadBblif.c.

{
    Bbl_Man_t * p;
    Abc_Ntk_t * pNtkNew;
    // read the file
    p = Bbl_ManReadBinaryBlif( pFileName );
    pNtkNew = Bbl_ManToAig( p );
    Bbl_ManStop( p );
    // check the result
    if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
    {
        printf( "Io_ReadBaf: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

Abc_Ntk_t* Io_ReadBench	(	char *	pFileName,
		int	fCheck
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Reads the network from a BENCH file.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file ioReadBench.c.

{
    Extra_FileReader_t * p;
    Abc_Ntk_t * pNtk;

    // start the file
    p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t,()=" );
    if ( p == NULL )
        return NULL;

    // read the network
    pNtk = Io_ReadBenchNetwork( p );
    Extra_FileReaderFree( p );
    if ( pNtk == NULL )
        return NULL;

    // make sure that everything is okay with the network structure
    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadBench: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
        return NULL;
    }
    return pNtk;
}

void Io_ReadBenchInit	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

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

Synopsis [Reads initial state in BENCH format.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file ioReadBench.c.

{
    char pBuffer[1000];
    FILE * pFile;
    char * pToken;
    Abc_Obj_t * pObj;
    int Num;
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Io_ReadBenchInit(): Failed to open file \"%s\".\n", pFileName );
        return;
    }
    while ( fgets( pBuffer, 999, pFile ) )
    {
        pToken = strtok( pBuffer, " \n\t\r" );
        // find the latch output
        Num = Nm_ManFindIdByName( pNtk->pManName, pToken, ABC_OBJ_BO );
        if ( Num < 0 )
        {
            printf( "Io_ReadBenchInit(): Cannot find register with output %s.\n", pToken );
            continue;
        }
        pObj = Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
        if ( !Abc_ObjIsLatch(pObj) )
        {
            printf( "Io_ReadBenchInit(): The signal is not a register output %s.\n", pToken );
            continue;
        }
        // assign the new init state
        pToken = strtok( NULL, " \n\t\r" );
        if ( pToken[0] == '0' )
            Abc_LatchSetInit0( pObj );
        else if ( pToken[0] == '1' )
            Abc_LatchSetInit1( pObj );
        else if ( pToken[0] == '2' )
            Abc_LatchSetInitDc( pObj );
        else
        {
            printf( "Io_ReadBenchInit(): The signal %s has unknown initial value (%s).\n", 
                Abc_ObjName(Abc_ObjFanout0(pObj)), pToken );
            continue;
        }
    }
    fclose( pFile );
}

Abc_Ntk_t* Io_ReadBlif	(	char *	pFileName,
		int	fCheck
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Reads the (hierarchical) network from the BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file ioReadBlif.c.

{
    Io_ReadBlif_t * p;
    Abc_Ntk_t * pNtk;

    // start the file
    p = Io_ReadBlifFile( pFileName );
    if ( p == NULL )
        return NULL;

    // read the hierarchical network
    pNtk = Io_ReadBlifNetwork( p );
    if ( pNtk == NULL )
    {
        Io_ReadBlifFree( p );
        return NULL;
    }
    pNtk->pSpec = Extra_UtilStrsav( pFileName );
    Abc_NtkTimeInitialize( pNtk, NULL );
    Io_ReadBlifFree( p );

    // make sure that everything is okay with the network structure
    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadBlif: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
        return NULL;
    }
    return pNtk;
}

Abc_Ntk_t* Io_ReadBlifMv	(	char *	pFileName,
		int	fBlifMv,
		int	fCheck
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Reads the network from the BLIF or BLIF-MV file.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file ioReadBlifMv.c.

{
    FILE * pFile;
    Io_MvMan_t * p;
    Abc_Ntk_t * pNtk, * pExdc;
    Abc_Des_t * pDesign = NULL; 
    char * pDesignName;
    int RetValue, i;
    char * pLtlProp;

    // check that the file is available
    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Io_ReadBlifMv(): The file is unavailable (absent or open).\n" );
        return 0;
    }
    fclose( pFile );

    // start the file reader
    p = Io_MvAlloc();
    p->fBlifMv   = fBlifMv;
    p->fUseReset = 1;
    p->pFileName = pFileName;
    p->pBuffer   = Io_MvLoadFile( pFileName );
    if ( p->pBuffer == NULL )
    {
        Io_MvFree( p );
        return NULL;
    }
    // set the design name
    pDesignName  = Extra_FileNameGeneric( pFileName );
    p->pDesign   = Abc_DesCreate( pDesignName );
    ABC_FREE( pDesignName );
    // free the HOP manager
    Hop_ManStop( (Hop_Man_t *)p->pDesign->pManFunc );
    p->pDesign->pManFunc = NULL;
    // prepare the file for parsing
    Io_MvReadPreparse( p );
    // parse interfaces of each network and construct the network
    if ( Io_MvReadInterfaces( p ) )
        pDesign = Io_MvParse( p );
    if ( p->sError[0] )
        fprintf( stdout, "%s\n", p->sError );
    Io_MvFree( p );
    if ( pDesign == NULL )
        return NULL;
// pDesign should be linked to all models of the design

    // make sure that everything is okay with the network structure
    if ( fCheck )
    {
        Vec_PtrForEachEntry( Abc_Ntk_t *, pDesign->vModules, pNtk, i )
        {
            if ( !Abc_NtkCheckRead( pNtk ) )
            {
                printf( "Io_ReadBlifMv: The network check has failed for model %s.\n", pNtk->pName );
                Abc_DesFree( pDesign, NULL );
                return NULL;
            }
        }
    }

//Abc_DesPrint( pDesign );

    // check if there is an EXDC network
    if ( Vec_PtrSize(pDesign->vModules) > 1 )
    {
        pNtk = (Abc_Ntk_t *)Vec_PtrEntry(pDesign->vModules, 0);
        Vec_PtrForEachEntryStart( Abc_Ntk_t *, pDesign->vModules, pExdc, i, 1 )
            if ( !strcmp(pExdc->pName, "EXDC") )
            {
                assert( pNtk->pExdc == NULL );
                pNtk->pExdc = pExdc;
                Vec_PtrRemove(pDesign->vModules, pExdc);
                pExdc->pDesign = NULL;
                i--;
            }
            else
                pNtk = pExdc;
    }

    // detect top-level model
    RetValue = Abc_DesFindTopLevelModels( pDesign );
    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
    if ( RetValue > 1 )
        printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
            Vec_PtrSize(pDesign->vTops), pNtk->pName );

    // extract the master network
    pNtk->pDesign = pDesign;
    pDesign->pManFunc = NULL;

    // verify the design for cyclic dependence
    assert( Vec_PtrSize(pDesign->vModules) > 0 );
    if ( Vec_PtrSize(pDesign->vModules) == 1 )
    {
//        printf( "Warning: The design is not hierarchical.\n" );
        Abc_DesFree( pDesign, pNtk );
        pNtk->pDesign = NULL;
        pNtk->pSpec = Extra_UtilStrsav( pFileName );
    }
    else
        Abc_NtkIsAcyclicHierarchy( pNtk );

//Io_WriteBlifMv( pNtk, "_temp_.mv" );
    if ( pNtk->pSpec == NULL )
        pNtk->pSpec = Extra_UtilStrsav( pFileName );

    vGlobalLtlArray = Vec_PtrAlloc( 100 );
    Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i )
        Vec_PtrPush( pNtk->vLtlProperties, pLtlProp );
    Vec_PtrFreeP( &vGlobalLtlArray );
    return pNtk;
}

Abc_Obj_t* Io_ReadCreateBuf	(	Abc_Ntk_t *	pNtk,
		char *	pNameIn,
		char *	pNameOut
	)

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

Synopsis [Create an inverter or buffer for the given net.]

Description [Assumes that the nets already exist.]

SideEffects []

SeeAlso []

Definition at line 795 of file ioUtil.c.

{
    Abc_Obj_t * pNet, * pNode;
    pNet  = Abc_NtkFindNet(pNtk, pNameIn);     assert( pNet );
    pNode = Abc_NtkCreateNodeBuf(pNtk, pNet);
    pNet  = Abc_NtkFindNet(pNtk, pNameOut);    assert( pNet );
    Abc_ObjAddFanin( pNet, pNode );
    return pNet;
}

Abc_Obj_t* Io_ReadCreateConst	(	Abc_Ntk_t *	pNtk,
		char *	pName,
		int	fConst1
	)

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

Synopsis [Create a constant 0 node driving the net with this name.]

Description [Assumes that the net already exists.]

SideEffects []

SeeAlso []

Definition at line 754 of file ioUtil.c.

{
    Abc_Obj_t * pNet, * pTerm;
    pTerm = fConst1? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
    pNet  = Abc_NtkFindNet(pNtk, pName);    assert( pNet );
    Abc_ObjAddFanin( pNet, pTerm );
    return pTerm;
}

Abc_Obj_t* Io_ReadCreateInv	(	Abc_Ntk_t *	pNtk,
		char *	pNameIn,
		char *	pNameOut
	)

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

Synopsis [Create an inverter or buffer for the given net.]

Description [Assumes that the nets already exist.]

SideEffects []

SeeAlso []

Definition at line 774 of file ioUtil.c.

{
    Abc_Obj_t * pNet, * pNode;
    pNet  = Abc_NtkFindNet(pNtk, pNameIn);     assert( pNet );
    pNode = Abc_NtkCreateNodeInv(pNtk, pNet);
    pNet  = Abc_NtkFindNet(pNtk, pNameOut);    assert( pNet );
    Abc_ObjAddFanin( pNet, pNode );
    return pNode;
}

Abc_Obj_t* Io_ReadCreateLatch	(	Abc_Ntk_t *	pNtk,
		char *	pNetLI,
		char *	pNetLO
	)

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

Synopsis [Create a latch with the given input/output.]

Description [By default, the latch value is unknown (ABC_INIT_NONE).]

SideEffects []

SeeAlso []

Definition at line 660 of file ioUtil.c.

{
    Abc_Obj_t * pLatch, * pTerm, * pNet;
    // get the LI net
    pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI );
    // add the BO terminal
    pTerm = Abc_NtkCreateBi( pNtk );
    Abc_ObjAddFanin( pTerm, pNet );
    // add the latch box
    pLatch = Abc_NtkCreateLatch( pNtk );
    Abc_ObjAddFanin( pLatch, pTerm  );
    // add the BI terminal
    pTerm = Abc_NtkCreateBo( pNtk );
    Abc_ObjAddFanin( pTerm, pLatch );
    // get the LO net
    pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO );
    Abc_ObjAddFanin( pNet, pTerm );
    // set latch name
    Abc_ObjAssignName( pLatch, pNetLO, "L" );
    return pLatch;
}

Abc_Obj_t* Io_ReadCreateNode	(	Abc_Ntk_t *	pNtk,
		char *	pNameOut,
		char *	pNamesIn[],
		int	nInputs
	)

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

Synopsis [Create node and the net driven by it.]

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file ioUtil.c.

{
    Abc_Obj_t * pNet, * pNode;
    int i;
    // create a new node 
    pNode = Abc_NtkCreateNode( pNtk );
    // add the fanin nets
    for ( i = 0; i < nInputs; i++ )
    {
        pNet = Abc_NtkFindOrCreateNet( pNtk, pNamesIn[i] );
        Abc_ObjAddFanin( pNode, pNet );
    }
    // add the fanout net
    pNet = Abc_NtkFindOrCreateNet( pNtk, pNameOut );
    Abc_ObjAddFanin( pNet, pNode );
    return pNode;
}

Abc_Obj_t* Io_ReadCreatePi	(	Abc_Ntk_t *	pNtk,
		char *	pName
	)

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

Synopsis [Creates PI terminal and net.]

Description []

SideEffects []

SeeAlso []

Definition at line 610 of file ioUtil.c.

{
    Abc_Obj_t * pNet, * pTerm;
    // get the PI net
    pNet  = Abc_NtkFindNet( pNtk, pName );
    if ( pNet )
        printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
    // add the PI node
    pTerm = Abc_NtkCreatePi( pNtk );
    Abc_ObjAddFanin( pNet, pTerm );
    return pTerm;
}

Abc_Obj_t* Io_ReadCreatePo	(	Abc_Ntk_t *	pNtk,
		char *	pName
	)

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

Synopsis [Creates PO terminal and net.]

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file ioUtil.c.

{
    Abc_Obj_t * pNet, * pTerm;
    // get the PO net
    pNet  = Abc_NtkFindNet( pNtk, pName );
    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
        printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
    // add the PO node
    pTerm = Abc_NtkCreatePo( pNtk );
    Abc_ObjAddFanin( pTerm, pNet );
    return pTerm;
}

Abc_Obj_t* Io_ReadCreateResetLatch	(	Abc_Ntk_t *	pNtk,
		int	fBlifMv
	)

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

Synopsis [Create the reset latch with data=1 and init=0.]

Description []

SideEffects []

SeeAlso []

Definition at line 693 of file ioUtil.c.

{
    Abc_Obj_t * pLatch, * pNode;
    Abc_Obj_t * pNetLI, * pNetLO;
    // create latch with 0 init value
//    pLatch = Io_ReadCreateLatch( pNtk, "_resetLI_", "_resetLO_" );
    pNetLI = Abc_NtkCreateNet( pNtk );
    pNetLO = Abc_NtkCreateNet( pNtk );
    Abc_ObjAssignName( pNetLI, Abc_ObjName(pNetLI), NULL );
    Abc_ObjAssignName( pNetLO, Abc_ObjName(pNetLO), NULL );
    pLatch = Io_ReadCreateLatch( pNtk, Abc_ObjName(pNetLI), Abc_ObjName(pNetLO) );
    // set the initial value
    Abc_LatchSetInit0( pLatch );
    // feed the latch with constant1- node
//    pNode = Abc_NtkCreateNode( pNtk );   
//    pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, "2\n1\n" );
    pNode = Abc_NtkCreateNodeConst1( pNtk );
    Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pNode );
    return pLatch;
}

Abc_Obj_t* Io_ReadCreateResetMux	(	Abc_Ntk_t *	pNtk,
		char *	pResetLO,
		char *	pDataLI,
		int	fBlifMv
	)

Abc_Ntk_t* Io_ReadEdif	(	char *	pFileName,
		int	fCheck
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Reads the network from an EDIF file.]

Description [Works only for the ISCAS benchmarks.]

SideEffects []

SeeAlso []

Definition at line 47 of file ioReadEdif.c.

{
    Extra_FileReader_t * p;
    Abc_Ntk_t * pNtk;

    printf( "Currently this parser does not work!\n" );
    return NULL;

    // start the file
    p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t()" );
    if ( p == NULL )
        return NULL;

    // read the network
    pNtk = Io_ReadEdifNetwork( p );
    Extra_FileReaderFree( p );
    if ( pNtk == NULL )
        return NULL;

    // make sure that everything is okay with the network structure
    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadEdif: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
        return NULL;
    }
    return pNtk;
}

Abc_Ntk_t* Io_ReadEqn	(	char *	pFileName,
		int	fCheck
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Reads the network from a BENCH file.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file ioReadEqn.c.

{
    Extra_FileReader_t * p;
    Abc_Ntk_t * pNtk;

    // start the file
    p = Extra_FileReaderAlloc( pFileName, "#", ";", "=" );
    if ( p == NULL )
        return NULL;

    // read the network
    pNtk = Io_ReadEqnNetwork( p );
    Extra_FileReaderFree( p );
    if ( pNtk == NULL )
        return NULL;

    // make sure that everything is okay with the network structure
    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadEqn: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
        return NULL;
    }
    return pNtk;
}

Io_FileType_t Io_ReadFileType

(

char *

pFileName

)

DECLARATIONS ///.

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

FileName [ioUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedures to write the network in BENCH format.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Returns the file type.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file ioUtil.c.

{
    char * pExt;
    if ( pFileName == NULL )
        return IO_FILE_NONE;
    pExt = Extra_FileNameExtension( pFileName );
    if ( pExt == NULL )
        return IO_FILE_NONE;
    if ( !strcmp( pExt, "aig" ) )
        return IO_FILE_AIGER;
    if ( !strcmp( pExt, "baf" ) )
        return IO_FILE_BAF;
    if ( !strcmp( pExt, "bblif" ) )
        return IO_FILE_BBLIF;
    if ( !strcmp( pExt, "blif" ) )
        return IO_FILE_BLIF;
    if ( !strcmp( pExt, "bench" ) )
        return IO_FILE_BENCH;
    if ( !strcmp( pExt, "cnf" ) )
        return IO_FILE_CNF;
    if ( !strcmp( pExt, "dot" ) )
        return IO_FILE_DOT;
    if ( !strcmp( pExt, "edif" ) )
        return IO_FILE_EDIF;
    if ( !strcmp( pExt, "eqn" ) )
        return IO_FILE_EQN;
    if ( !strcmp( pExt, "gml" ) )
        return IO_FILE_GML;
    if ( !strcmp( pExt, "list" ) )
        return IO_FILE_LIST;
    if ( !strcmp( pExt, "mv" ) )
        return IO_FILE_BLIFMV;
    if ( !strcmp( pExt, "pla" ) )
        return IO_FILE_PLA;
    if ( !strcmp( pExt, "smv" ) )
        return IO_FILE_SMV;
    if ( !strcmp( pExt, "v" ) )
        return IO_FILE_VERILOG;
    return IO_FILE_UNKNOWN;
}

Io_FileType_t Io_ReadLibType

(

char *

pFileName

)

Abc_Ntk_t* Io_ReadNetlist	(	char *	pFileName,
		Io_FileType_t	FileType,
		int	fCheck
	)

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

Synopsis [Read the network from a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file ioUtil.c.

{
    FILE * pFile;
    Abc_Ntk_t * pNtk;
    if ( FileType == IO_FILE_NONE || FileType == IO_FILE_UNKNOWN )
    {
        fprintf( stdout, "Generic file reader requires a known file extension to open \"%s\".\n", pFileName );
        return NULL;
    }
    // check if the file exists
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Cannot open input file \"%s\". ", pFileName );
        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" )) )
            fprintf( stdout, "Did you mean \"%s\"?", pFileName );
        fprintf( stdout, "\n" );
       return NULL;
    }
    fclose( pFile );
    // read the AIG
    if ( FileType == IO_FILE_AIGER || FileType == IO_FILE_BAF || FileType == IO_FILE_BBLIF )
    {
        if ( FileType == IO_FILE_AIGER )
            pNtk = Io_ReadAiger( pFileName, fCheck );
        else if ( FileType == IO_FILE_BAF )
            pNtk = Io_ReadBaf( pFileName, fCheck );
        else // if ( FileType == IO_FILE_BBLIF )
            pNtk = Io_ReadBblif( pFileName, fCheck );
        if ( pNtk == NULL )
        {
            fprintf( stdout, "Reading AIG from file has failed.\n" );
            return NULL;
        }
        return pNtk;
    }
    // read the new netlist
    if ( FileType == IO_FILE_BLIF )
//        pNtk = Io_ReadBlif( pFileName, fCheck );
        pNtk = Io_ReadBlifMv( pFileName, 0, fCheck );
    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
        pNtk = Io_ReadBlifMv( pFileName, 1, fCheck );
    else if ( FileType == IO_FILE_BENCH )
        pNtk = Io_ReadBench( pFileName, fCheck );
    else if ( FileType == IO_FILE_EDIF )
        pNtk = Io_ReadEdif( pFileName, fCheck );
    else if ( FileType == IO_FILE_EQN )
        pNtk = Io_ReadEqn( pFileName, fCheck );
    else if ( FileType == IO_FILE_PLA )
        pNtk = Io_ReadPla( pFileName, 0, fCheck );
    else if ( FileType == IO_FILE_VERILOG )
        pNtk = Io_ReadVerilog( pFileName, fCheck );
    else 
    {
        fprintf( stderr, "Unknown file format.\n" );
        return NULL;
    }
    if ( pNtk == NULL )
    {
        fprintf( stdout, "Reading network from file has failed.\n" );
        return NULL;
    }
    if ( fCheck && (Abc_NtkBlackboxNum(pNtk) || Abc_NtkWhiteboxNum(pNtk)) )
    {
        int i, fCycle = 0;
        Abc_Ntk_t * pModel;
        fprintf( stdout, "Warning: The network contains hierarchy.\n" );
        Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pModel, i )
                if ( !Abc_NtkIsAcyclicWithBoxes( pModel ) )
                    fCycle = 1;
        if ( fCycle )
        {
            Abc_NtkDelete( pNtk );
            return NULL;    
        }
    }
    return pNtk;
}

Abc_Ntk_t* Io_ReadPla	(	char *	pFileName,
		int	fZeros,
		int	fCheck
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Reads the network from a PLA file.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file ioReadPla.c.

{
    Extra_FileReader_t * p;
    Abc_Ntk_t * pNtk;

    // start the file
    p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t|" );
//    p = Extra_FileReaderAlloc( pFileName, "", "\n\r", " \t|" );
    if ( p == NULL )
        return NULL;

    // read the network
    pNtk = Io_ReadPlaNetwork( p, fZeros );
    Extra_FileReaderFree( p );
    if ( pNtk == NULL )
        return NULL;

    // make sure that everything is okay with the network structure
    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadPla: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
        return NULL;
    }
    return pNtk;
}

Abc_Ntk_t* Io_ReadVerilog	(	char *	pFileName,
		int	fCheck
	)

DECLARATIONS ///.

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

FileName [ioReadVerilog.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedure to read network from file.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Reads hierarchical design from the Verilog file.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file ioReadVerilog.c.

{
    Abc_Ntk_t * pNtk, * pTemp;
    Abc_Des_t * pDesign;
    int i, RetValue;

    // parse the verilog file
    pDesign = Ver_ParseFile( pFileName, NULL, fCheck, 1 );
    if ( pDesign == NULL )
        return NULL;

    // detect top-level model
    RetValue = Abc_DesFindTopLevelModels( pDesign );
    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
    if ( RetValue > 1 )
    {
        printf( "Warning: The design has %d root-level modules: ", Vec_PtrSize(pDesign->vTops) );
        Vec_PtrForEachEntry( Abc_Ntk_t *, pDesign->vTops, pTemp, i )
            printf( " %s", Abc_NtkName(pTemp) );
        printf( "\n" );
        printf( "The first one (%s) will be used.\n", pNtk->pName );
    }

    // extract the master network
    pNtk->pDesign = pDesign;
    pDesign->pManFunc = NULL;

    // verify the design for cyclic dependence
    assert( Vec_PtrSize(pDesign->vModules) > 0 );
    if ( Vec_PtrSize(pDesign->vModules) == 1 )
    {
//        printf( "Warning: The design is not hierarchical.\n" );
        Abc_DesFree( pDesign, pNtk );
        pNtk->pDesign = NULL;
        pNtk->pSpec = Extra_UtilStrsav( pFileName );
    }
    else
    {
        // check that there is no cyclic dependency
        Abc_NtkIsAcyclicHierarchy( pNtk );
    }

//Io_WriteVerilog( pNtk, "_temp.v" );
//    Abc_NtkPrintBoxInfo( pNtk );
    return pNtk;
}

void Io_Write	(	Abc_Ntk_t *	pNtk,
		char *	pFileName,
		Io_FileType_t	FileType
	)

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

Synopsis [Write the network into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file ioUtil.c.

{
    Abc_Ntk_t * pNtkTemp, * pNtkCopy;
    // check if the current network is available
    if ( pNtk == NULL )
    {
        fprintf( stdout, "Empty network.\n" );
        return;
    }
    // check if the file extension if given
    if ( FileType == IO_FILE_NONE || FileType == IO_FILE_UNKNOWN )
    {
        fprintf( stdout, "The generic file writer requires a known file extension.\n" );
        return;
    }
    // write the AIG formats
    if ( FileType == IO_FILE_AIGER || FileType == IO_FILE_BAF )
    {
        if ( !Abc_NtkIsStrash(pNtk) )
        {
            fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
            return;
        }
        if ( FileType == IO_FILE_AIGER )
            Io_WriteAiger( pNtk, pFileName, 1, 0, 0 );
        else //if ( FileType == IO_FILE_BAF )
            Io_WriteBaf( pNtk, pFileName );
        return;
    }
    // write non-netlist types
    if ( FileType == IO_FILE_CNF )
    {
        Io_WriteCnf( pNtk, pFileName, 0 );
        return;
    }
    if ( FileType == IO_FILE_DOT )
    {
        Io_WriteDot( pNtk, pFileName );
        return;
    }
    if ( FileType == IO_FILE_GML )
    {
        Io_WriteGml( pNtk, pFileName );
        return;
    }
    if ( FileType == IO_FILE_BBLIF )
    {
        if ( !Abc_NtkIsLogic(pNtk) )
        {
            fprintf( stdout, "Writing Binary BLIF is only possible for logic networks.\n" );
            return;
        }
        if ( !Abc_NtkHasSop(pNtk) )
            Abc_NtkToSop( pNtk, 0 );
        Io_WriteBblif( pNtk, pFileName );
        return;
    }
/*
    if ( FileType == IO_FILE_BLIFMV )
    {
        Io_WriteBlifMv( pNtk, pFileName );
        return;
    }
*/
    // convert logic network into netlist
    if ( FileType == IO_FILE_PLA )
    {
        if ( Abc_NtkLevel(pNtk) > 1 )
        {
            fprintf( stdout, "PLA writing is available for collapsed networks.\n" );
            return;
        }
        if ( Abc_NtkIsComb(pNtk) )
            pNtkTemp = Abc_NtkToNetlist( pNtk );
        else
        {
            fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
            pNtkCopy = Abc_NtkDup( pNtk );
            Abc_NtkMakeComb( pNtkCopy, 0 );
            pNtkTemp = Abc_NtkToNetlist( pNtk );
            Abc_NtkDelete( pNtkCopy );
        }
        if ( !Abc_NtkToSop( pNtkTemp, 1 ) )
            return;
    }
    else if ( FileType == IO_FILE_BENCH )
    {
        if ( !Abc_NtkIsStrash(pNtk) )
        {
            fprintf( stdout, "Writing traditional BENCH is available for AIGs only (use \"write_bench\").\n" );
            return;
        }
        pNtkTemp = Abc_NtkToNetlistBench( pNtk );
    }
    else if ( FileType == IO_FILE_SMV )
    {
        if ( !Abc_NtkIsStrash(pNtk) )
        {
            fprintf( stdout, "Writing traditional SMV is available for AIGs only.\n" );
            return;
        }
        pNtkTemp = Abc_NtkToNetlistBench( pNtk );
    }
    else
        pNtkTemp = Abc_NtkToNetlist( pNtk );

    if ( pNtkTemp == NULL )
    {
        fprintf( stdout, "Converting to netlist has failed.\n" );
        return;
    }

    if ( FileType == IO_FILE_BLIF )
    {
        if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
            Abc_NtkToSop( pNtkTemp, 0 );
        Io_WriteBlif( pNtkTemp, pFileName, 1, 0, 0 );
    }
    else if ( FileType == IO_FILE_BLIFMV )
    {
        if ( !Abc_NtkConvertToBlifMv( pNtkTemp ) )
            return;
        Io_WriteBlifMv( pNtkTemp, pFileName );
    }
    else if ( FileType == IO_FILE_BENCH )
        Io_WriteBench( pNtkTemp, pFileName );
    else if ( FileType == IO_FILE_BOOK )
        Io_WriteBook( pNtkTemp, pFileName );
    else if ( FileType == IO_FILE_PLA )
        Io_WritePla( pNtkTemp, pFileName );
    else if ( FileType == IO_FILE_EQN )
    {
        if ( !Abc_NtkHasAig(pNtkTemp) )
            Abc_NtkToAig( pNtkTemp );
        Io_WriteEqn( pNtkTemp, pFileName );
    }
    else if ( FileType == IO_FILE_SMV )
        Io_WriteSmv( pNtkTemp, pFileName );
    else if ( FileType == IO_FILE_VERILOG )
    {
        if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
            Abc_NtkToAig( pNtkTemp );
        Io_WriteVerilog( pNtkTemp, pFileName );
    }
    else 
        fprintf( stderr, "Unknown file format.\n" );
    Abc_NtkDelete( pNtkTemp );
}

void Io_WriteAiger	(	Abc_Ntk_t *	pNtk,
		char *	pFileName,
		int	fWriteSymbols,
		int	fCompact,
		int	fUnique
	)

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

Synopsis [Writes the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file ioWriteAiger.c.

{
    ProgressBar * pProgress;
//    FILE * pFile;
    Abc_Obj_t * pObj, * pDriver, * pLatch;
    int i, nNodes, nBufferSize, bzError, Pos, fExtended;
    unsigned char * pBuffer;
    unsigned uLit0, uLit1, uLit;
    bz2file b;

    // define unique writing
    if ( fUnique )
    {
        fWriteSymbols = 0;
        fCompact = 0;
    }

    fExtended = Abc_NtkConstrNum(pNtk);

    // check that the network is valid
    assert( Abc_NtkIsStrash(pNtk) );
    Abc_NtkForEachLatch( pNtk, pObj, i )
        if ( !Abc_LatchIsInit0(pObj) )
        {
            if ( !fCompact )
            {
                fExtended = 1;
                break;
            }
            fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
            return;
        }

    // write the GZ file
    if (!strncmp(pFileName+strlen(pFileName)-3,".gz",3)) 
    {
        Io_WriteAigerGz( pNtk, pFileName, fWriteSymbols );
        return;
    }

    memset(&b,0,sizeof(b));
    b.nBytesMax = (1<<12);
    b.buf = ABC_ALLOC( char,b.nBytesMax );

    // start the output stream
    b.f = fopen( pFileName, "wb" ); 
    if ( b.f == NULL )
    {
        fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName );
        ABC_FREE(b.buf);
        return;
    }
    if (!strncmp(pFileName+strlen(pFileName)-4,".bz2",4)) {
        b.b = BZ2_bzWriteOpen( &bzError, b.f, 9, 0, 0 );
        if ( bzError != BZ_OK ) {
            BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
            fprintf( stdout, "Ioa_WriteBlif(): Cannot start compressed stream.\n" );
            fclose( b.f );
            ABC_FREE(b.buf);
            return;
        }
    }

    // set the node numbers to be used in the output file
    nNodes = 0;
    Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Io_ObjSetAigerNum( pObj, nNodes++ );
    Abc_AigForEachAnd( pNtk, pObj, i )
        Io_ObjSetAigerNum( pObj, nNodes++ );

    // write the header "M I L O A" where M = I + L + A
    fprintfBz2Aig( &b, "aig%s %u %u %u %u %u", 
        fCompact? "2" : "",
        Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
        Abc_NtkPiNum(pNtk),
        Abc_NtkLatchNum(pNtk),
        fExtended ? 0 : Abc_NtkPoNum(pNtk),
        Abc_NtkNodeNum(pNtk) );
    // write the extended header "B C J F"
    if ( fExtended )
        fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
    fprintfBz2Aig( &b, "\n" );

    // if the driver node is a constant, we need to complement the literal below
    // because, in the AIGER format, literal 0/1 is represented as number 0/1
    // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0

    Abc_NtkInvertConstraints( pNtk );
    if ( !fCompact ) 
    {
        // write latch drivers
        Abc_NtkForEachLatch( pNtk, pLatch, i )
        {
            pObj = Abc_ObjFanin0(pLatch);
            pDriver = Abc_ObjFanin0(pObj);
            uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
            if ( Abc_LatchIsInit0(pLatch) )
                fprintfBz2Aig( &b, "%u\n", uLit );
            else if ( Abc_LatchIsInit1(pLatch) )
                fprintfBz2Aig( &b, "%u 1\n", uLit );
            else
            {
                // Both None and DC are written as 'uninitialized' e.g. a free boolean value
                assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
                fprintfBz2Aig( &b, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
            }
        }
        // write PO drivers
        Abc_NtkForEachPo( pNtk, pObj, i )
        {
            pDriver = Abc_ObjFanin0(pObj);
            fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
        }
    }
    else
    {
        Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
        Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
        if ( !b.b )
            fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), b.f );
        else
        {
            BZ2_bzWrite( &bzError, b.b, Vec_StrArray(vBinary), Vec_StrSize(vBinary) );
            if (bzError == BZ_IO_ERROR) {
                fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
                fclose( b.f );
                ABC_FREE(b.buf);
                Vec_StrFree( vBinary );
                return;
            }
        }
        Vec_StrFree( vBinary );
        Vec_IntFree( vLits );
    }
    Abc_NtkInvertConstraints( pNtk );

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
    pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
    Abc_AigForEachAnd( pNtk, pObj, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        uLit  = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
        uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
        uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
        if ( uLit0 > uLit1 )
        {
            unsigned Temp = uLit0;
            uLit0 = uLit1;
            uLit1 = Temp;
        }
        assert( uLit1 < uLit );
        Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit  - uLit1) );
        Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
        if ( Pos > nBufferSize - 10 )
        {
            printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
            fclose( b.f );
            ABC_FREE(b.buf);
            Extra_ProgressBarStop( pProgress );
            return;
        }
    }
    assert( Pos < nBufferSize );
    Extra_ProgressBarStop( pProgress );

    // write the buffer
    if ( !b.b )
        fwrite( pBuffer, 1, Pos, b.f );
    else
    {
        BZ2_bzWrite( &bzError, b.b, pBuffer, Pos );
        if (bzError == BZ_IO_ERROR) {
            fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
            fclose( b.f );
            ABC_FREE(b.buf);
            return;
        }
    }
    ABC_FREE( pBuffer );

    // write the symbol table
    if ( fWriteSymbols )
    {
        // write PIs
        Abc_NtkForEachPi( pNtk, pObj, i )
            fprintfBz2Aig( &b, "i%d %s\n", i, Abc_ObjName(pObj) );
        // write latches
        Abc_NtkForEachLatch( pNtk, pObj, i )
            fprintfBz2Aig( &b, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
        // write POs
        Abc_NtkForEachPo( pNtk, pObj, i )
            if ( !fExtended )
                fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) );
            else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
                fprintfBz2Aig( &b, "b%d %s\n", i, Abc_ObjName(pObj) );
            else
                fprintfBz2Aig( &b, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
    }

    // write the comment
    fprintfBz2Aig( &b, "c" );
    if ( !fUnique )
    {
        if ( pNtk->pName && strlen(pNtk->pName) > 0 )
            fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
        fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
        fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
    }

    // close the file
    if (b.b) {
        BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
        if (bzError == BZ_IO_ERROR) {
            fprintf( stdout, "Io_WriteAiger(): I/O error closing compressed stream.\n" );
            fclose( b.f );
            ABC_FREE(b.buf);
            return;
        }
    }
    fclose( b.f );
    ABC_FREE(b.buf);
}

void Io_WriteAigerCex	(	Abc_Cex_t *	pCex,
		Abc_Ntk_t *	pNtk,
		void *	pG,
		char *	pFileName
	)

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

Synopsis [Writes the AIG in the binary AIGER format.]

Description []

SideEffects []

SeeAlso []

Definition at line 880 of file ioWriteAiger.c.

{
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
    FILE * pFile;
    Aig_Man_t * pAig;
    Aig_Obj_t * pObj, * pObj2;
    Gia_Man_t * pGia = (Gia_Man_t *)pG;
    int k, f, b;
    assert( pCex != NULL );

    // derive AIG
    if ( pNtk != NULL && 
         Abc_NtkPiNum(pNtk)    == pCex->nPis && 
         Abc_NtkLatchNum(pNtk) == pCex->nRegs )
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
    }
    else if ( pGia != NULL && 
         Gia_ManPiNum(pGia)  == pCex->nPis && 
         Gia_ManRegNum(pGia) == pCex->nRegs )
    {
        pAig = Gia_ManToAigSimple( pGia );
    }
    else
    {
        printf( "AIG parameters do not match those of the CEX.\n" );
        return;
    }

    // create output file
    pFile = fopen( pFileName, "wb" );
    fprintf( pFile, "1\n" );
    b = pCex->nRegs;
    for ( k = 0; k < pCex->nRegs; k++ )
        fprintf( pFile, "0" );
    fprintf( pFile, " " );
    Aig_ManCleanMarkA( pAig );
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        for ( k = 0; k < pCex->nPis; k++ )
        {
            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData, b) );
            Aig_ManCi( pAig, k )->fMarkA = Abc_InfoHasBit(pCex->pData, b++);
        }
        fprintf( pFile, " " );
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) &
                           (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj));
        Saig_ManForEachPo( pAig, pObj, k )
            fprintf( pFile, "%d", pObj->fMarkA );
        fprintf( pFile, " " );
        Saig_ManForEachLi( pAig, pObj, k )
            fprintf( pFile, "%d", pObj->fMarkA );
        fprintf( pFile, "\n" );
        if ( f == pCex->iFrame )
            break;
        Saig_ManForEachLi( pAig, pObj, k )
            fprintf( pFile, "%d", pObj->fMarkA );
        fprintf( pFile, " " );
        Saig_ManForEachLiLo( pAig, pObj, pObj2, k )
            pObj2->fMarkA = pObj->fMarkA;
    }  
    assert( b == pCex->nBits );
    fclose( pFile );
    Aig_ManCleanMarkA( pAig );
    Aig_ManStop( pAig );
}

void Io_WriteBaf	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

DECLARATIONS ///.

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

FileName [ioWriteBaf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedures to write AIG in the binary format.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Writes the AIG in the binary format.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file ioWriteBaf.c.

{
    ProgressBar * pProgress;
    FILE * pFile;
    Abc_Obj_t * pObj;
    int i, nNodes, nAnds, nBufferSize;
    unsigned * pBufferNode;
    assert( Abc_NtkIsStrash(pNtk) );
    // start the output stream
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteBaf(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }

    // write the comment
    fprintf( pFile, "# BAF (Binary Aig Format) for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );

    // write the network name
    fprintf( pFile, "%s%c", pNtk->pName, 0 );
    // write the number of PIs
    fprintf( pFile, "%d%c", Abc_NtkPiNum(pNtk), 0 );
    // write the number of POs
    fprintf( pFile, "%d%c", Abc_NtkPoNum(pNtk), 0 );
    // write the number of latches
    fprintf( pFile, "%d%c", Abc_NtkLatchNum(pNtk), 0 );
    // write the number of internal nodes
    fprintf( pFile, "%d%c", Abc_NtkNodeNum(pNtk), 0 );

    // write PIs
    Abc_NtkForEachPi( pNtk, pObj, i )
        fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
    // write POs
    Abc_NtkForEachPo( pNtk, pObj, i )
        fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
    // write latches
    Abc_NtkForEachLatch( pNtk, pObj, i )
    {
        fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
        fprintf( pFile, "%s%c", Abc_ObjName(Abc_ObjFanin0(pObj)), 0 );
        fprintf( pFile, "%s%c", Abc_ObjName(Abc_ObjFanout0(pObj)), 0 );
    }

    // set the node numbers to be used in the output file
    Abc_NtkCleanCopy( pNtk );
    nNodes = 1;
    Abc_NtkForEachCi( pNtk, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)nNodes++;
    Abc_AigForEachAnd( pNtk, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)nNodes++;

    // write the nodes into the buffer
    nAnds = 0;
    nBufferSize = Abc_NtkNodeNum(pNtk) * 2 + Abc_NtkCoNum(pNtk);
    pBufferNode = ABC_ALLOC( unsigned, nBufferSize );
    pProgress = Extra_ProgressBarStart( stdout, nBufferSize );
    Abc_AigForEachAnd( pNtk, pObj, i )
    {
        Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
        pBufferNode[nAnds++] = (((int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | (int)Abc_ObjFaninC0(pObj);
        pBufferNode[nAnds++] = (((int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy) << 1) | (int)Abc_ObjFaninC1(pObj);
    }

    // write the COs into the buffer
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
        pBufferNode[nAnds] = (((int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | (int)Abc_ObjFaninC0(pObj);
        if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) )
            pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((int)(ABC_PTRINT_T)Abc_ObjData(Abc_ObjFanout0(pObj)) & 3);
        nAnds++;
    }
    Extra_ProgressBarStop( pProgress );
    assert( nBufferSize == nAnds );

    // write the buffer
    fwrite( pBufferNode, 1, sizeof(int) * nBufferSize, pFile );
    fclose( pFile );
    ABC_FREE( pBufferNode );
}

void Io_WriteBblif	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

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

Synopsis [Writes the AIG in the binary format.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file ioWriteBblif.c.

{
    Bbl_Man_t * p;
    p = Bbl_ManFromAbc( pNtk );
//Bbl_ManPrintStats( p );
//Bbl_ManDumpBlif( p, "test_bbl.blif" );
    Bbl_ManDumpBinaryBlif( p, pFileName );
    Bbl_ManStop( p );
}

int Io_WriteBench	(	Abc_Ntk_t *	pNtk,
		const char *	pFileName
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Writes the network in BENCH format.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file ioWriteBench.c.

{
    Abc_Ntk_t * pExdc;
    FILE * pFile;
    assert( Abc_NtkIsSopNetlist(pNtk) );
    if ( !Io_WriteBenchCheckNames(pNtk) )
    {
        fprintf( stdout, "Io_WriteBench(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
        return 0;
    }
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
        return 0;
    }
    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the network
    Io_WriteBenchOne( pFile, pNtk );
    // write EXDC network if it exists
    pExdc = Abc_NtkExdc( pNtk );
    if ( pExdc )
        printf( "Io_WriteBench: EXDC is not written (warning).\n" );
    // finalize the file
    fclose( pFile );
    return 1;
}

int Io_WriteBenchLut	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

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

Synopsis [Writes the network in BENCH format with LUTs and DFFRSE.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file ioWriteBench.c.

{
    Abc_Ntk_t * pExdc;
    FILE * pFile;
    assert( Abc_NtkIsAigNetlist(pNtk) );
    if ( !Io_WriteBenchCheckNames(pNtk) )
    {
        fprintf( stdout, "Io_WriteBenchLut(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
        return 0;
    }
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
        return 0;
    }
    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the network
    Io_WriteBenchLutOne( pFile, pNtk );
    // write EXDC network if it exists
    pExdc = Abc_NtkExdc( pNtk );
    if ( pExdc )
        printf( "Io_WriteBench: EXDC is not written (warning).\n" );
    // finalize the file
    fclose( pFile );
    return 1;
}

void Io_WriteBlif	(	Abc_Ntk_t *	pNtk,
		char *	FileName,
		int	fWriteLatches,
		int	fBb2Wb,
		int	fSeq
	)

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

Synopsis [Write the network into a BLIF file with the given name.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file ioWriteBlif.c.

{
    FILE * pFile;
    Abc_Ntk_t * pNtkTemp;
    int i;
    assert( Abc_NtkIsNetlist(pNtk) );
    // start writing the file
    pFile = fopen( FileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteBlif(): Cannot open the output file.\n" );
        return;
    }
    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the master network
    Io_NtkWrite( pFile, pNtk, fWriteLatches, fBb2Wb, fSeq );
    // make sure there is no logic hierarchy
//    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
    // write the hierarchy if present
    if ( Abc_NtkBlackboxNum(pNtk) > 0 || Abc_NtkWhiteboxNum(pNtk) > 0 )
    {
        Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNtkTemp, i )
        {
            if ( pNtkTemp == pNtk )
                continue;
            fprintf( pFile, "\n\n" );
            Io_NtkWrite( pFile, pNtkTemp, fWriteLatches, fBb2Wb, fSeq );
        }
    }
    fclose( pFile );
}

void Io_WriteBlifLogic	(	Abc_Ntk_t *	pNtk,
		char *	FileName,
		int	fWriteLatches
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Write the network into a BLIF file with the given name.]

Description []

SideEffects []

SeeAlso []

Definition at line 59 of file ioWriteBlif.c.

{
    Abc_Ntk_t * pNtkTemp;
    // derive the netlist
    pNtkTemp = Abc_NtkToNetlist(pNtk);
    if ( pNtkTemp == NULL )
    {
        fprintf( stdout, "Writing BLIF has failed.\n" );
        return;
    }
    Io_WriteBlif( pNtkTemp, FileName, fWriteLatches, 0, 0 );
    Abc_NtkDelete( pNtkTemp );
}

void Io_WriteBlifMv	(	Abc_Ntk_t *	pNtk,
		char *	FileName
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Write the network into a BLIF file with the given name.]

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file ioWriteBlifMv.c.

{
    FILE * pFile;
    Abc_Ntk_t * pNtkTemp;
    int i;
    assert( Abc_NtkIsNetlist(pNtk) );
    assert( Abc_NtkHasBlifMv(pNtk) );
    // start writing the file
    pFile = fopen( FileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteBlifMv(): Cannot open the output file.\n" );
        return;
    }
    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the master network
    Io_NtkWriteBlifMv( pFile, pNtk );
    // write the remaining networks
    if ( pNtk->pDesign )
    {
        Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNtkTemp, i )
        {
            if ( pNtkTemp == pNtk )
                continue;
            fprintf( pFile, "\n\n" );
            Io_NtkWriteBlifMv( pFile, pNtkTemp );
        }
    }
    fclose( pFile );
}

void Io_WriteBlifSpecial	(	Abc_Ntk_t *	pNtk,
		char *	FileName,
		char *	pLutStruct,
		int	fUseHie
	)

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

Synopsis [Write the network into a BLIF file with the given name.]

Description []

SideEffects []

SeeAlso []

Definition at line 1378 of file ioWriteBlif.c.

{
    Abc_Ntk_t * pNtkTemp;
    assert( Abc_NtkIsLogic(pNtk) );
    Abc_NtkToSop( pNtk, 0 );
    // derive the netlist
    pNtkTemp = Abc_NtkToNetlist(pNtk);
    if ( pNtkTemp == NULL )
    {
        fprintf( stdout, "Writing BLIF has failed.\n" );
        return;
    }
    if ( pLutStruct && fUseHie )
        Io_WriteBlifInt( pNtkTemp, FileName, pLutStruct, 1 );
    else
        Io_WriteBlifInt( pNtkTemp, FileName, pLutStruct, 0 );
    Abc_NtkDelete( pNtkTemp );
}

void Io_WriteBook	(	Abc_Ntk_t *	pNtk,
		char *	FileName
	)

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

Synopsis [Write the network into a BOOK file with the given name.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file ioWriteBook.c.

{

    FILE * pFileNodes, * pFileNets, * pFileAux;
    FILE * pFileScl, * pFilePl, * pFileWts;
    char * FileExt = ABC_CALLOC( char, strlen(FileName)+7 );
    unsigned coreCellArea=0;
    Abc_Ntk_t * pExdc, * pNtkTemp;
    int i;

    assert( Abc_NtkIsNetlist(pNtk) );
    // start writing the files
    strcpy(FileExt, FileName);
    pFileNodes = fopen( strcat(FileExt,".nodes"), "w" );
    strcpy(FileExt, FileName);
    pFileNets  = fopen( strcat(FileExt,".nets"), "w" );
    strcpy(FileExt, FileName);
    pFileAux   = fopen( strcat(FileExt,".aux"), "w" );

        // write the aux file
    if ( (pFileNodes == NULL) || (pFileNets == NULL) || (pFileAux == NULL) )
    {
        fclose( pFileAux );
        fprintf( stdout, "Io_WriteBook(): Cannot open the output files.\n" );
        return;
    }
    fprintf( pFileAux, "RowBasedPlacement : %s.nodes %s.nets %s.scl %s.pl %s.wts", 
         FileName, FileName, FileName, FileName, FileName );
    fclose( pFileAux );

    // write the master network
    coreCellArea+=Io_NtkWriteNodes( pFileNodes, pNtk );
    Io_NtkWriteNets( pFileNets, pNtk );

    // write EXDC network if it exists
    pExdc = Abc_NtkExdc( pNtk );
    if ( pExdc )
    {
    coreCellArea+=Io_NtkWriteNodes( pFileNodes, pNtk );
        Io_NtkWriteNets( pFileNets, pNtk );
    }

    // make sure there is no logic hierarchy
    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );

    // write the hierarchy if present
    if ( Abc_NtkBlackboxNum(pNtk) > 0 )
    {
        Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNtkTemp, i )
        {
            if ( pNtkTemp == pNtk )
                continue;
            coreCellArea+=Io_NtkWriteNodes( pFileNodes, pNtkTemp );
            Io_NtkWriteNets( pFileNets, pNtkTemp );
        }
    }
    fclose( pFileNodes );
    fclose( pFileNets );

    strcpy(FileExt, FileName);
    pFileScl = fopen( strcat(FileExt,".scl"), "w" );
    strcpy(FileExt, FileName);
    pFilePl  = fopen( strcat(FileExt,".pl"), "w" );
    strcpy(FileExt, FileName);
    pFileWts   = fopen( strcat(FileExt,".wts"), "w" );
    ABC_FREE(FileExt);

    Io_NtkBuildLayout( pFileScl, pFilePl, pNtk, 1.0, 10, coreCellArea );
    fclose( pFileScl );
    fclose( pFilePl );
    fclose( pFileWts );
}

int Io_WriteCnf	(	Abc_Ntk_t *	pNtk,
		char *	pFileName,
		int	fAllPrimes
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Write the miter cone into a CNF file for the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file ioWriteCnf.c.

{
    sat_solver * pSat;
    if ( Abc_NtkIsStrash(pNtk) )
        printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" );
    else
        printf( "Io_WriteCnf() warning: Generating CNF by convering logic nodes into CNF clauses.\n" );
    if ( Abc_NtkPoNum(pNtk) != 1 )
    {
        fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" );
        return 0;
    }
    if ( Abc_NtkLatchNum(pNtk) != 0 )
    {
        fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" );
        return 0;
    }
    if ( Abc_NtkNodeNum(pNtk) == 0 )
    {
        fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" );
        return 0;
    }
    // convert to logic BDD network
    if ( Abc_NtkIsLogic(pNtk) )
        Abc_NtkToBdd( pNtk );
    // create solver with clauses
    pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
    if ( pSat == NULL )
    {
        fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
        return 1;
    }        
    // write the clauses
    s_pNtk = pNtk;
    Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
    s_pNtk = NULL;
    // free the solver
    sat_solver_delete( pSat );
    return 1;
}

void Io_WriteDot	(	Abc_Ntk_t *	pNtk,
		char *	FileName
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Writes the graph structure of network for DOT.]

Description [Useful for graph visualization using tools such as GraphViz: http://www.graphviz.org/]

SideEffects []

SeeAlso []

Definition at line 51 of file ioWriteDot.c.

{
    Vec_Ptr_t * vNodes;
    vNodes = Abc_NtkCollectObjects( pNtk );
    Io_WriteDotNtk( pNtk, vNodes, NULL, FileName, 0, 0 );
    Vec_PtrFree( vNodes );
}

void Io_WriteDotNtk	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t *	vNodes,
		Vec_Ptr_t *	vNodesShow,
		char *	pFileName,
		int	fGateNames,
		int	fUseReverse
	)

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

Synopsis [Writes the graph structure of network for DOT.]

Description [Useful for graph visualization using tools such as GraphViz: http://www.graphviz.org/]

SideEffects []

SeeAlso []

Definition at line 71 of file ioWriteDot.c.

{
    FILE * pFile;
    Abc_Obj_t * pNode, * pFanin;
    char * pSopString;
    int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
    int Limit = 300;

    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );

    if ( vNodes->nSize < 1 )
    {
        printf( "The set has no nodes. DOT file is not written.\n" );
        return;
    }

    if ( vNodes->nSize > Limit )
    {
        printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
        return;
    }

    // start the stream
    if ( (pFile = fopen( pFileName, "w" )) == NULL )
    {
        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
        return;
    }

    // transform logic functions from BDD to SOP
    if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
    {
        if ( !Abc_NtkBddToSop(pNtk, 0) )
        {
            printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
            return;
        }
    }

    // mark the nodes from the set
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        pNode->fMarkC = 1;
    if ( vNodesShow )
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
            pNode->fMarkB = 1;

    // get the levels of nodes
    LevelMax = Abc_NtkLevel( pNtk );
    if ( fUseReverse )
    {
        LevelMin = Abc_NtkLevelReverse( pNtk );
        assert( LevelMax == LevelMin );
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
            if ( Abc_ObjIsNode(pNode) )
                pNode->Level = LevelMax - pNode->Level + 1;
    }

    // find the largest and the smallest levels
    LevelMin = 10000;
    LevelMax = -1;
    fHasCos  = 0;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( Abc_ObjIsCo(pNode) )
        {
            fHasCos = 1;
            continue;
        }
        if ( LevelMin > (int)pNode->Level )
            LevelMin = pNode->Level;
        if ( LevelMax < (int)pNode->Level )
            LevelMax = pNode->Level;
    }

    // set the level of the CO nodes
    if ( fHasCos )
    {
        LevelMax++;
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( Abc_ObjIsCo(pNode) )
                pNode->Level = LevelMax;
        }
    }

    // write the DOT header
    fprintf( pFile, "# %s\n",  "Network structure generated by ABC" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "digraph network {\n" );
    fprintf( pFile, "size = \"7.5,10\";\n" );
//    fprintf( pFile, "size = \"10,8.5\";\n" );
//    fprintf( pFile, "size = \"14,11\";\n" );
//    fprintf( pFile, "page = \"8,11\";\n" );
//  fprintf( pFile, "ranksep = 0.5;\n" );
//  fprintf( pFile, "nodesep = 0.5;\n" );
    fprintf( pFile, "center = true;\n" );
//    fprintf( pFile, "orientation = landscape;\n" );
//  fprintf( pFile, "edge [fontsize = 10];\n" );
//  fprintf( pFile, "edge [dir = none];\n" );
    fprintf( pFile, "edge [dir = back];\n" );
    fprintf( pFile, "\n" );

    // labels on the left of the picture
    fprintf( pFile, "{\n" );
    fprintf( pFile, "  node [shape = plaintext];\n" );
    fprintf( pFile, "  edge [style = invis];\n" );
    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
    // generate node names with labels
    for ( Level = LevelMax; Level >= LevelMin; Level-- )
    {
        // the visible node name
        fprintf( pFile, "  Level%d", Level );
        fprintf( pFile, " [label = " );
        // label name
        fprintf( pFile, "\"" );
        fprintf( pFile, "\"" );
        fprintf( pFile, "];\n" );
    }

    // genetate the sequence of visible/invisible nodes to mark levels
    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
    for ( Level = LevelMax; Level >= LevelMin; Level-- )
    {
        // the visible node name
        fprintf( pFile, "  Level%d",  Level );
        // the connector
        if ( Level != LevelMin )
            fprintf( pFile, " ->" );
        else
            fprintf( pFile, ";" );
    }
    fprintf( pFile, "\n" );
    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate title box on top
    fprintf( pFile, "{\n" );
    fprintf( pFile, "  rank = same;\n" );
    fprintf( pFile, "  LevelTitle1;\n" );
    fprintf( pFile, "  title1 [shape=plaintext,\n" );
    fprintf( pFile, "          fontsize=20,\n" );
    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
    fprintf( pFile, "          label=\"" );
    fprintf( pFile, "%s", "Network structure visualized by ABC" );
    fprintf( pFile, "\\n" );
    fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
    fprintf( pFile, "\"\n" );
    fprintf( pFile, "         ];\n" );
    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate statistics box
    fprintf( pFile, "{\n" );
    fprintf( pFile, "  rank = same;\n" );
    fprintf( pFile, "  LevelTitle2;\n" );
    fprintf( pFile, "  title2 [shape=plaintext,\n" );
    fprintf( pFile, "          fontsize=18,\n" );
    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
    fprintf( pFile, "          label=\"" );
    if ( Abc_NtkObjNum(pNtk) == Vec_PtrSize(vNodes) )
        fprintf( pFile, "The network contains %d logic nodes and %d latches.", Abc_NtkNodeNum(pNtk), Abc_NtkLatchNum(pNtk) );
    else
        fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Abc_NtkCountLogicNodes(vNodes), LevelMax - LevelMin + 1 );
    fprintf( pFile, "\\n" );
    fprintf( pFile, "\"\n" );
    fprintf( pFile, "         ];\n" );
    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate the POs
    if ( fHasCos )
    {
        fprintf( pFile, "{\n" );
        fprintf( pFile, "  rank = same;\n" );
        // the labeling node of this level
        fprintf( pFile, "  Level%d;\n",  LevelMax );
        // generate the PO nodes
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( !Abc_ObjIsCo(pNode) )
                continue;
            fprintf( pFile, "  Node%d [label = \"%s%s\"", 
                pNode->Id, 
                (Abc_ObjIsBi(pNode)? Abc_ObjName(Abc_ObjFanout0(pNode)):Abc_ObjName(pNode)), 
                (Abc_ObjIsBi(pNode)? "_in":"") );
            fprintf( pFile, ", shape = %s", (Abc_ObjIsBi(pNode)? "box":"invtriangle") );
            if ( pNode->fMarkB )
                fprintf( pFile, ", style = filled" );
            fprintf( pFile, ", color = coral, fillcolor = coral" );
            fprintf( pFile, "];\n" );
        }
        fprintf( pFile, "}" );
        fprintf( pFile, "\n" );
        fprintf( pFile, "\n" );
    }

    // generate nodes of each rank
    for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
    {
        fprintf( pFile, "{\n" );
        fprintf( pFile, "  rank = same;\n" );
        // the labeling node of this level
        fprintf( pFile, "  Level%d;\n",  Level );
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( (int)pNode->Level != Level )
                continue;
            if ( Abc_ObjFaninNum(pNode) == 0 )
                continue;

/*
            int SuppSize;
            Vec_Ptr_t * vSupp;
            if ( (int)pNode->Level != Level )
                continue;
            if ( Abc_ObjFaninNum(pNode) == 0 )
                continue;
            vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 );
            SuppSize = Vec_PtrSize( vSupp );
            Vec_PtrFree( vSupp ); 
*/

//            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
            if ( Abc_NtkIsStrash(pNtk) )
                pSopString = "";
            else if ( Abc_NtkHasMapping(pNtk) && fGateNames )
                pSopString = Mio_GateReadName((Mio_Gate_t *)pNode->pData);
            else if ( Abc_NtkHasMapping(pNtk) )
                pSopString = Abc_NtkPrintSop(Mio_GateReadSop((Mio_Gate_t *)pNode->pData));
            else
                pSopString = Abc_NtkPrintSop((char *)pNode->pData);
            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
//            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, 
//                SuppSize, 
//                pSopString );

            fprintf( pFile, ", shape = ellipse" );
            if ( pNode->fMarkB )
                fprintf( pFile, ", style = filled" );
            fprintf( pFile, "];\n" );
        }
        fprintf( pFile, "}" );
        fprintf( pFile, "\n" );
        fprintf( pFile, "\n" );
    }

    // generate the PI nodes if any
    if ( LevelMin == 0 )
    {
        fprintf( pFile, "{\n" );
        fprintf( pFile, "  rank = same;\n" );
        // the labeling node of this level
        fprintf( pFile, "  Level%d;\n",  LevelMin );
        // generate the PO nodes
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( !Abc_ObjIsCi(pNode) )
            {
                // check if the costant node is present
                if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 )
                {
                    fprintf( pFile, "  Node%d [label = \"Const%d\"", pNode->Id, Abc_NtkIsStrash(pNode->pNtk) || Abc_NodeIsConst1(pNode) );
                    fprintf( pFile, ", shape = ellipse" );
                    if ( pNode->fMarkB )
                        fprintf( pFile, ", style = filled" );
                    fprintf( pFile, ", color = coral, fillcolor = coral" );
                    fprintf( pFile, "];\n" );
                }
                continue;
            }
            fprintf( pFile, "  Node%d [label = \"%s\"", 
                pNode->Id, 
                (Abc_ObjIsBo(pNode)? Abc_ObjName(Abc_ObjFanin0(pNode)):Abc_ObjName(pNode)) );
            fprintf( pFile, ", shape = %s", (Abc_ObjIsBo(pNode)? "box":"triangle") );
            if ( pNode->fMarkB )
                fprintf( pFile, ", style = filled" );
            fprintf( pFile, ", color = coral, fillcolor = coral" );
            fprintf( pFile, "];\n" );
        }
        fprintf( pFile, "}" );
        fprintf( pFile, "\n" );
        fprintf( pFile, "\n" );
    }

    // generate invisible edges from the square down
    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( (int)pNode->Level != LevelMax )
            continue;
        fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
    }
    // generate invisible edges among the COs
    Prev = -1;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( (int)pNode->Level != LevelMax )
            continue;
        if ( !Abc_ObjIsPo(pNode) )
            continue;
        if ( Prev >= 0 )
            fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, pNode->Id );
        Prev = pNode->Id;
    }

    // generate edges
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( Abc_ObjIsLatch(pNode) )
            continue;
        Abc_ObjForEachFanin( pNode, pFanin, k )
        {
            if ( Abc_ObjIsLatch(pFanin) )
                continue;
            fCompl = 0;
            if ( Abc_NtkIsStrash(pNtk) )
                fCompl = Abc_ObjFaninC(pNode, k);
            // generate the edge from this node to the next
            fprintf( pFile, "Node%d",  pNode->Id );
            fprintf( pFile, " -> " );
            fprintf( pFile, "Node%d",  pFanin->Id );
            fprintf( pFile, " [style = %s", fCompl? "dotted" : "bold" );
//            fprintf( pFile, ", label = \"%c\"", 'a' + k );
            fprintf( pFile, "]" );
            fprintf( pFile, ";\n" );
        }
    }

    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );
    fclose( pFile );

    // unmark the nodes from the set
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        pNode->fMarkC = 0;
    if ( vNodesShow )
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
            pNode->fMarkB = 0;

    // convert the network back into BDDs if this is how it was
    if ( fHasBdds )
        Abc_NtkSopToBdd(pNtk);
}

void Io_WriteDotSeq	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t *	vNodes,
		Vec_Ptr_t *	vNodesShow,
		char *	pFileName,
		int	fGateNames,
		int	fUseReverse
	)

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

Synopsis [Writes the graph structure of network for DOT.]

Description [Useful for graph visualization using tools such as GraphViz: http://www.graphviz.org/]

SideEffects []

SeeAlso []

Definition at line 434 of file ioWriteDot.c.

{
    FILE * pFile;
    Abc_Obj_t * pNode, * pFanin;
    char * pSopString;
    int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
    int Limit = 300;

    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );

    if ( vNodes->nSize < 1 )
    {
        printf( "The set has no nodes. DOT file is not written.\n" );
        return;
    }

    if ( vNodes->nSize > Limit )
    {
        printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
        return;
    }

    // start the stream
    if ( (pFile = fopen( pFileName, "w" )) == NULL )
    {
        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
        return;
    }

    // transform logic functions from BDD to SOP
    if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
    {
        if ( !Abc_NtkBddToSop(pNtk, 0) )
        {
            printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
            return;
        }
    }

    // mark the nodes from the set
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        pNode->fMarkC = 1;
    if ( vNodesShow )
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
            pNode->fMarkB = 1;

    // get the levels of nodes
    LevelMax = Abc_NtkLevel( pNtk );
    if ( fUseReverse )
    {
        LevelMin = Abc_NtkLevelReverse( pNtk );
        assert( LevelMax == LevelMin );
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
            if ( Abc_ObjIsNode(pNode) )
                pNode->Level = LevelMax - pNode->Level + 1;
    }

    // find the largest and the smallest levels
    LevelMin = 10000;
    LevelMax = -1;
    fHasCos  = 0;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( Abc_ObjIsCo(pNode) )
        {
            fHasCos = 1;
            continue;
        }
        if ( LevelMin > (int)pNode->Level )
            LevelMin = pNode->Level;
        if ( LevelMax < (int)pNode->Level )
            LevelMax = pNode->Level;
    }

    // set the level of the CO nodes
    if ( fHasCos )
    {
        LevelMax++;
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( Abc_ObjIsCo(pNode) )
                pNode->Level = LevelMax;
        }
    }

    // write the DOT header
    fprintf( pFile, "# %s\n",  "Network structure generated by ABC" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "digraph network {\n" );
    fprintf( pFile, "size = \"7.5,10\";\n" );
//    fprintf( pFile, "size = \"10,8.5\";\n" );
//    fprintf( pFile, "size = \"14,11\";\n" );
//    fprintf( pFile, "page = \"8,11\";\n" );
//  fprintf( pFile, "ranksep = 0.5;\n" );
//  fprintf( pFile, "nodesep = 0.5;\n" );
    fprintf( pFile, "center = true;\n" );
//    fprintf( pFile, "orientation = landscape;\n" );
//  fprintf( pFile, "edge [fontsize = 10];\n" );
//  fprintf( pFile, "edge [dir = none];\n" );
    fprintf( pFile, "edge [dir = back];\n" );
    fprintf( pFile, "\n" );

    // labels on the left of the picture
    fprintf( pFile, "{\n" );
    fprintf( pFile, "  node [shape = plaintext];\n" );
    fprintf( pFile, "  edge [style = invis];\n" );
    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
    // generate node names with labels
    for ( Level = LevelMax; Level >= LevelMin; Level-- )
    {
        // the visible node name
        fprintf( pFile, "  Level%d", Level );
        fprintf( pFile, " [label = " );
        // label name
        fprintf( pFile, "\"" );
        fprintf( pFile, "\"" );
        fprintf( pFile, "];\n" );
    }

    // genetate the sequence of visible/invisible nodes to mark levels
    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
    for ( Level = LevelMax; Level >= LevelMin; Level-- )
    {
        // the visible node name
        fprintf( pFile, "  Level%d",  Level );
        // the connector
        if ( Level != LevelMin )
            fprintf( pFile, " ->" );
        else
            fprintf( pFile, ";" );
    }
    fprintf( pFile, "\n" );
    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate title box on top
    fprintf( pFile, "{\n" );
    fprintf( pFile, "  rank = same;\n" );
    fprintf( pFile, "  LevelTitle1;\n" );
    fprintf( pFile, "  title1 [shape=plaintext,\n" );
    fprintf( pFile, "          fontsize=20,\n" );
    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
    fprintf( pFile, "          label=\"" );
    fprintf( pFile, "%s", "Network structure visualized by ABC" );
    fprintf( pFile, "\\n" );
    fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
    fprintf( pFile, "\"\n" );
    fprintf( pFile, "         ];\n" );
    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate statistics box
    fprintf( pFile, "{\n" );
    fprintf( pFile, "  rank = same;\n" );
    fprintf( pFile, "  LevelTitle2;\n" );
    fprintf( pFile, "  title2 [shape=plaintext,\n" );
    fprintf( pFile, "          fontsize=18,\n" );
    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
    fprintf( pFile, "          label=\"" );
    if ( Abc_NtkObjNum(pNtk) == Vec_PtrSize(vNodes) )
        fprintf( pFile, "The network contains %d logic nodes and %d latches.", Abc_NtkNodeNum(pNtk), Abc_NtkLatchNum(pNtk) );
    else
        fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Abc_NtkCountLogicNodes(vNodes), LevelMax - LevelMin + 1 );
    fprintf( pFile, "\\n" );
    fprintf( pFile, "\"\n" );
    fprintf( pFile, "         ];\n" );
    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate the POs
    if ( fHasCos )
    {
        fprintf( pFile, "{\n" );
        fprintf( pFile, "  rank = same;\n" );
        // the labeling node of this level
        fprintf( pFile, "  Level%d;\n",  LevelMax );
        // generate the PO nodes
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( !Abc_ObjIsPo(pNode) )
                continue;
            fprintf( pFile, "  Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
            fprintf( pFile, ", shape = %s", "invtriangle" );
            if ( pNode->fMarkB )
                fprintf( pFile, ", style = filled" );
            fprintf( pFile, ", color = coral, fillcolor = coral" );
            fprintf( pFile, "];\n" );
        }
        fprintf( pFile, "}" );
        fprintf( pFile, "\n" );
        fprintf( pFile, "\n" );
    }

    // generate nodes of each rank
    for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
    {
        fprintf( pFile, "{\n" );
        fprintf( pFile, "  rank = same;\n" );
        // the labeling node of this level
        fprintf( pFile, "  Level%d;\n",  Level );
        Abc_NtkForEachNode( pNtk, pNode, i )
        {
            if ( (int)pNode->Level != Level )
                continue;
//            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
            if ( Abc_NtkIsStrash(pNtk) )
                pSopString = "";
            else if ( Abc_NtkHasMapping(pNtk) && fGateNames )
                pSopString = Mio_GateReadName((Mio_Gate_t *)pNode->pData);
            else if ( Abc_NtkHasMapping(pNtk) )
                pSopString = Abc_NtkPrintSop(Mio_GateReadSop((Mio_Gate_t *)pNode->pData));
            else
                pSopString = Abc_NtkPrintSop((char *)pNode->pData);
            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );

            fprintf( pFile, ", shape = ellipse" );
            if ( pNode->fMarkB )
                fprintf( pFile, ", style = filled" );
            fprintf( pFile, "];\n" );
        }
        fprintf( pFile, "}" );
        fprintf( pFile, "\n" );
        fprintf( pFile, "\n" );
    }

    // generate the PI nodes if any
    if ( LevelMin == 0 )
    {
        fprintf( pFile, "{\n" );
        fprintf( pFile, "  rank = same;\n" );
        // the labeling node of this level
        fprintf( pFile, "  Level%d;\n",  LevelMin );
        // generate the PO nodes
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        {
            if ( pNode->Level > 0 )
                continue;
            if ( !Abc_ObjIsPi(pNode) )
            {
                // check if the costant node is present
                if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 )
                {
                    fprintf( pFile, "  Node%d [label = \"Const1\"", pNode->Id );
                    fprintf( pFile, ", shape = ellipse" );
                    if ( pNode->fMarkB )
                        fprintf( pFile, ", style = filled" );
                    fprintf( pFile, ", color = coral, fillcolor = coral" );
                    fprintf( pFile, "];\n" );
                }
                continue;
            }
            fprintf( pFile, "  Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
            fprintf( pFile, ", shape = %s", "triangle" );
            if ( pNode->fMarkB )
                fprintf( pFile, ", style = filled" );
            fprintf( pFile, ", color = coral, fillcolor = coral" );
            fprintf( pFile, "];\n" );
        }
        fprintf( pFile, "}" );
        fprintf( pFile, "\n" );
        fprintf( pFile, "\n" );
    }

//    fprintf( pFile, "{\n" );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( !Abc_ObjIsLatch(pNode) )
            continue;
        fprintf( pFile, "Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
        fprintf( pFile, ", shape = box" );
        if ( pNode->fMarkB )
            fprintf( pFile, ", style = filled" );
        fprintf( pFile, ", color = coral, fillcolor = coral" );
        fprintf( pFile, "];\n" );
    }
//    fprintf( pFile, "}" );
//    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );

    // generate invisible edges from the square down
    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( (int)pNode->Level != LevelMax )
            continue;
        if ( !Abc_ObjIsPo(pNode) )
            continue;
        fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
    }
    // generate invisible edges among the COs
    Prev = -1;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( (int)pNode->Level != LevelMax )
            continue;
        if ( !Abc_ObjIsPo(pNode) )
            continue;
        if ( Prev >= 0 )
            fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, pNode->Id );
        Prev = pNode->Id;
    }

    // generate edges
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( Abc_ObjIsBi(pNode) || Abc_ObjIsBo(pNode) )
            continue;
        Abc_ObjForEachFanin( pNode, pFanin, k )
        {
            fCompl = 0;
            if ( Abc_NtkIsStrash(pNtk) )
            {
                if ( Abc_ObjIsBi(pFanin) )
                    fCompl = Abc_ObjFaninC(pFanin, k);
                else
                    fCompl = Abc_ObjFaninC(pNode, k);
            }
            if ( Abc_ObjIsBi(pFanin) || Abc_ObjIsBo(pFanin) )
                pFanin = Abc_ObjFanin0(pFanin);
            if ( Abc_ObjIsBi(pFanin) || Abc_ObjIsBo(pFanin) )
                pFanin = Abc_ObjFanin0(pFanin);
            if ( !pFanin->fMarkC )
                continue;

            // generate the edge from this node to the next
            fprintf( pFile, "Node%d",  pNode->Id );
            fprintf( pFile, " -> " );
            fprintf( pFile, "Node%d",  pFanin->Id );
            fprintf( pFile, " [style = %s", fCompl? "dotted" : "bold" );
//            fprintf( pFile, ", label = \"%c\"", 'a' + k );
            fprintf( pFile, "]" );
            fprintf( pFile, ";\n" );
        }
    }

    fprintf( pFile, "}" );
    fprintf( pFile, "\n" );
    fprintf( pFile, "\n" );
    fclose( pFile );

    // unmark the nodes from the set
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
        pNode->fMarkC = 0;
    if ( vNodesShow )
        Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
            pNode->fMarkB = 0;

    // convert the network back into BDDs if this is how it was
    if ( fHasBdds )
        Abc_NtkSopToBdd(pNtk);
}

void Io_WriteEqn	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Writes the logic network in the equation format.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file ioWriteEqn.c.

{
    FILE * pFile;

    assert( Abc_NtkIsAigNetlist(pNtk) );
    if ( Abc_NtkLatchNum(pNtk) > 0 )
        printf( "Warning: only combinational portion is being written.\n" );

    // check that the names are fine for the EQN format
    if ( !Io_NtkWriteEqnCheck(pNtk) )
        return;

    // start the output stream
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteEqn(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
    fprintf( pFile, "# Equations for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );

    // write the equations for the network
    Io_NtkWriteEqnOne( pFile, pNtk );
    fprintf( pFile, "\n" );
    fclose( pFile );
}

void Io_WriteGml	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

DECLARATIONS ///.

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

FileName [ioWriteGml.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedures to write the graph structure of AIG in GML.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Writes the graph structure of AIG in GML.]

Description [Useful for graph visualization using tools such as yEd: http://www.yworks.com/]

SideEffects []

SeeAlso []

Definition at line 46 of file ioWriteGml.c.

{
    FILE * pFile;
    Abc_Obj_t * pObj, * pFanin;
    int i, k;

    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk)  );

    // start the output stream
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteGml(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
    fprintf( pFile, "# GML for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    fprintf( pFile, "graph [\n" );

    // output the POs
    fprintf( pFile, "\n" );
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
        fprintf( pFile, "        graphics [ type \"triangle\" fill \"#00FFFF\" ]\n" );   // blue
        fprintf( pFile, "    ]\n" );
    }
    // output the PIs
    fprintf( pFile, "\n" );
    Abc_NtkForEachPi( pNtk, pObj, i )
    {
        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
        fprintf( pFile, "        graphics [ type \"triangle\" fill \"#00FF00\" ]\n" );   // green
        fprintf( pFile, "    ]\n" );
    }
    // output the latches
    fprintf( pFile, "\n" );
    Abc_NtkForEachLatch( pNtk, pObj, i )
    {
        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
        fprintf( pFile, "        graphics [ type \"rectangle\" fill \"#FF0000\" ]\n" );   // red
        fprintf( pFile, "    ]\n" );
    }
    // output the nodes
    fprintf( pFile, "\n" );
    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
        fprintf( pFile, "        graphics [ type \"ellipse\" fill \"#CCCCFF\" ]\n" );     // grey
        fprintf( pFile, "    ]\n" );
    }

    // output the edges
    fprintf( pFile, "\n" );
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        Abc_ObjForEachFanin( pObj, pFanin, k )
        {
            fprintf( pFile, "    edge [ source %5d   target %5d\n", pObj->Id, pFanin->Id );
            fprintf( pFile, "        graphics [ type \"line\" arrow \"first\" ]\n" );
            fprintf( pFile, "    ]\n" );
        }
    }

    fprintf( pFile, "]\n" );
    fprintf( pFile, "\n" );
    fclose( pFile );
}

void Io_WriteHie	(	Abc_Ntk_t *	pNtk,
		char *	pBaseName,
		char *	pFileName
	)

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

Synopsis [Write the network into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 477 of file ioUtil.c.

{
    Abc_Ntk_t * pNtkTemp, * pNtkResult, * pNtkBase = NULL;
    int i;
    // check if the current network is available
    if ( pNtk == NULL )
    {
        fprintf( stdout, "Empty network.\n" );
        return;
    }

    // read the base network
    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
    if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIF )
        pNtkBase = Io_ReadBlifMv( pBaseName, 0, 1 );
    else if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIFMV )
        pNtkBase = Io_ReadBlifMv( pBaseName, 1, 1 );
    else if ( Io_ReadFileType(pBaseName) == IO_FILE_VERILOG )
        pNtkBase = Io_ReadVerilog( pBaseName, 1 );
    else 
        fprintf( stderr, "Unknown input file format.\n" );
    if ( pNtkBase == NULL )
        return;

    // flatten logic hierarchy if present
    if ( Abc_NtkWhiteboxNum(pNtkBase) > 0 && pNtk->nBarBufs == 0 )
    {
        pNtkBase = Abc_NtkFlattenLogicHierarchy( pNtkTemp = pNtkBase );
        Abc_NtkDelete( pNtkTemp );
        if ( pNtkBase == NULL )
            return;
    }

    // reintroduce the boxes into the netlist
    if ( pNtk->nBarBufs > 0 )
    {
        // derive the netlist
        pNtkResult = Abc_NtkToNetlist( pNtk );
        pNtkResult = Abc_NtkFromBarBufs( pNtkBase, pNtkTemp = pNtkResult );
        Abc_NtkDelete( pNtkTemp );
        if ( pNtkResult )
            printf( "Hierarchy writer replaced %d barbufs by hierarchy boundaries.\n", pNtk->nBarBufs );
    }
    else if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIFMV ) 
    {
        if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
        {
            printf( "Hierarchy writer does not support BLIF-MV with blackboxes.\n" );
            Abc_NtkDelete( pNtkBase );
            return;
        }
        // convert the current network to BLIF-MV
        assert( !Abc_NtkIsNetlist(pNtk) );
        pNtkResult = Abc_NtkToNetlist( pNtk );
        if ( !Abc_NtkConvertToBlifMv( pNtkResult ) )
        {
            Abc_NtkDelete( pNtkBase );
            return;
        }
        // reintroduce the network
        pNtkResult = Abc_NtkInsertBlifMv( pNtkBase, pNtkTemp = pNtkResult );
        Abc_NtkDelete( pNtkTemp );
    }
    else if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
    {
        // derive the netlist
        pNtkResult = Abc_NtkToNetlist( pNtk );
        pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult );
        Abc_NtkDelete( pNtkTemp );
        if ( pNtkResult )
            printf( "Hierarchy writer reintroduced %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) );
    }
    else
    {
        printf( "Warning: The output network does not contain blackboxes.\n" );
        pNtkResult = Abc_NtkToNetlist( pNtk );
    }
    Abc_NtkDelete( pNtkBase );
    if ( pNtkResult == NULL )
        return;

    // write the resulting network
    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
    {
        if ( pNtkResult->pDesign )
        {
            Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkResult->pDesign->vModules, pNtkTemp, i )
                if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
                    Abc_NtkToSop( pNtkTemp, 0 );
        }
        else
        {
            if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
                Abc_NtkToSop( pNtkResult, 0 );
        }
        Io_WriteBlif( pNtkResult, pFileName, 1, 0, 0 );
    }
    else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG )
    {
        if ( pNtkResult->pDesign )
        {
            Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkResult->pDesign->vModules, pNtkTemp, i )
                if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
                    Abc_NtkToAig( pNtkTemp );
        }
        else
        {
            if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
                Abc_NtkToAig( pNtkResult );
        }
        Io_WriteVerilog( pNtkResult, pFileName );
    }
    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
    {
        Io_WriteBlifMv( pNtkResult, pFileName );
    }
    else 
        fprintf( stderr, "Unknown output file format.\n" );

    Abc_NtkDelete( pNtkResult );
}

void Io_WriteList	(	Abc_Ntk_t *	pNtk,
		char *	pFileName,
		int	fUseHost
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Writes the adjacency list for a sequential AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file ioWriteList.c.

{
    FILE * pFile;
    Abc_Obj_t * pObj;
    int i;

//    assert( Abc_NtkIsSeq(pNtk)  );

    // start the output stream
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteList(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }

    fprintf( pFile, "# Adjacency list for sequential AIG \"%s\"\n", pNtk->pName );
    fprintf( pFile, "# written by ABC on %s\n", Extra_TimeStamp() );

    // write the constant node
    if ( Abc_ObjFanoutNum( Abc_AigConst1(pNtk) ) > 0 )
        Io_WriteListEdge( pFile, Abc_AigConst1(pNtk) );

    // write the PI edges
    Abc_NtkForEachPi( pNtk, pObj, i )
        Io_WriteListEdge( pFile, pObj );

    // write the internal nodes
    Abc_AigForEachAnd( pNtk, pObj, i )
        Io_WriteListEdge( pFile, pObj );

    // write the host node
    if ( fUseHost )
        Io_WriteListHost( pFile, pNtk );
    else
        Abc_NtkForEachPo( pNtk, pObj, i )
            Io_WriteListEdge( pFile, pObj );

    fprintf( pFile, "\n" );
    fclose( pFile );
}

int Io_WritePla	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Writes the network in PLA format.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file ioWritePla.c.

{
    Abc_Ntk_t * pExdc;
    FILE * pFile;

    assert( Abc_NtkIsSopNetlist(pNtk) );
    assert( Abc_NtkLevel(pNtk) == 1 );

    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WritePla(): Cannot open the output file.\n" );
        return 0;
    }
    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the network
    Io_WritePlaOne( pFile, pNtk );
    // write EXDC network if it exists
    pExdc = Abc_NtkExdc( pNtk );
    if ( pExdc )
        printf( "Io_WritePla: EXDC is not written (warning).\n" );
    // finalize the file
    fclose( pFile );
    return 1;
}

int Io_WriteSmv	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

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

Synopsis [Writes the network in SMV format.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file ioWriteSmv.c.

{
    Abc_Ntk_t * pExdc;
    FILE * pFile;
    assert( Abc_NtkIsSopNetlist(pNtk) );
    if ( !Io_WriteSmvCheckNames(pNtk) )
    {
        fprintf( stdout, "Io_WriteSmv(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the SMV format. Use \"short_names\".\n" );
        return 0;
    }
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteSmv(): Cannot open the output file.\n" );
        return 0;
    }
    fprintf( pFile, "-- benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the network
    Io_WriteSmvOne( pFile, pNtk );
    // write EXDC network if it exists
    pExdc = Abc_NtkExdc( pNtk );
    if ( pExdc )
        printf( "Io_WriteSmv: EXDC is not written (warning).\n" );
    // finalize the file
    fclose( pFile );
    return 1;
}

void Io_WriteTimingInfo	(	FILE *	pFile,
		Abc_Ntk_t *	pNtk
	)

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

Synopsis [Writes the timing info.]

Description []

SideEffects []

SeeAlso []

Definition at line 665 of file ioWriteBlif.c.

{
    Abc_Obj_t * pNode;
    Abc_Time_t * pTime, * pTimeDef;
    int i;

    if ( pNtk->pManTime == NULL )
        return;

    fprintf( pFile, "\n" );

    if ( pNtk->AndGateDelay != 0.0 )
        fprintf( pFile, ".and_gate_delay %g\n", pNtk->AndGateDelay );

    pTimeDef = Abc_NtkReadDefaultArrival( pNtk );
    if ( pTimeDef->Rise != 0.0 || pTimeDef->Fall != 0.0 )
        fprintf( pFile, ".default_input_arrival %g %g\n", pTimeDef->Rise, pTimeDef->Fall );
    Abc_NtkForEachPi( pNtk, pNode, i )
    {
        pTime = Abc_NodeReadArrival(pNode);
        if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
            continue;
        fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(Abc_ObjFanout0(pNode)), pTime->Rise, pTime->Fall );
    }

    pTimeDef = Abc_NtkReadDefaultRequired( pNtk );
    if ( pTimeDef->Rise != ABC_INFINITY || pTimeDef->Fall != ABC_INFINITY )
        fprintf( pFile, ".default_output_required %g %g\n", pTimeDef->Rise, pTimeDef->Fall );
    Abc_NtkForEachPo( pNtk, pNode, i )
    {
        pTime = Abc_NodeReadRequired(pNode);
        if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
            continue;
        fprintf( pFile, ".output_required %s %g %g\n", Abc_ObjName(Abc_ObjFanin0(pNode)), pTime->Rise, pTime->Fall );
    }

    fprintf( pFile, "\n" );

    pTimeDef = Abc_NtkReadDefaultInputDrive( pNtk );
    if ( pTimeDef->Rise != 0.0 || pTimeDef->Fall != 0.0 )
        fprintf( pFile, ".default_input_drive %g %g\n", pTimeDef->Rise, pTimeDef->Fall );
    if ( Abc_NodeReadInputDrive( pNtk, 0 ) )
        Abc_NtkForEachPi( pNtk, pNode, i )
        {
            pTime = Abc_NodeReadInputDrive( pNtk, i );
            if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
                continue;
            fprintf( pFile, ".input_drive %s %g %g\n", Abc_ObjName(Abc_ObjFanout0(pNode)), pTime->Rise, pTime->Fall );
        }

    pTimeDef = Abc_NtkReadDefaultOutputLoad( pNtk );
    if ( pTimeDef->Rise != 0.0 || pTimeDef->Fall != 0.0 )
        fprintf( pFile, ".default_output_load %g %g\n", pTimeDef->Rise, pTimeDef->Fall );
    if ( Abc_NodeReadOutputLoad( pNtk, 0 ) )
        Abc_NtkForEachPo( pNtk, pNode, i )
        {
            pTime = Abc_NodeReadOutputLoad( pNtk, i );
            if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
                continue;
            fprintf( pFile, ".output_load %s %g %g\n", Abc_ObjName(Abc_ObjFanin0(pNode)), pTime->Rise, pTime->Fall );
        }

    fprintf( pFile, "\n" );
}

void Io_WriteVerilog	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Write verilog.]

Description []

SideEffects []

SeeAlso []

Definition at line 57 of file ioWriteVerilog.c.

{
    Abc_Ntk_t * pNetlist;
    FILE * pFile;
    int i;
    // can only write nodes represented using local AIGs
    if ( !Abc_NtkIsAigNetlist(pNtk) && !Abc_NtkIsMappedNetlist(pNtk) )
    {
        printf( "Io_WriteVerilog(): Can produce Verilog for mapped or AIG netlists only.\n" );
        return;
    }
    // start the output stream
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }

    // write the equations for the network
    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    fprintf( pFile, "\n" );

    // write modules
    if ( pNtk->pDesign )
    {
        // write the network first
        Io_WriteVerilogInt( pFile, pNtk );
        // write other things
        Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNetlist, i )
        {
            assert( Abc_NtkIsNetlist(pNetlist) );
            if ( pNetlist == pNtk )
                continue;
            fprintf( pFile, "\n" );
            Io_WriteVerilogInt( pFile, pNetlist );
        }
    }
    else
    {
        Io_WriteVerilogInt( pFile, pNtk );
    }

    fprintf( pFile, "\n" );
    fclose( pFile );
}