ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
ioReadAiger.c File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/bzlib/bzlib.h"
#include "misc/zlib/zlib.h"
#include "ioAbc.h"
Include dependency graph for ioReadAiger.c:

Go to the source code of this file.

Classes

struct  buflist
 

Typedefs

typedef struct buflist buflist
 

Functions

Vec_Int_t * Io_WriteDecodeLiterals (char **ppPos, int nEntries)
 
Abc_Ntk_t * Io_ReadAiger (char *pFileName, int fCheck)
 FUNCTION DECLARATIONS ///.
 

Typedef Documentation

◆ buflist

typedef struct buflist buflist

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

Synopsis [Reads the file into a character buffer.]

Description []

SideEffects []

SeeAlso []

Function Documentation

◆ Io_ReadAiger()

Abc_Ntk_t * Io_ReadAiger ( char * pFileName,
int fCheck )

FUNCTION DECLARATIONS ///.

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file ioReadAiger.c.

235{
236 ProgressBar * pProgress;
237 FILE * pFile;
238 Vec_Ptr_t * vNodes, * vTerms;
239 Vec_Int_t * vLits = NULL;
240 Abc_Obj_t * pObj, * pNode0, * pNode1;
241 Abc_Ntk_t * pNtkNew;
242 int nTotal, nInputs, nOutputs, nLatches, nAnds;
243 int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
244 int nFileSize = -1, iTerm, nDigits, i;
245 char * pContents, * pDrivers = NULL, * pSymbols, * pCur, * pName, * pType;
246 unsigned uLit0, uLit1, uLit;
247 int RetValue;
248
249 // read the file into the buffer
250 if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
251 pContents = Ioa_ReadLoadFileBz2Aig( pFileName, &nFileSize );
252 else if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
253 pContents = Ioa_ReadLoadFileGzAig( pFileName, &nFileSize );
254 else
255 {
256// pContents = Ioa_ReadLoadFile( pFileName );
257 nFileSize = Extra_FileSize( pFileName );
258 pFile = fopen( pFileName, "rb" );
259 pContents = ABC_ALLOC( char, nFileSize );
260 RetValue = fread( pContents, nFileSize, 1, pFile );
261 fclose( pFile );
262 }
263
264
265 // check if the input file format is correct
266 if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
267 {
268 fprintf( stdout, "Wrong input file format.\n" );
269 ABC_FREE( pContents );
270 return NULL;
271 }
272
273 // read the parameters (M I L O A + B C J F)
274 pCur = pContents; while ( *pCur != ' ' ) pCur++; pCur++;
275 // read the number of objects
276 nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
277 // read the number of inputs
278 nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
279 // read the number of latches
280 nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
281 // read the number of outputs
282 nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
283 // read the number of nodes
284 nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
285 if ( *pCur == ' ' )
286 {
287// assert( nOutputs == 0 );
288 // read the number of properties
289 pCur++;
290 nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
291 nOutputs += nBad;
292 }
293 if ( *pCur == ' ' )
294 {
295 // read the number of properties
296 pCur++;
297 nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
298 nOutputs += nConstr;
299 }
300 if ( *pCur == ' ' )
301 {
302 // read the number of properties
303 pCur++;
304 nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
305 nOutputs += nJust;
306 }
307 if ( *pCur == ' ' )
308 {
309 // read the number of properties
310 pCur++;
311 nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
312 nOutputs += nFair;
313 }
314 if ( *pCur != '\n' )
315 {
316 fprintf( stdout, "The parameter line is in a wrong format.\n" );
317 ABC_FREE( pContents );
318 return NULL;
319 }
320 pCur++;
321
322 // check the parameters
323 if ( nTotal != nInputs + nLatches + nAnds )
324 {
325 fprintf( stdout, "The number of objects does not match.\n" );
326 ABC_FREE( pContents );
327 return NULL;
328 }
329 if ( nJust || nFair )
330 {
331 fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
332 ABC_FREE( pContents );
333 return NULL;
334 }
335
336 if ( nConstr )
337 {
338 if ( nConstr == 1 )
339 fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
340 else
341 fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
342 }
343
344 // allocate the empty AIG
345 pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
346 pName = Extra_FileNameGeneric( pFileName );
347 pNtkNew->pName = Extra_UtilStrsav( pName );
348 pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
349 ABC_FREE( pName );
350 pNtkNew->nConstrs = nConstr;
351
352 // prepare the array of nodes
353 vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
354 Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );
355
356 // create the PIs
357 for ( i = 0; i < nInputs; i++ )
358 {
359 pObj = Abc_NtkCreatePi(pNtkNew);
360 Vec_PtrPush( vNodes, pObj );
361 }
362 // create the POs
363 for ( i = 0; i < nOutputs; i++ )
364 {
365 pObj = Abc_NtkCreatePo(pNtkNew);
366 }
367 // create the latches
368 nDigits = Abc_Base10Log( nLatches );
369 for ( i = 0; i < nLatches; i++ )
370 {
371 pObj = Abc_NtkCreateLatch(pNtkNew);
372 Abc_LatchSetInit0( pObj );
373 pNode0 = Abc_NtkCreateBi(pNtkNew);
374 pNode1 = Abc_NtkCreateBo(pNtkNew);
375 Abc_ObjAddFanin( pObj, pNode0 );
376 Abc_ObjAddFanin( pNode1, pObj );
377 Vec_PtrPush( vNodes, pNode1 );
378 // assign names to latch and its input
379// Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
380// printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
381 }
382
383
384 if ( pContents[3] == ' ' ) // standard AIGER
385 {
386 // remember the beginning of latch/PO literals
387 pDrivers = pCur;
388 // scroll to the beginning of the binary data
389 for ( i = 0; i < nLatches + nOutputs; )
390 if ( *pCur++ == '\n' )
391 i++;
392 }
393 else // modified AIGER
394 {
395 vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
396 }
397
398 // create the AND gates
399 pProgress = Extra_ProgressBarStart( stdout, nAnds );
400 for ( i = 0; i < nAnds; i++ )
401 {
402 Extra_ProgressBarUpdate( pProgress, i, NULL );
403 uLit = ((i + 1 + nInputs + nLatches) << 1);
404 uLit1 = uLit - Io_ReadAigerDecode( &pCur );
405 uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
406// assert( uLit1 > uLit0 );
407 pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
408 pNode1 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
409 assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
410 Vec_PtrPush( vNodes, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pNode0, pNode1) );
411 }
412 Extra_ProgressBarStop( pProgress );
413
414 // remember the place where symbols begin
415 pSymbols = pCur;
416
417 // read the latch driver literals
418 pCur = pDrivers;
419 if ( pContents[3] == ' ' ) // standard AIGER
420 {
421 Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
422 {
423 uLit0 = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
424 if ( *pCur == ' ' ) // read initial value
425 {
426 int Init;
427 pCur++;
428 Init = atoi( pCur );
429 if ( Init == 0 )
430 Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) );
431 else if ( Init == 1 )
432 Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
433 else
434 {
435 assert( Init == Abc_Var2Lit(1+Abc_NtkPiNum(pNtkNew)+i, 0) );
436 // uninitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf
437 Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) );
438 }
439 while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
440 }
441 if ( *pCur != '\n' )
442 {
443 fprintf( stdout, "The initial value of latch number %d is not recognized.\n", i );
444 return NULL;
445 }
446 pCur++;
447
448 pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
449 Abc_ObjAddFanin( pObj, pNode0 );
450 }
451 // read the PO driver literals
452 Abc_NtkForEachPo( pNtkNew, pObj, i )
453 {
454 uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
455 pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
456 Abc_ObjAddFanin( pObj, pNode0 );
457 }
458 }
459 else
460 {
461 // read the latch driver literals
462 Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
463 {
464 uLit0 = Vec_IntEntry( vLits, i );
465 pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
466 Abc_ObjAddFanin( pObj, pNode0 );
467 }
468 // read the PO driver literals
469 Abc_NtkForEachPo( pNtkNew, pObj, i )
470 {
471 uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
472 pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
473 Abc_ObjAddFanin( pObj, pNode0 );
474 }
475 Vec_IntFree( vLits );
476 }
477
478 // read the names if present
479 pCur = pSymbols;
480 if ( pCur < pContents + nFileSize && *pCur != 'c' )
481 {
482 int Counter = 0;
483 int fNodeNames = 0;
484 while ( pCur < pContents + nFileSize && *pCur != 'c' )
485 {
486 // get the terminal type
487 pType = pCur;
488 if ( *pCur == 'i' )
489 vTerms = pNtkNew->vPis;
490 else if ( *pCur == 'l' )
491 vTerms = pNtkNew->vBoxes;
492 else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
493 vTerms = pNtkNew->vPos;
494 else if ( *pCur == 'n' )
495 {
496 fNodeNames++;
497 while ( *pCur++ != '\n' );
498 continue;
499 }
500 else
501 {
502// fprintf( stdout, "Wrong terminal type.\n" );
503 return NULL;
504 }
505 // get the terminal number
506 iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
507 // get the node
508 if ( iTerm >= Vec_PtrSize(vTerms) )
509 {
510 fprintf( stdout, "The number of terminal is out of bound.\n" );
511 return NULL;
512 }
513 pObj = (Abc_Obj_t *)Vec_PtrEntry( vTerms, iTerm );
514 if ( *pType == 'l' )
515 pObj = Abc_ObjFanout0(pObj);
516 // assign the name
517 pName = pCur; while ( *pCur++ != '\n' );
518 // assign this name
519 *(pCur-1) = 0;
520 Abc_ObjAssignName( pObj, pName, NULL );
521 if ( *pType == 'l' )
522 {
523 Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
524 Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
525 }
526 // mark the node as named
527 pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
528 }
529
530 // assign the remaining names
531 Abc_NtkForEachPi( pNtkNew, pObj, i )
532 {
533 if ( pObj->pCopy ) continue;
534 Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
535 Counter++;
536 }
537 Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
538 {
539 if ( pObj->pCopy ) continue;
540 Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
541 Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
542 Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
543 Counter++;
544 }
545 Abc_NtkForEachPo( pNtkNew, pObj, i )
546 {
547 if ( pObj->pCopy ) continue;
548 Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
549 Counter++;
550 }
551// if ( Counter )
552// printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
553 if ( fNodeNames )
554 printf( "Io_ReadAiger(): The names of internal nodes are not supported. Ignoring %d node names.\n", fNodeNames );
555 }
556 else
557 {
558// printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
559 Abc_NtkShortNames( pNtkNew );
560 }
561
562 // read the name of the model if given
563 pCur = pSymbols;
564 if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
565 {
566 pCur++;
567 if ( *pCur == 'n' )
568 {
569 pCur++;
570 // read model name
571 if ( strlen(pCur) > 0 )
572 {
573 ABC_FREE( pNtkNew->pName );
574 pNtkNew->pName = Extra_UtilStrsav( pCur );
575 }
576 }
577 }
578
579 // skipping the comments
580 ABC_FREE( pContents );
581 Vec_PtrFree( vNodes );
582
583 // remove the extra nodes
584 Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
585
586 // update polarity of the additional outputs
587 if ( nBad || nConstr || nJust || nFair )
588 Abc_NtkInvertConstraints( pNtkNew );
589
590 // check the result
591 if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
592 {
593 printf( "Io_ReadAiger: The network check has failed.\n" );
594 Abc_NtkDelete( pNtkNew );
595 return NULL;
596 }
597 return pNtkNew;
598}
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkAlloc
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition abcNtk.c:53
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:84
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition abc.h:520
Abc_NtkCheckRead
ABC_DLL int Abc_NtkCheckRead(Abc_Ntk_t *pNtk)
Definition abcCheck.c:80
Abc_Aig_t
struct Abc_Aig_t_ Abc_Aig_t
Definition abc.h:117
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition abcNames.c:69
ABC_NTK_STRASH
@ ABC_NTK_STRASH
Definition abc.h:58
Abc_NtkForEachLatchOutput
#define Abc_NtkForEachLatchOutput(pNtk, pObj, i)
Definition abc.h:506
Abc_NtkInvertConstraints
ABC_DLL void Abc_NtkInvertConstraints(Abc_Ntk_t *pNtk)
Definition abcUtil.c:2244
Abc_AigCleanup
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition abcAig.c:194
Abc_AigAnd
ABC_DLL Abc_Obj_t * Abc_AigAnd(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition abcAig.c:700
Abc_NtkForEachLatchInput
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
Definition abc.h:503
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition abc.h:516
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition abcNtk.c:1421
ABC_FUNC_AIG
@ ABC_FUNC_AIG
Definition abc.h:67
Abc_NtkShortNames
ABC_DLL void Abc_NtkShortNames(Abc_Ntk_t *pNtk)
Definition abcNames.c:619
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition abcAig.c:683
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ProgressBar
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
Extra_FileSize
int Extra_FileSize(char *pFileName)
Definition extraUtilFile.c:327
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition extraUtilUtil.c:179
Extra_FileNameGeneric
char * Extra_FileNameGeneric(char *FileName)
Definition extraUtilFile.c:172
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Io_WriteDecodeLiterals
Vec_Int_t * Io_WriteDecodeLiterals(char **ppPos, int nEntries)
Definition ioReadAiger.c:79
Abc_Ntk_t_::pName
char * pName
Definition abc.h:158
Abc_Ntk_t_::nConstrs
int nConstrs
Definition abc.h:173
Abc_Ntk_t_::vPos
Vec_Ptr_t * vPos
Definition abc.h:164
Abc_Ntk_t_::vBoxes
Vec_Ptr_t * vBoxes
Definition abc.h:168
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition abc.h:191
Abc_Ntk_t_::pSpec
char * pSpec
Definition abc.h:159
Abc_Ntk_t_::vPis
Vec_Ptr_t * vPis
Definition abc.h:163
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition abc.h:148
assert
#define assert(ex)
Definition util_old.h:213
strncmp
int strncmp()
strlen
int strlen()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Io_WriteDecodeLiterals()

Vec_Int_t * Io_WriteDecodeLiterals ( char ** ppPos,
int nEntries )

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

Synopsis [Decodes the encoded array of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file ioReadAiger.c.

80{
81 Vec_Int_t * vLits;
82 int Lit, LitPrev, Diff, i;
83 vLits = Vec_IntAlloc( nEntries );
84 LitPrev = Io_ReadAigerDecode( ppPos );
85 Vec_IntPush( vLits, LitPrev );
86 for ( i = 1; i < nEntries; i++ )
87 {
88// Diff = Lit - LitPrev;
89// Diff = (Lit < LitPrev)? -Diff : Diff;
90// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
91 Diff = Io_ReadAigerDecode( ppPos );
92 Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
93 Lit = Diff + LitPrev;
94 Vec_IntPush( vLits, Lit );
95 LitPrev = Lit;
96 }
97 return vLits;
98}
Here is the caller graph for this function: