src/base/io/ioReadAiger.c File Reference
#include "io.h"
Include dependency graph for ioReadAiger.c:
Go to the source code of this file.
Functions | |
| unsigned | Io_ReadAigerDecode (char **ppPos) |
| Abc_Ntk_t * | Io_ReadAiger (char *pFileName, int fCheck) |
Function Documentation
| Abc_Ntk_t* Io_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 ioReadAiger.c.
00046 { 00047 ProgressBar * pProgress; 00048 FILE * pFile; 00049 Vec_Ptr_t * vNodes, * vTerms; 00050 Abc_Obj_t * pObj, * pNode0, * pNode1; 00051 Abc_Ntk_t * pNtkNew; 00052 int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i; 00053 char * pContents, * pDrivers, * pSymbols, * pCur, * pName, * pType; 00054 unsigned uLit0, uLit1, uLit; 00055 00056 // read the file into the buffer 00057 nFileSize = Extra_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 // allocate the empty AIG 00071 pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); 00072 pName = Extra_FileNameGeneric( pFileName ); 00073 pNtkNew->pName = Extra_UtilStrsav( pName ); 00074 pNtkNew->pSpec = Extra_UtilStrsav( pFileName ); 00075 free( pName ); 00076 00077 00078 // read the file type 00079 pCur = pContents; while ( *pCur++ != ' ' ); 00080 // read the number of objects 00081 nTotal = atoi( pCur ); while ( *pCur++ != ' ' ); 00082 // read the number of inputs 00083 nInputs = atoi( pCur ); while ( *pCur++ != ' ' ); 00084 // read the number of latches 00085 nLatches = atoi( pCur ); while ( *pCur++ != ' ' ); 00086 // read the number of outputs 00087 nOutputs = atoi( pCur ); while ( *pCur++ != ' ' ); 00088 // read the number of nodes 00089 nAnds = atoi( pCur ); while ( *pCur++ != '\n' ); 00090 // check the parameters 00091 if ( nTotal != nInputs + nLatches + nAnds ) 00092 { 00093 fprintf( stdout, "The paramters are wrong.\n" ); 00094 return NULL; 00095 } 00096 00097 // prepare the array of nodes 00098 vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); 00099 Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) ); 00100 00101 // create the PIs 00102 for ( i = 0; i < nInputs; i++ ) 00103 { 00104 pObj = Abc_NtkCreatePi(pNtkNew); 00105 Vec_PtrPush( vNodes, pObj ); 00106 } 00107 // create the POs 00108 for ( i = 0; i < nOutputs; i++ ) 00109 { 00110 pObj = Abc_NtkCreatePo(pNtkNew); 00111 } 00112 // create the latches 00113 nDigits = Extra_Base10Log( nLatches ); 00114 for ( i = 0; i < nLatches; i++ ) 00115 { 00116 pObj = Abc_NtkCreateLatch(pNtkNew); 00117 Abc_LatchSetInit0( pObj ); 00118 pNode0 = Abc_NtkCreateBi(pNtkNew); 00119 pNode1 = Abc_NtkCreateBo(pNtkNew); 00120 Abc_ObjAddFanin( pObj, pNode0 ); 00121 Abc_ObjAddFanin( pNode1, pObj ); 00122 Vec_PtrPush( vNodes, pNode1 ); 00123 // assign names to latch and its input 00124 // Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); 00125 // printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); 00126 } 00127 00128 // remember the beginning of latch/PO literals 00129 pDrivers = pCur; 00130 00131 // scroll to the beginning of the binary data 00132 for ( i = 0; i < nLatches + nOutputs; ) 00133 if ( *pCur++ == '\n' ) 00134 i++; 00135 00136 // create the AND gates 00137 pProgress = Extra_ProgressBarStart( stdout, nAnds ); 00138 for ( i = 0; i < nAnds; i++ ) 00139 { 00140 Extra_ProgressBarUpdate( pProgress, i, NULL ); 00141 uLit = ((i + 1 + nInputs + nLatches) << 1); 00142 uLit1 = uLit - Io_ReadAigerDecode( &pCur ); 00143 uLit0 = uLit1 - Io_ReadAigerDecode( &pCur ); 00144 // assert( uLit1 > uLit0 ); 00145 pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); 00146 pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); 00147 assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches ); 00148 Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) ); 00149 } 00150 Extra_ProgressBarStop( pProgress ); 00151 00152 // remember the place where symbols begin 00153 pSymbols = pCur; 00154 00155 // read the latch driver literals 00156 pCur = pDrivers; 00157 Abc_NtkForEachLatchInput( pNtkNew, pObj, i ) 00158 { 00159 uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); 00160 pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); 00161 Abc_ObjAddFanin( pObj, pNode0 ); 00162 00163 // printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id ); 00164 00165 } 00166 // read the PO driver literals 00167 Abc_NtkForEachPo( pNtkNew, pObj, i ) 00168 { 00169 uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); 00170 pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); 00171 Abc_ObjAddFanin( pObj, pNode0 ); 00172 } 00173 00174 // read the names if present 00175 pCur = pSymbols; 00176 if ( *pCur != 'c' ) 00177 { 00178 int Counter = 0; 00179 while ( pCur < pContents + nFileSize && *pCur != 'c' ) 00180 { 00181 // get the terminal type 00182 pType = pCur; 00183 if ( *pCur == 'i' ) 00184 vTerms = pNtkNew->vPis; 00185 else if ( *pCur == 'l' ) 00186 vTerms = pNtkNew->vBoxes; 00187 else if ( *pCur == 'o' ) 00188 vTerms = pNtkNew->vPos; 00189 else 00190 { 00191 fprintf( stdout, "Wrong terminal type.\n" ); 00192 return NULL; 00193 } 00194 // get the terminal number 00195 iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); 00196 // get the node 00197 if ( iTerm >= Vec_PtrSize(vTerms) ) 00198 { 00199 fprintf( stdout, "The number of terminal is out of bound.\n" ); 00200 return NULL; 00201 } 00202 pObj = Vec_PtrEntry( vTerms, iTerm ); 00203 if ( *pType == 'l' ) 00204 pObj = Abc_ObjFanout0(pObj); 00205 // assign the name 00206 pName = pCur; while ( *pCur++ != '\n' ); 00207 // assign this name 00208 *(pCur-1) = 0; 00209 Abc_ObjAssignName( pObj, pName, NULL ); 00210 if ( *pType == 'l' ) 00211 { 00212 Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" ); 00213 Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" ); 00214 } 00215 // mark the node as named 00216 pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); 00217 } 00218 00219 // assign the remaining names 00220 Abc_NtkForEachPi( pNtkNew, pObj, i ) 00221 { 00222 if ( pObj->pCopy ) continue; 00223 Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); 00224 Counter++; 00225 } 00226 Abc_NtkForEachLatchOutput( pNtkNew, pObj, i ) 00227 { 00228 if ( pObj->pCopy ) continue; 00229 Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); 00230 Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" ); 00231 Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" ); 00232 Counter++; 00233 } 00234 Abc_NtkForEachPo( pNtkNew, pObj, i ) 00235 { 00236 if ( pObj->pCopy ) continue; 00237 Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); 00238 Counter++; 00239 } 00240 if ( Counter ) 00241 printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter ); 00242 } 00243 else 00244 { 00245 // printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" ); 00246 Abc_NtkShortNames( pNtkNew ); 00247 } 00248 00249 // read the name of the model if given 00250 if ( *pCur == 'c' ) 00251 { 00252 if ( !strncmp( pCur + 2, ".model", 6 ) ) 00253 { 00254 char * pTemp; 00255 for ( pTemp = pCur + 9; *pTemp && *pTemp != '\n'; pTemp++ ); 00256 *pTemp = 0; 00257 free( pNtkNew->pName ); 00258 pNtkNew->pName = Extra_UtilStrsav( pCur + 9 ); 00259 } 00260 } 00261 00262 00263 // skipping the comments 00264 free( pContents ); 00265 Vec_PtrFree( vNodes ); 00266 00267 // remove the extra nodes 00268 Abc_AigCleanup( pNtkNew->pManFunc ); 00269 00270 // check the result 00271 if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) ) 00272 { 00273 printf( "Io_ReadAiger: The network check has failed.\n" ); 00274 Abc_NtkDelete( pNtkNew ); 00275 return NULL; 00276 } 00277 return pNtkNew; 00278 }
| unsigned Io_ReadAigerDecode | ( | char ** | ppPos | ) |
CFile****************************************************************
FileName [ioReadAiger.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
- ioReadAiger.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 293 of file ioReadAiger.c.
