src/aig/ioa/ioa.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "bar.h"
#include "aig.h"
Include dependency graph for ioa.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

Aig_Man_t * Ioa_ReadAiger (char *pFileName, int fCheck)
void Ioa_WriteAiger (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols)
int Ioa_FileSize (char *pFileName)
char * Ioa_FileNameGeneric (char *FileName)
char * Ioa_TimeStamp ()

Function Documentation

char* Ioa_FileNameGeneric ( char *  FileName  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file ioaUtil.c.

00071 {
00072     char * pDot;
00073     char * pUnd;
00074     char * pRes;
00075     
00076     // find the generic name of the file
00077     pRes = Aig_UtilStrsav( FileName );
00078     // find the pointer to the "." symbol in the file name
00079 //  pUnd = strstr( FileName, "_" );
00080     pUnd = NULL;
00081     pDot = strstr( FileName, "." );
00082     if ( pUnd )
00083         pRes[pUnd - FileName] = 0;
00084     else if ( pDot )
00085         pRes[pDot - FileName] = 0;
00086     return pRes;
00087 }

int Ioa_FileSize ( char *  pFileName  ) 

CFile****************************************************************

FileName [ioaUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Procedures to read binary AIGER format developed by Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - December 16, 2006.]

Revision [

Id
ioaUtil.c,v 1.00 2006/12/16 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Returns the file size.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 43 of file ioaUtil.c.

00044 {
00045     FILE * pFile;
00046     int nFileSize;
00047     pFile = fopen( pFileName, "r" );
00048     if ( pFile == NULL )
00049     {
00050         printf( "Ioa_FileSize(): The file is unavailable (absent or open).\n" );
00051         return 0;
00052     }
00053     fseek( pFile, 0, SEEK_END );  
00054     nFileSize = ftell( pFile ); 
00055     fclose( pFile );
00056     return nFileSize;
00057 }

Aig_Man_t* Ioa_ReadAiger ( char *  pFileName,
int  fCheck 
)

CFile****************************************************************

FileName [ioa.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
ioa.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

] INCLUDES /// PARAMETERS /// BASIC TYPES /// MACRO DEFINITIONS /// ITERATORS /// FUNCTION DECLARATIONS ///

FUNCTION DEFINITIONS ///Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ioaReadAig.c.

00046 {
00047     Bar_Progress_t * pProgress;
00048     FILE * pFile;
00049     Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
00050     Aig_Obj_t * pObj, * pNode0, * pNode1;
00051     Aig_Man_t * pManNew;
00052     int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
00053     char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
00054     unsigned uLit0, uLit1, uLit;
00055 
00056     // read the file into the buffer
00057     nFileSize = Ioa_FileSize( pFileName );
00058     pFile = fopen( pFileName, "rb" );
00059     pContents = ALLOC( char, nFileSize );
00060     fread( pContents, nFileSize, 1, pFile );
00061     fclose( pFile );
00062 
00063     // check if the input file format is correct
00064     if ( strncmp(pContents, "aig", 3) != 0 )
00065     {
00066         fprintf( stdout, "Wrong input file format.\n" );
00067         return NULL;
00068     }
00069 
00070     // read the file type
00071     pCur = pContents;         while ( *pCur++ != ' ' );
00072     // read the number of objects
00073     nTotal = atoi( pCur );    while ( *pCur++ != ' ' );
00074     // read the number of inputs
00075     nInputs = atoi( pCur );   while ( *pCur++ != ' ' );
00076     // read the number of latches
00077     nLatches = atoi( pCur );  while ( *pCur++ != ' ' );
00078     // read the number of outputs
00079     nOutputs = atoi( pCur );  while ( *pCur++ != ' ' );
00080     // read the number of nodes
00081     nAnds = atoi( pCur );     while ( *pCur++ != '\n' );  
00082     // check the parameters
00083     if ( nTotal != nInputs + nLatches + nAnds )
00084     {
00085         fprintf( stdout, "The paramters are wrong.\n" );
00086         return NULL;
00087     }
00088 
00089     // allocate the empty AIG
00090     pManNew = Aig_ManStart( nAnds );
00091     pName = Ioa_FileNameGeneric( pFileName );
00092     pManNew->pName = Aig_UtilStrsav( pName );
00093 //    pManNew->pSpec = Ioa_UtilStrsav( pFileName );
00094     free( pName );
00095 
00096     // prepare the array of nodes
00097     vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
00098     Vec_PtrPush( vNodes, Aig_ManConst0(pManNew) );
00099 
00100     // create the PIs
00101     for ( i = 0; i < nInputs + nLatches; i++ )
00102     {
00103         pObj = Aig_ObjCreatePi(pManNew);    
00104         Vec_PtrPush( vNodes, pObj );
00105     }
00106 /*
00107     // create the POs
00108     for ( i = 0; i < nOutputs + nLatches; i++ )
00109     {
00110         pObj = Aig_ObjCreatePo(pManNew);   
00111     }
00112 */
00113     // create the latches
00114     pManNew->nRegs = nLatches;
00115 /*
00116     nDigits = Ioa_Base10Log( nLatches );
00117     for ( i = 0; i < nLatches; i++ )
00118     {
00119         pObj = Aig_ObjCreateLatch(pManNew);
00120         Aig_LatchSetInit0( pObj );
00121         pNode0 = Aig_ObjCreateBi(pManNew);
00122         pNode1 = Aig_ObjCreateBo(pManNew);
00123         Aig_ObjAddFanin( pObj, pNode0 );
00124         Aig_ObjAddFanin( pNode1, pObj );
00125         Vec_PtrPush( vNodes, pNode1 );
00126         // assign names to latch and its input
00127 //        Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
00128 //        printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id );
00129     } 
00130 */
00131     
00132     // remember the beginning of latch/PO literals
00133     pDrivers = pCur;
00134 
00135     // scroll to the beginning of the binary data
00136     for ( i = 0; i < nLatches + nOutputs; )
00137         if ( *pCur++ == '\n' )
00138             i++;
00139 
00140     // create the AND gates
00141     pProgress = Bar_ProgressStart( stdout, nAnds );
00142     for ( i = 0; i < nAnds; i++ )
00143     {
00144         Bar_ProgressUpdate( pProgress, i, NULL );
00145         uLit = ((i + 1 + nInputs + nLatches) << 1);
00146         uLit1 = uLit  - Ioa_ReadAigerDecode( &pCur );
00147         uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
00148 //        assert( uLit1 > uLit0 );
00149         pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
00150         pNode1 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
00151         assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
00152         Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
00153     }
00154     Bar_ProgressStop( pProgress );
00155 
00156     // remember the place where symbols begin
00157     pSymbols = pCur;
00158 
00159     // read the latch driver literals
00160     vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
00161     pCur = pDrivers;
00162 //    Aig_ManForEachLatchInput( pManNew, pObj, i )
00163     for ( i = 0; i < nLatches; i++ )
00164     {
00165         uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
00166         pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
00167 //        Aig_ObjAddFanin( pObj, pNode0 );
00168         Vec_PtrPush( vDrivers, pNode0 );
00169     }
00170     // read the PO driver literals
00171 //    Aig_ManForEachPo( pManNew, pObj, i )
00172     for ( i = 0; i < nOutputs; i++ )
00173     {
00174         uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
00175         pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
00176 //        Aig_ObjAddFanin( pObj, pNode0 );
00177         Vec_PtrPush( vDrivers, pNode0 );
00178     }
00179 
00180 
00181     // create the POs
00182     for ( i = 0; i < nOutputs; i++ )
00183         Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
00184     for ( i = 0; i < nLatches; i++ )
00185         Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, i) );
00186     Vec_PtrFree( vDrivers );
00187 
00188 /*
00189     // read the names if present
00190     pCur = pSymbols;
00191     if ( *pCur != 'c' )
00192     {
00193         int Counter = 0;
00194         while ( pCur < pContents + nFileSize && *pCur != 'c' )
00195         {
00196             // get the terminal type
00197             pType = pCur;
00198             if ( *pCur == 'i' )
00199                 vTerms = pManNew->vPis;
00200             else if ( *pCur == 'l' )
00201                 vTerms = pManNew->vBoxes;
00202             else if ( *pCur == 'o' )
00203                 vTerms = pManNew->vPos;
00204             else
00205             {
00206                 fprintf( stdout, "Wrong terminal type.\n" );
00207                 return NULL;
00208             }
00209             // get the terminal number
00210             iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
00211             // get the node
00212             if ( iTerm >= Vec_PtrSize(vTerms) )
00213             {
00214                 fprintf( stdout, "The number of terminal is out of bound.\n" );
00215                 return NULL;
00216             }
00217             pObj = Vec_PtrEntry( vTerms, iTerm );
00218             if ( *pType == 'l' )
00219                 pObj = Aig_ObjFanout0(pObj);
00220             // assign the name
00221             pName = pCur;          while ( *pCur++ != '\n' );
00222             // assign this name 
00223             *(pCur-1) = 0;
00224             Aig_ObjAssignName( pObj, pName, NULL );
00225             if ( *pType == 'l' )
00226             {
00227                 Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
00228                 Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
00229             }
00230             // mark the node as named
00231             pObj->pCopy = (Aig_Obj_t *)Aig_ObjName(pObj);
00232         } 
00233 
00234         // assign the remaining names
00235         Aig_ManForEachPi( pManNew, pObj, i )
00236         {
00237             if ( pObj->pCopy ) continue;
00238             Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
00239             Counter++;
00240         }
00241         Aig_ManForEachLatchOutput( pManNew, pObj, i )
00242         {
00243             if ( pObj->pCopy ) continue;
00244             Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
00245             Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
00246             Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
00247             Counter++;
00248         }
00249         Aig_ManForEachPo( pManNew, pObj, i )
00250         {
00251             if ( pObj->pCopy ) continue;
00252             Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
00253             Counter++;
00254         }
00255         if ( Counter )
00256             printf( "Ioa_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
00257     }
00258     else
00259     {
00260 //        printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
00261         Aig_ManShortNames( pManNew );
00262     }
00263 */
00264 
00265     // skipping the comments
00266     free( pContents );
00267     Vec_PtrFree( vNodes );
00268 
00269     // remove the extra nodes
00270     Aig_ManCleanup( pManNew );
00271 
00272     // check the result
00273     if ( fCheck && !Aig_ManCheck( pManNew ) )
00274     {
00275         printf( "Ioa_ReadAiger: The network check has failed.\n" );
00276         Aig_ManStop( pManNew );
00277         return NULL;
00278     }
00279     return pManNew;
00280 }

char* Ioa_TimeStamp (  ) 

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

Synopsis [Returns the time stamp.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 100 of file ioaUtil.c.

00101 {
00102     static char Buffer[100];
00103         char * TimeStamp;
00104         time_t ltime;
00105     // get the current time
00106         time( &ltime );
00107         TimeStamp = asctime( localtime( &ltime ) );
00108         TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
00109     strcpy( Buffer, TimeStamp );
00110     return Buffer;
00111 }

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

FUNCTION DEFINITIONS ///Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file ioaWriteAig.c.

00150 {
00151     Bar_Progress_t * pProgress;
00152     FILE * pFile;
00153     Aig_Obj_t * pObj, * pDriver;
00154     int i, nNodes, Pos, nBufferSize;
00155     unsigned char * pBuffer;
00156     unsigned uLit0, uLit1, uLit;
00157 
00158 //    assert( Aig_ManIsStrash(pMan) );
00159     // start the output stream
00160     pFile = fopen( pFileName, "wb" );
00161     if ( pFile == NULL )
00162     {
00163         fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
00164         return;
00165     }
00166 /*
00167     Aig_ManForEachLatch( pMan, pObj, i )
00168         if ( !Aig_LatchIsInit0(pObj) )
00169         {
00170             fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
00171             return;
00172         }
00173 */
00174     // set the node numbers to be used in the output file
00175     nNodes = 0;
00176     Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
00177     Aig_ManForEachPi( pMan, pObj, i )
00178         Ioa_ObjSetAigerNum( pObj, nNodes++ );
00179     Aig_ManForEachNode( pMan, pObj, i )
00180         Ioa_ObjSetAigerNum( pObj, nNodes++ );
00181 
00182     // write the header "M I L O A" where M = I + L + A
00183     fprintf( pFile, "aig %u %u %u %u %u\n", 
00184         Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), 
00185         Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
00186         Aig_ManRegNum(pMan),
00187         Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
00188         Aig_ManNodeNum(pMan) );
00189 
00190     // if the driver node is a constant, we need to complement the literal below
00191     // because, in the AIGER format, literal 0/1 is represented as number 0/1
00192     // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
00193 
00194     // write latch drivers
00195     Aig_ManForEachLiSeq( pMan, pObj, i )
00196     {
00197         pDriver = Aig_ObjFanin0(pObj);
00198         fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
00199     }
00200 
00201     // write PO drivers
00202     Aig_ManForEachPoSeq( pMan, pObj, i )
00203     {
00204         pDriver = Aig_ObjFanin0(pObj);
00205         fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
00206     }
00207 
00208     // write the nodes into the buffer
00209     Pos = 0;
00210     nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
00211     pBuffer = ALLOC( char, nBufferSize );
00212     pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
00213     Aig_ManForEachNode( pMan, pObj, i )
00214     {
00215         Bar_ProgressUpdate( pProgress, i, NULL );
00216         uLit  = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
00217         uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
00218         uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
00219         assert( uLit0 < uLit1 );
00220         Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
00221         Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
00222         if ( Pos > nBufferSize - 10 )
00223         {
00224             printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
00225                 fclose( pFile );
00226             return;
00227         }
00228     }
00229     assert( Pos < nBufferSize );
00230     Bar_ProgressStop( pProgress );
00231 
00232     // write the buffer
00233     fwrite( pBuffer, 1, Pos, pFile );
00234     free( pBuffer );
00235 /*
00236     // write the symbol table
00237     if ( fWriteSymbols )
00238     {
00239         // write PIs
00240         Aig_ManForEachPi( pMan, pObj, i )
00241             fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
00242         // write latches
00243         Aig_ManForEachLatch( pMan, pObj, i )
00244             fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
00245         // write POs
00246         Aig_ManForEachPo( pMan, pObj, i )
00247             fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
00248     }
00249 */
00250     // write the comment
00251     fprintf( pFile, "c\n" );
00252     if ( pMan->pName )
00253         fprintf( pFile, ".model %s\n", pMan->pName );
00254     fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() );
00255     fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
00256         fclose( pFile );
00257 }

Generated on Tue Jan 5 12:18:22 2010 for abc70930 by  doxygen 1.6.1