ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
saigIoa.c
Go to the documentation of this file.
1
20
21#include <math.h>
22#include "saig.h"
23
25
26
30
34
46char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
47{
48 static char Buffer[1000];
49 if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
50 sprintf( Buffer, "n%0*d", (unsigned char)Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
51 else if ( Saig_ObjIsPi(p, pObj) )
52 sprintf( Buffer, "pi%0*d", (unsigned char)Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) );
53 else if ( Saig_ObjIsPo(p, pObj) )
54 sprintf( Buffer, "po%0*d", (unsigned char)Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) );
55 else if ( Saig_ObjIsLo(p, pObj) )
56 sprintf( Buffer, "lo%0*d", (unsigned char)Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) );
57 else if ( Saig_ObjIsLi(p, pObj) )
58 sprintf( Buffer, "li%0*d", (unsigned char)Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) );
59 else
60 assert( 0 );
61 return Buffer;
62}
63
75void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
76{
77 FILE * pFile;
78 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
79 int i;
80 if ( Aig_ManCoNum(p) == 0 )
81 {
82 printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
83 return;
84 }
86 // write input file
87 pFile = fopen( pFileName, "w" );
88 if ( pFile == NULL )
89 {
90 printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
91 return;
92 }
93 fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
94 fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
95 fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n",
96 Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p),
97 Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
98 fprintf( pFile, ".model %s\n", p->pName );
99 // write primary inputs
100 fprintf( pFile, ".inputs" );
101 Aig_ManForEachPiSeq( p, pObj, i )
102 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
103 fprintf( pFile, "\n" );
104 // write primary outputs
105 fprintf( pFile, ".outputs" );
106 Aig_ManForEachPoSeq( p, pObj, i )
107 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
108 fprintf( pFile, "\n" );
109 // write registers
110 if ( Aig_ManRegNum(p) )
111 {
112 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
113 {
114 fprintf( pFile, ".latch" );
115 fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
116 fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
117 fprintf( pFile, " 0\n" );
118 }
119 }
120 // check if constant is used
121 if ( Aig_ObjRefs(Aig_ManConst1(p)) )
122 fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
123 // write the nodes in the DFS order
124 Aig_ManForEachNode( p, pObj, i )
125 {
126 fprintf( pFile, ".names" );
127 fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
128 fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
129 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
130 fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
131 }
132 // write the POs
133 Aig_ManForEachCo( p, pObj, i )
134 {
135 fprintf( pFile, ".names" );
136 fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
137 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
138 fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
139 }
140 fprintf( pFile, ".end\n" );
141 fclose( pFile );
142}
143
155char * Saig_ManReadToken( FILE * pFile )
156{
157 static char Buffer[1000];
158 if ( fscanf( pFile, "%s", Buffer ) == 1 )
159 return Buffer;
160 return NULL;
161}
162
174int Saig_ManReadNumber( Aig_Man_t * p, char * pToken )
175{
176 if ( pToken[0] == 'n' )
177 return atoi( pToken + 1 );
178 if ( pToken[0] == 'p' )
179 return atoi( pToken + 2 );
180 if ( pToken[0] == 'l' )
181 return atoi( pToken + 2 );
182 assert( 0 );
183 return -1;
184}
185
197Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken )
198{
199 int Num;
200 if ( pToken[0] == 'n' )
201 {
202 Num = atoi( pToken + 1 );
203 return Aig_ManObj( p, pNum2Id[Num] );
204 }
205 if ( pToken[0] == 'p' )
206 {
207 pToken++;
208 if ( pToken[0] == 'i' )
209 {
210 Num = atoi( pToken + 1 );
211 return Aig_ManCi( p, Num );
212 }
213 if ( pToken[0] == 'o' )
214 return NULL;
215 assert( 0 );
216 return NULL;
217 }
218 if ( pToken[0] == 'l' )
219 {
220 pToken++;
221 if ( pToken[0] == 'o' )
222 {
223 Num = atoi( pToken + 1 );
224 return Saig_ManLo( p, Num );
225 }
226 if ( pToken[0] == 'i' )
227 return NULL;
228 assert( 0 );
229 return NULL;
230 }
231 assert( 0 );
232 return NULL;
233}
234
246Aig_Man_t * Saig_ManReadBlif( char * pFileName )
247{
248 FILE * pFile;
249 Aig_Man_t * p;
250 Aig_Obj_t * pFanin0, * pFanin1, * pNode;
251 char * pToken;
252 int i, nPis, nPos, nRegs, Number;
253 int * pNum2Id = NULL; // mapping of node numbers in the file into AIG node IDs
254 // open the file
255 pFile = fopen( pFileName, "r" );
256 if ( pFile == NULL )
257 {
258 printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
259 return NULL;
260 }
261 // skip through the comments
262 for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
263 if ( pToken == NULL )
264 { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
265 // get he model
266 pToken = Saig_ManReadToken( pFile );
267 if ( pToken == NULL )
268 { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
269 // start the package
270 p = Aig_ManStart( 10000 );
271 p->pName = Abc_UtilStrsav( pToken );
272 p->pSpec = Abc_UtilStrsav( pFileName );
273 // count PIs
274 pToken = Saig_ManReadToken( pFile );
275 if ( pToken == NULL || strcmp( pToken, ".inputs" ) )
276 { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
277 for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
278 // count POs
279 if ( pToken == NULL || strcmp( pToken, ".outputs" ) )
280 { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
281 for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
282 // count latches
283 if ( pToken == NULL )
284 { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
285 for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
286 {
287 pToken = Saig_ManReadToken( pFile );
288 if ( pToken == NULL )
289 { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
290 pToken = Saig_ManReadToken( pFile );
291 if ( pToken == NULL )
292 { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
293 pToken = Saig_ManReadToken( pFile );
294 if ( pToken == NULL )
295 { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
296 pToken = Saig_ManReadToken( pFile );
297 if ( pToken == NULL )
298 { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
299 }
300 // create PIs and LOs
301 for ( i = 0; i < nPis + nRegs; i++ )
303 Aig_ManSetRegNum( p, nRegs );
304 // create nodes
305 for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
306 {
307 // first token
308 pToken = Saig_ManReadToken( pFile );
309 if ( i == 0 && pToken[0] == 'n' )
310 { // constant node
311 // read 1
312 pToken = Saig_ManReadToken( pFile );
313 if ( pToken == NULL || strcmp( pToken, "1" ) )
314 { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
315 // read next
316 pToken = Saig_ManReadToken( pFile );
317 if ( pToken == NULL )
318 { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
319 continue;
320 }
321 pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );
322
323 // second token
324 pToken = Saig_ManReadToken( pFile );
325 if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
326 { // buffer
327 // read complemented attribute
328 pToken = Saig_ManReadToken( pFile );
329 if ( pToken == NULL )
330 { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
331 if ( pToken[0] == '0' )
332 pFanin0 = Aig_Not(pFanin0);
333 // read 1
334 pToken = Saig_ManReadToken( pFile );
335 if ( pToken == NULL || strcmp( pToken, "1" ) )
336 { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
337 Aig_ObjCreateCo( p, pFanin0 );
338 // read next
339 pToken = Saig_ManReadToken( pFile );
340 if ( pToken == NULL )
341 { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
342 continue;
343 }
344
345 // third token
346 // regular node
347 pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
348 pToken = Saig_ManReadToken( pFile );
349 Number = Saig_ManReadNumber( p, pToken );
350 // allocate mapping
351 if ( pNum2Id == NULL )
352 {
353// extern double pow( double x, double y );
354 int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
355 pNum2Id = ABC_CALLOC( int, Size );
356 }
357
358 // other tokens
359 // get the complemented attributes
360 pToken = Saig_ManReadToken( pFile );
361 if ( pToken == NULL )
362 { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
363 if ( pToken[0] == '0' )
364 pFanin0 = Aig_Not(pFanin0);
365 if ( pToken[1] == '0' )
366 pFanin1 = Aig_Not(pFanin1);
367 // read 1
368 pToken = Saig_ManReadToken( pFile );
369 if ( pToken == NULL || strcmp( pToken, "1" ) )
370 { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
371 // read next
372 pToken = Saig_ManReadToken( pFile );
373 if ( pToken == NULL )
374 { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }
375
376 // create new node
377 pNode = Aig_And( p, pFanin0, pFanin1 );
378 if ( Aig_IsComplement(pNode) )
379 { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
380 // set mapping
381 pNum2Id[ Number ] = pNode->Id;
382 }
383 if ( pToken == NULL || strcmp( pToken, ".end" ) )
384 { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
385 if ( nPos + nRegs != Aig_ManCoNum(p) )
386 { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
387 // add non-node objects to the mapping
388 Aig_ManForEachCi( p, pNode, i )
389 pNum2Id[pNode->Id] = pNode->Id;
390// ABC_FREE( pNum2Id );
391 p->pData = pNum2Id;
392 // check the new manager
393 Aig_ManSetRegNum( p, nRegs );
394 if ( !Aig_ManCheck(p) )
395 printf( "Saig_ManReadBlif(): Check has failed.\n" );
396 return p;
397}
398
402
403
405
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition aigUtil.c:978
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition aig.h:438
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition aig.h:444
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition aig.h:450
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition aigCheck.c:45
Cube * p
Definition exorList.c:222
int Saig_ManReadNumber(Aig_Man_t *p, char *pToken)
Definition saigIoa.c:174
Aig_Obj_t * Saig_ManReadNode(Aig_Man_t *p, int *pNum2Id, char *pToken)
Definition saigIoa.c:197
char * Saig_ManReadToken(FILE *pFile)
Definition saigIoa.c:155
ABC_NAMESPACE_IMPL_START char * Saig_ObjName(Aig_Man_t *p, Aig_Obj_t *pObj)
DECLARATIONS ///.
Definition saigIoa.c:46
Aig_Man_t * Saig_ManReadBlif(char *pFileName)
Definition saigIoa.c:246
void Saig_ManDumpBlif(Aig_Man_t *p, char *pFileName)
Definition saigIoa.c:75
int Id
Definition aig.h:85
#define assert(ex)
Definition util_old.h:213
int strlen()
int strcmp()
char * sprintf()