1 /**CFile****************************************************************
2 
3   FileName    [giaAiger.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Scalable AIG package.]
8 
9   Synopsis    [Procedures to read/write binary AIGER format developed by
10   Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
11 
12   Author      [Alan Mishchenko]
13 
14   Affiliation [UC Berkeley]
15 
16   Date        [Ver. 1.0. Started - June 20, 2005.]
17 
18   Revision    [$Id: giaAiger.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
19 
20 ***********************************************************************/
21 
22 #include "gia.h"
23 #include "misc/tim/tim.h"
24 #include "base/main/main.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 #define XAIG_VERBOSE 0
29 
30 ////////////////////////////////////////////////////////////////////////
31 ///                        DECLARATIONS                              ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 ////////////////////////////////////////////////////////////////////////
35 ///                     FUNCTION DEFINITIONS                         ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 /**Function*************************************************************
39 
40   Synopsis    []
41 
42   Description []
43 
44   SideEffects []
45 
46   SeeAlso     []
47 
48 ***********************************************************************/
Gia_FileFixName(char * pFileName)49 void Gia_FileFixName( char * pFileName )
50 {
51     char * pName;
52     for ( pName = pFileName; *pName; pName++ )
53         if ( *pName == '>' )
54             *pName = '\\';
55 }
Gia_FileNameGeneric(char * FileName)56 char * Gia_FileNameGeneric( char * FileName )
57 {
58     char * pDot, * pRes;
59     pRes = Abc_UtilStrsav( FileName );
60     if ( (pDot = strrchr( pRes, '.' )) )
61         *pDot = 0;
62     return pRes;
63 }
Gia_FileSize(char * pFileName)64 int Gia_FileSize( char * pFileName )
65 {
66     FILE * pFile;
67     int nFileSize;
68     pFile = fopen( pFileName, "r" );
69     if ( pFile == NULL )
70     {
71         printf( "Gia_FileSize(): The file is unavailable (absent or open).\n" );
72         return 0;
73     }
74     fseek( pFile, 0, SEEK_END );
75     nFileSize = ftell( pFile );
76     fclose( pFile );
77     return nFileSize;
78 }
Gia_FileWriteBufferSize(FILE * pFile,int nSize)79 void Gia_FileWriteBufferSize( FILE * pFile, int nSize )
80 {
81     unsigned char Buffer[5];
82     Gia_AigerWriteInt( Buffer, nSize );
83     fwrite( Buffer, 1, 4, pFile );
84 }
85 
86 /**Function*************************************************************
87 
88   Synopsis    [Create the array of literals to be written.]
89 
90   Description []
91 
92   SideEffects []
93 
94   SeeAlso     []
95 
96 ***********************************************************************/
Gia_AigerCollectLiterals(Gia_Man_t * p)97 Vec_Int_t * Gia_AigerCollectLiterals( Gia_Man_t * p )
98 {
99     Vec_Int_t * vLits;
100     Gia_Obj_t * pObj;
101     int i;
102     vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
103     Gia_ManForEachRi( p, pObj, i )
104         Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
105     Gia_ManForEachPo( p, pObj, i )
106         Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
107     return vLits;
108 }
Gia_AigerReadLiterals(unsigned char ** ppPos,int nEntries)109 Vec_Int_t * Gia_AigerReadLiterals( unsigned char ** ppPos, int nEntries )
110 {
111     Vec_Int_t * vLits;
112     int Lit, LitPrev, Diff, i;
113     vLits = Vec_IntAlloc( nEntries );
114     LitPrev = Gia_AigerReadUnsigned( ppPos );
115     Vec_IntPush( vLits, LitPrev );
116     for ( i = 1; i < nEntries; i++ )
117     {
118 //        Diff = Lit - LitPrev;
119 //        Diff = (Lit < LitPrev)? -Diff : Diff;
120 //        Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
121         Diff = Gia_AigerReadUnsigned( ppPos );
122         Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
123         Lit  = Diff + LitPrev;
124         Vec_IntPush( vLits, Lit );
125         LitPrev = Lit;
126     }
127     return vLits;
128 }
Gia_AigerWriteLiterals(Vec_Int_t * vLits)129 Vec_Str_t * Gia_AigerWriteLiterals( Vec_Int_t * vLits )
130 {
131     Vec_Str_t * vBinary;
132     int Pos = 0, Lit, LitPrev, Diff, i;
133     vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
134     LitPrev = Vec_IntEntry( vLits, 0 );
135     Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev );
136     Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
137     {
138         Diff = Lit - LitPrev;
139         Diff = (Lit < LitPrev)? -Diff : Diff;
140         Diff = (Diff << 1) | (int)(Lit < LitPrev);
141         Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
142         LitPrev = Lit;
143         if ( Pos + 10 > vBinary->nCap )
144             Vec_StrGrow( vBinary, vBinary->nCap+1 );
145     }
146     vBinary->nSize = Pos;
147 /*
148     // verify
149     {
150         extern Vec_Int_t * Gia_AigerReadLiterals( char ** ppPos, int nEntries );
151         char * pPos = Vec_StrArray( vBinary );
152         Vec_Int_t * vTemp = Gia_AigerReadLiterals( &pPos, Vec_IntSize(vLits) );
153         for ( i = 0; i < Vec_IntSize(vLits); i++ )
154         {
155             int Entry1 = Vec_IntEntry(vLits,i);
156             int Entry2 = Vec_IntEntry(vTemp,i);
157             assert( Entry1 == Entry2 );
158         }
159         Vec_IntFree( vTemp );
160     }
161 */
162     return vBinary;
163 }
164 
165 /**Function*************************************************************
166 
167   Synopsis    [Reads the AIG in the binary AIGER format.]
168 
169   Description []
170 
171   SideEffects []
172 
173   SeeAlso     []
174 
175 ***********************************************************************/
Gia_AigerReadFromMemory(char * pContents,int nFileSize,int fGiaSimple,int fSkipStrash,int fCheck)176 Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck )
177 {
178     Gia_Man_t * pNew, * pTemp;
179     Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
180     Vec_Int_t * vNodes, * vDrivers, * vInits = NULL;
181     int iObj, iNode0, iNode1, fHieOnly = 0;
182     int nTotal, nInputs, nOutputs, nLatches, nAnds, i;
183     int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
184     unsigned char * pDrivers, * pSymbols, * pCur;
185     unsigned uLit0, uLit1, uLit;
186 
187     // read the parameters (M I L O A + B C J F)
188     pCur = (unsigned char *)pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
189     // read the number of objects
190     nTotal = atoi( (const char *)pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
191     // read the number of inputs
192     nInputs = atoi( (const char *)pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
193     // read the number of latches
194     nLatches = atoi( (const char *)pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
195     // read the number of outputs
196     nOutputs = atoi( (const char *)pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
197     // read the number of nodes
198     nAnds = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
199     if ( *pCur == ' ' )
200     {
201 //        assert( nOutputs == 0 );
202         // read the number of properties
203         pCur++;
204         nBad = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
205         nOutputs += nBad;
206     }
207     if ( *pCur == ' ' )
208     {
209         // read the number of properties
210         pCur++;
211         nConstr = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
212         nOutputs += nConstr;
213     }
214     if ( *pCur == ' ' )
215     {
216         // read the number of properties
217         pCur++;
218         nJust = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
219         nOutputs += nJust;
220     }
221     if ( *pCur == ' ' )
222     {
223         // read the number of properties
224         pCur++;
225         nFair = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
226         nOutputs += nFair;
227     }
228     if ( *pCur != '\n' )
229     {
230         fprintf( stdout, "The parameter line is in a wrong format.\n" );
231         return NULL;
232     }
233     pCur++;
234 
235     // check the parameters
236     if ( nTotal != nInputs + nLatches + nAnds )
237     {
238         fprintf( stdout, "The number of objects does not match.\n" );
239         return NULL;
240     }
241     if ( nJust || nFair )
242     {
243         fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
244         return NULL;
245     }
246 
247     if ( nConstr )
248     {
249         if ( nConstr == 1 )
250             fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
251         else
252             fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
253     }
254 
255     // allocate the empty AIG
256     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
257     pNew->nConstrs = nConstr;
258     pNew->fGiaSimple = fGiaSimple;
259 
260     // prepare the array of nodes
261     vNodes = Vec_IntAlloc( 1 + nTotal );
262     Vec_IntPush( vNodes, 0 );
263 
264     // create the PIs
265     for ( i = 0; i < nInputs + nLatches; i++ )
266     {
267         iObj = Gia_ManAppendCi(pNew);
268         Vec_IntPush( vNodes, iObj );
269     }
270 
271     // remember the beginning of latch/PO literals
272     pDrivers = pCur;
273     if ( pContents[3] == ' ' ) // standard AIGER
274     {
275         // scroll to the beginning of the binary data
276         for ( i = 0; i < nLatches + nOutputs; )
277             if ( *pCur++ == '\n' )
278                 i++;
279     }
280     else // modified AIGER
281     {
282         vLits = Gia_AigerReadLiterals( &pCur, nLatches + nOutputs );
283     }
284 
285     // create the AND gates
286     if ( !fGiaSimple && !fSkipStrash )
287         Gia_ManHashAlloc( pNew );
288     for ( i = 0; i < nAnds; i++ )
289     {
290         uLit = ((i + 1 + nInputs + nLatches) << 1);
291         uLit1 = uLit  - Gia_AigerReadUnsigned( &pCur );
292         uLit0 = uLit1 - Gia_AigerReadUnsigned( &pCur );
293 //        assert( uLit1 > uLit0 );
294         iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
295         iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
296         assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
297         if ( !fGiaSimple && fSkipStrash )
298         {
299             if ( iNode0 == iNode1 )
300                 Vec_IntPush( vNodes, Gia_ManAppendBuf(pNew, iNode0) );
301             else
302                 Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
303         }
304         else
305             Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
306     }
307     if ( !fGiaSimple && !fSkipStrash )
308         Gia_ManHashStop( pNew );
309 
310     // remember the place where symbols begin
311     pSymbols = pCur;
312 
313     // read the latch driver literals
314     vDrivers = Vec_IntAlloc( nLatches + nOutputs );
315     if ( pContents[3] == ' ' ) // standard AIGER
316     {
317         vInits = Vec_IntAlloc( nLatches );
318         pCur = pDrivers;
319         for ( i = 0; i < nLatches; i++ )
320         {
321             uLit0 = atoi( (char *)pCur );
322             while ( *pCur != ' ' && *pCur != '\n' )
323                 pCur++;
324             if ( *pCur == ' ' )
325             {
326                 pCur++;
327                 Vec_IntPush( vInits, atoi( (char *)pCur ) );
328                 while ( *pCur++ != '\n' );
329             }
330             else
331             {
332                 pCur++;
333                 Vec_IntPush( vInits, 0 );
334             }
335             iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
336             Vec_IntPush( vDrivers, iNode0 );
337         }
338         // read the PO driver literals
339         for ( i = 0; i < nOutputs; i++ )
340         {
341             uLit0 = atoi( (char *)pCur );   while ( *pCur++ != '\n' );
342             iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
343             Vec_IntPush( vDrivers, iNode0 );
344         }
345 
346     }
347     else
348     {
349         // read the latch driver literals
350         for ( i = 0; i < nLatches; i++ )
351         {
352             uLit0 = Vec_IntEntry( vLits, i );
353             iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
354             Vec_IntPush( vDrivers, iNode0 );
355         }
356         // read the PO driver literals
357         for ( i = 0; i < nOutputs; i++ )
358         {
359             uLit0 = Vec_IntEntry( vLits, i+nLatches );
360             iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
361             Vec_IntPush( vDrivers, iNode0 );
362         }
363         Vec_IntFree( vLits );
364     }
365 
366     // create the POs
367     for ( i = 0; i < nOutputs; i++ )
368         Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
369     for ( i = 0; i < nLatches; i++ )
370         Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
371     Vec_IntFree( vDrivers );
372 
373     // create the latches
374     Gia_ManSetRegNum( pNew, nLatches );
375 
376     // read signal names if they are of the special type
377     pCur = pSymbols;
378     if ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
379     {
380         int fBreakUsed = 0;
381         unsigned char * pCurOld = pCur;
382         pNew->vUserPiIds = Vec_IntStartFull( nInputs );
383         pNew->vUserPoIds = Vec_IntStartFull( nOutputs );
384         pNew->vUserFfIds = Vec_IntStartFull( nLatches );
385         while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
386         {
387             int iTerm;
388             char * pType = (char *)pCur;
389             // check terminal type
390             if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l'  )
391             {
392 //                fprintf( stdout, "Wrong terminal type.\n" );
393                 fBreakUsed = 1;
394                 break;
395             }
396             // get terminal number
397             iTerm = atoi( (char *)++pCur );  while ( *pCur++ != ' ' );
398             // skip spaces
399             while ( *pCur == ' ' )
400                 pCur++;
401             // decode the user numbers:
402             // flops are named: @l<num>
403             // PIs are named: @i<num>
404             // POs are named: @o<num>
405             if ( *pCur++ != '@' )
406             {
407                 fBreakUsed = 1;
408                 break;
409             }
410             if ( *pCur == 'i' && *pType == 'i' )
411                 Vec_IntWriteEntry( pNew->vUserPiIds, iTerm, atoi((char *)pCur+1) );
412             else if ( *pCur == 'o' && *pType == 'o' )
413                 Vec_IntWriteEntry( pNew->vUserPoIds, iTerm, atoi((char *)pCur+1) );
414             else if ( *pCur == 'l' && *pType == 'l' )
415                 Vec_IntWriteEntry( pNew->vUserFfIds, iTerm, atoi((char *)pCur+1) );
416             else
417             {
418                 fprintf( stdout, "Wrong name format.\n" );
419                 fBreakUsed = 1;
420                 break;
421             }
422             // skip digits
423             while ( *pCur++ != '\n' );
424         }
425         // in case of abnormal termination, remove the arrays
426         if ( fBreakUsed )
427         {
428             unsigned char * pName;
429             int Entry, nInvars, nConstr, iTerm;
430 
431             Vec_Int_t * vPoNames = Vec_IntStartFull( nOutputs );
432 
433             Vec_IntFreeP( &pNew->vUserPiIds );
434             Vec_IntFreeP( &pNew->vUserPoIds );
435             Vec_IntFreeP( &pNew->vUserFfIds );
436 
437             // try to figure out signal names
438             fBreakUsed = 0;
439             pCur = (unsigned char *)pCurOld;
440             while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
441             {
442                 // get the terminal type
443                 if ( *pCur == 'i' || *pCur == 'l' )
444                 {
445                     // skip till the end of the line
446                     while ( *pCur++ != '\n' );
447                     *(pCur-1) = 0;
448                     continue;
449                 }
450                 if ( *pCur != 'o' )
451                 {
452 //                    fprintf( stdout, "Wrong terminal type.\n" );
453                     fBreakUsed = 1;
454                     break;
455                 }
456                 // get the terminal number
457                 iTerm = atoi( (char *)++pCur );  while ( *pCur++ != ' ' );
458                 // get the node
459                 if ( iTerm < 0 || iTerm >= nOutputs )
460                 {
461                     fprintf( stdout, "The output number (%d) is out of range.\n", iTerm );
462                     fBreakUsed = 1;
463                     break;
464                 }
465                 if ( Vec_IntEntry(vPoNames, iTerm) != ~0 )
466                 {
467                     fprintf( stdout, "The output number (%d) is listed twice.\n", iTerm );
468                     fBreakUsed = 1;
469                     break;
470                 }
471 
472                 // get the name
473                 pName = pCur;          while ( *pCur++ != '\n' );
474                 *(pCur-1) = 0;
475                 // assign the name
476                 Vec_IntWriteEntry( vPoNames, iTerm, pName - (unsigned char *)pContents );
477             }
478 
479             // check that all names are assigned
480             if ( !fBreakUsed )
481             {
482                 nInvars = nConstr = 0;
483                 vPoTypes = Vec_IntStart( Gia_ManPoNum(pNew) );
484                 Vec_IntForEachEntry( vPoNames, Entry, i )
485                 {
486                     if ( Entry == ~0 )
487                         continue;
488                     if ( strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
489                     {
490                         Vec_IntWriteEntry( vPoTypes, i, 1 );
491                         nConstr++;
492                     }
493                     if ( strncmp( pContents+Entry, "invariant:", 10 ) == 0 )
494                     {
495                         Vec_IntWriteEntry( vPoTypes, i, 2 );
496                         nInvars++;
497                     }
498                 }
499                 if ( nConstr )
500                     fprintf( stdout, "Recognized and added %d constraints.\n", nConstr );
501                 if ( nInvars )
502                     fprintf( stdout, "Recognized and skipped %d invariants.\n", nInvars );
503                 if ( nConstr == 0 && nInvars == 0 )
504                     Vec_IntFreeP( &vPoTypes );
505             }
506             Vec_IntFree( vPoNames );
507         }
508     }
509 
510 
511     // check if there are other types of information to read
512     if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
513     {
514         int fVerbose = XAIG_VERBOSE;
515         Vec_Str_t * vStr;
516         unsigned char * pCurTemp;
517         pCur++;
518         // skip new line if present
519 //        if ( *pCur == '\n' )
520 //            pCur++;
521         while ( pCur < (unsigned char *)pContents + nFileSize )
522         {
523             // read extra AIG
524             if ( *pCur == 'a' )
525             {
526                 pCur++;
527                 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );             pCur += 4;
528                 memcpy( Vec_StrArray(vStr), pCur, (size_t)Vec_StrSize(vStr) );
529                 pCur += Vec_StrSize(vStr);
530                 pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0, 0 );
531                 Vec_StrFree( vStr );
532                 if ( fVerbose ) printf( "Finished reading extension \"a\".\n" );
533             }
534             // read number of constraints
535             else if ( *pCur == 'c' )
536             {
537                 pCur++;
538                 assert( Gia_AigerReadInt(pCur) == 4 );                     pCur += 4;
539                 pNew->nConstrs = Gia_AigerReadInt( pCur );                 pCur += 4;
540                 if ( fVerbose ) printf( "Finished reading extension \"c\".\n" );
541             }
542             // read delay information
543             else if ( *pCur == 'd' )
544             {
545                 pCur++;
546                 assert( Gia_AigerReadInt(pCur) == 4 );                     pCur += 4;
547                 pNew->nAnd2Delay = Gia_AigerReadInt(pCur);                 pCur += 4;
548                 if ( fVerbose ) printf( "Finished reading extension \"d\".\n" );
549             }
550             else if ( *pCur == 'i' )
551             {
552                 pCur++;
553                 nInputs = Gia_AigerReadInt(pCur)/4;                        pCur += 4;
554                 pNew->vInArrs  = Vec_FltStart( nInputs );
555                 memcpy( Vec_FltArray(pNew->vInArrs),  pCur, (size_t)4*nInputs );   pCur += 4*nInputs;
556                 if ( fVerbose ) printf( "Finished reading extension \"i\".\n" );
557             }
558             else if ( *pCur == 'o' )
559             {
560                 pCur++;
561                 nOutputs = Gia_AigerReadInt(pCur)/4;                       pCur += 4;
562                 pNew->vOutReqs  = Vec_FltStart( nOutputs );
563                 memcpy( Vec_FltArray(pNew->vOutReqs),  pCur, (size_t)4*nOutputs ); pCur += 4*nOutputs;
564                 if ( fVerbose ) printf( "Finished reading extension \"o\".\n" );
565             }
566             // read equivalence classes
567             else if ( *pCur == 'e' )
568             {
569                 extern Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize );
570                 pCur++;
571                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;              pCur += 4;
572                 pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
573                 pNew->pNexts = Gia_ManDeriveNexts( pNew );
574                 assert( pCur == pCurTemp );
575                 if ( fVerbose ) printf( "Finished reading extension \"e\".\n" );
576             }
577             // read flop classes
578             else if ( *pCur == 'f' )
579             {
580                 pCur++;
581                 assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) );   pCur += 4;
582                 pNew->vFlopClasses  = Vec_IntStart( Gia_ManRegNum(pNew) );
583                 memcpy( Vec_IntArray(pNew->vFlopClasses),  pCur, (size_t)4*Gia_ManRegNum(pNew) );   pCur += 4*Gia_ManRegNum(pNew);
584                 if ( fVerbose ) printf( "Finished reading extension \"f\".\n" );
585             }
586             // read gate classes
587             else if ( *pCur == 'g' )
588             {
589                 pCur++;
590                 assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) );   pCur += 4;
591                 pNew->vGateClasses  = Vec_IntStart( Gia_ManObjNum(pNew) );
592                 memcpy( Vec_IntArray(pNew->vGateClasses),  pCur, (size_t)4*Gia_ManObjNum(pNew) );   pCur += 4*Gia_ManObjNum(pNew);
593                 if ( fVerbose ) printf( "Finished reading extension \"g\".\n" );
594             }
595             // read hierarchy information
596             else if ( *pCur == 'h' )
597             {
598                 pCur++;
599                 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );          pCur += 4;
600                 memcpy( Vec_StrArray(vStr), pCur, (size_t)Vec_StrSize(vStr) );
601                 pCur += Vec_StrSize(vStr);
602                 pNew->pManTime = Tim_ManLoad( vStr, 1 );
603                 Vec_StrFree( vStr );
604                 fHieOnly = 1;
605                 if ( fVerbose ) printf( "Finished reading extension \"h\".\n" );
606             }
607             // read packing
608             else if ( *pCur == 'k' )
609             {
610                 extern Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize );
611                 int nSize;
612                 pCur++;
613                 nSize = Gia_AigerReadInt(pCur);
614                 pCurTemp = pCur + nSize + 4;                            pCur += 4;
615                 pNew->vPacking = Gia_AigerReadPacking( &pCur, nSize );
616                 assert( pCur == pCurTemp );
617                 if ( fVerbose ) printf( "Finished reading extension \"k\".\n" );
618             }
619             // read mapping
620             else if ( *pCur == 'm' )
621             {
622                 extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
623                 extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize );
624                 extern Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs );
625                 int nSize;
626                 pCur++;
627                 nSize = Gia_AigerReadInt(pCur);
628                 pCurTemp = pCur + nSize + 4;           pCur += 4;
629                 pNew->vMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew) );
630                 assert( pCur == pCurTemp );
631                 if ( fVerbose ) printf( "Finished reading extension \"m\".\n" );
632             }
633             // read model name
634             else if ( *pCur == 'n' )
635             {
636                 pCur++;
637                 if ( (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z') || (*pCur >= '0' && *pCur <= '9') )
638                 {
639                     pNew->pName = Abc_UtilStrsav( (char *)pCur );       pCur += strlen(pNew->pName) + 1;
640                 }
641                 else
642                 {
643                     pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;       pCur += 4;
644                     ABC_FREE( pNew->pName );
645                     pNew->pName = Abc_UtilStrsav( (char *)pCur );       pCur += strlen(pNew->pName) + 1;
646                     assert( pCur == pCurTemp );
647                 }
648             }
649             // read placement
650             else if ( *pCur == 'p' )
651             {
652                 Gia_Plc_t * pPlacement;
653                 pCur++;
654                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
655                 pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) );
656                 memcpy( pPlacement, pCur, (size_t)4*Gia_ManObjNum(pNew) );      pCur += 4*Gia_ManObjNum(pNew);
657                 assert( pCur == pCurTemp );
658                 pNew->pPlacement = pPlacement;
659                 if ( fVerbose ) printf( "Finished reading extension \"p\".\n" );
660             }
661             // read register classes
662             else if ( *pCur == 'r' )
663             {
664                 int i, nRegs;
665                 pCur++;
666                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
667                 nRegs = Gia_AigerReadInt(pCur);                         pCur += 4;
668                 //nRegs = (pCurTemp - pCur)/4;
669                 pNew->vRegClasses = Vec_IntAlloc( nRegs );
670                 for ( i = 0; i < nRegs; i++ )
671                     Vec_IntPush( pNew->vRegClasses, Gia_AigerReadInt(pCur) ), pCur += 4;
672                 assert( pCur == pCurTemp );
673                 if ( fVerbose ) printf( "Finished reading extension \"r\".\n" );
674             }
675             // read register inits
676             else if ( *pCur == 's' )
677             {
678                 int i, nRegs;
679                 pCur++;
680                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
681                 nRegs = Gia_AigerReadInt(pCur);                         pCur += 4;
682                 pNew->vRegInits = Vec_IntAlloc( nRegs );
683                 for ( i = 0; i < nRegs; i++ )
684                     Vec_IntPush( pNew->vRegInits, Gia_AigerReadInt(pCur) ), pCur += 4;
685                 assert( pCur == pCurTemp );
686                 if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
687             }
688             // read configuration data
689             else if ( *pCur == 'b' )
690             {
691                 int nSize;
692                 pCur++;
693                 nSize = Gia_AigerReadInt(pCur);
694                 pCurTemp = pCur + nSize + 4;                            pCur += 4;
695                 pNew->pCellStr = Abc_UtilStrsav( (char*)pCur );         pCur += strlen((char*)pCur) + 1;
696                 nSize = nSize - strlen(pNew->pCellStr) - 1;
697                 assert( nSize % 4 == 0 );
698                 pNew->vConfigs = Vec_IntAlloc(nSize / 4);
699 //                memcpy(Vec_IntArray(pNew->vConfigs), pCur, (size_t)nSize);      pCur += nSize;
700                 for ( i = 0; i < nSize / 4; i++ )
701                     Vec_IntPush( pNew->vConfigs, Gia_AigerReadInt(pCur) ), pCur += 4;
702                 assert( pCur == pCurTemp );
703                 if ( fVerbose ) printf( "Finished reading extension \"b\".\n" );
704             }
705             // read choices
706             else if ( *pCur == 'q' )
707             {
708                 int i, nPairs, iRepr, iNode;
709                 assert( !Gia_ManHasChoices(pNew) );
710                 pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(pNew) );
711                 pCur++;
712                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
713                 nPairs = Gia_AigerReadInt(pCur);                        pCur += 4;
714                 for ( i = 0; i < nPairs; i++ )
715                 {
716                     iRepr = Gia_AigerReadInt(pCur);                     pCur += 4;
717                     iNode = Gia_AigerReadInt(pCur);                     pCur += 4;
718                     pNew->pSibls[iRepr] = iNode;
719                     assert( iRepr > iNode );
720                 }
721                 assert( pCur == pCurTemp );
722                 if ( fVerbose ) printf( "Finished reading extension \"q\".\n" );
723             }
724             // read switching activity
725             else if ( *pCur == 'u' )
726             {
727                 unsigned char * pSwitching;
728                 pCur++;
729                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
730                 pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) );
731                 memcpy( pSwitching, pCur, (size_t)Gia_ManObjNum(pNew) );        pCur += Gia_ManObjNum(pNew);
732                 assert( pCur == pCurTemp );
733                 if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
734             }
735             // read timing manager
736             else if ( *pCur == 't' )
737             {
738                 pCur++;
739                 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );          pCur += 4;
740                 memcpy( Vec_StrArray(vStr), pCur, (size_t)Vec_StrSize(vStr) );  pCur += Vec_StrSize(vStr);
741                 pNew->pManTime = Tim_ManLoad( vStr, 0 );
742                 Vec_StrFree( vStr );
743                 if ( fVerbose ) printf( "Finished reading extension \"t\".\n" );
744             }
745             // read object classes
746             else if ( *pCur == 'v' )
747             {
748                 pCur++;
749                 pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4;
750                 memcpy( Vec_IntArray(pNew->vObjClasses), pCur, (size_t)4*Vec_IntSize(pNew->vObjClasses) );
751                 pCur += 4*Vec_IntSize(pNew->vObjClasses);
752                 if ( fVerbose ) printf( "Finished reading extension \"v\".\n" );
753             }
754             // read edge information
755             else if ( *pCur == 'w' )
756             {
757                 Vec_Int_t * vPairs;
758                 int i, nPairs;
759                 pCur++;
760                 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
761                 nPairs = Gia_AigerReadInt(pCur);                        pCur += 4;
762                 vPairs = Vec_IntAlloc( 2*nPairs );
763                 for ( i = 0; i < 2*nPairs; i++ )
764                     Vec_IntPush( vPairs, Gia_AigerReadInt(pCur) ),      pCur += 4;
765                 assert( pCur == pCurTemp );
766                 if ( fSkipStrash )
767                 {
768                     Gia_ManEdgeFromArray( pNew, vPairs );
769                     if ( fVerbose ) printf( "Finished reading extension \"w\".\n" );
770                 }
771                 else
772                     printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
773                 Vec_IntFree( vPairs );
774             }
775             else break;
776         }
777     }
778 
779     // skipping the comments
780     Vec_IntFree( vNodes );
781 
782     // update polarity of the additional outputs
783     if ( nBad || nConstr || nJust || nFair )
784         Gia_ManInvertConstraints( pNew );
785 
786     // clean the PO drivers
787     if ( vPoTypes )
788     {
789         pNew = Gia_ManDupWithConstraints( pTemp = pNew, vPoTypes );
790         Gia_ManStop( pTemp );
791         Vec_IntFreeP( &vPoTypes );
792     }
793 
794     if ( !fGiaSimple && !fSkipStrash && Gia_ManHasDangling(pNew) )
795     {
796         Tim_Man_t * pManTime;
797         Gia_Man_t * pAigExtra;
798         Vec_Int_t * vFlopMap, * vGateMap, * vObjMap, * vRegClasses, * vRegInits;
799         vRegClasses = pNew->vRegClasses;  pNew->vRegClasses    = NULL;
800         vRegInits   = pNew->vRegInits;    pNew->vRegInits      = NULL;
801         vFlopMap    = pNew->vFlopClasses; pNew->vFlopClasses   = NULL;
802         vGateMap    = pNew->vGateClasses; pNew->vGateClasses   = NULL;
803         vObjMap     = pNew->vObjClasses;  pNew->vObjClasses    = NULL;
804         pManTime = (Tim_Man_t *)pNew->pManTime; pNew->pManTime = NULL;
805         pAigExtra   = pNew->pAigExtra;    pNew->pAigExtra      = NULL;
806         pNew = Gia_ManCleanup( pTemp = pNew );
807         if ( (vGateMap || vObjMap) && (Gia_ManObjNum(pNew) < Gia_ManObjNum(pTemp)) )
808             printf( "Cleanup removed objects after reading. Old gate/object abstraction maps are invalid!\n" );
809         Gia_ManStop( pTemp );
810         pNew->vRegClasses  = vRegClasses;
811         pNew->vRegInits    = vRegInits;
812         pNew->vFlopClasses = vFlopMap;
813         pNew->vGateClasses = vGateMap;
814         pNew->vObjClasses  = vObjMap;
815         pNew->pManTime     = pManTime;
816         pNew->pAigExtra    = pAigExtra;
817     }
818 
819     if ( fHieOnly )
820     {
821 //        Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
822         if ( Abc_FrameReadLibBox() == NULL )
823             printf( "Warning: Creating unit-delay box delay tables because box library is not available.\n" );
824         Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs );
825     }
826     Vec_FltFreeP( &pNew->vInArrs );
827     Vec_FltFreeP( &pNew->vOutReqs );
828 /*
829     // check the result
830     if ( fCheck && !Gia_ManCheck( pNew ) )
831     {
832         printf( "Gia_AigerRead: The network check has failed.\n" );
833         Gia_ManStop( pNew );
834         return NULL;
835     }
836 */
837 
838     if ( vInits && Vec_IntSum(vInits) )
839     {
840         char * pInit = ABC_ALLOC( char, Vec_IntSize(vInits) + 1 );
841         Gia_Obj_t * pObj;
842         int i;
843         assert( Vec_IntSize(vInits) == Gia_ManRegNum(pNew) );
844         Gia_ManForEachRo( pNew, pObj, i )
845         {
846             if ( Vec_IntEntry(vInits, i) == 0 )
847                 pInit[i] = '0';
848             else if ( Vec_IntEntry(vInits, i) == 1 )
849                 pInit[i] = '1';
850             else
851             {
852                 assert( Vec_IntEntry(vInits, i) == Abc_Var2Lit(Gia_ObjId(pNew, pObj), 0) );
853                 // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf
854                 pInit[i] = 'X';
855             }
856         }
857         pInit[i] = 0;
858         pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 );
859         pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
860         Gia_ManStop( pTemp );
861         ABC_FREE( pInit );
862     }
863     Vec_IntFreeP( &vInits );
864     if ( !fGiaSimple && !fSkipStrash && pNew->vMapping )
865     {
866         Abc_Print( 0, "Structural hashing enabled while reading AIGER invalidated the mapping.  Consider using \"&r -s\".\n" );
867         Vec_IntFreeP( &pNew->vMapping );
868     }
869     return pNew;
870 }
871 
872 /**Function*************************************************************
873 
874   Synopsis    [Reads the AIG in the binary AIGER format.]
875 
876   Description []
877 
878   SideEffects []
879 
880   SeeAlso     []
881 
882 ***********************************************************************/
Gia_AigerRead(char * pFileName,int fGiaSimple,int fSkipStrash,int fCheck)883 Gia_Man_t * Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck )
884 {
885     FILE * pFile;
886     Gia_Man_t * pNew;
887     char * pName, * pContents;
888     int nFileSize;
889     int RetValue;
890 
891     // read the file into the buffer
892     Gia_FileFixName( pFileName );
893     nFileSize = Gia_FileSize( pFileName );
894     pFile = fopen( pFileName, "rb" );
895     pContents = ABC_ALLOC( char, nFileSize );
896     RetValue = fread( pContents, nFileSize, 1, pFile );
897     fclose( pFile );
898 
899     pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fGiaSimple, fSkipStrash, fCheck );
900     ABC_FREE( pContents );
901     if ( pNew )
902     {
903         ABC_FREE( pNew->pName );
904         pName = Gia_FileNameGeneric( pFileName );
905         pNew->pName = Abc_UtilStrsav( pName );
906         ABC_FREE( pName );
907 
908         assert( pNew->pSpec == NULL );
909         pNew->pSpec = Abc_UtilStrsav( pFileName );
910     }
911     return pNew;
912 }
913 
914 
915 
916 /**Function*************************************************************
917 
918   Synopsis    [Writes the AIG in into the memory buffer.]
919 
920   Description [The resulting buffer constains the AIG in AIGER format.
921   The resulting buffer should be deallocated by the user.]
922 
923   SideEffects []
924 
925   SeeAlso     []
926 
927 ***********************************************************************/
Gia_AigerWriteIntoMemoryStr(Gia_Man_t * p)928 Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p )
929 {
930     Vec_Str_t * vBuffer;
931     Gia_Obj_t * pObj;
932     int nNodes = 0, i, uLit, uLit0, uLit1;
933     // set the node numbers to be used in the output file
934     Gia_ManConst0(p)->Value = nNodes++;
935     Gia_ManForEachCi( p, pObj, i )
936         pObj->Value = nNodes++;
937     Gia_ManForEachAnd( p, pObj, i )
938         pObj->Value = nNodes++;
939 
940     // write the header "M I L O A" where M = I + L + A
941     vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
942     Vec_StrPrintStr( vBuffer, "aig " );
943     Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
944     Vec_StrPrintStr( vBuffer, " " );
945     Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
946     Vec_StrPrintStr( vBuffer, " " );
947     Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
948     Vec_StrPrintStr( vBuffer, " " );
949     Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
950     Vec_StrPrintStr( vBuffer, " " );
951     Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
952     Vec_StrPrintStr( vBuffer, "\n" );
953 
954     // write latch drivers
955     Gia_ManForEachRi( p, pObj, i )
956     {
957         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
958         Vec_StrPrintNum( vBuffer, uLit );
959         Vec_StrPrintStr( vBuffer, "\n" );
960     }
961 
962     // write PO drivers
963     Gia_ManForEachPo( p, pObj, i )
964     {
965         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
966         Vec_StrPrintNum( vBuffer, uLit );
967         Vec_StrPrintStr( vBuffer, "\n" );
968     }
969     // write the nodes into the buffer
970     Gia_ManForEachAnd( p, pObj, i )
971     {
972         uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
973         uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
974         uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
975         assert( uLit0 != uLit1 );
976         if ( uLit0 > uLit1 )
977         {
978             int Temp = uLit0;
979             uLit0 = uLit1;
980             uLit1 = Temp;
981         }
982         Gia_AigerWriteUnsigned( vBuffer, uLit  - uLit1 );
983         Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
984     }
985     Vec_StrPrintStr( vBuffer, "c" );
986     return vBuffer;
987 }
988 
989 /**Function*************************************************************
990 
991   Synopsis    [Writes the AIG in into the memory buffer.]
992 
993   Description [The resulting buffer constains the AIG in AIGER format.
994   The CI/CO/AND nodes are assumed to be ordered according to some rule.
995   The resulting buffer should be deallocated by the user.]
996 
997   SideEffects [Note that in vCos, PIs are order first, followed by latches!]
998 
999   SeeAlso     []
1000 
1001 ***********************************************************************/
Gia_AigerWriteIntoMemoryStrPart(Gia_Man_t * p,Vec_Int_t * vCis,Vec_Int_t * vAnds,Vec_Int_t * vCos,int nRegs)1002 Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
1003 {
1004     Vec_Str_t * vBuffer;
1005     Gia_Obj_t * pObj;
1006     int nNodes = 0, i, uLit, uLit0, uLit1;
1007     // set the node numbers to be used in the output file
1008     Gia_ManConst0(p)->Value = nNodes++;
1009     Gia_ManForEachObjVec( vCis, p, pObj, i )
1010     {
1011         assert( Gia_ObjIsCi(pObj) );
1012         pObj->Value = nNodes++;
1013     }
1014     Gia_ManForEachObjVec( vAnds, p, pObj, i )
1015     {
1016         assert( Gia_ObjIsAnd(pObj) );
1017         pObj->Value = nNodes++;
1018     }
1019 
1020     // write the header "M I L O A" where M = I + L + A
1021     vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
1022     Vec_StrPrintStr( vBuffer, "aig " );
1023     Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) );
1024     Vec_StrPrintStr( vBuffer, " " );
1025     Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs );
1026     Vec_StrPrintStr( vBuffer, " " );
1027     Vec_StrPrintNum( vBuffer, nRegs );
1028     Vec_StrPrintStr( vBuffer, " " );
1029     Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs );
1030     Vec_StrPrintStr( vBuffer, " " );
1031     Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) );
1032     Vec_StrPrintStr( vBuffer, "\n" );
1033 
1034     // write latch drivers
1035     Gia_ManForEachObjVec( vCos, p, pObj, i )
1036     {
1037         assert( Gia_ObjIsCo(pObj) );
1038         if ( i < Vec_IntSize(vCos) - nRegs )
1039             continue;
1040         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1041         Vec_StrPrintNum( vBuffer, uLit );
1042         Vec_StrPrintStr( vBuffer, "\n" );
1043     }
1044     // write output drivers
1045     Gia_ManForEachObjVec( vCos, p, pObj, i )
1046     {
1047         assert( Gia_ObjIsCo(pObj) );
1048         if ( i >= Vec_IntSize(vCos) - nRegs )
1049             continue;
1050         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1051         Vec_StrPrintNum( vBuffer, uLit );
1052         Vec_StrPrintStr( vBuffer, "\n" );
1053     }
1054 
1055     // write the nodes into the buffer
1056     Gia_ManForEachObjVec( vAnds, p, pObj, i )
1057     {
1058         uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
1059         uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1060         uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
1061         assert( uLit0 != uLit1 );
1062         if ( uLit0 > uLit1 )
1063         {
1064             int Temp = uLit0;
1065             uLit0 = uLit1;
1066             uLit1 = Temp;
1067         }
1068         Gia_AigerWriteUnsigned( vBuffer, uLit  - uLit1 );
1069         Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
1070     }
1071     Vec_StrPrintStr( vBuffer, "c" );
1072     return vBuffer;
1073 }
1074 
1075 /**Function*************************************************************
1076 
1077   Synopsis    [Writes the AIG in the binary AIGER format.]
1078 
1079   Description []
1080 
1081   SideEffects []
1082 
1083   SeeAlso     []
1084 
1085 ***********************************************************************/
Gia_AigerWrite(Gia_Man_t * pInit,char * pFileName,int fWriteSymbols,int fCompact,int fWriteNewLine)1086 void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine )
1087 {
1088     int fVerbose = XAIG_VERBOSE;
1089     FILE * pFile;
1090     Gia_Man_t * p;
1091     Gia_Obj_t * pObj;
1092     Vec_Str_t * vStrExt;
1093     int i, nBufferSize, Pos;
1094     unsigned char * pBuffer;
1095     unsigned uLit0, uLit1, uLit;
1096     assert( pInit->nXors == 0 && pInit->nMuxes == 0 );
1097 
1098     if ( Gia_ManCoNum(pInit) == 0 )
1099     {
1100         printf( "AIG cannot be written because it has no POs.\n" );
1101         return;
1102     }
1103 
1104     // start the output stream
1105     pFile = fopen( pFileName, "wb" );
1106     if ( pFile == NULL )
1107     {
1108         fprintf( stdout, "Gia_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName );
1109         return;
1110     }
1111 
1112     // create normalized AIG
1113     if ( !Gia_ManIsNormalized(pInit) )
1114     {
1115 //        printf( "Gia_AigerWrite(): Normalizing AIG for writing.\n" );
1116         p = Gia_ManDupNormalize( pInit, 0 );
1117         Gia_ManTransferMapping( p, pInit );
1118         Gia_ManTransferPacking( p, pInit );
1119         Gia_ManTransferTiming( p, pInit );
1120         p->nConstrs   = pInit->nConstrs;
1121     }
1122     else
1123         p = pInit;
1124 
1125     // write the header "M I L O A" where M = I + L + A
1126     fprintf( pFile, "aig%s %u %u %u %u %u",
1127         fCompact? "2" : "",
1128         Gia_ManCiNum(p) + Gia_ManAndNum(p),
1129         Gia_ManPiNum(p),
1130         Gia_ManRegNum(p),
1131         Gia_ManConstrNum(p) ? 0 : Gia_ManPoNum(p),
1132         Gia_ManAndNum(p) );
1133     // write the extended header "B C J F"
1134     if ( Gia_ManConstrNum(p) )
1135         fprintf( pFile, " %u %u", Gia_ManPoNum(p) - Gia_ManConstrNum(p), Gia_ManConstrNum(p) );
1136     fprintf( pFile, "\n" );
1137 
1138     Gia_ManInvertConstraints( p );
1139     if ( !fCompact )
1140     {
1141         // write latch drivers
1142         Gia_ManForEachRi( p, pObj, i )
1143             fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) );
1144         // write PO drivers
1145         Gia_ManForEachPo( p, pObj, i )
1146             fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) );
1147     }
1148     else
1149     {
1150         Vec_Int_t * vLits = Gia_AigerCollectLiterals( p );
1151         Vec_Str_t * vBinary = Gia_AigerWriteLiterals( vLits );
1152         fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
1153         Vec_StrFree( vBinary );
1154         Vec_IntFree( vLits );
1155     }
1156     Gia_ManInvertConstraints( p );
1157 
1158     // write the nodes into the buffer
1159     Pos = 0;
1160     nBufferSize = 8 * Gia_ManAndNum(p) + 100; // skeptically assuming 3 chars per one AIG edge
1161     pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
1162     Gia_ManForEachAnd( p, pObj, i )
1163     {
1164         uLit  = Abc_Var2Lit( i, 0 );
1165         uLit0 = Gia_ObjFaninLit0( pObj, i );
1166         uLit1 = Gia_ObjFaninLit1( pObj, i );
1167         assert( p->fGiaSimple || Gia_ManBufNum(p) || uLit0 < uLit1 );
1168         Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit  - uLit1 );
1169         Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit1 - uLit0 );
1170         if ( Pos > nBufferSize - 10 )
1171         {
1172             printf( "Gia_AigerWrite(): AIGER generation has failed because the allocated buffer is too small.\n" );
1173             fclose( pFile );
1174             if ( p != pInit )
1175                 Gia_ManStop( p );
1176             return;
1177         }
1178     }
1179     assert( Pos < nBufferSize );
1180 
1181     // write the buffer
1182     fwrite( pBuffer, 1, Pos, pFile );
1183     ABC_FREE( pBuffer );
1184 
1185     // write the symbol table
1186     if ( p->vNamesIn && p->vNamesOut )
1187     {
1188         assert( Vec_PtrSize(p->vNamesIn)  == Gia_ManCiNum(p) );
1189         assert( Vec_PtrSize(p->vNamesOut) == Gia_ManCoNum(p) );
1190         // write PIs
1191         Gia_ManForEachPi( p, pObj, i )
1192             fprintf( pFile, "i%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, i) );
1193         // write latches
1194         Gia_ManForEachRo( p, pObj, i )
1195             fprintf( pFile, "l%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, Gia_ManPiNum(p) + i) );
1196         // write POs
1197         Gia_ManForEachPo( p, pObj, i )
1198             fprintf( pFile, "o%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesOut, i) );
1199     }
1200 
1201     // write the comment
1202     if ( fWriteNewLine )
1203         fprintf( pFile, "c\n" );
1204     else
1205         fprintf( pFile, "c" );
1206 
1207     // write additional AIG
1208     if ( p->pAigExtra )
1209     {
1210         fprintf( pFile, "a" );
1211         vStrExt = Gia_AigerWriteIntoMemoryStr( p->pAigExtra );
1212         Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1213         fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1214         Vec_StrFree( vStrExt );
1215         if ( fVerbose ) printf( "Finished writing extension \"a\".\n" );
1216     }
1217     // write constraints
1218     if ( p->nConstrs )
1219     {
1220         fprintf( pFile, "c" );
1221         Gia_FileWriteBufferSize( pFile, 4 );
1222         Gia_FileWriteBufferSize( pFile, p->nConstrs );
1223     }
1224     // write timing information
1225     if ( p->nAnd2Delay )
1226     {
1227         fprintf( pFile, "d" );
1228         Gia_FileWriteBufferSize( pFile, 4 );
1229         Gia_FileWriteBufferSize( pFile, p->nAnd2Delay );
1230     }
1231     if ( p->pManTime )
1232     {
1233         float * pTimes;
1234         pTimes = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime );
1235         if ( pTimes )
1236         {
1237             fprintf( pFile, "i" );
1238             Gia_FileWriteBufferSize( pFile, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
1239             fwrite( pTimes, 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
1240             ABC_FREE( pTimes );
1241             if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
1242         }
1243         pTimes = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime );
1244         if ( pTimes )
1245         {
1246             fprintf( pFile, "o" );
1247             Gia_FileWriteBufferSize( pFile, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
1248             fwrite( pTimes, 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
1249             ABC_FREE( pTimes );
1250             if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
1251         }
1252     }
1253     // write equivalences
1254     if ( p->pReprs && p->pNexts )
1255     {
1256         extern Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p );
1257         fprintf( pFile, "e" );
1258         vStrExt = Gia_WriteEquivClasses( p );
1259         Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1260         fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1261         Vec_StrFree( vStrExt );
1262     }
1263     // write flop classes
1264     if ( p->vFlopClasses )
1265     {
1266         fprintf( pFile, "f" );
1267         Gia_FileWriteBufferSize( pFile, 4*Gia_ManRegNum(p) );
1268         assert( Vec_IntSize(p->vFlopClasses) == Gia_ManRegNum(p) );
1269         fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile );
1270     }
1271     // write gate classes
1272     if ( p->vGateClasses )
1273     {
1274         fprintf( pFile, "g" );
1275         Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1276         assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
1277         fwrite( Vec_IntArray(p->vGateClasses), 1, 4*Gia_ManObjNum(p), pFile );
1278     }
1279     // write hierarchy info
1280     if ( p->pManTime )
1281     {
1282         fprintf( pFile, "h" );
1283         vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 1 );
1284         Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1285         fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1286         Vec_StrFree( vStrExt );
1287         if ( fVerbose ) printf( "Finished writing extension \"h\".\n" );
1288     }
1289     // write packing
1290     if ( p->vPacking )
1291     {
1292         extern Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking );
1293         fprintf( pFile, "k" );
1294         vStrExt = Gia_WritePacking( p->vPacking );
1295         Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1296         fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1297         Vec_StrFree( vStrExt );
1298         if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
1299     }
1300     // write edges
1301     if ( p->vEdge1 )
1302     {
1303         Vec_Int_t * vPairs = Gia_ManEdgeToArray( p );
1304         int i;
1305         fprintf( pFile, "w" );
1306         Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(vPairs)+1) );
1307         Gia_FileWriteBufferSize( pFile, Vec_IntSize(vPairs)/2 );
1308         for ( i = 0; i < Vec_IntSize(vPairs); i++ )
1309             Gia_FileWriteBufferSize( pFile, Vec_IntEntry(vPairs, i) );
1310         Vec_IntFree( vPairs );
1311     }
1312     // write mapping
1313     if ( Gia_ManHasMapping(p) )
1314     {
1315         extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
1316         extern Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p );
1317         extern Vec_Str_t * Gia_AigerWriteMappingDoc( Gia_Man_t * p );
1318         fprintf( pFile, "m" );
1319         vStrExt = Gia_AigerWriteMappingDoc( p );
1320         Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1321         fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1322         Vec_StrFree( vStrExt );
1323         if ( fVerbose ) printf( "Finished writing extension \"m\".\n" );
1324     }
1325     // write placement
1326     if ( p->pPlacement )
1327     {
1328         fprintf( pFile, "p" );
1329         Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1330         fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile );
1331     }
1332     // write register classes
1333     if ( p->vRegClasses )
1334     {
1335         int i;
1336         fprintf( pFile, "r" );
1337         Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(p->vRegClasses)+1) );
1338         Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegClasses) );
1339         for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
1340             Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
1341     }
1342     // write register inits
1343     if ( p->vRegInits )
1344     {
1345         int i;
1346         fprintf( pFile, "s" );
1347         Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(p->vRegInits)+1) );
1348         Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegInits) );
1349         for ( i = 0; i < Vec_IntSize(p->vRegInits); i++ )
1350             Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegInits, i) );
1351     }
1352     // write configuration data
1353     if ( p->vConfigs )
1354     {
1355         fprintf( pFile, "b" );
1356         assert( p->pCellStr != NULL );
1357         Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(p->vConfigs) + strlen(p->pCellStr) + 1 );
1358         fwrite( p->pCellStr, 1, strlen(p->pCellStr) + 1, pFile );
1359 //        fwrite( Vec_IntArray(p->vConfigs), 1, 4*Vec_IntSize(p->vConfigs), pFile );
1360         for ( i = 0; i < Vec_IntSize(p->vConfigs); i++ )
1361             Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vConfigs, i) );
1362     }
1363     // write choices
1364     if ( Gia_ManHasChoices(p) )
1365     {
1366         int i, nPairs = 0;
1367         fprintf( pFile, "q" );
1368         for ( i = 0; i < Gia_ManObjNum(p); i++ )
1369             nPairs += (Gia_ObjSibl(p, i) > 0);
1370         Gia_FileWriteBufferSize( pFile, 4*(nPairs * 2 + 1) );
1371         Gia_FileWriteBufferSize( pFile, nPairs );
1372         for ( i = 0; i < Gia_ManObjNum(p); i++ )
1373             if ( Gia_ObjSibl(p, i) )
1374             {
1375                 assert( i > Gia_ObjSibl(p, i) );
1376                 Gia_FileWriteBufferSize( pFile, i );
1377                 Gia_FileWriteBufferSize( pFile, Gia_ObjSibl(p, i) );
1378             }
1379         if ( fVerbose ) printf( "Finished writing extension \"q\".\n" );
1380     }
1381     // write switching activity
1382     if ( p->pSwitching )
1383     {
1384         fprintf( pFile, "u" );
1385         Gia_FileWriteBufferSize( pFile, Gia_ManObjNum(p) );
1386         fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile );
1387     }
1388 /*
1389     // write timing information
1390     if ( p->pManTime )
1391     {
1392         fprintf( pFile, "t" );
1393         vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 0 );
1394         Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1395         fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1396         Vec_StrFree( vStrExt );
1397     }
1398 */
1399     // write object classes
1400     if ( p->vObjClasses )
1401     {
1402         fprintf( pFile, "v" );
1403         Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1404         assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
1405         fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
1406     }
1407     // write name
1408     if ( p->pName )
1409     {
1410         fprintf( pFile, "n" );
1411         Gia_FileWriteBufferSize( pFile, strlen(p->pName)+1 );
1412         fwrite( p->pName, 1, strlen(p->pName), pFile );
1413         fprintf( pFile, "%c", '\0' );
1414     }
1415     // write comments
1416     if ( fWriteNewLine )
1417         fprintf( pFile, "c\n" );
1418     fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
1419     fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
1420     fclose( pFile );
1421     if ( p != pInit )
1422     {
1423         Gia_ManTransferTiming( pInit, p );
1424         Gia_ManStop( p );
1425     }
1426 }
1427 
1428 /**Function*************************************************************
1429 
1430   Synopsis    [Writes the AIG in the binary AIGER format.]
1431 
1432   Description []
1433 
1434   SideEffects []
1435 
1436   SeeAlso     []
1437 
1438 ***********************************************************************/
Gia_DumpAiger(Gia_Man_t * p,char * pFilePrefix,int iFileNum,int nFileNumDigits)1439 void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits )
1440 {
1441     char Buffer[100];
1442     sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
1443     Gia_AigerWrite( p, Buffer, 0, 0, 0 );
1444 }
1445 
1446 /**Function*************************************************************
1447 
1448   Synopsis    [Writes the AIG in the binary AIGER format.]
1449 
1450   Description []
1451 
1452   SideEffects []
1453 
1454   SeeAlso     []
1455 
1456 ***********************************************************************/
Gia_AigerWriteSimple(Gia_Man_t * pInit,char * pFileName)1457 void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName )
1458 {
1459     FILE * pFile;
1460     Vec_Str_t * vStr;
1461     if ( Gia_ManPoNum(pInit) == 0 )
1462     {
1463         printf( "Gia_AigerWriteSimple(): AIG cannot be written because it has no POs.\n" );
1464         return;
1465     }
1466     // start the output stream
1467     pFile = fopen( pFileName, "wb" );
1468     if ( pFile == NULL )
1469     {
1470         fprintf( stdout, "Gia_AigerWriteSimple(): Cannot open the output file \"%s\".\n", pFileName );
1471         return;
1472     }
1473     // write the buffer
1474     vStr = Gia_AigerWriteIntoMemoryStr( pInit );
1475     fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
1476     Vec_StrFree( vStr );
1477     fclose( pFile );
1478 }
1479 
1480 ////////////////////////////////////////////////////////////////////////
1481 ///                       END OF FILE                                ///
1482 ////////////////////////////////////////////////////////////////////////
1483 
1484 
1485 ABC_NAMESPACE_IMPL_END
1486 
1487