ioaReadAig.c 14.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    [ioaReadAiger.c]

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

  Revision    [$Id: ioaReadAiger.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
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

Alan Mishchenko committed
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
  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     []

***********************************************************************/
unsigned Ioa_ReadAigerDecode( char ** ppPos )
{
    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     []

***********************************************************************/
Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries )
{
    Vec_Int_t * vLits;
    int Lit, LitPrev, Diff, i;
    vLits = Vec_IntAlloc( nEntries );
    LitPrev = Ioa_ReadAigerDecode( ppPos );
    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);
        Diff = Ioa_ReadAigerDecode( ppPos );
        Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
        Lit  = Diff + LitPrev;
        Vec_IntPush( vLits, Lit );
        LitPrev = Lit;
    }
    return vLits;
}


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

Alan Mishchenko committed
94
  Synopsis    [Reads the AIG in from the memory buffer.]
Alan Mishchenko committed
95

Alan Mishchenko committed
96
  Description [The buffer constains the AIG in AIGER format. The size gives
97
  the number of bytes in the buffer. The buffer is allocated by the user 
Alan Mishchenko committed
98
  and not deallocated by this procedure.]
Alan Mishchenko committed
99 100 101 102 103 104
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
105
Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
Alan Mishchenko committed
106
{
Alan Mishchenko committed
107
    Vec_Int_t * vLits = NULL;
Alan Mishchenko committed
108 109
    Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
    Aig_Obj_t * pObj, * pNode0, * pNode1;
Alan Mishchenko committed
110
    Aig_Man_t * pNew;
Alan Mishchenko committed
111
    int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
112
    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
Alan Mishchenko committed
113
    char * pDrivers, * pSymbols, * pCur;//, * pType;
Alan Mishchenko committed
114 115 116
    unsigned uLit0, uLit1, uLit;

    // check if the input file format is correct
Alan Mishchenko committed
117
    if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
Alan Mishchenko committed
118 119 120 121 122
    {
        fprintf( stdout, "Wrong input file format.\n" );
        return NULL;
    }

123 124
    // read the parameters (M I L O A + B C J F)
    pCur = pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
125
    // read the number of objects
126
    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
127
    // read the number of inputs
128
    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
129
    // read the number of latches
130
    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
131
    // read the number of outputs
132
    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
Alan Mishchenko committed
133
    // read the number of nodes
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
    if ( *pCur == ' ' )
    {
        assert( nOutputs == 0 );
        // 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" );
        return NULL;
    }
    pCur++;

Alan Mishchenko committed
171 172 173
    // check the parameters
    if ( nTotal != nInputs + nLatches + nAnds )
    {
174 175 176 177 178 179
        fprintf( stdout, "The number of objects does not match.\n" );
        return NULL;
    }
    if ( nJust || nFair )
    {
        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
Alan Mishchenko committed
180 181 182
        return NULL;
    }

183 184 185 186 187 188 189 190
    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 );
    }

Alan Mishchenko committed
191
    // allocate the empty AIG
Alan Mishchenko committed
192
    pNew = Aig_ManStart( nAnds );
193
    pNew->nConstrs = nConstr;
Alan Mishchenko committed
194 195 196

    // prepare the array of nodes
    vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
Alan Mishchenko committed
197
    Vec_PtrPush( vNodes, Aig_ManConst0(pNew) );
Alan Mishchenko committed
198 199 200 201

    // create the PIs
    for ( i = 0; i < nInputs + nLatches; i++ )
    {
202
        pObj = Aig_ObjCreateCi(pNew);    
Alan Mishchenko committed
203 204 205 206 207 208
        Vec_PtrPush( vNodes, pObj );
    }
/*
    // create the POs
    for ( i = 0; i < nOutputs + nLatches; i++ )
    {
209
        pObj = Aig_ObjCreateCo(pNew);   
Alan Mishchenko committed
210 211 212
    }
*/
    // create the latches
Alan Mishchenko committed
213
    pNew->nRegs = nLatches;
Alan Mishchenko committed
214 215 216 217
/*
    nDigits = Ioa_Base10Log( nLatches );
    for ( i = 0; i < nLatches; i++ )
    {
Alan Mishchenko committed
218
        pObj = Aig_ObjCreateLatch(pNew);
Alan Mishchenko committed
219
        Aig_LatchSetInit0( pObj );
Alan Mishchenko committed
220 221
        pNode0 = Aig_ObjCreateBi(pNew);
        pNode1 = Aig_ObjCreateBo(pNew);
Alan Mishchenko committed
222 223 224 225 226 227 228
        Aig_ObjAddFanin( pObj, pNode0 );
        Aig_ObjAddFanin( pNode1, pObj );
        Vec_PtrPush( vNodes, pNode1 );
        // assign names to latch and its input
//        Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
//        printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id );
    } 
Alan Mishchenko committed
229 230
*/ 

Alan Mishchenko committed
231 232
    // remember the beginning of latch/PO literals
    pDrivers = pCur;
Alan Mishchenko committed
233 234 235 236 237 238 239 240 241 242 243
    if ( pContents[3] == ' ' ) // standard AIGER
    {
        // scroll to the beginning of the binary data
        for ( i = 0; i < nLatches + nOutputs; )
            if ( *pCur++ == '\n' )
                i++;
    }
    else // modified AIGER
    {
        vLits = Ioa_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
    }
Alan Mishchenko committed
244 245

    // create the AND gates
Alan Mishchenko committed
246
//    pProgress = Bar_ProgressStart( stdout, nAnds );
Alan Mishchenko committed
247 248
    for ( i = 0; i < nAnds; i++ )
    {
Alan Mishchenko committed
249
//        Bar_ProgressUpdate( pProgress, i, NULL );
Alan Mishchenko committed
250 251 252 253
        uLit = ((i + 1 + nInputs + nLatches) << 1);
        uLit1 = uLit  - Ioa_ReadAigerDecode( &pCur );
        uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
//        assert( uLit1 > uLit0 );
254 255
        pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
        pNode1 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
Alan Mishchenko committed
256
        assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
Alan Mishchenko committed
257
        Vec_PtrPush( vNodes, Aig_And(pNew, pNode0, pNode1) );
Alan Mishchenko committed
258
    }
Alan Mishchenko committed
259
//    Bar_ProgressStop( pProgress );
Alan Mishchenko committed
260 261 262 263 264 265

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

    // read the latch driver literals
    vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
Alan Mishchenko committed
266
    if ( pContents[3] == ' ' ) // standard AIGER
Alan Mishchenko committed
267
    {
Alan Mishchenko committed
268 269 270 271
        pCur = pDrivers;
        for ( i = 0; i < nLatches; i++ )
        {
            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
272
            pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Alan Mishchenko committed
273 274 275 276 277 278
            Vec_PtrPush( vDrivers, pNode0 );
        }
        // read the PO driver literals
        for ( i = 0; i < nOutputs; i++ )
        {
            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
279
            pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Alan Mishchenko committed
280 281 282
            Vec_PtrPush( vDrivers, pNode0 );
        }

Alan Mishchenko committed
283
    }
Alan Mishchenko committed
284
    else
Alan Mishchenko committed
285
    {
Alan Mishchenko committed
286 287 288 289
        // read the latch driver literals
        for ( i = 0; i < nLatches; i++ )
        {
            uLit0 = Vec_IntEntry( vLits, i );
290
            pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Alan Mishchenko committed
291 292 293 294 295 296
            Vec_PtrPush( vDrivers, pNode0 );
        }
        // read the PO driver literals
        for ( i = 0; i < nOutputs; i++ )
        {
            uLit0 = Vec_IntEntry( vLits, i+nLatches );
297
            pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Alan Mishchenko committed
298 299 300
            Vec_PtrPush( vDrivers, pNode0 );
        }
        Vec_IntFree( vLits );
Alan Mishchenko committed
301 302 303 304
    }

    // create the POs
    for ( i = 0; i < nOutputs; i++ )
305
        Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vDrivers, nLatches + i) );
Alan Mishchenko committed
306
    for ( i = 0; i < nLatches; i++ )
307
        Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vDrivers, i) );
Alan Mishchenko committed
308 309 310 311 312 313 314 315 316 317 318 319 320
    Vec_PtrFree( vDrivers );

/*
    // read the names if present
    pCur = pSymbols;
    if ( *pCur != 'c' )
    {
        int Counter = 0;
        while ( pCur < pContents + nFileSize && *pCur != 'c' )
        {
            // get the terminal type
            pType = pCur;
            if ( *pCur == 'i' )
Alan Mishchenko committed
321
                vTerms = pNew->vPis;
Alan Mishchenko committed
322
            else if ( *pCur == 'l' )
Alan Mishchenko committed
323
                vTerms = pNew->vBoxes;
Alan Mishchenko committed
324
            else if ( *pCur == 'o' )
Alan Mishchenko committed
325
                vTerms = pNew->vPos;
Alan Mishchenko committed
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
            else
            {
                fprintf( stdout, "Wrong terminal type.\n" );
                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;
            }
            pObj = Vec_PtrEntry( vTerms, iTerm );
            if ( *pType == 'l' )
                pObj = Aig_ObjFanout0(pObj);
            // assign the name
            pName = pCur;          while ( *pCur++ != '\n' );
            // assign this name 
            *(pCur-1) = 0;
            Aig_ObjAssignName( pObj, pName, NULL );
            if ( *pType == 'l' )
            {
                Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
                Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
            }
            // mark the node as named
            pObj->pCopy = (Aig_Obj_t *)Aig_ObjName(pObj);
        } 

        // assign the remaining names
357
        Aig_ManForEachCi( pNew, pObj, i )
Alan Mishchenko committed
358 359 360 361 362
        {
            if ( pObj->pCopy ) continue;
            Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
            Counter++;
        }
Alan Mishchenko committed
363
        Aig_ManForEachLatchOutput( pNew, pObj, i )
Alan Mishchenko committed
364 365 366 367 368 369 370
        {
            if ( pObj->pCopy ) continue;
            Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
            Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
            Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
            Counter++;
        }
371
        Aig_ManForEachCo( pNew, pObj, i )
Alan Mishchenko committed
372 373 374 375 376 377 378 379 380 381 382
        {
            if ( pObj->pCopy ) continue;
            Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
            Counter++;
        }
        if ( Counter )
            printf( "Ioa_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
    }
    else
    {
//        printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
Alan Mishchenko committed
383
        Aig_ManShortNames( pNew );
Alan Mishchenko committed
384 385
    }
*/
Alan Mishchenko committed
386 387 388 389 390 391 392 393 394
    pCur = pSymbols;
    if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
    {
        pCur++;
        if ( *pCur == 'n' )
        {
            pCur++;
            // read model name
            ABC_FREE( pNew->pName );
395
            pNew->pName = Abc_UtilStrsav( pCur );
Alan Mishchenko committed
396 397
        }
    }
Alan Mishchenko committed
398 399 400 401 402

    // skipping the comments
    Vec_PtrFree( vNodes );

    // remove the extra nodes
Alan Mishchenko committed
403 404
    Aig_ManCleanup( pNew );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
Alan Mishchenko committed
405

406 407 408 409
    // update polarity of the additional outputs
    if ( nBad || nConstr || nJust || nFair )
        Aig_ManInvertConstraints( pNew );

Alan Mishchenko committed
410
    // check the result
Alan Mishchenko committed
411
    if ( fCheck && !Aig_ManCheck( pNew ) )
Alan Mishchenko committed
412 413
    {
        printf( "Ioa_ReadAiger: The network check has failed.\n" );
Alan Mishchenko committed
414
        Aig_ManStop( pNew );
Alan Mishchenko committed
415 416
        return NULL;
    }
Alan Mishchenko committed
417
    return pNew;
Alan Mishchenko committed
418 419
}

Alan Mishchenko committed
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
/**Function*************************************************************

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

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
{
    FILE * pFile;
    Aig_Man_t * pNew;
    char * pName, * pContents;
436
    int nFileSize, RetValue;
Alan Mishchenko committed
437 438 439 440 441

    // read the file into the buffer
    nFileSize = Ioa_FileSize( pFileName );
    pFile = fopen( pFileName, "rb" );
    pContents = ABC_ALLOC( char, nFileSize );
442
    RetValue = fread( pContents, nFileSize, 1, pFile );
Alan Mishchenko committed
443 444 445 446 447 448 449
    fclose( pFile );

    pNew = Ioa_ReadAigerFromMemory( pContents, nFileSize, fCheck );
    ABC_FREE( pContents );
    if ( pNew )
    {
        pName = Ioa_FileNameGeneric( pFileName );
450
        pNew->pName = Abc_UtilStrsav( pName );
Alan Mishchenko committed
451 452 453 454 455 456
//        pNew->pSpec = Ioa_UtilStrsav( pFileName );
        ABC_FREE( pName );
    }
    return pNew;
}

Alan Mishchenko committed
457 458 459 460 461 462

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


463 464
ABC_NAMESPACE_IMPL_END