1 /**CFile****************************************************************
2
3 FileName [ioaWriteAiger.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Command processing package.]
8
9 Synopsis [Procedures to 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 - December 16, 2006.]
17
18 Revision [$Id: ioaWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
19
20 ***********************************************************************/
21
22 #include "ioa.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 /*
32 The following is taken from the AIGER format description,
33 which can be found at http://fmv.jku.at/aiger
34 */
35
36
37 /*
38 The AIGER And-Inverter Graph (AIG) Format Version 20061129
39 ----------------------------------------------------------
40 Armin Biere, Johannes Kepler University, 2006
41
42 This report describes the AIG file format as used by the AIGER library.
43 The purpose of this report is not only to motivate and document the
44 format, but also to allow independent implementations of writers and
45 readers by giving precise and unambiguous definitions.
46
47 ...
48
49 Introduction
50
51 The name AIGER contains as one part the acronym AIG of And-Inverter
52 Graphs and also if pronounced in German sounds like the name of the
53 'Eiger', a mountain in the Swiss alps. This choice should emphasize the
54 origin of this format. It was first openly discussed at the Alpine
55 Verification Meeting 2006 in Ascona as a way to provide a simple, compact
56 file format for a model checking competition affiliated to CAV 2007.
57
58 ...
59
60 Binary Format Definition
61
62 The binary format is semantically a subset of the ASCII format with a
63 slightly different syntax. The binary format may need to reencode
64 literals, but translating a file in binary format into ASCII format and
65 then back in to binary format will result in the same file.
66
67 The main differences of the binary format to the ASCII format are as
68 follows. After the header the list of input literals and all the
69 current state literals of a latch can be omitted. Furthermore the
70 definitions of the AND gates are binary encoded. However, the symbol
71 table and the comment section are as in the ASCII format.
72
73 The header of an AIGER file in binary format has 'aig' as format
74 identifier, but otherwise is identical to the ASCII header. The standard
75 file extension for the binary format is therefore '.aig'.
76
77 A header for the binary format is still in ASCII encoding:
78
79 aig M I L O A
80
81 Constants, variables and literals are handled in the same way as in the
82 ASCII format. The first simplifying restriction is on the variable
83 indices of inputs and latches. The variable indices of inputs come first,
84 followed by the pseudo-primary inputs of the latches and then the variable
85 indices of all LHS of AND gates:
86
87 input variable indices 1, 2, ... , I
88 latch variable indices I+1, I+2, ... , (I+L)
89 AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
90
91 The corresponding unsigned literals are
92
93 input literals 2, 4, ... , 2*I
94 latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
95 AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
96
97 All literals have to be defined, and therefore 'M = I + L + A'. With this
98 restriction it becomes possible that the inputs and the current state
99 literals of the latches do not have to be listed explicitly. Therefore,
100 after the header only the list of 'L' next state literals follows, one per
101 latch on a single line, and then the 'O' outputs, again one per line.
102
103 In the binary format we assume that the AND gates are ordered and respect
104 the child parent relation. AND gates with smaller literals on the LHS
105 come first. Therefore we can assume that the literals on the right-hand
106 side of a definition of an AND gate are smaller than the LHS literal.
107 Furthermore we can sort the literals on the RHS, such that the larger
108 literal comes first. A definition thus consists of three literals
109
110 lhs rhs0 rhs1
111
112 with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are
113 pairwise different to avoid combinational self loops. Since the LHS
114 indices of the definitions are all consecutive (as even integers),
115 the binary format does not have to keep 'lhs'. In addition, we can use
116 the order restriction and only write the differences 'delta0' and 'delta1'
117 instead of 'rhs0' and 'rhs1', with
118
119 delta0 = lhs - rhs0, delta1 = rhs0 - rhs1
120
121 The differences will all be strictly positive, and in practice often very
122 small. We can take advantage of this fact by the simple little-endian
123 encoding of unsigned integers of the next section. After the binary delta
124 encoding of the RHSs of all AND gates, the optional symbol table and
125 optional comment section start in the same format as in the ASCII case.
126
127 ...
128
129 */
130
Ioa_ObjMakeLit(int Var,int fCompl)131 static int Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
Ioa_ObjAigerNum(Aig_Obj_t * pObj)132 static int Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return pObj->iData; }
Ioa_ObjSetAigerNum(Aig_Obj_t * pObj,unsigned Num)133 static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->iData = Num; }
134
135 ////////////////////////////////////////////////////////////////////////
136 /// FUNCTION DEFINITIONS ///
137 ////////////////////////////////////////////////////////////////////////
138
139 /**Function*************************************************************
140
141 Synopsis [Adds one unsigned AIG edge to the output buffer.]
142
143 Description [This procedure is a slightly modified version of Armin Biere's
144 procedure "void encode (FILE * file, unsigned x)" ]
145
146 SideEffects [Returns the current writing position.]
147
148 SeeAlso []
149
150 ***********************************************************************/
Ioa_WriteAigerEncode(unsigned char * pBuffer,int Pos,unsigned x)151 int Ioa_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
152 {
153 unsigned char ch;
154 while (x & ~0x7f)
155 {
156 ch = (x & 0x7f) | 0x80;
157 // putc (ch, file);
158 pBuffer[Pos++] = ch;
159 x >>= 7;
160 }
161 ch = x;
162 // putc (ch, file);
163 pBuffer[Pos++] = ch;
164 return Pos;
165 }
166
167 /**Function*************************************************************
168
169 Synopsis [Adds one unsigned AIG edge to the output buffer.]
170
171 Description [This procedure is a slightly modified version of Armin Biere's
172 procedure "void encode (FILE * file, unsigned x)" ]
173
174 SideEffects [Returns the current writing position.]
175
176 SeeAlso []
177
178 ***********************************************************************/
Ioa_WriteAigerEncodeStr(Vec_Str_t * vStr,unsigned x)179 void Ioa_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x )
180 {
181 unsigned char ch;
182 while (x & ~0x7f)
183 {
184 ch = (x & 0x7f) | 0x80;
185 // putc (ch, file);
186 // pBuffer[Pos++] = ch;
187 Vec_StrPush( vStr, ch );
188 x >>= 7;
189 }
190 ch = x;
191 // putc (ch, file);
192 // pBuffer[Pos++] = ch;
193 Vec_StrPush( vStr, ch );
194 }
195
196 /**Function*************************************************************
197
198 Synopsis [Create the array of literals to be written.]
199
200 Description []
201
202 SideEffects []
203
204 SeeAlso []
205
206 ***********************************************************************/
Ioa_WriteAigerLiterals(Aig_Man_t * pMan)207 Vec_Int_t * Ioa_WriteAigerLiterals( Aig_Man_t * pMan )
208 {
209 Vec_Int_t * vLits;
210 Aig_Obj_t * pObj, * pDriver;
211 int i;
212 vLits = Vec_IntAlloc( Aig_ManCoNum(pMan) );
213 Aig_ManForEachLiSeq( pMan, pObj, i )
214 {
215 pDriver = Aig_ObjFanin0(pObj);
216 Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
217 }
218 Aig_ManForEachPoSeq( pMan, pObj, i )
219 {
220 pDriver = Aig_ObjFanin0(pObj);
221 Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
222 }
223 return vLits;
224 }
225
226 /**Function*************************************************************
227
228 Synopsis [Creates the binary encoded array of literals.]
229
230 Description []
231
232 SideEffects []
233
234 SeeAlso []
235
236 ***********************************************************************/
Ioa_WriteEncodeLiterals(Vec_Int_t * vLits)237 Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits )
238 {
239 Vec_Str_t * vBinary;
240 int Pos = 0, Lit, LitPrev, Diff, i;
241 vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
242 LitPrev = Vec_IntEntry( vLits, 0 );
243 Pos = Ioa_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev );
244 Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
245 {
246 Diff = Lit - LitPrev;
247 Diff = (Lit < LitPrev)? -Diff : Diff;
248 Diff = (Diff << 1) | (int)(Lit < LitPrev);
249 Pos = Ioa_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
250 LitPrev = Lit;
251 if ( Pos + 10 > vBinary->nCap )
252 Vec_StrGrow( vBinary, vBinary->nCap+1 );
253 }
254 vBinary->nSize = Pos;
255 /*
256 // verify
257 {
258 extern Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries );
259 char * pPos = Vec_StrArray( vBinary );
260 Vec_Int_t * vTemp = Ioa_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
261 for ( i = 0; i < Vec_IntSize(vLits); i++ )
262 {
263 int Entry1 = Vec_IntEntry(vLits,i);
264 int Entry2 = Vec_IntEntry(vTemp,i);
265 assert( Entry1 == Entry2 );
266 }
267 Vec_IntFree( vTemp );
268 }
269 */
270 return vBinary;
271 }
272
273 /**Function*************************************************************
274
275 Synopsis [Writes the AIG in into the memory buffer.]
276
277 Description [The resulting buffer constains the AIG in AIGER format.
278 The returned size (pnSize) gives the number of bytes in the buffer.
279 The resulting buffer should be deallocated by the user.]
280
281 SideEffects []
282
283 SeeAlso []
284
285 ***********************************************************************/
Ioa_WriteAigerIntoMemoryStr(Aig_Man_t * pMan)286 Vec_Str_t * Ioa_WriteAigerIntoMemoryStr( Aig_Man_t * pMan )
287 {
288 Vec_Str_t * vBuffer;
289 Aig_Obj_t * pObj, * pDriver;
290 int nNodes, i, uLit, uLit0, uLit1;
291 // set the node numbers to be used in the output file
292 nNodes = 0;
293 Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
294 Aig_ManForEachCi( pMan, pObj, i )
295 Ioa_ObjSetAigerNum( pObj, nNodes++ );
296 Aig_ManForEachNode( pMan, pObj, i )
297 Ioa_ObjSetAigerNum( pObj, nNodes++ );
298
299 // write the header "M I L O A" where M = I + L + A
300 /*
301 fprintf( pFile, "aig%s %u %u %u %u %u\n",
302 fCompact? "2" : "",
303 Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan),
304 Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
305 Aig_ManRegNum(pMan),
306 Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
307 Aig_ManNodeNum(pMan) );
308 */
309 vBuffer = Vec_StrAlloc( 3*Aig_ManObjNum(pMan) );
310 Vec_StrPrintStr( vBuffer, "aig " );
311 Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan) );
312 Vec_StrPrintStr( vBuffer, " " );
313 Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
314 Vec_StrPrintStr( vBuffer, " " );
315 Vec_StrPrintNum( vBuffer, Aig_ManRegNum(pMan) );
316 Vec_StrPrintStr( vBuffer, " " );
317 Vec_StrPrintNum( vBuffer, Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
318 Vec_StrPrintStr( vBuffer, " " );
319 Vec_StrPrintNum( vBuffer, Aig_ManNodeNum(pMan) );
320 Vec_StrPrintStr( vBuffer, "\n" );
321
322 // write latch drivers
323 Aig_ManForEachLiSeq( pMan, pObj, i )
324 {
325 pDriver = Aig_ObjFanin0(pObj);
326 uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) );
327 // fprintf( pFile, "%u\n", uLit );
328 Vec_StrPrintNum( vBuffer, uLit );
329 Vec_StrPrintStr( vBuffer, "\n" );
330 }
331
332 // write PO drivers
333 Aig_ManForEachPoSeq( pMan, pObj, i )
334 {
335 pDriver = Aig_ObjFanin0(pObj);
336 uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) );
337 // fprintf( pFile, "%u\n", uLit );
338 Vec_StrPrintNum( vBuffer, uLit );
339 Vec_StrPrintStr( vBuffer, "\n" );
340 }
341 // write the nodes into the buffer
342 Aig_ManForEachNode( pMan, pObj, i )
343 {
344 uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
345 uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
346 uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
347 assert( uLit0 != uLit1 );
348 if ( uLit0 > uLit1 )
349 {
350 int Temp = uLit0;
351 uLit0 = uLit1;
352 uLit1 = Temp;
353 }
354 // Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
355 // Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
356 Ioa_WriteAigerEncodeStr( vBuffer, uLit - uLit1 );
357 Ioa_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
358 }
359 Vec_StrPrintStr( vBuffer, "c" );
360 return vBuffer;
361 }
362
363 /**Function*************************************************************
364
365 Synopsis [Writes the AIG in into the memory buffer.]
366
367 Description [The resulting buffer constains the AIG in AIGER format.
368 The returned size (pnSize) gives the number of bytes in the buffer.
369 The resulting buffer should be deallocated by the user.]
370
371 SideEffects []
372
373 SeeAlso []
374
375 ***********************************************************************/
Ioa_WriteAigerIntoMemory(Aig_Man_t * pMan,int * pnSize)376 char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
377 {
378 char * pBuffer;
379 Vec_Str_t * vBuffer;
380 vBuffer = Ioa_WriteAigerIntoMemoryStr( pMan );
381 if ( pMan->pName )
382 {
383 Vec_StrPrintStr( vBuffer, "n" );
384 Vec_StrPrintStr( vBuffer, pMan->pName );
385 Vec_StrPush( vBuffer, 0 );
386 }
387 // prepare the return values
388 *pnSize = Vec_StrSize( vBuffer );
389 pBuffer = Vec_StrReleaseArray( vBuffer );
390 Vec_StrFree( vBuffer );
391 return pBuffer;
392 }
393
394 /**Function*************************************************************
395
396 Synopsis [This procedure is used to test the above procedure.]
397
398 Description []
399
400 SideEffects []
401
402 SeeAlso []
403
404 ***********************************************************************/
Ioa_WriteAigerBufferTest(Aig_Man_t * pMan,char * pFileName,int fWriteSymbols,int fCompact)405 void Ioa_WriteAigerBufferTest( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
406 {
407 FILE * pFile;
408 char * pBuffer;
409 int nSize;
410 if ( Aig_ManCoNum(pMan) == 0 )
411 {
412 printf( "AIG cannot be written because it has no POs.\n" );
413 return;
414 }
415 // start the output stream
416 pFile = fopen( pFileName, "wb" );
417 if ( pFile == NULL )
418 {
419 fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
420 return;
421 }
422 // write the buffer
423 pBuffer = Ioa_WriteAigerIntoMemory( pMan, &nSize );
424 fwrite( pBuffer, 1, nSize, pFile );
425 ABC_FREE( pBuffer );
426 // write the comment
427 // fprintf( pFile, "c" );
428 // if ( pMan->pName )
429 // fprintf( pFile, "n%s%c", pMan->pName, '\0' );
430 fprintf( pFile, "\nThis file was produced by the IOA package in ABC on %s\n", Ioa_TimeStamp() );
431 fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
432 fclose( pFile );
433 }
434
435 /**Function*************************************************************
436
437 Synopsis [Writes the AIG in the binary AIGER format.]
438
439 Description []
440
441 SideEffects []
442
443 SeeAlso []
444
445 ***********************************************************************/
Ioa_WriteAiger(Aig_Man_t * pMan,char * pFileName,int fWriteSymbols,int fCompact)446 void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
447 {
448 // Bar_Progress_t * pProgress;
449 FILE * pFile;
450 Aig_Obj_t * pObj, * pDriver;
451 int i, nNodes, nBufferSize, Pos;
452 unsigned char * pBuffer;
453 unsigned uLit0, uLit1, uLit;
454
455 if ( Aig_ManCoNum(pMan) == 0 )
456 {
457 printf( "AIG cannot be written because it has no POs.\n" );
458 return;
459 }
460
461 // assert( Aig_ManIsStrash(pMan) );
462 // start the output stream
463 pFile = fopen( pFileName, "wb" );
464 if ( pFile == NULL )
465 {
466 fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
467 return;
468 }
469 /*
470 Aig_ManForEachLatch( pMan, pObj, i )
471 if ( !Aig_LatchIsInit0(pObj) )
472 {
473 fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
474 return;
475 }
476 */
477 // set the node numbers to be used in the output file
478 nNodes = 0;
479 Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
480 Aig_ManForEachCi( pMan, pObj, i )
481 Ioa_ObjSetAigerNum( pObj, nNodes++ );
482 Aig_ManForEachNode( pMan, pObj, i )
483 Ioa_ObjSetAigerNum( pObj, nNodes++ );
484
485 // write the header "M I L O A" where M = I + L + A
486 fprintf( pFile, "aig%s %u %u %u %u %u",
487 fCompact? "2" : "",
488 Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan),
489 Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
490 Aig_ManRegNum(pMan),
491 Aig_ManConstrNum(pMan) ? 0 : Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
492 Aig_ManNodeNum(pMan) );
493 // write the extended header "B C J F"
494 if ( Aig_ManConstrNum(pMan) )
495 fprintf( pFile, " %u %u", Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
496 fprintf( pFile, "\n" );
497
498 // if the driver node is a constant, we need to complement the literal below
499 // because, in the AIGER format, literal 0/1 is represented as number 0/1
500 // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
501
502 Aig_ManInvertConstraints( pMan );
503 if ( !fCompact )
504 {
505 // write latch drivers
506 Aig_ManForEachLiSeq( pMan, pObj, i )
507 {
508 pDriver = Aig_ObjFanin0(pObj);
509 fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
510 }
511
512 // write PO drivers
513 Aig_ManForEachPoSeq( pMan, pObj, i )
514 {
515 pDriver = Aig_ObjFanin0(pObj);
516 fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
517 }
518 }
519 else
520 {
521 Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan );
522 Vec_Str_t * vBinary = Ioa_WriteEncodeLiterals( vLits );
523 fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
524 Vec_StrFree( vBinary );
525 Vec_IntFree( vLits );
526 }
527 Aig_ManInvertConstraints( pMan );
528
529 // write the nodes into the buffer
530 Pos = 0;
531 nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
532 pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
533 // pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
534 Aig_ManForEachNode( pMan, pObj, i )
535 {
536 // Bar_ProgressUpdate( pProgress, i, NULL );
537 uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
538 uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
539 uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
540 assert( uLit0 != uLit1 );
541 if ( uLit0 > uLit1 )
542 {
543 int Temp = uLit0;
544 uLit0 = uLit1;
545 uLit1 = Temp;
546 }
547 Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
548 Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
549 if ( Pos > nBufferSize - 10 )
550 {
551 printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
552 fclose( pFile );
553 return;
554 }
555 }
556 assert( Pos < nBufferSize );
557 // Bar_ProgressStop( pProgress );
558
559 // write the buffer
560 fwrite( pBuffer, 1, Pos, pFile );
561 ABC_FREE( pBuffer );
562 /*
563 // write the symbol table
564 if ( fWriteSymbols )
565 {
566 int bads;
567 // write PIs
568 Aig_ManForEachPiSeq( pMan, pObj, i )
569 fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
570 // write latches
571 Aig_ManForEachLoSeq( pMan, pObj, i )
572 fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
573 // write POs
574 bads = Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan);
575 Aig_ManForEachPoSeq( pMan, pObj, i )
576 if ( !Aig_ManConstrNum(pMan) )
577 fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
578 else if ( i < bads )
579 fprintf( pFile, "b%d %s\n", i, Aig_ObjName(pObj) );
580 else
581 fprintf( pFile, "c%d %s\n", i - bads, Aig_ObjName(pObj) );
582 }
583 */
584 // write the comment
585 fprintf( pFile, "c" );
586 if ( pMan->pName )
587 fprintf( pFile, "n%s%c", pMan->pName, '\0' );
588 fprintf( pFile, "\nThis file was produced by the IOA package in ABC on %s\n", Ioa_TimeStamp() );
589 fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
590 fclose( pFile );
591 }
592
593 ////////////////////////////////////////////////////////////////////////
594 /// END OF FILE ///
595 ////////////////////////////////////////////////////////////////////////
596
597
598 ABC_NAMESPACE_IMPL_END
599
600