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