src/base/io/ioWriteAiger.c File Reference

#include "io.h"

Include dependency graph for ioWriteAiger.c:

Go to the source code of this file.

Functions
static unsigned	Io_ObjMakeLit (int Var, int fCompl)
static unsigned	Io_ObjAigerNum (Abc_Obj_t *pObj)
static void	Io_ObjSetAigerNum (Abc_Obj_t *pObj, unsigned Num)
int	Io_WriteAigerEncode (char *pBuffer, int Pos, unsigned x)
void	Io_WriteAiger (Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols)

---

Function Documentation

static unsigned Io_ObjAigerNum

(

Abc_Obj_t *

pObj

)

[static]

Definition at line 129 of file ioWriteAiger.c.

{ return (unsigned)pObj->pCopy;  }

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

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

FileName [ioWriteAiger.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

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

] DECLARATIONS ///

Definition at line 128 of file ioWriteAiger.c.

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

static void Io_ObjSetAigerNum	(	Abc_Obj_t *	pObj,
		unsigned	Num
	)			[static]

Definition at line 130 of file ioWriteAiger.c.

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

void Io_WriteAiger	(	Abc_Ntk_t *	pNtk,
		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 ioWriteAiger.c.

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

    assert( Abc_NtkIsStrash(pNtk) );
    // start the output stream
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
    Abc_NtkForEachLatch( pNtk, pObj, i )
        if ( !Abc_LatchIsInit0(pObj) )
        {
            fprintf( stdout, "Io_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;
    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
    fprintf( pFile, "aig %u %u %u %u %u\n", 
        Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
        Abc_NtkPiNum(pNtk),
        Abc_NtkLatchNum(pNtk),
        Abc_NtkPoNum(pNtk),
        Abc_NtkNodeNum(pNtk) );

    // 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
    Abc_NtkForEachLatchInput( pNtk, pObj, i )
    {
        pDriver = Abc_ObjFanin0(pObj);
        fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
    }

    // write PO drivers
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
        pDriver = Abc_ObjFanin0(pObj);
        fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
    }

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
    pBuffer = ALLOC( 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) );
        assert( uLit0 < uLit1 );
        Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
        Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
        if ( Pos > nBufferSize - 10 )
        {
            printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
                fclose( pFile );
            return;
        }
    }
    assert( Pos < nBufferSize );
    Extra_ProgressBarStop( pProgress );

    // write the buffer
    fwrite( pBuffer, 1, Pos, pFile );
    free( pBuffer );

    // write the symbol table
    if ( fWriteSymbols )
    {
        // write PIs
        Abc_NtkForEachPi( pNtk, pObj, i )
            fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
        // write latches
        Abc_NtkForEachLatch( pNtk, pObj, i )
            fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
        // write POs
        Abc_NtkForEachPo( pNtk, pObj, i )
            fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
    }

    // write the comment
    fprintf( pFile, "c\n" );
    if ( pNtk->pName && strlen(pNtk->pName) > 0 )
        fprintf( pFile, ".model %s\n", pNtk->pName );
    fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
    fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
        fclose( pFile );
}

int Io_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 270 of file ioWriteAiger.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;
}