ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
ioaWriteAig.c File Reference
#include "ioa.h"
Include dependency graph for ioaWriteAig.c:

Go to the source code of this file.

Functions

int Ioa_WriteAigerEncode (unsigned char *pBuffer, int Pos, unsigned x)
 FUNCTION DEFINITIONS ///.
 
void Ioa_WriteAigerEncodeStr (Vec_Str_t *vStr, unsigned x)
 
Vec_Int_t * Ioa_WriteAigerLiterals (Aig_Man_t *pMan)
 
Vec_Str_t * Ioa_WriteEncodeLiterals (Vec_Int_t *vLits)
 
Vec_Str_t * Ioa_WriteAigerIntoMemoryStr (Aig_Man_t *pMan)
 
char * Ioa_WriteAigerIntoMemory (Aig_Man_t *pMan, int *pnSize)
 
void Ioa_WriteAigerBufferTest (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
 
void Ioa_WriteAiger (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
 

Function Documentation

◆ Ioa_WriteAiger()

void Ioa_WriteAiger ( Aig_Man_t * pMan,
char * pFileName,
int fWriteSymbols,
int fCompact )

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file ioaWriteAig.c.

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}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aig_ManInvertConstraints
void Aig_ManInvertConstraints(Aig_Man_t *pAig)
Definition aigUtil.c:1561
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition aig.h:447
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition aig.h:444
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Pos
ush Pos
Definition deflate.h:88
Ioa_WriteAigerLiterals
Vec_Int_t * Ioa_WriteAigerLiterals(Aig_Man_t *pMan)
Definition ioaWriteAig.c:207
Ioa_WriteEncodeLiterals
Vec_Str_t * Ioa_WriteEncodeLiterals(Vec_Int_t *vLits)
Definition ioaWriteAig.c:237
Ioa_WriteAigerEncode
int Ioa_WriteAigerEncode(unsigned char *pBuffer, int Pos, unsigned x)
FUNCTION DEFINITIONS ///.
Definition ioaWriteAig.c:151
Ioa_TimeStamp
char * Ioa_TimeStamp()
Definition ioaUtil.c:127
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ioa_WriteAigerBufferTest()

void Ioa_WriteAigerBufferTest ( Aig_Man_t * pMan,
char * pFileName,
int fWriteSymbols,
int fCompact )

Function*************************************************************

Synopsis [This procedure is used to test the above procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file ioaWriteAig.c.

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}
Ioa_WriteAigerIntoMemory
char * Ioa_WriteAigerIntoMemory(Aig_Man_t *pMan, int *pnSize)
Definition ioaWriteAig.c:376
Here is the call graph for this function:

◆ Ioa_WriteAigerEncode()

int Ioa_WriteAigerEncode ( unsigned char * pBuffer,
int Pos,
unsigned x )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Adds one unsigned AIG edge to the output buffer.]

Description [This procedure is a slightly modified version of Armin Biere's procedure "void encode (FILE * file, unsigned x)" ]

SideEffects [Returns the current writing position.]

SeeAlso []

Definition at line 151 of file ioaWriteAig.c.

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}
Here is the caller graph for this function:

◆ Ioa_WriteAigerEncodeStr()

void Ioa_WriteAigerEncodeStr ( Vec_Str_t * vStr,
unsigned x )

Function*************************************************************

Synopsis [Adds one unsigned AIG edge to the output buffer.]

Description [This procedure is a slightly modified version of Armin Biere's procedure "void encode (FILE * file, unsigned x)" ]

SideEffects [Returns the current writing position.]

SeeAlso []

Definition at line 179 of file ioaWriteAig.c.

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}
Here is the caller graph for this function:

◆ Ioa_WriteAigerIntoMemory()

char * Ioa_WriteAigerIntoMemory ( Aig_Man_t * pMan,
int * pnSize )

Function*************************************************************

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The returned size (pnSize) gives the number of bytes in the buffer. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 376 of file ioaWriteAig.c.

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}
Ioa_WriteAigerIntoMemoryStr
Vec_Str_t * Ioa_WriteAigerIntoMemoryStr(Aig_Man_t *pMan)
Definition ioaWriteAig.c:286
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ioa_WriteAigerIntoMemoryStr()

Vec_Str_t * Ioa_WriteAigerIntoMemoryStr ( Aig_Man_t * pMan)

Function*************************************************************

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The returned size (pnSize) gives the number of bytes in the buffer. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 286 of file ioaWriteAig.c.

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}
Ioa_WriteAigerEncodeStr
void Ioa_WriteAigerEncodeStr(Vec_Str_t *vStr, unsigned x)
Definition ioaWriteAig.c:179
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ioa_WriteAigerLiterals()

Vec_Int_t * Ioa_WriteAigerLiterals ( Aig_Man_t * pMan)

Function*************************************************************

Synopsis [Create the array of literals to be written.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file ioaWriteAig.c.

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}
Here is the caller graph for this function:

◆ Ioa_WriteEncodeLiterals()

Vec_Str_t * Ioa_WriteEncodeLiterals ( Vec_Int_t * vLits)

Function*************************************************************

Synopsis [Creates the binary encoded array of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file ioaWriteAig.c.

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}
Vec_Str_t_::nCap
int nCap
Definition bblif.c:49
Vec_Str_t_::nSize
int nSize
Definition bblif.c:50
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:
Here is the caller graph for this function: