ioaWriteAig.c 20.6 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
/**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 $]

***********************************************************************/

#include "ioa.h"

24 25 26
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

/*
    The following is taken from the AIGER format description, 
    which can be found at http://fmv.jku.at/aiger
*/


/*
         The AIGER And-Inverter Graph (AIG) Format Version 20061129
         ----------------------------------------------------------
              Armin Biere, Johannes Kepler University, 2006

  This report describes the AIG file format as used by the AIGER library.
  The purpose of this report is not only to motivate and document the
  format, but also to allow independent implementations of writers and
  readers by giving precise and unambiguous definitions.

  ...

Introduction

  The name AIGER contains as one part the acronym AIG of And-Inverter
  Graphs and also if pronounced in German sounds like the name of the
  'Eiger', a mountain in the Swiss alps.  This choice should emphasize the
  origin of this format. It was first openly discussed at the Alpine
  Verification Meeting 2006 in Ascona as a way to provide a simple, compact
  file format for a model checking competition affiliated to CAV 2007.

  ...

Binary Format Definition

  The binary format is semantically a subset of the ASCII format with a
  slightly different syntax.  The binary format may need to reencode
  literals, but translating a file in binary format into ASCII format and
  then back in to binary format will result in the same file.

  The main differences of the binary format to the ASCII format are as
  follows.  After the header the list of input literals and all the
  current state literals of a latch can be omitted.  Furthermore the
  definitions of the AND gates are binary encoded.  However, the symbol
  table and the comment section are as in the ASCII format.

  The header of an AIGER file in binary format has 'aig' as format
  identifier, but otherwise is identical to the ASCII header.  The standard
  file extension for the binary format is therefore '.aig'. 
  
  A header for the binary format is still in ASCII encoding:

    aig M I L O A

  Constants, variables and literals are handled in the same way as in the
  ASCII format.  The first simplifying restriction is on the variable
  indices of inputs and latches.  The variable indices of inputs come first,
  followed by the pseudo-primary inputs of the latches and then the variable
  indices of all LHS of AND gates:

    input variable indices        1,          2,  ... ,  I
    latch variable indices      I+1,        I+2,  ... ,  (I+L)
    AND variable indices      I+L+1,      I+L+2,  ... ,  (I+L+A) == M

  The corresponding unsigned literals are

    input literals                2,          4,  ... ,  2*I
    latch literals            2*I+2,      2*I+4,  ... ,  2*(I+L)
    AND literals          2*(I+L)+2,  2*(I+L)+4,  ... ,  2*(I+L+A) == 2*M
                    
  All literals have to be defined, and therefore 'M = I + L + A'.  With this
  restriction it becomes possible that the inputs and the current state
  literals of the latches do not have to be listed explicitly.  Therefore,
  after the header only the list of 'L' next state literals follows, one per
  latch on a single line, and then the 'O' outputs, again one per line.

  In the binary format we assume that the AND gates are ordered and respect
  the child parent relation.  AND gates with smaller literals on the LHS
  come first.  Therefore we can assume that the literals on the right-hand
  side of a definition of an AND gate are smaller than the LHS literal.
  Furthermore we can sort the literals on the RHS, such that the larger
  literal comes first.  A definition thus consists of three literals
    
      lhs rhs0 rhs1

  with 'lhs' even and 'lhs > rhs0 >= rhs1'.  Also the variable indices are
  pairwise different to avoid combinational self loops.  Since the LHS
  indices of the definitions are all consecutive (as even integers),
  the binary format does not have to keep 'lhs'.  In addition, we can use
  the order restriction and only write the differences 'delta0' and 'delta1'
  instead of 'rhs0' and 'rhs1', with

      delta0 = lhs - rhs0,  delta1 = rhs0 - rhs1
  
  The differences will all be strictly positive, and in practice often very
  small.  We can take advantage of this fact by the simple little-endian
  encoding of unsigned integers of the next section.  After the binary delta
  encoding of the RHSs of all AND gates, the optional symbol table and
  optional comment section start in the same format as in the ASCII case.

  ...

*/

Alan Mishchenko committed
131 132 133
static int      Ioa_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;  }
static int      Ioa_ObjAigerNum( Aig_Obj_t * pObj )                   { return pObj->iData;          }
static void     Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num )  { pObj->iData = Num;           }
Alan Mishchenko committed
134 135 136 137 138 139 140

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

Alan Mishchenko committed
141 142 143 144 145 146 147 148 149 150
  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     []

***********************************************************************/
Alan Mishchenko committed
151
int Ioa_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
Alan Mishchenko committed
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168
{
    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;
}

/**Function*************************************************************

169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
  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     []

***********************************************************************/
void Ioa_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x )
{
    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 );
}

/**Function*************************************************************

Alan Mishchenko committed
198 199 200 201 202 203 204 205 206 207 208 209 210 211
  Synopsis    [Create the array of literals to be written.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ioa_WriteAigerLiterals( Aig_Man_t * pMan )
{
    Vec_Int_t * vLits;
    Aig_Obj_t * pObj, * pDriver;
    int i;
212
    vLits = Vec_IntAlloc( Aig_ManCoNum(pMan) );
Alan Mishchenko committed
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
    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;
}

/**Function*************************************************************

  Synopsis    [Creates the binary encoded array of literals.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits )
{
    Vec_Str_t * vBinary;
    int Pos = 0, Lit, LitPrev, Diff, i;
    vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
    LitPrev = Vec_IntEntry( vLits, 0 );
Alan Mishchenko committed
243
    Pos = Ioa_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); 
Alan Mishchenko committed
244 245 246 247 248
    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
    {
        Diff = Lit - LitPrev;
        Diff = (Lit < LitPrev)? -Diff : Diff;
        Diff = (Diff << 1) | (int)(Lit < LitPrev);
Alan Mishchenko committed
249
        Pos = Ioa_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
Alan Mishchenko committed
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
        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;
}

/**Function*************************************************************

275 276 277 278 279 280 281 282 283 284 285
  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     []

***********************************************************************/
286
Vec_Str_t * Ioa_WriteAigerIntoMemoryStr( Aig_Man_t * pMan )
287 288 289 290 291 292 293
{
    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++ );
294
    Aig_ManForEachCi( pMan, pObj, i )
295 296 297 298 299 300 301 302
        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" : "",
303 304
        Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan), 
        Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
305
        Aig_ManRegNum(pMan),
306
        Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
307 308 309 310
        Aig_ManNodeNum(pMan) );
*/
    vBuffer = Vec_StrAlloc( 3*Aig_ManObjNum(pMan) );
    Vec_StrPrintStr( vBuffer, "aig " );
311
    Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan) );
312
    Vec_StrPrintStr( vBuffer, " " );
313
    Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
314 315 316
    Vec_StrPrintStr( vBuffer, " " );
    Vec_StrPrintNum( vBuffer, Aig_ManRegNum(pMan) );
    Vec_StrPrintStr( vBuffer, " " );
317
    Vec_StrPrintNum( vBuffer, Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
    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" );
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380
    return vBuffer;
}

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

***********************************************************************/
char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
{
    char * pBuffer;
    Vec_Str_t * vBuffer;
    vBuffer = Ioa_WriteAigerIntoMemoryStr( pMan );
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409
    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;
}

/**Function*************************************************************

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

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ioa_WriteAigerBufferTest( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
{
    FILE * pFile;
    char * pBuffer;
    int nSize;
410
    if ( Aig_ManCoNum(pMan) == 0 )
411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436
    {
        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 );
}

/**Function*************************************************************

Alan Mishchenko committed
437 438 439 440 441 442 443 444 445
  Synopsis    [Writes the AIG in the binary AIGER format.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
446
void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
Alan Mishchenko committed
447
{
Alan Mishchenko committed
448
//    Bar_Progress_t * pProgress;
Alan Mishchenko committed
449 450
    FILE * pFile;
    Aig_Obj_t * pObj, * pDriver;
Alan Mishchenko committed
451
    int i, nNodes, nBufferSize, Pos;
Alan Mishchenko committed
452 453 454
    unsigned char * pBuffer;
    unsigned uLit0, uLit1, uLit;

455
    if ( Aig_ManCoNum(pMan) == 0 )
Alan Mishchenko committed
456 457 458 459 460
    {
        printf( "AIG cannot be written because it has no POs.\n" );
        return;
    }

Alan Mishchenko committed
461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479
//    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++ );
480
    Aig_ManForEachCi( pMan, pObj, i )
Alan Mishchenko committed
481 482 483 484 485
        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
486
    fprintf( pFile, "aig%s %u %u %u %u %u", 
Alan Mishchenko committed
487
        fCompact? "2" : "",
488 489
        Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan), 
        Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
Alan Mishchenko committed
490
        Aig_ManRegNum(pMan),
491
        Aig_ManConstrNum(pMan) ? 0 : Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
Alan Mishchenko committed
492
        Aig_ManNodeNum(pMan) );
493 494
    // write the extended header "B C J F"
    if ( Aig_ManConstrNum(pMan) )
495
        fprintf( pFile, " %u %u", Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
496
    fprintf( pFile, "\n" ); 
Alan Mishchenko committed
497 498 499 500 501

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

502
    Aig_ManInvertConstraints( pMan );
Alan Mishchenko committed
503
    if ( !fCompact ) 
Alan Mishchenko committed
504
    {
Alan Mishchenko committed
505 506 507 508 509 510
        // 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) ) );
        }
Alan Mishchenko committed
511

Alan Mishchenko committed
512 513 514 515 516 517 518 519
        // 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
Alan Mishchenko committed
520
    {
Alan Mishchenko committed
521 522 523 524 525
        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 );
Alan Mishchenko committed
526
    }
527
    Aig_ManInvertConstraints( pMan );
Alan Mishchenko committed
528 529 530 531

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
Alan Mishchenko committed
532
    pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
Alan Mishchenko committed
533
//    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
Alan Mishchenko committed
534 535
    Aig_ManForEachNode( pMan, pObj, i )
    {
Alan Mishchenko committed
536
//        Bar_ProgressUpdate( pProgress, i, NULL );
Alan Mishchenko committed
537 538 539
        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) );
Alan Mishchenko committed
540 541 542 543 544 545 546
        assert( uLit0 != uLit1 );
        if ( uLit0 > uLit1 )
        {
            int Temp = uLit0;
            uLit0 = uLit1;
            uLit1 = Temp;
        }
Alan Mishchenko committed
547 548
        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
Alan Mishchenko committed
549 550 551 552 553 554 555 556
        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 );
Alan Mishchenko committed
557
//    Bar_ProgressStop( pProgress );
Alan Mishchenko committed
558 559 560

    // write the buffer
    fwrite( pBuffer, 1, Pos, pFile );
Alan Mishchenko committed
561
    ABC_FREE( pBuffer );
Alan Mishchenko committed
562 563 564 565 566
/*
    // write the symbol table
    if ( fWriteSymbols )
    {
        // write PIs
567
        Aig_ManForEachCi( pMan, pObj, i )
Alan Mishchenko committed
568 569 570 571 572
            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
573
        Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
574 575 576 577
            fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
    }
*/
    // write the comment
Alan Mishchenko committed
578
    fprintf( pFile, "c" );
Alan Mishchenko committed
579
    if ( pMan->pName )
Alan Mishchenko committed
580 581
        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() );
Alan Mishchenko committed
582 583 584 585 586 587 588 589 590
    fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
    fclose( pFile );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


591 592
ABC_NAMESPACE_IMPL_END