src/aig/ioa/ioaWriteAig.c File Reference

#include "ioa.h"

Include dependency graph for ioaWriteAig.c:

Go to the source code of this file.

Functions
static unsigned	Ioa_ObjMakeLit (int Var, int fCompl)
static unsigned	Ioa_ObjAigerNum (Aig_Obj_t *pObj)
static void	Ioa_ObjSetAigerNum (Aig_Obj_t *pObj, unsigned Num)
int	Ioa_WriteAigerEncode (char *pBuffer, int Pos, unsigned x)
void	Ioa_WriteAiger (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols)

---

Function Documentation

static unsigned Ioa_ObjAigerNum

(

Aig_Obj_t *

pObj

)

[static]

Definition at line 129 of file ioaWriteAig.c.

{ return (unsigned)pObj->pData;  }

static unsigned Ioa_ObjMakeLit	(	int	Var,
		int	fCompl
	)			[static]

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

] DECLARATIONS ///

Definition at line 128 of file ioaWriteAig.c.

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

static void Ioa_ObjSetAigerNum	(	Aig_Obj_t *	pObj,
		unsigned	Num
	)			[static]

Definition at line 130 of file ioaWriteAig.c.

{ pObj->pData = (void *)Num;     }

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file ioaWriteAig.c.

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

//    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_ManForEachPi( 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 %u %u %u %u %u\n", 
        Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), 
        Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
        Aig_ManRegNum(pMan),
        Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
        Aig_ManNodeNum(pMan) );

    // 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

    // 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) ) );
    }

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
    pBuffer = ALLOC( 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 );
        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 );
    free( pBuffer );
/*
    // write the symbol table
    if ( fWriteSymbols )
    {
        // write PIs
        Aig_ManForEachPi( pMan, pObj, i )
            fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
        // write latches
        Aig_ManForEachLatch( pMan, pObj, i )
            fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
        // write POs
        Aig_ManForEachPo( pMan, pObj, i )
            fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
    }
*/
    // write the comment
    fprintf( pFile, "c\n" );
    if ( pMan->pName )
        fprintf( pFile, ".model %s\n", pMan->pName );
    fprintf( pFile, "This file was produced by the AIG 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	(	char *	pBuffer,
		int	Pos,
		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 271 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;
}