/**CFile**************************************************************** FileName [miniaig.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [Minimalistic AIG package.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - September 29, 2012.] Revision [$Id: miniaig.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef MINI_AIG__mini_aig_h #define MINI_AIG__mini_aig_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include <stdio.h> #include <stdlib.h> #include <string.h> #include <assert.h> #ifndef _VERIFIC_DATABASE_H_ ABC_NAMESPACE_HEADER_START #endif //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// #define MINI_AIG_NULL (0x7FFFFFFF) #define MINI_AIG_START_SIZE (0x000000FF) //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// typedef struct Mini_Aig_t_ Mini_Aig_t; struct Mini_Aig_t_ { int nCap; int nSize; int nRegs; int * pArray; }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// // memory management #define MINI_AIG_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) #define MINI_AIG_CALLOC(type, num) ((type *) calloc((num), sizeof(type))) #define MINI_AIG_FALLOC(type, num) ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num))) #define MINI_AIG_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) #define MINI_AIG_REALLOC(type, obj, num) \ ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ ((type *) malloc(sizeof(type) * (num)))) // internal procedures static void Mini_AigGrow( Mini_Aig_t * p, int nCapMin ) { if ( p->nCap >= nCapMin ) return; p->pArray = MINI_AIG_REALLOC( int, p->pArray, nCapMin ); assert( p->pArray ); p->nCap = nCapMin; } static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 ) { if ( p->nSize + 2 > p->nCap ) { assert( p->nSize < MINI_AIG_NULL/4 ); if ( p->nCap < MINI_AIG_START_SIZE ) Mini_AigGrow( p, MINI_AIG_START_SIZE ); else Mini_AigGrow( p, 2 * p->nCap ); } p->pArray[p->nSize++] = Lit0; p->pArray[p->nSize++] = Lit1; } // accessing fanins static int Mini_AigNodeFanin0( Mini_Aig_t * p, int Id ) { assert( Id >= 0 && 2*Id < p->nSize ); assert( p->pArray[2*Id] == MINI_AIG_NULL || p->pArray[2*Id] < 2*Id ); return p->pArray[2*Id]; } static int Mini_AigNodeFanin1( Mini_Aig_t * p, int Id ) { assert( Id >= 0 && 2*Id < p->nSize ); assert( p->pArray[2*Id+1] == MINI_AIG_NULL || p->pArray[2*Id+1] < 2*Id ); return p->pArray[2*Id+1]; } // working with variables and literals static int Mini_AigVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } static int Mini_AigLit2Var( int Lit ) { return Lit >> 1; } static int Mini_AigLitIsCompl( int Lit ) { return Lit & 1; } static int Mini_AigLitNot( int Lit ) { return Lit ^ 1; } static int Mini_AigLitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } static int Mini_AigLitRegular( int Lit ) { return Lit & ~01; } static int Mini_AigLitConst0() { return 0; } static int Mini_AigLitConst1() { return 1; } static int Mini_AigLitIsConst0( int Lit ) { return Lit == 0; } static int Mini_AigLitIsConst1( int Lit ) { return Lit == 1; } static int Mini_AigLitIsConst( int Lit ) { return Lit == 0 || Lit == 1; } static int Mini_AigNodeNum( Mini_Aig_t * p ) { return p->nSize/2; } static int Mini_AigNodeIsConst( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id == 0; } static int Mini_AigNodeIsPi( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) == MINI_AIG_NULL; } static int Mini_AigNodeIsPo( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) == MINI_AIG_NULL; } static int Mini_AigNodeIsAnd( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) != MINI_AIG_NULL; } // working with sequential AIGs static int Mini_AigRegNum( Mini_Aig_t * p ) { return p->nRegs; } static void Mini_AigSetRegNum( Mini_Aig_t * p, int n ) { p->nRegs = n; } // iterators through objects #define Mini_AigForEachPi( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPi(p, i) ) {} else #define Mini_AigForEachPo( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPo(p, i) ) {} else #define Mini_AigForEachAnd( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsAnd(p, i) ) {} else // constructor/destructor static Mini_Aig_t * Mini_AigStart() { Mini_Aig_t * p; p = MINI_AIG_CALLOC( Mini_Aig_t, 1 ); p->nCap = MINI_AIG_START_SIZE; p->pArray = MINI_AIG_ALLOC( int, p->nCap ); Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL ); return p; } static void Mini_AigStop( Mini_Aig_t * p ) { MINI_AIG_FREE( p->pArray ); MINI_AIG_FREE( p ); } static int Mini_AigPiNum( Mini_Aig_t * p ) { int i, nPis = 0; Mini_AigForEachPi( p, i ) nPis++; return nPis; } static int Mini_AigPoNum( Mini_Aig_t * p ) { int i, nPos = 0; Mini_AigForEachPo( p, i ) nPos++; return nPos; } static int Mini_AigAndNum( Mini_Aig_t * p ) { int i, nNodes = 0; Mini_AigForEachAnd( p, i ) nNodes++; return nNodes; } static void Mini_AigPrintStats( Mini_Aig_t * p ) { printf( "MiniAIG stats: PI = %d PO = %d FF = %d AND = %d\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigRegNum(p), Mini_AigAndNum(p) ); } // serialization static void Mini_AigDump( Mini_Aig_t * p, char * pFileName ) { FILE * pFile; int RetValue; pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open file for writing \"%s\".\n", pFileName ); return; } RetValue = (int)fwrite( &p->nSize, sizeof(int), 1, pFile ); RetValue = (int)fwrite( &p->nRegs, sizeof(int), 1, pFile ); RetValue = (int)fwrite( p->pArray, sizeof(int), p->nSize, pFile ); fclose( pFile ); } static Mini_Aig_t * Mini_AigLoad( char * pFileName ) { Mini_Aig_t * p; FILE * pFile; int RetValue, nSize; pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) { printf( "Cannot open file for reading \"%s\".\n", pFileName ); return NULL; } RetValue = (int)fread( &nSize, sizeof(int), 1, pFile ); p = MINI_AIG_CALLOC( Mini_Aig_t, 1 ); p->nSize = p->nCap = nSize; p->pArray = MINI_AIG_ALLOC( int, p->nCap ); RetValue = (int)fread( &p->nRegs, sizeof(int), 1, pFile ); RetValue = (int)fread( p->pArray, sizeof(int), p->nSize, pFile ); fclose( pFile ); return p; } // creating nodes // (constant node is created when AIG manager is created) static int Mini_AigCreatePi( Mini_Aig_t * p ) { int Lit = p->nSize; Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL ); return Lit; } static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 ) { int Lit = p->nSize; assert( Lit0 >= 0 && Lit0 < Lit ); Mini_AigPush( p, Lit0, MINI_AIG_NULL ); return Lit; } // boolean operations static int Mini_AigAnd( Mini_Aig_t * p, int Lit0, int Lit1 ) { int Lit = p->nSize; assert( Lit0 >= 0 && Lit0 < Lit ); assert( Lit1 >= 0 && Lit1 < Lit ); if ( Lit0 < Lit1 ) Mini_AigPush( p, Lit0, Lit1 ); else Mini_AigPush( p, Lit1, Lit0 ); return Lit; } static int Mini_AigOr( Mini_Aig_t * p, int Lit0, int Lit1 ) { return Mini_AigLitNot( Mini_AigAnd( p, Mini_AigLitNot(Lit0), Mini_AigLitNot(Lit1) ) ); } static int Mini_AigMux( Mini_Aig_t * p, int LitC, int Lit1, int Lit0 ) { int Res0 = Mini_AigAnd( p, LitC, Lit1 ); int Res1 = Mini_AigAnd( p, Mini_AigLitNot(LitC), Lit0 ); return Mini_AigOr( p, Res0, Res1 ); } static int Mini_AigXor( Mini_Aig_t * p, int Lit0, int Lit1 ) { return Mini_AigMux( p, Lit0, Mini_AigLitNot(Lit1), Lit1 ); } static int Mini_AigXorSpecial( Mini_Aig_t * p, int Lit0, int Lit1 ) { int Lit = p->nSize; assert( Lit0 >= 0 && Lit0 < Lit ); assert( Lit1 >= 0 && Lit1 < Lit ); if ( Lit0 > Lit1 ) Mini_AigPush( p, Lit0, Lit1 ); else Mini_AigPush( p, Lit1, Lit0 ); return Lit; } static int Mini_AigAndMulti( Mini_Aig_t * p, int * pLits, int nLits ) { int i; assert( nLits > 0 ); while ( nLits > 1 ) { for ( i = 0; i < nLits/2; i++ ) pLits[i] = Mini_AigAnd(p, pLits[2*i], pLits[2*i+1]); if ( nLits & 1 ) pLits[i++] = pLits[nLits-1]; nLits = i; } return pLits[0]; } static int Mini_AigMuxMulti( Mini_Aig_t * p, int * pCtrl, int nCtrl, int * pData, int nData ) { int i, c; assert( nData > 0 ); if ( nCtrl == 0 ) return pData[0]; assert( nData <= (1 << nCtrl) ); for ( c = 0; c < nCtrl; c++ ) { for ( i = 0; i < nData/2; i++ ) pData[i] = Mini_AigMux( p, pCtrl[c], pData[2*i+1], pData[2*i] ); if ( nData & 1 ) pData[i++] = Mini_AigMux( p, pCtrl[c], 0, pData[nData-1] ); nData = i; } assert( nData == 1 ); return pData[0]; } static int Mini_AigMuxMulti_rec( Mini_Aig_t * p, int * pCtrl, int * pData, int nData ) { int Res0, Res1; assert( nData > 0 ); if ( nData == 1 ) return pData[0]; assert( nData % 2 == 0 ); Res0 = Mini_AigMuxMulti_rec( p, pCtrl+1, pData, nData/2 ); Res1 = Mini_AigMuxMulti_rec( p, pCtrl+1, pData+nData/2, nData/2 ); return Mini_AigMux( p, pCtrl[0], Res1, Res0 ); } static unsigned s_MiniTruths5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000, }; static inline int Mini_AigTt5HasVar( unsigned t, int iVar ) { return ((t << (1<<iVar)) & s_MiniTruths5[iVar]) != (t & s_MiniTruths5[iVar]); } static inline unsigned Mini_AigTt5Cofactor0( unsigned t, int iVar ) { assert( iVar >= 0 && iVar < 6 ); return (t & ~s_MiniTruths5[iVar]) | ((t & ~s_MiniTruths5[iVar]) << (1<<iVar)); } static inline unsigned Mini_AigTt5Cofactor1( unsigned t, int iVar ) { assert( iVar >= 0 && iVar < 6 ); return (t & s_MiniTruths5[iVar]) | ((t & s_MiniTruths5[iVar]) >> (1<<iVar)); } static inline int Mini_AigAndProp( Mini_Aig_t * p, int iLit0, int iLit1 ) { if ( iLit0 < 2 ) return iLit0 ? iLit1 : 0; if ( iLit1 < 2 ) return iLit1 ? iLit0 : 0; if ( iLit0 == iLit1 ) return iLit1; if ( iLit0 == Mini_AigLitNot(iLit1) ) return 0; return Mini_AigAnd( p, iLit0, iLit1 ); } static inline int Mini_AigMuxProp( Mini_Aig_t * p, int iCtrl, int iData1, int iData0 ) { int iTemp0 = Mini_AigAndProp( p, Mini_AigLitNot(iCtrl), iData0 ); int iTemp1 = Mini_AigAndProp( p, iCtrl, iData1 ); return Mini_AigLitNot( Mini_AigAndProp( p, Mini_AigLitNot(iTemp0), Mini_AigLitNot(iTemp1) ) ); } static inline int Mini_AigTruth( Mini_Aig_t * p, int * pVarLits, int nVars, unsigned Truth ) { int Var, Lit0, Lit1; if ( Truth == 0 ) return 0; if ( ~Truth == 0 ) return 1; assert( nVars > 0 ); // find the topmost var for ( Var = nVars-1; Var >= 0; Var-- ) if ( Mini_AigTt5HasVar( Truth, Var ) ) break; assert( Var >= 0 ); // cofactor Lit0 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor0(Truth, Var) ); Lit1 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor1(Truth, Var) ); return Mini_AigMuxProp( p, pVarLits[Var], Lit1, Lit0 ); } static char * Mini_AigPhase( Mini_Aig_t * p ) { char * pRes = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) ); int i; Mini_AigForEachAnd( p, i ) { int iFaninLit0 = Mini_AigNodeFanin0( p, i ); int iFaninLit1 = Mini_AigNodeFanin1( p, i ); int Phase0 = pRes[Mini_AigLit2Var(iFaninLit0)] ^ Mini_AigLitIsCompl(iFaninLit0); int Phase1 = pRes[Mini_AigLit2Var(iFaninLit1)] ^ Mini_AigLitIsCompl(iFaninLit1); pRes[i] = Phase0 & Phase1; } return pRes; } // procedure to check the topological order during AIG construction static int Mini_AigCheck( Mini_Aig_t * p ) { int status = 1; int i, iFaninLit0, iFaninLit1; Mini_AigForEachAnd( p, i ) { // get the fanin literals of this AND node iFaninLit0 = Mini_AigNodeFanin0( p, i ); iFaninLit1 = Mini_AigNodeFanin1( p, i ); // compare the fanin literals with the literal of the current node (2 * i) if ( iFaninLit0 >= 2 * i ) printf( "Fanin0 of AND node %d is not in a topological order.\n", i ), status = 0; if ( iFaninLit1 >= 2 * i ) printf( "Fanin0 of AND node %d is not in a topological order.\n", i ), status = 0; } Mini_AigForEachPo( p, i ) { // get the fanin literal of this PO node iFaninLit0 = Mini_AigNodeFanin0( p, i ); // compare the fanin literal with the literal of the current node (2 * i) if ( iFaninLit0 >= 2 * i ) printf( "Fanin0 of PO node %d is not in a topological order.\n", i ), status = 0; } return status; } // procedure to dump MiniAIG into a Verilog file static void Mini_AigDumpVerilog( char * pFileName, char * pModuleName, Mini_Aig_t * p ) { int i, k, iFaninLit0, iFaninLit1, Length = strlen(pModuleName), nPos = Mini_AigPoNum(p); char * pObjIsPi = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) ); FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open output file %s\n", pFileName ); MINI_AIG_FREE( pObjIsPi ); return; } // write interface //fprintf( pFile, "// This MiniAIG dump was produced by ABC on %s\n\n", Extra_TimeStamp() ); fprintf( pFile, "module %s (\n", pModuleName ); if ( Mini_AigPiNum(p) > 0 ) { fprintf( pFile, "%*sinput wire", Length+10, "" ); k = 0; Mini_AigForEachPi( p, i ) { if ( k++ % 12 == 0 ) fprintf( pFile, "\n%*s", Length+10, "" ); fprintf( pFile, "i%d, ", i ); pObjIsPi[i] = 1; } } fprintf( pFile, "\n%*soutput wire", Length+10, "" ); k = 0; Mini_AigForEachPo( p, i ) { if ( k++ % 12 == 0 ) fprintf( pFile, "\n%*s", Length+10, "" ); fprintf( pFile, "o%d%s", i, k==nPos ? "":", " ); } fprintf( pFile, "\n%*s);\n\n", Length+8, "" ); // write LUTs Mini_AigForEachAnd( p, i ) { iFaninLit0 = Mini_AigNodeFanin0( p, i ); iFaninLit1 = Mini_AigNodeFanin1( p, i ); fprintf( pFile, " assign n%d = ", i ); fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", pObjIsPi[iFaninLit0 >> 1] ? 'i':'n', iFaninLit0 >> 1 ); fprintf( pFile, " & " ); fprintf( pFile, "%s%c%d", (iFaninLit1 & 1) ? "~":"", pObjIsPi[iFaninLit1 >> 1] ? 'i':'n', iFaninLit1 >> 1 ); fprintf( pFile, ";\n" ); } // write assigns fprintf( pFile, "\n" ); Mini_AigForEachPo( p, i ) { iFaninLit0 = Mini_AigNodeFanin0( p, i ); fprintf( pFile, " assign o%d = ", i ); fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", pObjIsPi[iFaninLit0 >> 1] ? 'i':'n', iFaninLit0 >> 1 ); fprintf( pFile, ";\n" ); } fprintf( pFile, "\nendmodule // %s \n\n\n", pModuleName ); MINI_AIG_FREE( pObjIsPi ); fclose( pFile ); } // checks if MiniAIG is normalized (first inputs, then internal nodes, then outputs) static int Mini_AigIsNormalized( Mini_Aig_t * p ) { int nCiNum = Mini_AigPiNum(p); int nCoNum = Mini_AigPoNum(p); int i, nOffset = 1; for ( i = 0; i < nCiNum; i++ ) if ( !Mini_AigNodeIsPi( p, nOffset+i ) ) return 0; nOffset = Mini_AigNodeNum(p) - nCoNum; for ( i = 0; i < nCoNum; i++ ) if ( !Mini_AigNodeIsPo( p, nOffset+i ) ) return 0; return 1; } //////////////////////////////////////////////////////////////////////// /// MiniAIG reading from / write into AIGER /// //////////////////////////////////////////////////////////////////////// static unsigned Mini_AigerReadUnsigned( FILE * pFile ) { unsigned x = 0, i = 0; unsigned char ch; while ((ch = fgetc(pFile)) & 0x80) x |= (ch & 0x7f) << (7 * i++); return x | (ch << (7 * i)); } static void Mini_AigerWriteUnsigned( FILE * pFile, unsigned x ) { unsigned char ch; while (x & ~0x7f) { ch = (x & 0x7f) | 0x80; fputc( ch, pFile ); x >>= 7; } ch = x; fputc( ch, pFile ); } static int * Mini_AigerReadInt( char * pFileName, int * pnObjs, int * pnIns, int * pnLatches, int * pnOuts, int * pnAnds ) { int i, Temp, nTotal, nObjs, nIns, nLatches, nOuts, nAnds, * pObjs; FILE * pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) { fprintf( stdout, "Mini_AigerRead(): Cannot open the output file \"%s\".\n", pFileName ); return NULL; } if ( fgetc(pFile) != 'a' || fgetc(pFile) != 'i' || fgetc(pFile) != 'g' ) { fprintf( stdout, "Mini_AigerRead(): Can only read binary AIGER.\n" ); fclose( pFile ); return NULL; } if ( fscanf(pFile, "%d %d %d %d %d", &nTotal, &nIns, &nLatches, &nOuts, &nAnds) != 5 ) { fprintf( stdout, "Mini_AigerRead(): Cannot read the header line.\n" ); fclose( pFile ); return NULL; } if ( nTotal != nIns + nLatches + nAnds ) { fprintf( stdout, "The number of objects does not match.\n" ); fclose( pFile ); return NULL; } nObjs = 1 + nIns + 2*nLatches + nOuts + nAnds; pObjs = MINI_AIG_CALLOC( int, nObjs * 2 ); for ( i = 0; i <= nIns + nLatches; i++ ) pObjs[2*i] = pObjs[2*i+1] = MINI_AIG_NULL; // read flop input literals for ( i = 0; i < nLatches; i++ ) { while ( fgetc(pFile) != '\n' ); fscanf( pFile, "%d", &Temp ); pObjs[2*(nObjs-nLatches+i)+0] = Temp; pObjs[2*(nObjs-nLatches+i)+1] = MINI_AIG_NULL; } // read output literals for ( i = 0; i < nOuts; i++ ) { while ( fgetc(pFile) != '\n' ); fscanf( pFile, "%d", &Temp ); pObjs[2*(nObjs-nOuts-nLatches+i)+0] = Temp; pObjs[2*(nObjs-nOuts-nLatches+i)+1] = MINI_AIG_NULL; } // read the binary part while ( fgetc(pFile) != '\n' ); for ( i = 0; i < nAnds; i++ ) { int uLit = 2*(1+nIns+nLatches+i); int uLit1 = uLit - Mini_AigerReadUnsigned( pFile ); int uLit0 = uLit1 - Mini_AigerReadUnsigned( pFile ); pObjs[uLit+0] = uLit0; pObjs[uLit+1] = uLit1; } fclose( pFile ); if ( pnObjs ) *pnObjs = nObjs; if ( pnIns ) *pnIns = nIns; if ( pnLatches ) *pnLatches = nLatches; if ( pnOuts ) *pnOuts = nOuts; if ( pnAnds ) *pnAnds = nAnds; return pObjs; } static Mini_Aig_t * Mini_AigerRead( char * pFileName, int fVerbose ) { Mini_Aig_t * p; int nObjs, nIns, nLatches, nOuts, nAnds, * pObjs = Mini_AigerReadInt( pFileName, &nObjs, &nIns, &nLatches, &nOuts, &nAnds ); if ( pObjs == NULL ) return NULL; p = MINI_AIG_CALLOC( Mini_Aig_t, 1 ); p->nCap = 2*nObjs; p->nSize = 2*nObjs; p->nRegs = nLatches; p->pArray = pObjs; if ( fVerbose ) printf( "Loaded MiniAIG from the AIGER file \"%s\".\n", pFileName ); return p; } static void Mini_AigerWriteInt( char * pFileName, int * pObjs, int nObjs, int nIns, int nLatches, int nOuts, int nAnds ) { FILE * pFile = fopen( pFileName, "wb" ); int i; if ( pFile == NULL ) { fprintf( stdout, "Mini_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName ); return; } fprintf( pFile, "aig %d %d %d %d %d\n", nIns + nLatches + nAnds, nIns, nLatches, nOuts, nAnds ); for ( i = 0; i < nLatches; i++ ) fprintf( pFile, "%d\n", pObjs[2*(nObjs-nLatches+i)+0] ); for ( i = 0; i < nOuts; i++ ) fprintf( pFile, "%d\n", pObjs[2*(nObjs-nOuts-nLatches+i)+0] ); for ( i = 0; i < nAnds; i++ ) { int uLit = 2*(1+nIns+nLatches+i); int uLit0 = pObjs[uLit+0]; int uLit1 = pObjs[uLit+1]; Mini_AigerWriteUnsigned( pFile, uLit - uLit1 ); Mini_AigerWriteUnsigned( pFile, uLit1 - uLit0 ); } fprintf( pFile, "c\n" ); fclose( pFile ); } static void Mini_AigerWrite( char * pFileName, Mini_Aig_t * p, int fVerbose ) { int i, nIns = 0, nOuts = 0, nAnds = 0; assert( Mini_AigIsNormalized(p) ); for ( i = 1; i < Mini_AigNodeNum(p); i++ ) { if ( Mini_AigNodeIsPi(p, i) ) nIns++; else if ( Mini_AigNodeIsPo(p, i) ) nOuts++; else nAnds++; } Mini_AigerWriteInt( pFileName, p->pArray, p->nSize/2, nIns - p->nRegs, p->nRegs, nOuts - p->nRegs, nAnds ); if ( fVerbose ) printf( "Written MiniAIG into the AIGER file \"%s\".\n", pFileName ); } static void Mini_AigerTest( char * pFileNameIn, char * pFileNameOut ) { Mini_Aig_t * p = Mini_AigerRead( pFileNameIn, 1 ); if ( p == NULL ) return; printf( "Finished reading input file \"%s\".\n", pFileNameIn ); Mini_AigerWrite( pFileNameOut, p, 1 ); printf( "Finished writing output file \"%s\".\n", pFileNameOut ); Mini_AigStop( p ); } /* int main( int argc, char ** argv ) { if ( argc != 3 ) return 0; Mini_AigerTest( argv[1], argv[2] ); return 1; } */ //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #ifndef _VERIFIC_DATABASE_H_ ABC_NAMESPACE_HEADER_END #endif #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////