ioaWriteAig.c File Reference

#include "ioa.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START int	Ioa_ObjMakeLit (int Var, int fCompl)
	DECLARATIONS ///. More...
static int	Ioa_ObjAigerNum (Aig_Obj_t *pObj)
static void	Ioa_ObjSetAigerNum (Aig_Obj_t *pObj, unsigned Num)
int	Ioa_WriteAigerEncode (unsigned char *pBuffer, int Pos, unsigned x)
	FUNCTION DEFINITIONS ///. More...
void	Ioa_WriteAigerEncodeStr (Vec_Str_t *vStr, unsigned x)
Vec_Int_t *	Ioa_WriteAigerLiterals (Aig_Man_t *pMan)
Vec_Str_t *	Ioa_WriteEncodeLiterals (Vec_Int_t *vLits)
Vec_Str_t *	Ioa_WriteAigerIntoMemoryStr (Aig_Man_t *pMan)
char *	Ioa_WriteAigerIntoMemory (Aig_Man_t *pMan, int *pnSize)
void	Ioa_WriteAigerBufferTest (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
void	Ioa_WriteAiger (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)

Function Documentation

static int Ioa_ObjAigerNum ( Aig_Obj_t *  pObj )

static

Definition at line 132 of file ioaWriteAig.c.

{ return pObj->iData;          }

static ABC_NAMESPACE_IMPL_START int Ioa_ObjMakeLit ( int  Var, int  fCompl  )

static

DECLARATIONS ///.

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

FileName [ioaWriteAiger.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedures to write binary AIGER format developed by Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - December 16, 2006.]

Revision [

Id:

ioaWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp

]

Definition at line 131 of file ioaWriteAig.c.

{ return (Var << 1) | fCompl;  }

static void Ioa_ObjSetAigerNum ( Aig_Obj_t *  pObj, unsigned  Num  )

static

Definition at line 133 of file ioaWriteAig.c.

{ pObj->iData = Num;           }

void Ioa_WriteAiger	(	Aig_Man_t *	pMan,
		char *	pFileName,
		int	fWriteSymbols,
		int	fCompact
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file ioaWriteAig.c.

{
//    Bar_Progress_t * pProgress;
    FILE * pFile;
    Aig_Obj_t * pObj, * pDriver;
    int i, nNodes, nBufferSize, Pos;
    unsigned char * pBuffer;
    unsigned uLit0, uLit1, uLit;

    if ( Aig_ManCoNum(pMan) == 0 )
    {
        printf( "AIG cannot be written because it has no POs.\n" );
        return;
    }

//    assert( Aig_ManIsStrash(pMan) );
    // start the output stream
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
/*
    Aig_ManForEachLatch( pMan, pObj, i )
        if ( !Aig_LatchIsInit0(pObj) )
        {
            fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
            return;
        }
*/
    // set the node numbers to be used in the output file
    nNodes = 0;
    Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
    Aig_ManForEachCi( pMan, pObj, i )
        Ioa_ObjSetAigerNum( pObj, nNodes++ );
    Aig_ManForEachNode( pMan, pObj, i )
        Ioa_ObjSetAigerNum( pObj, nNodes++ );

    // write the header "M I L O A" where M = I + L + A
    fprintf( pFile, "aig%s %u %u %u %u %u", 
        fCompact? "2" : "",
        Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan), 
        Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
        Aig_ManRegNum(pMan),
        Aig_ManConstrNum(pMan) ? 0 : Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
        Aig_ManNodeNum(pMan) );
    // write the extended header "B C J F"
    if ( Aig_ManConstrNum(pMan) )
        fprintf( pFile, " %u %u", Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
    fprintf( pFile, "\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

    Aig_ManInvertConstraints( pMan );
    if ( !fCompact ) 
    {
        // write latch drivers
        Aig_ManForEachLiSeq( pMan, pObj, i )
        {
            pDriver = Aig_ObjFanin0(pObj);
            fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
        }

        // write PO drivers
        Aig_ManForEachPoSeq( pMan, pObj, i )
        {
            pDriver = Aig_ObjFanin0(pObj);
            fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
        }
    }
    else
    {
        Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan );
        Vec_Str_t * vBinary = Ioa_WriteEncodeLiterals( vLits );
        fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
        Vec_StrFree( vBinary );
        Vec_IntFree( vLits );
    }
    Aig_ManInvertConstraints( pMan );

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
    pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
//    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
    Aig_ManForEachNode( pMan, pObj, i )
    {
//        Bar_ProgressUpdate( pProgress, i, NULL );
        uLit  = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
        uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
        uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
        assert( uLit0 != uLit1 );
        if ( uLit0 > uLit1 )
        {
            int Temp = uLit0;
            uLit0 = uLit1;
            uLit1 = Temp;
        }
        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
        if ( Pos > nBufferSize - 10 )
        {
            printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
            fclose( pFile );
            return;
        }
    }
    assert( Pos < nBufferSize );
//    Bar_ProgressStop( pProgress );

    // write the buffer
    fwrite( pBuffer, 1, Pos, pFile );
    ABC_FREE( pBuffer );
/*
    // write the symbol table
    if ( fWriteSymbols )
    {
        int bads;
        // write PIs
        Aig_ManForEachPiSeq( pMan, pObj, i )
            fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
        // write latches
        Aig_ManForEachLoSeq( pMan, pObj, i )
            fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
        // write POs
        bads = Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan);
        Aig_ManForEachPoSeq( pMan, pObj, i )
            if ( !Aig_ManConstrNum(pMan) )
                fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
            else if ( i < bads )
                fprintf( pFile, "b%d %s\n", i, Aig_ObjName(pObj) );
            else
                fprintf( pFile, "c%d %s\n", i - bads, Aig_ObjName(pObj) );
    }
*/
    // write the comment
    fprintf( pFile, "c" );
    if ( pMan->pName )
        fprintf( pFile, "n%s%c", pMan->pName, '\0' );
    fprintf( pFile, "\nThis file was produced by the IOA package in ABC on %s\n", Ioa_TimeStamp() );
    fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
    fclose( pFile );
}

void Ioa_WriteAigerBufferTest	(	Aig_Man_t *	pMan,
		char *	pFileName,
		int	fWriteSymbols,
		int	fCompact
	)

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

Synopsis [This procedure is used to test the above procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file ioaWriteAig.c.

{
    FILE * pFile;
    char * pBuffer;
    int nSize;
    if ( Aig_ManCoNum(pMan) == 0 )
    {
        printf( "AIG cannot be written because it has no POs.\n" );
        return;
    }
    // start the output stream
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
    // write the buffer
    pBuffer = Ioa_WriteAigerIntoMemory( pMan, &nSize );
    fwrite( pBuffer, 1, nSize, pFile );
    ABC_FREE( pBuffer );
    // write the comment
//    fprintf( pFile, "c" );
//    if ( pMan->pName )
//        fprintf( pFile, "n%s%c", pMan->pName, '\0' );
    fprintf( pFile, "\nThis file was produced by the IOA package in ABC on %s\n", Ioa_TimeStamp() );
    fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
    fclose( pFile );
}

int Ioa_WriteAigerEncode	(	unsigned char *	pBuffer,
		int	Pos,
		unsigned	x
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Adds one unsigned AIG edge to the output buffer.]

Description [This procedure is a slightly modified version of Armin Biere's procedure "void encode (FILE * file, unsigned x)" ]

SideEffects [Returns the current writing position.]

SeeAlso []

Definition at line 151 of file ioaWriteAig.c.

{
    unsigned char ch;
    while (x & ~0x7f)
    {
        ch = (x & 0x7f) | 0x80;
//        putc (ch, file);
        pBuffer[Pos++] = ch;
        x >>= 7;
    }
    ch = x;
//    putc (ch, file);
    pBuffer[Pos++] = ch;
    return Pos;
}

void Ioa_WriteAigerEncodeStr	(	Vec_Str_t *	vStr,
		unsigned	x
	)

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

Synopsis [Adds one unsigned AIG edge to the output buffer.]

Description [This procedure is a slightly modified version of Armin Biere's procedure "void encode (FILE * file, unsigned x)" ]

SideEffects [Returns the current writing position.]

SeeAlso []

Definition at line 179 of file ioaWriteAig.c.

{
    unsigned char ch;
    while (x & ~0x7f)
    {
        ch = (x & 0x7f) | 0x80;
//        putc (ch, file);
//        pBuffer[Pos++] = ch;
        Vec_StrPush( vStr, ch );
        x >>= 7;
    }
    ch = x;
//    putc (ch, file);
//    pBuffer[Pos++] = ch;
    Vec_StrPush( vStr, ch );
}

char* Ioa_WriteAigerIntoMemory	(	Aig_Man_t *	pMan,
		int *	pnSize
	)

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

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The returned size (pnSize) gives the number of bytes in the buffer. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 376 of file ioaWriteAig.c.

{
    char * pBuffer;
    Vec_Str_t * vBuffer;
    vBuffer = Ioa_WriteAigerIntoMemoryStr( pMan );
    if ( pMan->pName )
    {
        Vec_StrPrintStr( vBuffer, "n" );
        Vec_StrPrintStr( vBuffer, pMan->pName );
        Vec_StrPush( vBuffer, 0 );
    }
    // prepare the return values
    *pnSize = Vec_StrSize( vBuffer );
    pBuffer = Vec_StrReleaseArray( vBuffer );
    Vec_StrFree( vBuffer );
    return pBuffer;
}

Vec_Str_t* Ioa_WriteAigerIntoMemoryStr

(

Aig_Man_t *

pMan

)

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

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The returned size (pnSize) gives the number of bytes in the buffer. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 286 of file ioaWriteAig.c.

{
    Vec_Str_t * vBuffer;
    Aig_Obj_t * pObj, * pDriver;
    int nNodes, i, uLit, uLit0, uLit1; 
    // set the node numbers to be used in the output file
    nNodes = 0;
    Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
    Aig_ManForEachCi( pMan, pObj, i )
        Ioa_ObjSetAigerNum( pObj, nNodes++ );
    Aig_ManForEachNode( pMan, pObj, i )
        Ioa_ObjSetAigerNum( pObj, nNodes++ );

    // write the header "M I L O A" where M = I + L + A
/*
    fprintf( pFile, "aig%s %u %u %u %u %u\n", 
        fCompact? "2" : "",
        Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan), 
        Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
        Aig_ManRegNum(pMan),
        Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
        Aig_ManNodeNum(pMan) );
*/
    vBuffer = Vec_StrAlloc( 3*Aig_ManObjNum(pMan) );
    Vec_StrPrintStr( vBuffer, "aig " );
    Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan) );
    Vec_StrPrintStr( vBuffer, " " );
    Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    Vec_StrPrintStr( vBuffer, " " );
    Vec_StrPrintNum( vBuffer, Aig_ManRegNum(pMan) );
    Vec_StrPrintStr( vBuffer, " " );
    Vec_StrPrintNum( vBuffer, Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
    Vec_StrPrintStr( vBuffer, " " );
    Vec_StrPrintNum( vBuffer, Aig_ManNodeNum(pMan) );
    Vec_StrPrintStr( vBuffer, "\n" );

    // write latch drivers
    Aig_ManForEachLiSeq( pMan, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        uLit    = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) );
//        fprintf( pFile, "%u\n", uLit );
        Vec_StrPrintNum( vBuffer, uLit );
        Vec_StrPrintStr( vBuffer, "\n" );
    }

    // write PO drivers
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        uLit    = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) );
//        fprintf( pFile, "%u\n", uLit );
        Vec_StrPrintNum( vBuffer, uLit );
        Vec_StrPrintStr( vBuffer, "\n" );
    }
    // write the nodes into the buffer
    Aig_ManForEachNode( pMan, pObj, i )
    {
        uLit  = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
        uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
        uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
        assert( uLit0 != uLit1 );
        if ( uLit0 > uLit1 )
        {
            int Temp = uLit0;
            uLit0 = uLit1;
            uLit1 = Temp;
        }
//        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
//        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
        Ioa_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
        Ioa_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
    }
    Vec_StrPrintStr( vBuffer, "c" );
    return vBuffer;
}

Vec_Int_t* Ioa_WriteAigerLiterals

(

Aig_Man_t *

pMan

)

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

Synopsis [Create the array of literals to be written.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file ioaWriteAig.c.

{
    Vec_Int_t * vLits;
    Aig_Obj_t * pObj, * pDriver;
    int i;
    vLits = Vec_IntAlloc( Aig_ManCoNum(pMan) );
    Aig_ManForEachLiSeq( pMan, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
    }
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
    }
    return vLits;
}

Vec_Str_t* Ioa_WriteEncodeLiterals

(

Vec_Int_t *

vLits

)

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

Synopsis [Creates the binary encoded array of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file ioaWriteAig.c.

{
    Vec_Str_t * vBinary;
    int Pos = 0, Lit, LitPrev, Diff, i;
    vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
    LitPrev = Vec_IntEntry( vLits, 0 );
    Pos = Ioa_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); 
    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
    {
        Diff = Lit - LitPrev;
        Diff = (Lit < LitPrev)? -Diff : Diff;
        Diff = (Diff << 1) | (int)(Lit < LitPrev);
        Pos = Ioa_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
        LitPrev = Lit;
        if ( Pos + 10 > vBinary->nCap )
            Vec_StrGrow( vBinary, vBinary->nCap+1 );
    }
    vBinary->nSize = Pos;
/*
    // verify
    {
        extern Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries );
        char * pPos = Vec_StrArray( vBinary );
        Vec_Int_t * vTemp = Ioa_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
        for ( i = 0; i < Vec_IntSize(vLits); i++ )
        {
            int Entry1 = Vec_IntEntry(vLits,i);
            int Entry2 = Vec_IntEntry(vTemp,i);
            assert( Entry1 == Entry2 );
        }
        Vec_IntFree( vTemp );
    }
*/
    return vBinary;
}