src/aig/ioa/ioaReadAig.c File Reference
#include "ioa.h"
Include dependency graph for ioaReadAig.c:
Go to the source code of this file.
Functions | |
| unsigned | Ioa_ReadAigerDecode (char **ppPos) |
| Aig_Man_t * | Ioa_ReadAiger (char *pFileName, int fCheck) |
Function Documentation
| Aig_Man_t* Ioa_ReadAiger | ( | char * | pFileName, | |
| int | fCheck | |||
| ) |
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 }
| unsigned Ioa_ReadAigerDecode | ( | char ** | ppPos | ) |
CFile****************************************************************
FileName [ioaReadAiger.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
- ioaReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp
] DECLARATIONS ///
Function*************************************************************
Synopsis [Extracts one unsigned AIG edge from the input buffer.]
Description [This procedure is a slightly modified version of Armin Biere's procedure "unsigned decode (FILE * file)". ]
SideEffects [Updates the current reading position.]
SeeAlso []
Definition at line 295 of file ioaReadAig.c.
