ioWriteAiger.c 30.1 KB
Newer Older
Alan Mishchenko committed
1 2
/**CFile****************************************************************

Alan Mishchenko committed
3
  FileName    [ioWriteAiger.c]
Alan Mishchenko committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17

  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.]

Alan Mishchenko committed
18
  Revision    [$Id: ioWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
Alan Mishchenko committed
19 20 21

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

Alan Mishchenko committed
22 23
// The code in this file is developed in collaboration with Mark Jarvin of Toronto.

24 25 26 27 28
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

29 30
#include "misc/bzlib/bzlib.h"
#include "misc/zlib/zlib.h"
Alan Mishchenko committed
31
#include "ioAbc.h"
Alan Mishchenko committed
32

Alan Mishchenko committed
33

34 35 36 37

ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
38 39 40 41
#ifdef _WIN32
#define vsnprintf _vsnprintf
#endif

Alan Mishchenko committed
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 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
////////////////////////////////////////////////////////////////////////
///                        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
146
static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;                   }
Alan Mishchenko committed
147
static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj )                   { return (unsigned)(ABC_PTRINT_T)pObj->pCopy;  }
148
static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Num;     }
Alan Mishchenko committed
149 150 151 152 153 154 155

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

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

Alan Mishchenko committed
156 157 158 159 160 161 162 163 164 165
  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
166
int Io_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
Alan Mishchenko committed
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
{
    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*************************************************************

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

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
193
Vec_Int_t * Io_WriteAigerLiterals( Abc_Ntk_t * pNtk )
Alan Mishchenko committed
194 195
{
    Vec_Int_t * vLits;
Alan Mishchenko committed
196
    Abc_Obj_t * pObj, * pDriver;
Alan Mishchenko committed
197
    int i;
Alan Mishchenko committed
198 199
    vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachLatchInput( pNtk, pObj, i )
Alan Mishchenko committed
200
    {
Alan Mishchenko committed
201 202
        pDriver = Abc_ObjFanin0(pObj);
        Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
Alan Mishchenko committed
203
    }
Alan Mishchenko committed
204
    Abc_NtkForEachPo( pNtk, pObj, i )
Alan Mishchenko committed
205
    {
Alan Mishchenko committed
206 207
        pDriver = Abc_ObjFanin0(pObj);
        Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
Alan Mishchenko committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
    }
    return vLits;
}

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

  Synopsis    [Creates the binary encoded array of literals.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
223
Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits )
Alan Mishchenko committed
224 225 226 227 228
{
    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
229
    Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); 
Alan Mishchenko committed
230 231 232 233 234
    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
    {
        Diff = Lit - LitPrev;
        Diff = (Lit < LitPrev)? -Diff : Diff;
        Diff = (Diff << 1) | (int)(Lit < LitPrev);
Alan Mishchenko committed
235
        Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
Alan Mishchenko committed
236 237 238 239 240 241 242 243
        LitPrev = Lit;
        if ( Pos + 10 > vBinary->nCap )
            Vec_StrGrow( vBinary, vBinary->nCap+1 );
    }
    vBinary->nSize = Pos;
/*
    // verify
    {
Alan Mishchenko committed
244
        extern Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries );
Alan Mishchenko committed
245
        char * pPos = Vec_StrArray( vBinary );
Alan Mishchenko committed
246
        Vec_Int_t * vTemp = Io_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
Alan Mishchenko committed
247 248 249 250 251 252 253 254 255 256 257 258 259
        for ( i = 0; i < Vec_IntSize(vLits); i++ )
        {
            int Entry1 = Vec_IntEntry(vLits,i);
            int Entry2 = Vec_IntEntry(vTemp,i);
            assert( Entry1 == Entry2 );
        }
    }
*/
    return vBinary;
}

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

Alan Mishchenko committed
260 261 262 263 264 265 266 267 268
  Synopsis    [Writes the AIG in the binary AIGER format.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
269
void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
Alan Mishchenko committed
270
{
Alan Mishchenko committed
271
    ProgressBar * pProgress;
Alan Mishchenko committed
272
    FILE * pFile;
Alan Mishchenko committed
273
    Abc_Obj_t * pObj, * pDriver;
Alan Mishchenko committed
274
    int i, nNodes, nBufferSize, Pos;
Alan Mishchenko committed
275 276 277
    unsigned char * pBuffer;
    unsigned uLit0, uLit1, uLit;

Alan Mishchenko committed
278
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
279 280 281 282 283 284 285
    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;
        }

Alan Mishchenko committed
286 287 288 289
    // start the output stream
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
Alan Mishchenko committed
290
        fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
Alan Mishchenko committed
291 292
        return;
    }
Alan Mishchenko committed
293

Alan Mishchenko committed
294 295
    // set the node numbers to be used in the output file
    nNodes = 0;
Alan Mishchenko committed
296 297 298 299 300
    Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Io_ObjSetAigerNum( pObj, nNodes++ );
    Abc_AigForEachAnd( pNtk, pObj, i )
        Io_ObjSetAigerNum( pObj, nNodes++ );
Alan Mishchenko committed
301 302

    // write the header "M I L O A" where M = I + L + A
303
    fprintf( pFile, "aig%s %u %u %u %u %u", 
Alan Mishchenko committed
304
        fCompact? "2" : "",
Alan Mishchenko committed
305 306 307
        Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
        Abc_NtkPiNum(pNtk),
        Abc_NtkLatchNum(pNtk),
308
        Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
Alan Mishchenko committed
309
        Abc_NtkNodeNum(pNtk) );
310 311 312 313
    // write the extended header "B C J F"
    if ( Abc_NtkConstrNum(pNtk) )
        fprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
    fprintf( pFile, "\n" );
Alan Mishchenko committed
314 315 316 317 318

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

319
    Abc_NtkInvertConstraints( pNtk );
Alan Mishchenko committed
320
    if ( !fCompact ) 
Alan Mishchenko committed
321
    {
Alan Mishchenko committed
322
        // write latch drivers
Alan Mishchenko committed
323
        Abc_NtkForEachLatchInput( pNtk, pObj, i )
Alan Mishchenko committed
324
        {
Alan Mishchenko committed
325 326
            pDriver = Abc_ObjFanin0(pObj);
            fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
Alan Mishchenko committed
327 328
        }
        // write PO drivers
Alan Mishchenko committed
329
        Abc_NtkForEachPo( pNtk, pObj, i )
Alan Mishchenko committed
330
        {
Alan Mishchenko committed
331 332
            pDriver = Abc_ObjFanin0(pObj);
            fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
Alan Mishchenko committed
333 334 335
        }
    }
    else
Alan Mishchenko committed
336
    {
Alan Mishchenko committed
337 338
        Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
        Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
Alan Mishchenko committed
339 340 341
        fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
        Vec_StrFree( vBinary );
        Vec_IntFree( vLits );
Alan Mishchenko committed
342
    }
343
    Abc_NtkInvertConstraints( pNtk );
Alan Mishchenko committed
344 345 346

    // write the nodes into the buffer
    Pos = 0;
Alan Mishchenko committed
347
    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
Alan Mishchenko committed
348
    pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
Alan Mishchenko committed
349 350
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
    Abc_AigForEachAnd( pNtk, pObj, i )
Alan Mishchenko committed
351
    {
Alan Mishchenko committed
352 353 354 355
        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) );
Alan Mishchenko committed
356
        assert( uLit0 < uLit1 );
Alan Mishchenko committed
357 358
        Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit  - uLit1) );
        Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
Alan Mishchenko committed
359 360
        if ( Pos > nBufferSize - 10 )
        {
Alan Mishchenko committed
361
            printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
Alan Mishchenko committed
362 363 364 365 366
            fclose( pFile );
            return;
        }
    }
    assert( Pos < nBufferSize );
Alan Mishchenko committed
367
    Extra_ProgressBarStop( pProgress );
Alan Mishchenko committed
368 369 370

    // write the buffer
    fwrite( pBuffer, 1, Pos, pFile );
Alan Mishchenko committed
371
    ABC_FREE( pBuffer );
Alan Mishchenko committed
372

Alan Mishchenko committed
373 374 375 376
    // write the symbol table
    if ( fWriteSymbols )
    {
        // write PIs
Alan Mishchenko committed
377 378
        Abc_NtkForEachPi( pNtk, pObj, i )
            fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
Alan Mishchenko committed
379
        // write latches
Alan Mishchenko committed
380 381
        Abc_NtkForEachLatch( pNtk, pObj, i )
            fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
Alan Mishchenko committed
382
        // write POs
Alan Mishchenko committed
383 384
        Abc_NtkForEachPo( pNtk, pObj, i )
            fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
Alan Mishchenko committed
385
    }
Alan Mishchenko committed
386

Alan Mishchenko committed
387 388
    // write the comment
    fprintf( pFile, "c\n" );
Alan Mishchenko committed
389 390 391
    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() );
Alan Mishchenko committed
392 393 394 395
    fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
    fclose( pFile );
}

Alan Mishchenko committed
396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 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 437 438 439
/**Function*************************************************************

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

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
{
    ProgressBar * pProgress;
    gzFile 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 = gzopen( pFileName, "wb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteAigerGz(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
    Abc_NtkForEachLatch( pNtk, pObj, i )
        if ( !Abc_LatchIsInit0(pObj) )
        {
            fprintf( stdout, "Io_WriteAigerGz(): 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
440
    gzprintf( pFile, "aig %u %u %u %u %u", 
Alan Mishchenko committed
441 442 443
              Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
              Abc_NtkPiNum(pNtk),
              Abc_NtkLatchNum(pNtk),
444
              Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
Alan Mishchenko committed
445
              Abc_NtkNodeNum(pNtk) );
446 447 448 449
    // write the extended header "B C J F"
    if ( Abc_NtkConstrNum(pNtk) )
        gzprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
    gzprintf( pFile, "\n" ); 
Alan Mishchenko committed
450 451 452 453 454 455

    // 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
456
    Abc_NtkInvertConstraints( pNtk );
Alan Mishchenko committed
457 458 459 460 461 462 463 464 465 466 467
    Abc_NtkForEachLatchInput( pNtk, pObj, i )
    {
        pDriver = Abc_ObjFanin0(pObj);
        gzprintf( 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);
        gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
    }
468
    Abc_NtkInvertConstraints( pNtk );
Alan Mishchenko committed
469 470 471 472

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
473
    pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
Alan Mishchenko committed
474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
    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" );
            gzclose( pFile );
            return;
        }
    }
    assert( Pos < nBufferSize );
    Extra_ProgressBarStop( pProgress );

    // write the buffer
    gzwrite(pFile, pBuffer, Pos);
Alan Mishchenko committed
496
    ABC_FREE( pBuffer );
Alan Mishchenko committed
497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520

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

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

Alan Mishchenko committed
521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
 
/**Function*************************************************************

  Synopsis    [Procedure to write data into BZ2 file.]

  Description [Based on the vsnprintf() man page.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
typedef struct bz2file {
  FILE   * f;
  BZFILE * b;
  char   * buf;
  int      nBytes;
  int      nBytesMax;
} bz2file;

int fprintfBz2Aig( bz2file * b, char * fmt, ... ) {
    if (b->b) {
        char * newBuf;
        int bzError;
        va_list ap;
        while (1) {
            va_start(ap,fmt);
            b->nBytes = vsnprintf(b->buf,b->nBytesMax,fmt,ap);
            va_end(ap);
            if (b->nBytes > -1 && b->nBytes < b->nBytesMax)
                break;
            if (b->nBytes > -1)
                b->nBytesMax = b->nBytes + 1;
            else
                b->nBytesMax *= 2;
Alan Mishchenko committed
556
            if ((newBuf = ABC_REALLOC( char,b->buf,b->nBytesMax )) == NULL)
Alan Mishchenko committed
557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587
                return -1;
            else
                b->buf = newBuf;
        }
        BZ2_bzWrite( &bzError, b->b, b->buf, b->nBytes );
        if (bzError == BZ_IO_ERROR) {
            fprintf( stdout, "Ioa_WriteBlif(): I/O error writing to compressed stream.\n" );
            return -1;
        }
        return b->nBytes;
    } else {
        int n;
        va_list ap;
        va_start(ap,fmt);
        n = vfprintf( b->f, fmt, ap);
        va_end(ap);
        return n;
    }
}

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

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

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
588
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique )
Alan Mishchenko committed
589 590 591 592
{
    ProgressBar * pProgress;
//    FILE * pFile;
    Abc_Obj_t * pObj, * pDriver;
Alan Mishchenko committed
593
    int i, nNodes, nBufferSize, bzError, Pos;
Alan Mishchenko committed
594 595 596 597
    unsigned char * pBuffer;
    unsigned uLit0, uLit1, uLit;
    bz2file b;

598 599 600 601 602 603 604
    // define unique writing
    if ( fUnique )
    {
        fWriteSymbols = 0;
        fCompact = 0;
    }

Alan Mishchenko committed
605 606 607 608 609 610 611 612 613
    // check that the network is valid
    assert( Abc_NtkIsStrash(pNtk) );
    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;
        }

Alan Mishchenko committed
614 615 616 617 618 619 620
    // write the GZ file
    if (!strncmp(pFileName+strlen(pFileName)-3,".gz",3)) 
    {
        Io_WriteAigerGz( pNtk, pFileName, fWriteSymbols );
        return;
    }

Alan Mishchenko committed
621 622
    memset(&b,0,sizeof(b));
    b.nBytesMax = (1<<12);
Alan Mishchenko committed
623
    b.buf = ABC_ALLOC( char,b.nBytesMax );
Alan Mishchenko committed
624 625 626 627 628 629

    // 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 );
Alan Mishchenko committed
630
        ABC_FREE(b.buf);
Alan Mishchenko committed
631 632 633 634 635 636 637 638
        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 );
Alan Mishchenko committed
639
            ABC_FREE(b.buf);
Alan Mishchenko committed
640 641 642 643 644 645 646 647 648 649 650 651 652
            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
653
    fprintfBz2Aig( &b, "aig%s %u %u %u %u %u", 
Alan Mishchenko committed
654 655 656 657
        fCompact? "2" : "",
        Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
        Abc_NtkPiNum(pNtk),
        Abc_NtkLatchNum(pNtk),
658
        Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
Alan Mishchenko committed
659
        Abc_NtkNodeNum(pNtk) );
660 661 662 663
    // write the extended header "B C J F"
    if ( Abc_NtkConstrNum(pNtk) )
        fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
    fprintfBz2Aig( &b, "\n" );
Alan Mishchenko committed
664 665 666 667 668

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

669
    Abc_NtkInvertConstraints( pNtk );
Alan Mishchenko committed
670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696
    if ( !fCompact ) 
    {
        // write latch drivers
        Abc_NtkForEachLatchInput( pNtk, pObj, i )
        {
            pDriver = Abc_ObjFanin0(pObj);
            fprintfBz2Aig( &b, "%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);
            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 );
Alan Mishchenko committed
697
                ABC_FREE(b.buf);
698
                Vec_StrFree( vBinary );
Alan Mishchenko committed
699 700 701 702 703 704
                return;
            }
        }
        Vec_StrFree( vBinary );
        Vec_IntFree( vLits );
    }
705
    Abc_NtkInvertConstraints( pNtk );
Alan Mishchenko committed
706 707 708 709

    // write the nodes into the buffer
    Pos = 0;
    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
Alan Mishchenko committed
710
    pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
Alan Mishchenko committed
711 712 713 714 715 716 717 718 719 720 721 722 723 724
    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, (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 );
Alan Mishchenko committed
725
            ABC_FREE(b.buf);
726
            Extra_ProgressBarStop( pProgress );
Alan Mishchenko committed
727 728 729 730 731 732 733 734 735 736 737 738 739 740 741
            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 );
Alan Mishchenko committed
742
            ABC_FREE(b.buf);
Alan Mishchenko committed
743 744 745
            return;
        }
    }
Alan Mishchenko committed
746
    ABC_FREE( pBuffer );
Alan Mishchenko committed
747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762

    // 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 )
            fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) );
    }

    // write the comment
Alan Mishchenko committed
763
    fprintfBz2Aig( &b, "c" );
764 765 766 767 768 769 770
    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" );
    }
Alan Mishchenko committed
771 772 773 774 775 776 777

    // 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 );
Alan Mishchenko committed
778
            ABC_FREE(b.buf);
Alan Mishchenko committed
779 780 781 782
            return;
        }
    }
    fclose( b.f );
Alan Mishchenko committed
783
    ABC_FREE(b.buf);
Alan Mishchenko committed
784 785
}

786
ABC_NAMESPACE_IMPL_END
787

788 789
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"
790

791 792
ABC_NAMESPACE_IMPL_START

793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844
/**Function*************************************************************

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

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName )
{
    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++ )
        {
845
            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData, b) );
846
            Aig_ManCi( pAig, k )->fMarkA = Abc_InfoHasBit(pCex->pData, b++);
847 848 849 850 851
        }
        fprintf( pFile, " " );
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) &
                           (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj));
852
        Aig_ManForEachCo( pAig, pObj, k )
853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873
            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 );
}

Alan Mishchenko committed
874 875 876 877 878
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


879 880
ABC_NAMESPACE_IMPL_END