ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
ioWriteAiger.c File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/bzlib/bzlib.h"
#include "misc/zlib/zlib.h"
#include "ioAbc.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"
Include dependency graph for ioWriteAiger.c:

Go to the source code of this file.

Classes

struct  bz2file
 

Typedefs

typedef struct bz2file bz2file
 

Functions

int Io_WriteAigerEncode (unsigned char *pBuffer, int Pos, unsigned x)
 FUNCTION DEFINITIONS ///.
 
Vec_Int_t * Io_WriteAigerLiterals (Abc_Ntk_t *pNtk)
 
Vec_Str_t * Io_WriteEncodeLiterals (Vec_Int_t *vLits)
 
void Io_WriteAiger_old (Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact)
 
void Io_WriteAigerGz (Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols)
 
int fprintfBz2Aig (bz2file *b, char *fmt,...)
 
void Io_WriteAiger (Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact, int fUnique)
 
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Io_WriteAigerCex (Abc_Cex_t *pCex, Abc_Ntk_t *pNtk, void *pG, char *pFileName)
 

Typedef Documentation

◆ bz2file

typedef struct bz2file bz2file

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

Synopsis [Procedure to write data into BZ2 file.]

Description [Based on the vsnprintf() man page.]

SideEffects []

SeeAlso []

Function Documentation

◆ fprintfBz2Aig()

int fprintfBz2Aig ( bz2file * b,
char * fmt,
... )

Definition at line 588 of file ioWriteAiger.c.

588 {
589 if (b->b) {
590 char * newBuf;
591 int bzError;
592 va_list ap;
593 while (1) {
594 va_start(ap,fmt);
595 b->nBytes = vsnprintf(b->buf,b->nBytesMax,fmt,ap);
596 va_end(ap);
597 if (b->nBytes > -1 && b->nBytes < b->nBytesMax)
598 break;
599 if (b->nBytes > -1)
600 b->nBytesMax = b->nBytes + 1;
601 else
602 b->nBytesMax *= 2;
603 if ((newBuf = ABC_REALLOC( char,b->buf,b->nBytesMax )) == NULL)
604 return -1;
605 else
606 b->buf = newBuf;
607 }
608 BZ2_bzWrite( &bzError, b->b, b->buf, b->nBytes );
609 if (bzError == BZ_IO_ERROR) {
610 fprintf( stdout, "Ioa_WriteBlif(): I/O error writing to compressed stream.\n" );
611 return -1;
612 }
613 return b->nBytes;
614 } else {
615 int n;
616 va_list ap;
617 va_start(ap,fmt);
618 n = vfprintf( b->f, fmt, ap);
619 va_end(ap);
620 return n;
621 }
622}
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
BZ2_bzWrite
void BZ_API BZ2_bzWrite(int *bzerror, BZFILE *b, void *buf, int len)
Definition bzlib.c:976
BZ_IO_ERROR
#define BZ_IO_ERROR
Definition bzlib.h:44
bz2file::nBytesMax
int nBytesMax
Definition ioWriteAiger.c:585
bz2file::f
FILE * f
Definition ioWriteAiger.c:581
bz2file::b
BZFILE * b
Definition ioWriteAiger.c:582
bz2file::buf
char * buf
Definition ioWriteAiger.c:583
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Io_WriteAiger()

void Io_WriteAiger ( Abc_Ntk_t * pNtk,
char * pFileName,
int fWriteSymbols,
int fCompact,
int fUnique )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file ioWriteAiger.c.

636{
637 ProgressBar * pProgress;
638// FILE * pFile;
639 Abc_Obj_t * pObj, * pDriver, * pLatch;
640 int i, nNodes, nBufferSize, bzError, Pos, fExtended;
641 unsigned char * pBuffer;
642 unsigned uLit0, uLit1, uLit;
643 bz2file b;
644
645 // define unique writing
646 if ( fUnique )
647 {
648 fWriteSymbols = 0;
649 fCompact = 0;
650 }
651
652 fExtended = Abc_NtkConstrNum(pNtk);
653
654 // check that the network is valid
655 assert( Abc_NtkIsStrash(pNtk) );
656 Abc_NtkForEachLatch( pNtk, pObj, i )
657 if ( !Abc_LatchIsInit0(pObj) )
658 {
659 if ( !fCompact )
660 {
661 fExtended = 1;
662 break;
663 }
664 fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
665 return;
666 }
667
668 // write the GZ file
669 if (!strncmp(pFileName+strlen(pFileName)-3,".gz",3))
670 {
671 Io_WriteAigerGz( pNtk, pFileName, fWriteSymbols );
672 return;
673 }
674
675 memset(&b,0,sizeof(b));
676 b.nBytesMax = (1<<12);
677 b.buf = ABC_ALLOC( char,b.nBytesMax );
678
679 // start the output stream
680 b.f = fopen( pFileName, "wb" );
681 if ( b.f == NULL )
682 {
683 fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
684 ABC_FREE(b.buf);
685 return;
686 }
687 if (!strncmp(pFileName+strlen(pFileName)-4,".bz2",4)) {
688 b.b = BZ2_bzWriteOpen( &bzError, b.f, 9, 0, 0 );
689 if ( bzError != BZ_OK ) {
690 BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
691 fprintf( stdout, "Io_WriteAiger(): Cannot start compressed stream.\n" );
692 fclose( b.f );
693 ABC_FREE(b.buf);
694 return;
695 }
696 }
697
698 // set the node numbers to be used in the output file
699 nNodes = 0;
700 Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
701 Abc_NtkForEachCi( pNtk, pObj, i )
702 Io_ObjSetAigerNum( pObj, nNodes++ );
703 Abc_AigForEachAnd( pNtk, pObj, i )
704 Io_ObjSetAigerNum( pObj, nNodes++ );
705
706 // write the header "M I L O A" where M = I + L + A
707 fprintfBz2Aig( &b, "aig%s %u %u %u %u %u",
708 fCompact? "2" : "",
709 Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
710 Abc_NtkPiNum(pNtk),
711 Abc_NtkLatchNum(pNtk),
712 fExtended ? 0 : Abc_NtkPoNum(pNtk),
713 Abc_NtkNodeNum(pNtk) );
714 // write the extended header "B C J F"
715 if ( fExtended )
716 fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
717 fprintfBz2Aig( &b, "\n" );
718
719 // if the driver node is a constant, we need to complement the literal below
720 // because, in the AIGER format, literal 0/1 is represented as number 0/1
721 // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
722
723 Abc_NtkInvertConstraints( pNtk );
724 if ( !fCompact )
725 {
726 // write latch drivers
727 Abc_NtkForEachLatch( pNtk, pLatch, i )
728 {
729 pObj = Abc_ObjFanin0(pLatch);
730 pDriver = Abc_ObjFanin0(pObj);
731 uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
732 if ( Abc_LatchIsInit0(pLatch) )
733 fprintfBz2Aig( &b, "%u\n", uLit );
734 else if ( Abc_LatchIsInit1(pLatch) )
735 fprintfBz2Aig( &b, "%u 1\n", uLit );
736 else
737 {
738 // Both None and DC are written as 'uninitialized' e.g. a free boolean value
739 assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
740 fprintfBz2Aig( &b, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
741 }
742 }
743 // write PO drivers
744 Abc_NtkForEachPo( pNtk, pObj, i )
745 {
746 pDriver = Abc_ObjFanin0(pObj);
747 fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
748 }
749 }
750 else
751 {
752 Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
753 Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
754 if ( !b.b )
755 fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), b.f );
756 else
757 {
758 BZ2_bzWrite( &bzError, b.b, Vec_StrArray(vBinary), Vec_StrSize(vBinary) );
759 if (bzError == BZ_IO_ERROR) {
760 fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
761 fclose( b.f );
762 ABC_FREE(b.buf);
763 Vec_StrFree( vBinary );
764 return;
765 }
766 }
767 Vec_StrFree( vBinary );
768 Vec_IntFree( vLits );
769 }
770 Abc_NtkInvertConstraints( pNtk );
771
772 // write the nodes into the buffer
773 Pos = 0;
774 nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
775 pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
776 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
777 Abc_AigForEachAnd( pNtk, pObj, i )
778 {
779 Extra_ProgressBarUpdate( pProgress, i, NULL );
780 uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
781 uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
782 uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
783 if ( uLit0 > uLit1 )
784 {
785 unsigned Temp = uLit0;
786 uLit0 = uLit1;
787 uLit1 = Temp;
788 }
789 assert( uLit1 < uLit );
790 Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
791 Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
792 if ( Pos > nBufferSize - 10 )
793 {
794 printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
795 fclose( b.f );
796 ABC_FREE(b.buf);
797 Extra_ProgressBarStop( pProgress );
798 return;
799 }
800 }
801 assert( Pos < nBufferSize );
802 Extra_ProgressBarStop( pProgress );
803
804 // write the buffer
805 if ( !b.b )
806 fwrite( pBuffer, 1, Pos, b.f );
807 else
808 {
809 BZ2_bzWrite( &bzError, b.b, pBuffer, Pos );
810 if (bzError == BZ_IO_ERROR) {
811 fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
812 fclose( b.f );
813 ABC_FREE(b.buf);
814 return;
815 }
816 }
817 ABC_FREE( pBuffer );
818
819 // write the symbol table
820 if ( fWriteSymbols )
821 {
822 // write PIs
823 Abc_NtkForEachPi( pNtk, pObj, i )
824 fprintfBz2Aig( &b, "i%d %s\n", i, Abc_ObjName(pObj) );
825 // write latches
826 Abc_NtkForEachLatch( pNtk, pObj, i )
827 fprintfBz2Aig( &b, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
828 // write POs
829 Abc_NtkForEachPo( pNtk, pObj, i )
830 if ( !fExtended )
831 fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) );
832 else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
833 fprintfBz2Aig( &b, "b%d %s\n", i, Abc_ObjName(pObj) );
834 else
835 fprintfBz2Aig( &b, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
836 }
837
838 // write the comment
839 fprintfBz2Aig( &b, "c" );
840 if ( !fUnique )
841 {
842 if ( pNtk->pName && strlen(pNtk->pName) > 0 )
843 fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
844 fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
845 fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
846 }
847
848 // close the file
849 if (b.b) {
850 BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
851 if (bzError == BZ_IO_ERROR) {
852 fprintf( stdout, "Io_WriteAiger(): I/O error closing compressed stream.\n" );
853 fclose( b.f );
854 ABC_FREE(b.buf);
855 return;
856 }
857 }
858 fclose( b.f );
859 ABC_FREE(b.buf);
860}
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_AigForEachAnd
#define Abc_AigForEachAnd(pNtk, pNode, i)
Definition abc.h:488
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition abc.h:520
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition abc.h:500
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
Abc_NtkInvertConstraints
ABC_DLL void Abc_NtkInvertConstraints(Abc_Ntk_t *pNtk)
Definition abcUtil.c:2244
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition abc.h:516
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition abcAig.c:683
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
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
ProgressBar
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
BZ2_bzWriteOpen
BZFILE *BZ_API BZ2_bzWriteOpen(int *bzerror, FILE *f, int blockSize100k, int verbosity, int workFactor)
Definition bzlib.c:928
BZ2_bzWriteClose
void BZ_API BZ2_bzWriteClose(int *bzerror, BZFILE *b, int abandon, unsigned int *nbytes_in, unsigned int *nbytes_out)
Definition bzlib.c:1021
BZ_OK
#define BZ_OK
Definition bzlib.h:34
Pos
ush Pos
Definition deflate.h:88
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_TimeStamp
char * Extra_TimeStamp()
Definition extraUtilFile.c:465
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Io_WriteEncodeLiterals
Vec_Str_t * Io_WriteEncodeLiterals(Vec_Int_t *vLits)
Definition ioWriteAiger.c:223
Io_WriteAigerEncode
int Io_WriteAigerEncode(unsigned char *pBuffer, int Pos, unsigned x)
FUNCTION DEFINITIONS ///.
Definition ioWriteAiger.c:166
fprintfBz2Aig
int fprintfBz2Aig(bz2file *b, char *fmt,...)
Definition ioWriteAiger.c:588
Io_WriteAigerLiterals
Vec_Int_t * Io_WriteAigerLiterals(Abc_Ntk_t *pNtk)
Definition ioWriteAiger.c:193
Io_WriteAigerGz
void Io_WriteAigerGz(Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols)
Definition ioWriteAiger.c:436
Abc_Ntk_t_::pName
char * pName
Definition abc.h:158
assert
#define assert(ex)
Definition util_old.h:213
strncmp
int strncmp()
memset
char * memset()
strlen
int strlen()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Io_WriteAiger_old()

void Io_WriteAiger_old ( Abc_Ntk_t * pNtk,
char * pFileName,
int fWriteSymbols,
int fCompact )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file ioWriteAiger.c.

270{
271 ProgressBar * pProgress;
272 FILE * pFile;
273 Abc_Obj_t * pObj, * pDriver, * pLatch;
274 int i, nNodes, nBufferSize, Pos, fExtended;
275 unsigned char * pBuffer;
276 unsigned uLit0, uLit1, uLit;
277
278 fExtended = Abc_NtkConstrNum(pNtk);
279
280 assert( Abc_NtkIsStrash(pNtk) );
281 Abc_NtkForEachLatch( pNtk, pObj, i )
282 if ( !Abc_LatchIsInit0(pObj) )
283 {
284 if ( !fCompact )
285 {
286 fExtended = 1;
287 break;
288 }
289 fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
290 return;
291 }
292
293 // start the output stream
294 pFile = fopen( pFileName, "wb" );
295 if ( pFile == NULL )
296 {
297 fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
298 return;
299 }
300
301 // set the node numbers to be used in the output file
302 nNodes = 0;
303 Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
304 Abc_NtkForEachCi( pNtk, pObj, i )
305 Io_ObjSetAigerNum( pObj, nNodes++ );
306 Abc_AigForEachAnd( pNtk, pObj, i )
307 Io_ObjSetAigerNum( pObj, nNodes++ );
308
309 // write the header "M I L O A" where M = I + L + A
310 fprintf( pFile, "aig%s %u %u %u %u %u",
311 fCompact? "2" : "",
312 Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
313 Abc_NtkPiNum(pNtk),
314 Abc_NtkLatchNum(pNtk),
315 fExtended ? 0 : Abc_NtkPoNum(pNtk),
316 Abc_NtkNodeNum(pNtk) );
317 // write the extended header "B C J F"
318 if ( fExtended )
319 fprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
320 fprintf( pFile, "\n" );
321
322 // if the driver node is a constant, we need to complement the literal below
323 // because, in the AIGER format, literal 0/1 is represented as number 0/1
324 // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
325
326 Abc_NtkInvertConstraints( pNtk );
327 if ( !fCompact )
328 {
329 // write latch drivers
330 Abc_NtkForEachLatch( pNtk, pLatch, i )
331 {
332 pObj = Abc_ObjFanin0(pLatch);
333 pDriver = Abc_ObjFanin0(pObj);
334 uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
335 if ( Abc_LatchIsInit0(pLatch) )
336 fprintf( pFile, "%u\n", uLit );
337 else if ( Abc_LatchIsInit1(pLatch) )
338 fprintf( pFile, "%u 1\n", uLit );
339 else
340 {
341 // Both None and DC are written as 'uninitialized' e.g. a free boolean value
342 assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
343 fprintf( pFile, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
344 }
345 }
346 // write PO drivers
347 Abc_NtkForEachPo( pNtk, pObj, i )
348 {
349 pDriver = Abc_ObjFanin0(pObj);
350 fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
351 }
352 }
353 else
354 {
355 Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
356 Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
357 fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
358 Vec_StrFree( vBinary );
359 Vec_IntFree( vLits );
360 }
361 Abc_NtkInvertConstraints( pNtk );
362
363 // write the nodes into the buffer
364 Pos = 0;
365 nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
366 pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
367 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
368 Abc_AigForEachAnd( pNtk, pObj, i )
369 {
370 Extra_ProgressBarUpdate( pProgress, i, NULL );
371 uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
372 uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
373 uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
374 if ( uLit0 > uLit1 )
375 {
376 unsigned Temp = uLit0;
377 uLit0 = uLit1;
378 uLit1 = Temp;
379 }
380 assert( uLit1 < uLit );
381 Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
382 Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
383 if ( Pos > nBufferSize - 10 )
384 {
385 printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
386 fclose( pFile );
387 return;
388 }
389 }
390 assert( Pos < nBufferSize );
391 Extra_ProgressBarStop( pProgress );
392
393 // write the buffer
394 fwrite( pBuffer, 1, Pos, pFile );
395 ABC_FREE( pBuffer );
396
397 // write the symbol table
398 if ( fWriteSymbols )
399 {
400 // write PIs
401 Abc_NtkForEachPi( pNtk, pObj, i )
402 fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
403 // write latches
404 Abc_NtkForEachLatch( pNtk, pObj, i )
405 fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
406 // write POs
407 Abc_NtkForEachPo( pNtk, pObj, i )
408 if ( !fExtended )
409 fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
410 else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
411 fprintf( pFile, "b%d %s\n", i, Abc_ObjName(pObj) );
412 else
413 fprintf( pFile, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
414 }
415
416 // write the comment
417 fprintf( pFile, "c\n" );
418 if ( pNtk->pName && strlen(pNtk->pName) > 0 )
419 fprintf( pFile, ".model %s\n", pNtk->pName );
420 fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
421 fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
422 fclose( pFile );
423}
Here is the call graph for this function:

◆ Io_WriteAigerCex()

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Io_WriteAigerCex ( Abc_Cex_t * pCex,
Abc_Ntk_t * pNtk,
void * pG,
char * pFileName )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 880 of file ioWriteAiger.c.

881{
882 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
883 FILE * pFile;
884 Aig_Man_t * pAig;
885 Aig_Obj_t * pObj, * pObj2;
886 Gia_Man_t * pGia = (Gia_Man_t *)pG;
887 int k, f, b;
888 assert( pCex != NULL );
889
890 // derive AIG
891 if ( pNtk != NULL &&
892 Abc_NtkPiNum(pNtk) == pCex->nPis &&
893 Abc_NtkLatchNum(pNtk) == pCex->nRegs )
894 {
895 pAig = Abc_NtkToDar( pNtk, 0, 1 );
896 }
897 else if ( pGia != NULL &&
898 Gia_ManPiNum(pGia) == pCex->nPis &&
899 Gia_ManRegNum(pGia) == pCex->nRegs )
900 {
901 pAig = Gia_ManToAigSimple( pGia );
902 }
903 else
904 {
905 printf( "AIG parameters do not match those of the CEX.\n" );
906 return;
907 }
908
909 // create output file
910 pFile = fopen( pFileName, "wb" );
911 fprintf( pFile, "1\n" );
912 b = pCex->nRegs;
913 for ( k = 0; k < pCex->nRegs; k++ )
914 fprintf( pFile, "0" );
915 fprintf( pFile, " " );
916 Aig_ManCleanMarkA( pAig );
917 Aig_ManConst1(pAig)->fMarkA = 1;
918 for ( f = 0; f <= pCex->iFrame; f++ )
919 {
920 for ( k = 0; k < pCex->nPis; k++ )
921 {
922 fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData, b) );
923 Aig_ManCi( pAig, k )->fMarkA = Abc_InfoHasBit(pCex->pData, b++);
924 }
925 fprintf( pFile, " " );
926 Aig_ManForEachNode( pAig, pObj, k )
927 pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) &
928 (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj));
929 Aig_ManForEachCo( pAig, pObj, k )
930 pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj));
931 Saig_ManForEachPo( pAig, pObj, k )
932 fprintf( pFile, "%d", pObj->fMarkA );
933 fprintf( pFile, " " );
934 Saig_ManForEachLi( pAig, pObj, k )
935 fprintf( pFile, "%d", pObj->fMarkA );
936 fprintf( pFile, "\n" );
937 if ( f == pCex->iFrame )
938 break;
939 Saig_ManForEachLi( pAig, pObj, k )
940 fprintf( pFile, "%d", pObj->fMarkA );
941 fprintf( pFile, " " );
942 Saig_ManForEachLiLo( pAig, pObj, pObj2, k )
943 pObj2->fMarkA = pObj->fMarkA;
944 }
945 assert( b == pCex->nBits );
946 fclose( pFile );
947 Aig_ManCleanMarkA( pAig );
948 Aig_ManStop( pAig );
949}
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition aigUtil.c:148
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
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_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition giaAig.c:408
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition abcDar.c:237
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Here is the call graph for this function:

◆ Io_WriteAigerEncode()

int Io_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 166 of file ioWriteAiger.c.

167{
168 unsigned char ch;
169 while (x & ~0x7f)
170 {
171 ch = (x & 0x7f) | 0x80;
172// putc (ch, file);
173 pBuffer[Pos++] = ch;
174 x >>= 7;
175 }
176 ch = x;
177// putc (ch, file);
178 pBuffer[Pos++] = ch;
179 return Pos;
180}
Here is the caller graph for this function:

◆ Io_WriteAigerGz()

void Io_WriteAigerGz ( Abc_Ntk_t * pNtk,
char * pFileName,
int fWriteSymbols )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 436 of file ioWriteAiger.c.

437{
438 ProgressBar * pProgress;
439 gzFile pFile;
440 Abc_Obj_t * pObj, * pDriver, * pLatch;
441 int i, nNodes, Pos, nBufferSize, fExtended;
442 unsigned char * pBuffer;
443 unsigned uLit0, uLit1, uLit;
444
445 assert( Abc_NtkIsStrash(pNtk) );
446 // start the output stream
447 pFile = gzopen( pFileName, "wb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
448 if ( pFile == NULL )
449 {
450 fprintf( stdout, "Io_WriteAigerGz(): Cannot open the output file \"%s\".\n", pFileName );
451 return;
452 }
453
454 fExtended = Abc_NtkConstrNum(pNtk);
455
456 // set the node numbers to be used in the output file
457 nNodes = 0;
458 Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
459 Abc_NtkForEachCi( pNtk, pObj, i )
460 Io_ObjSetAigerNum( pObj, nNodes++ );
461 Abc_AigForEachAnd( pNtk, pObj, i )
462 Io_ObjSetAigerNum( pObj, nNodes++ );
463
464 // write the header "M I L O A" where M = I + L + A
465 gzprintf( pFile, "aig %u %u %u %u %u",
466 Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
467 Abc_NtkPiNum(pNtk),
468 Abc_NtkLatchNum(pNtk),
469 fExtended ? 0 : Abc_NtkPoNum(pNtk),
470 Abc_NtkNodeNum(pNtk) );
471 // write the extended header "B C J F"
472 if ( fExtended )
473 gzprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
474 gzprintf( pFile, "\n" );
475
476 // if the driver node is a constant, we need to complement the literal below
477 // because, in the AIGER format, literal 0/1 is represented as number 0/1
478 // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
479
480 // write latch drivers
481 Abc_NtkInvertConstraints( pNtk );
482 Abc_NtkForEachLatch( pNtk, pLatch, i )
483 {
484 pObj = Abc_ObjFanin0(pLatch);
485 pDriver = Abc_ObjFanin0(pObj);
486 uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) );
487 if ( Abc_LatchIsInit0(pLatch) )
488 gzprintf( pFile, "%u\n", uLit );
489 else if ( Abc_LatchIsInit1(pLatch) )
490 gzprintf( pFile, "%u 1\n", uLit );
491 else
492 {
493 // Both None and DC are written as 'uninitialized' e.g. a free boolean value
494 assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) );
495 gzprintf( pFile, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanout0(pLatch)), 0 ) );
496 }
497 }
498 // write PO drivers
499 Abc_NtkForEachPo( pNtk, pObj, i )
500 {
501 pDriver = Abc_ObjFanin0(pObj);
502 gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
503 }
504 Abc_NtkInvertConstraints( pNtk );
505
506 // write the nodes into the buffer
507 Pos = 0;
508 nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
509 pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
510 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
511 Abc_AigForEachAnd( pNtk, pObj, i )
512 {
513 Extra_ProgressBarUpdate( pProgress, i, NULL );
514 uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
515 uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
516 uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
517 if ( uLit0 > uLit1 )
518 {
519 unsigned Temp = uLit0;
520 uLit0 = uLit1;
521 uLit1 = Temp;
522 }
523 assert( uLit1 < uLit );
524 Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
525 Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
526 if ( Pos > nBufferSize - 10 )
527 {
528 printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
529 gzclose( pFile );
530 return;
531 }
532 }
533 assert( Pos < nBufferSize );
534 Extra_ProgressBarStop( pProgress );
535
536 // write the buffer
537 gzwrite(pFile, pBuffer, Pos);
538 ABC_FREE( pBuffer );
539
540 // write the symbol table
541 if ( fWriteSymbols )
542 {
543 // write PIs
544 Abc_NtkForEachPi( pNtk, pObj, i )
545 gzprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
546 // write latches
547 Abc_NtkForEachLatch( pNtk, pObj, i )
548 gzprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
549 // write POs
550 Abc_NtkForEachPo( pNtk, pObj, i )
551 if ( !fExtended )
552 gzprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
553 else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
554 gzprintf( pFile, "b%d %s\n", i, Abc_ObjName(pObj) );
555 else
556 gzprintf( pFile, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) );
557 }
558
559 // write the comment
560 gzprintf( pFile, "c\n" );
561 if ( pNtk->pName && strlen(pNtk->pName) > 0 )
562 gzprintf( pFile, ".model %s\n", pNtk->pName );
563 gzprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
564 gzprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
565 gzclose( pFile );
566}
gzclose
ABC_NAMESPACE_IMPL_START int ZEXPORT gzclose(gzFile file)
Definition gzclose.c:18
gzopen
gzFile ZEXPORT gzopen(const char *path, const char *mode)
Definition gzlib.c:198
gzprintf
int ZEXPORTVA gzprintf(gzFile file, const char *format, int a1, int a2, int a3, int a4, int a5, int a6, int a7, int a8, int a9, int a10, int a11, int a12, int a13, int a14, int a15, int a16, int a17, int a18, int a19, int a20)
Definition gzwrite.c:347
gzwrite
int ZEXPORT gzwrite(gzFile file, voidpc buf, unsigned len)
Definition gzwrite.c:145
gzFile
voidp gzFile
Definition zlib.h:1173
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Io_WriteAigerLiterals()

Vec_Int_t * Io_WriteAigerLiterals ( Abc_Ntk_t * pNtk)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file ioWriteAiger.c.

194{
195 Vec_Int_t * vLits;
196 Abc_Obj_t * pObj, * pDriver;
197 int i;
198 vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
199 Abc_NtkForEachLatchInput( pNtk, pObj, i )
200 {
201 pDriver = Abc_ObjFanin0(pObj);
202 Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
203 }
204 Abc_NtkForEachPo( pNtk, pObj, i )
205 {
206 pDriver = Abc_ObjFanin0(pObj);
207 Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
208 }
209 return vLits;
210}
Abc_NtkForEachLatchInput
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
Definition abc.h:503
Here is the caller graph for this function:

◆ Io_WriteEncodeLiterals()

Vec_Str_t * Io_WriteEncodeLiterals ( Vec_Int_t * vLits)

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

Synopsis [Creates the binary encoded array of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file ioWriteAiger.c.

224{
225 Vec_Str_t * vBinary;
226 int Pos = 0, Lit, LitPrev, Diff, i;
227 vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
228 LitPrev = Vec_IntEntry( vLits, 0 );
229 Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev );
230 Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
231 {
232 Diff = Lit - LitPrev;
233 Diff = (Lit < LitPrev)? -Diff : Diff;
234 Diff = (Diff << 1) | (int)(Lit < LitPrev);
235 Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
236 LitPrev = Lit;
237 if ( Pos + 10 > vBinary->nCap )
238 Vec_StrGrow( vBinary, vBinary->nCap+1 );
239 }
240 vBinary->nSize = Pos;
241/*
242 // verify
243 {
244 extern Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries );
245 char * pPos = Vec_StrArray( vBinary );
246 Vec_Int_t * vTemp = Io_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
247 for ( i = 0; i < Vec_IntSize(vLits); i++ )
248 {
249 int Entry1 = Vec_IntEntry(vLits,i);
250 int Entry2 = Vec_IntEntry(vTemp,i);
251 assert( Entry1 == Entry2 );
252 }
253 }
254*/
255 return vBinary;
256}
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: