ioReadAiger.c 19.3 KB
Newer Older
Alan Mishchenko committed
1 2
/**CFile****************************************************************

Alan Mishchenko committed
3
  FileName    [ioReadAiger.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 read 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: ioReadAiger.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"
31
#include "ioAbc.h"
Alan Mishchenko committed
32

33 34 35
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
36 37 38 39 40 41 42 43 44 45
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

Alan Mishchenko committed
46 47 48 49 50 51 52 53 54 55
  Synopsis    [Extracts one unsigned AIG edge from the input buffer.]

  Description [This procedure is a slightly modified version of Armin Biere's
  procedure "unsigned decode (FILE * file)". ]
  
  SideEffects [Updates the current reading position.]

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
56
static inline unsigned Io_ReadAigerDecode( char ** ppPos )
Alan Mishchenko committed
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
{
    unsigned x = 0, i = 0;
    unsigned char ch;

//    while ((ch = getnoneofch (file)) & 0x80)
    while ((ch = *(*ppPos)++) & 0x80)
        x |= (ch & 0x7f) << (7 * i++);

    return x | (ch << (7 * i));
}

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

  Synopsis    [Decodes the encoded array of literals.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
79
Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries )
Alan Mishchenko committed
80 81 82 83
{
    Vec_Int_t * vLits;
    int Lit, LitPrev, Diff, i;
    vLits = Vec_IntAlloc( nEntries );
Alan Mishchenko committed
84
    LitPrev = Io_ReadAigerDecode( ppPos );
Alan Mishchenko committed
85 86 87 88 89 90
    Vec_IntPush( vLits, LitPrev );
    for ( i = 1; i < nEntries; i++ )
    {
//        Diff = Lit - LitPrev;
//        Diff = (Lit < LitPrev)? -Diff : Diff;
//        Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
Alan Mishchenko committed
91
        Diff = Io_ReadAigerDecode( ppPos );
Alan Mishchenko committed
92 93 94 95 96 97 98 99
        Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
        Lit  = Diff + LitPrev;
        Vec_IntPush( vLits, Lit );
        LitPrev = Lit;
    }
    return vLits;
}

Alan Mishchenko committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117

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

  Synopsis    [Reads the file into a character buffer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
typedef struct buflist {
  char buf[1<<20];
  int nBuf;
  struct buflist * next;
} buflist;

Alan Mishchenko committed
118
static char * Ioa_ReadLoadFileBz2Aig( char * pFileName, int * pFileSize )
Alan Mishchenko committed
119 120 121 122 123 124 125 126
{
    FILE    * pFile;
    int       nFileSize = 0;
    char    * pContents;
    BZFILE  * b;
    int       bzError;
    struct buflist * pNext;
    buflist * bufHead = NULL, * buf = NULL;
127
    int RetValue;
Alan Mishchenko committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141

    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Ioa_ReadLoadFileBz2(): The file is unavailable (absent or open).\n" );
        return NULL;
    }
    b = BZ2_bzReadOpen(&bzError,pFile,0,0,NULL,0);
    if (bzError != BZ_OK) {
        printf( "Ioa_ReadLoadFileBz2(): BZ2_bzReadOpen() failed with error %d.\n",bzError );
        return NULL;
    }
    do {
        if (!bufHead)
Alan Mishchenko committed
142
            buf = bufHead = ABC_ALLOC( buflist, 1 );
Alan Mishchenko committed
143
        else
Alan Mishchenko committed
144
            buf = buf->next = ABC_ALLOC( buflist, 1 );
Alan Mishchenko committed
145 146 147 148 149 150 151 152
        nFileSize += buf->nBuf = BZ2_bzRead(&bzError,b,buf->buf,1<<20);
        buf->next = NULL;
    } while (bzError == BZ_OK);
    if (bzError == BZ_STREAM_END) {
        // we're okay
        char * p;
        int nBytes = 0;
        BZ2_bzReadClose(&bzError,b);
Alan Mishchenko committed
153
        p = pContents = ABC_ALLOC( char, nFileSize + 10 );
Alan Mishchenko committed
154 155 156 157 158 159
        buf = bufHead;
        do {
            memcpy(p+nBytes,buf->buf,buf->nBuf);
            nBytes += buf->nBuf;
//        } while((buf = buf->next));
            pNext = buf->next;
Alan Mishchenko committed
160
            ABC_FREE( buf );
Alan Mishchenko committed
161 162 163 164 165 166 167 168 169 170 171
        } while((buf = pNext));
    } else if (bzError == BZ_DATA_ERROR_MAGIC) {
        // not a BZIP2 file
        BZ2_bzReadClose(&bzError,b);
        fseek( pFile, 0, SEEK_END );
        nFileSize = ftell( pFile );
        if ( nFileSize == 0 )
        {
            printf( "Ioa_ReadLoadFileBz2(): The file is empty.\n" );
            return NULL;
        }
Alan Mishchenko committed
172
        pContents = ABC_ALLOC( char, nFileSize + 10 );
Alan Mishchenko committed
173
        rewind( pFile );
174
        RetValue = fread( pContents, nFileSize, 1, pFile );
Alan Mishchenko committed
175 176 177 178 179 180 181 182
    } else { 
        // Some other error.
        printf( "Ioa_ReadLoadFileBz2(): Unable to read the compressed BLIF.\n" );
        return NULL;
    }
    fclose( pFile );
    // finish off the file with the spare .end line
    // some benchmarks suddenly break off without this line
Alan Mishchenko committed
183 184
//    strcpy( pContents + nFileSize, "\n.end\n" );
    *pFileSize = nFileSize;
Alan Mishchenko committed
185 186 187
    return pContents;
}

Alan Mishchenko committed
188 189
/**Function*************************************************************

Alan Mishchenko committed
190 191 192 193 194 195 196 197 198 199 200 201
  Synopsis    [Reads the file into a character buffer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static char * Ioa_ReadLoadFileGzAig( char * pFileName, int * pFileSize )
{
    const int READ_BLOCK_SIZE = 100000;
202
    gzFile pFile;
Alan Mishchenko committed
203 204 205
    char * pContents;
    int amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
    pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
Alan Mishchenko committed
206
    pContents = ABC_ALLOC( char, nFileSize );        
Alan Mishchenko committed
207 208 209 210
    readBlock = 0;
    while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) {
        //printf("%d: read %d bytes\n", readBlock, amtRead);
        nFileSize += READ_BLOCK_SIZE;
Alan Mishchenko committed
211
        pContents = ABC_REALLOC(char, pContents, nFileSize);
Alan Mishchenko committed
212 213 214 215 216 217 218 219 220 221 222 223 224
        ++readBlock;
    }
    //printf("%d: read %d bytes\n", readBlock, amtRead);
    assert( amtRead != -1 ); // indicates a zlib error
    nFileSize -= (READ_BLOCK_SIZE - amtRead);
    gzclose(pFile);
    *pFileSize = nFileSize;
    return pContents;
}


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

Alan Mishchenko committed
225 226 227 228 229 230 231 232 233
  Synopsis    [Reads the AIG in the binary AIGER format.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
234
Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Alan Mishchenko committed
235
{
Alan Mishchenko committed
236
    ProgressBar * pProgress;
Alan Mishchenko committed
237
    FILE * pFile;
Alan Mishchenko committed
238
    Vec_Ptr_t * vNodes, * vTerms;
Alan Mishchenko committed
239
    Vec_Int_t * vLits = NULL;
Alan Mishchenko committed
240 241
    Abc_Obj_t * pObj, * pNode0, * pNode1;
    Abc_Ntk_t * pNtkNew;
242 243 244
    int nTotal, nInputs, nOutputs, nLatches, nAnds;
    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
    int nFileSize = -1, iTerm, nDigits, i;
Alan Mishchenko committed
245
    char * pContents, * pDrivers = NULL, * pSymbols, * pCur, * pName, * pType;
Alan Mishchenko committed
246
    unsigned uLit0, uLit1, uLit;
247
    int RetValue;
Alan Mishchenko committed
248 249

    // read the file into the buffer
Alan Mishchenko committed
250
    if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
Alan Mishchenko committed
251 252 253
        pContents = Ioa_ReadLoadFileBz2Aig( pFileName, &nFileSize );
    else if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
        pContents = Ioa_ReadLoadFileGzAig( pFileName, &nFileSize );
Alan Mishchenko committed
254 255 256 257 258
    else
    {
//        pContents = Ioa_ReadLoadFile( pFileName );
        nFileSize = Extra_FileSize( pFileName );
        pFile = fopen( pFileName, "rb" );
Alan Mishchenko committed
259
        pContents = ABC_ALLOC( char, nFileSize );
260
        RetValue = fread( pContents, nFileSize, 1, pFile );
Alan Mishchenko committed
261 262 263
        fclose( pFile );
    }

Alan Mishchenko committed
264 265

    // check if the input file format is correct
Alan Mishchenko committed
266
    if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
Alan Mishchenko committed
267 268
    {
        fprintf( stdout, "Wrong input file format.\n" );
269
        ABC_FREE( pContents );
Alan Mishchenko committed
270 271 272
        return NULL;
    }

273 274
    // read the parameters (M I L O A + B C J F)
    pCur = pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
275
    // read the number of objects
276
    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
277
    // read the number of inputs
278
    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
279
    // read the number of latches
280
    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
281
    // read the number of outputs
282
    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
283
    // read the number of nodes
284 285 286
    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
    if ( *pCur == ' ' )
    {
287
//        assert( nOutputs == 0 );
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
        // read the number of properties
        pCur++;
        nBad = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nBad;
    }
    if ( *pCur == ' ' )
    {
        // read the number of properties
        pCur++;
        nConstr = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nConstr;
    }
    if ( *pCur == ' ' )
    {
        // read the number of properties
        pCur++;
        nJust = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nJust;
    }
    if ( *pCur == ' ' )
    {
        // read the number of properties
        pCur++;
        nFair = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
        nOutputs += nFair;
    }
    if ( *pCur != '\n' )
    {
        fprintf( stdout, "The parameter line is in a wrong format.\n" );
        ABC_FREE( pContents );
        return NULL;
    }
    pCur++;

Alan Mishchenko committed
322 323 324
    // check the parameters
    if ( nTotal != nInputs + nLatches + nAnds )
    {
325 326
        fprintf( stdout, "The number of objects does not match.\n" );
        ABC_FREE( pContents );
Alan Mishchenko committed
327 328
        return NULL;
    }
329 330
    if ( nJust || nFair )
    {
331
        fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
        ABC_FREE( pContents );
        return NULL;
    }

    if ( nConstr )
    {
        if ( nConstr == 1 )
            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
        else
            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
    }

    // allocate the empty AIG
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pName = Extra_FileNameGeneric( pFileName );
    pNtkNew->pName = Extra_UtilStrsav( pName );
    pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
    ABC_FREE( pName );
    pNtkNew->nConstrs = nConstr;
Alan Mishchenko committed
351 352 353

    // prepare the array of nodes
    vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
Alan Mishchenko committed
354
    Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );
Alan Mishchenko committed
355 356

    // create the PIs
Alan Mishchenko committed
357
    for ( i = 0; i < nInputs; i++ )
Alan Mishchenko committed
358
    {
Alan Mishchenko committed
359
        pObj = Abc_NtkCreatePi(pNtkNew);    
Alan Mishchenko committed
360 361 362
        Vec_PtrPush( vNodes, pObj );
    }
    // create the POs
Alan Mishchenko committed
363
    for ( i = 0; i < nOutputs; i++ )
Alan Mishchenko committed
364
    {
Alan Mishchenko committed
365
        pObj = Abc_NtkCreatePo(pNtkNew);   
Alan Mishchenko committed
366 367
    }
    // create the latches
368
    nDigits = Abc_Base10Log( nLatches );
Alan Mishchenko committed
369 370
    for ( i = 0; i < nLatches; i++ )
    {
Alan Mishchenko committed
371 372 373 374 375 376
        pObj = Abc_NtkCreateLatch(pNtkNew);
        Abc_LatchSetInit0( pObj );
        pNode0 = Abc_NtkCreateBi(pNtkNew);
        pNode1 = Abc_NtkCreateBo(pNtkNew);
        Abc_ObjAddFanin( pObj, pNode0 );
        Abc_ObjAddFanin( pNode1, pObj );
Alan Mishchenko committed
377 378
        Vec_PtrPush( vNodes, pNode1 );
        // assign names to latch and its input
Alan Mishchenko committed
379 380
//        Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
//        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
Alan Mishchenko committed
381
    } 
Alan Mishchenko committed
382
    
Alan Mishchenko committed
383 384 385

    if ( pContents[3] == ' ' ) // standard AIGER
    {
Alan Mishchenko committed
386 387
        // remember the beginning of latch/PO literals
        pDrivers = pCur;
Alan Mishchenko committed
388 389 390 391 392 393
        // scroll to the beginning of the binary data
        for ( i = 0; i < nLatches + nOutputs; )
            if ( *pCur++ == '\n' )
                i++;
    }
    else // modified AIGER
Alan Mishchenko committed
394
    { 
Alan Mishchenko committed
395
        vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
Alan Mishchenko committed
396
    }
Alan Mishchenko committed
397 398

    // create the AND gates
Alan Mishchenko committed
399
    pProgress = Extra_ProgressBarStart( stdout, nAnds );
Alan Mishchenko committed
400 401
    for ( i = 0; i < nAnds; i++ )
    {
Alan Mishchenko committed
402
        Extra_ProgressBarUpdate( pProgress, i, NULL );
Alan Mishchenko committed
403
        uLit = ((i + 1 + nInputs + nLatches) << 1);
Alan Mishchenko committed
404 405
        uLit1 = uLit  - Io_ReadAigerDecode( &pCur );
        uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
Alan Mishchenko committed
406
//        assert( uLit1 > uLit0 );
407 408
        pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
        pNode1 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
Alan Mishchenko committed
409
        assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
410
        Vec_PtrPush( vNodes, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pNode0, pNode1) );
Alan Mishchenko committed
411
    }
Alan Mishchenko committed
412
    Extra_ProgressBarStop( pProgress );
Alan Mishchenko committed
413 414 415 416 417

    // remember the place where symbols begin
    pSymbols = pCur;

    // read the latch driver literals
Alan Mishchenko committed
418
    pCur = pDrivers;
Alan Mishchenko committed
419
    if ( pContents[3] == ' ' ) // standard AIGER
Alan Mishchenko committed
420
    {
Alan Mishchenko committed
421
        Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
Alan Mishchenko committed
422
        {
423 424 425
            uLit0 = atoi( pCur );  while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
            if ( *pCur == ' ' ) // read initial value
            {
426
                int Init;
427
                pCur++;
428 429
                Init = atoi( pCur );
                if ( Init == 0 )
430
                    Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) );
431
                else if ( Init == 1 )
432
                    Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
433
                else 
434 435 436
                {
                    assert( Init == Abc_Var2Lit(1+Abc_NtkPiNum(pNtkNew)+i, 0) ); 
                    // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf
437
                    Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) );
438
                }
439 440 441 442 443 444 445 446 447
                while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
            }
            if ( *pCur != '\n' )
            {
                fprintf( stdout, "The initial value of latch number %d is not recongnized.\n", i );
                return NULL;
            }
            pCur++;

448
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Alan Mishchenko committed
449
            Abc_ObjAddFanin( pObj, pNode0 );
Alan Mishchenko committed
450 451
        }
        // read the PO driver literals
Alan Mishchenko committed
452
        Abc_NtkForEachPo( pNtkNew, pObj, i )
Alan Mishchenko committed
453 454
        {
            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
455
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Alan Mishchenko committed
456
            Abc_ObjAddFanin( pObj, pNode0 );
Alan Mishchenko committed
457
        }
Alan Mishchenko committed
458
    }
Alan Mishchenko committed
459
    else
Alan Mishchenko committed
460
    {
Alan Mishchenko committed
461
        // read the latch driver literals
Alan Mishchenko committed
462
        Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
Alan Mishchenko committed
463 464
        {
            uLit0 = Vec_IntEntry( vLits, i );
465
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Alan Mishchenko committed
466
            Abc_ObjAddFanin( pObj, pNode0 );
Alan Mishchenko committed
467 468
        }
        // read the PO driver literals
Alan Mishchenko committed
469
        Abc_NtkForEachPo( pNtkNew, pObj, i )
Alan Mishchenko committed
470
        {
Alan Mishchenko committed
471
            uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
472
            pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Alan Mishchenko committed
473
            Abc_ObjAddFanin( pObj, pNode0 );
Alan Mishchenko committed
474 475
        }
        Vec_IntFree( vLits );
Alan Mishchenko committed
476
    }
Alan Mishchenko committed
477
 
Alan Mishchenko committed
478 479
    // read the names if present
    pCur = pSymbols;
480
    if ( pCur < pContents + nFileSize && *pCur != 'c' )
Alan Mishchenko committed
481 482 483 484 485 486 487
    {
        int Counter = 0;
        while ( pCur < pContents + nFileSize && *pCur != 'c' )
        {
            // get the terminal type
            pType = pCur;
            if ( *pCur == 'i' )
Alan Mishchenko committed
488
                vTerms = pNtkNew->vPis;
Alan Mishchenko committed
489
            else if ( *pCur == 'l' )
Alan Mishchenko committed
490
                vTerms = pNtkNew->vBoxes;
491
            else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
Alan Mishchenko committed
492
                vTerms = pNtkNew->vPos;
Alan Mishchenko committed
493 494
            else
            {
495
//                fprintf( stdout, "Wrong terminal type.\n" );
Alan Mishchenko committed
496 497 498 499 500 501 502 503 504 505
                return NULL;
            }
            // get the terminal number
            iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
            // get the node
            if ( iTerm >= Vec_PtrSize(vTerms) )
            {
                fprintf( stdout, "The number of terminal is out of bound.\n" );
                return NULL;
            }
506
            pObj = (Abc_Obj_t *)Vec_PtrEntry( vTerms, iTerm );
Alan Mishchenko committed
507
            if ( *pType == 'l' )
Alan Mishchenko committed
508
                pObj = Abc_ObjFanout0(pObj);
Alan Mishchenko committed
509 510 511 512
            // assign the name
            pName = pCur;          while ( *pCur++ != '\n' );
            // assign this name 
            *(pCur-1) = 0;
Alan Mishchenko committed
513
            Abc_ObjAssignName( pObj, pName, NULL );
Alan Mishchenko committed
514 515
            if ( *pType == 'l' )
            {
Alan Mishchenko committed
516 517
                Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
                Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
Alan Mishchenko committed
518 519
            }
            // mark the node as named
Alan Mishchenko committed
520
            pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
Alan Mishchenko committed
521 522 523
        } 

        // assign the remaining names
Alan Mishchenko committed
524
        Abc_NtkForEachPi( pNtkNew, pObj, i )
Alan Mishchenko committed
525 526
        {
            if ( pObj->pCopy ) continue;
Alan Mishchenko committed
527
            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Alan Mishchenko committed
528 529
            Counter++;
        }
Alan Mishchenko committed
530
        Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
Alan Mishchenko committed
531 532
        {
            if ( pObj->pCopy ) continue;
Alan Mishchenko committed
533 534 535
            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
            Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
            Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
Alan Mishchenko committed
536 537
            Counter++;
        }
Alan Mishchenko committed
538
        Abc_NtkForEachPo( pNtkNew, pObj, i )
Alan Mishchenko committed
539 540
        {
            if ( pObj->pCopy ) continue;
Alan Mishchenko committed
541
            Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Alan Mishchenko committed
542 543
            Counter++;
        }
Alan Mishchenko committed
544 545
//        if ( Counter )
//            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
Alan Mishchenko committed
546 547 548
    }
    else
    {
Alan Mishchenko committed
549 550
//        printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
        Abc_NtkShortNames( pNtkNew );
Alan Mishchenko committed
551
    }
Alan Mishchenko committed
552 553

    // read the name of the model if given
Alan Mishchenko committed
554 555
    pCur = pSymbols;
    if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
Alan Mishchenko committed
556
    {
Alan Mishchenko committed
557 558
        pCur++;
        if ( *pCur == 'n' )
Alan Mishchenko committed
559
        {
Alan Mishchenko committed
560 561
            pCur++;
            // read model name
562 563 564 565 566
            if ( strlen(pCur) > 0 )
            {
                ABC_FREE( pNtkNew->pName );
                pNtkNew->pName = Extra_UtilStrsav( pCur );
            }
Alan Mishchenko committed
567 568 569
        }
    }

Alan Mishchenko committed
570
    // skipping the comments
Alan Mishchenko committed
571
    ABC_FREE( pContents );
Alan Mishchenko committed
572 573 574
    Vec_PtrFree( vNodes );

    // remove the extra nodes
575
    Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
Alan Mishchenko committed
576

577 578 579 580
    // update polarity of the additional outputs
    if ( nBad || nConstr || nJust || nFair )
        Abc_NtkInvertConstraints( pNtkNew );

Alan Mishchenko committed
581
    // check the result
Alan Mishchenko committed
582
    if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
Alan Mishchenko committed
583
    {
Alan Mishchenko committed
584 585
        printf( "Io_ReadAiger: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
Alan Mishchenko committed
586 587
        return NULL;
    }
Alan Mishchenko committed
588
    return pNtkNew;
Alan Mishchenko committed
589 590 591
}


Alan Mishchenko committed
592

Alan Mishchenko committed
593 594 595 596 597
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


598 599
ABC_NAMESPACE_IMPL_END