abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
ioa.h File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_HEADER_START
Aig_Man_t * 		Ioa_ReadAigerFromMemory (char *pContents, int nFileSize, int fCheck)
 INCLUDES ///. More...
 
Aig_Man_t * Ioa_ReadAiger (char *pFileName, int fCheck)
 
Vec_Str_t * Ioa_WriteAigerIntoMemoryStr (Aig_Man_t *pMan)
 
char * Ioa_WriteAigerIntoMemory (Aig_Man_t *pMan, int *pnSize)
 
void Ioa_WriteAiger (Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
 
int Ioa_FileSize (char *pFileName)
 DECLARATIONS ///. More...
 
char * Ioa_FileNameGeneric (char *FileName)
 
char * Ioa_FileNameGenericAppend (char *pBase, char *pSuffix)
 
char * Ioa_TimeStamp ()
 

Function Documentation

char* Ioa_FileNameGeneric ( char *  FileName)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file ioaUtil.c.

74 {
75  char * pDot, * pRes;
76  pRes = Abc_UtilStrsav( FileName );
77  if ( (pDot = strrchr( pRes, '.' )) )
78  *pDot = 0;
79  return pRes;
80 }
strrchr
char * strrchr()
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
char* Ioa_FileNameGenericAppend ( char *  pBase,
char *  pSuffix 
)

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

Synopsis [Returns the composite name of the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file ioaUtil.c.

94 {
95  static char Buffer[1000];
96  char * pDot;
97  if ( pBase == NULL )
98  {
99  strcpy( Buffer, pSuffix );
100  return Buffer;
101  }
102  strcpy( Buffer, pBase );
103  if ( (pDot = strrchr( Buffer, '.' )) )
104  *pDot = 0;
105  strcat( Buffer, pSuffix );
106  // find the last occurrance of slash
107  for ( pDot = Buffer + strlen(Buffer) - 1; pDot >= Buffer; pDot-- )
108  if (!((*pDot >= '0' && *pDot <= '9') ||
109  (*pDot >= 'a' && *pDot <= 'z') ||
110  (*pDot >= 'A' && *pDot <= 'Z') ||
111  *pDot == '_' || *pDot == '.') )
112  break;
113  return pDot + 1;
114 }
strcpy
char * strcpy()
strcat
char * strcat()
strlen
int strlen()
strrchr
char * strrchr()
int Ioa_FileSize ( char *  pFileName)

DECLARATIONS ///.

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

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

Synopsis [Returns the file size.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 46 of file ioaUtil.c.

47 {
48  FILE * pFile;
49  int nFileSize;
50  pFile = fopen( pFileName, "r" );
51  if ( pFile == NULL )
52  {
53  printf( "Ioa_FileSize(): The file is unavailable (absent or open).\n" );
54  return 0;
55  }
56  fseek( pFile, 0, SEEK_END );
57  nFileSize = ftell( pFile );
58  fclose( pFile );
59  return nFileSize;
60 }
SEEK_END
#define SEEK_END
Definition: zconf.h:392
Aig_Man_t* Ioa_ReadAiger ( char *  pFileName,
int  fCheck 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file ioaReadAig.c.

432 {
433  FILE * pFile;
434  Aig_Man_t * pNew;
435  char * pName, * pContents;
436  int nFileSize, RetValue;
437 
438  // read the file into the buffer
439  nFileSize = Ioa_FileSize( pFileName );
440  pFile = fopen( pFileName, "rb" );
441  pContents = ABC_ALLOC( char, nFileSize );
442  RetValue = fread( pContents, nFileSize, 1, pFile );
443  fclose( pFile );
444 
445  pNew = Ioa_ReadAigerFromMemory( pContents, nFileSize, fCheck );
446  ABC_FREE( pContents );
447  if ( pNew )
448  {
449  pName = Ioa_FileNameGeneric( pFileName );
450  ABC_FREE( pNew->pName );
451  pNew->pName = Abc_UtilStrsav( pName );
452  pNew->pSpec = Abc_UtilStrsav( pFileName );
453  ABC_FREE( pName );
454  }
455  return pNew;
456 }
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Ioa_ReadAigerFromMemory
Aig_Man_t * Ioa_ReadAigerFromMemory(char *pContents, int nFileSize, int fCheck)
INCLUDES ///.
Definition: ioaReadAig.c:105
Ioa_FileSize
int Ioa_FileSize(char *pFileName)
DECLARATIONS ///.
Definition: ioaUtil.c:46
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ioa_FileNameGeneric
char * Ioa_FileNameGeneric(char *FileName)
Definition: ioaUtil.c:73
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
ABC_NAMESPACE_HEADER_START Aig_Man_t* Ioa_ReadAigerFromMemory ( char *  pContents,
int  nFileSize,
int  fCheck 
)

INCLUDES ///.

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

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

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

Synopsis [Reads the AIG in from the memory buffer.]

Description [The buffer constains the AIG in AIGER format. The size gives the number of bytes in the buffer. The buffer is allocated by the user and not deallocated by this procedure.]

SideEffects []

SeeAlso []

Definition at line 105 of file ioaReadAig.c.

106 {
107  Vec_Int_t * vLits = NULL;
108  Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
109  Aig_Obj_t * pObj, * pNode0, * pNode1;
110  Aig_Man_t * pNew;
111  int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
112  int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
113  char * pDrivers, * pSymbols, * pCur;//, * pType;
114  unsigned uLit0, uLit1, uLit;
115 
116  // check if the input file format is correct
117  if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
118  {
119  fprintf( stdout, "Wrong input file format.\n" );
120  return NULL;
121  }
122 
123  // read the parameters (M I L O A + B C J F)
124  pCur = pContents; while ( *pCur != ' ' ) pCur++; pCur++;
125  // read the number of objects
126  nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
127  // read the number of inputs
128  nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
129  // read the number of latches
130  nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
131  // read the number of outputs
132  nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
133  // read the number of nodes
134  nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
135  if ( *pCur == ' ' )
136  {
137  assert( nOutputs == 0 );
138  // read the number of properties
139  pCur++;
140  nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
141  nOutputs += nBad;
142  }
143  if ( *pCur == ' ' )
144  {
145  // read the number of properties
146  pCur++;
147  nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
148  nOutputs += nConstr;
149  }
150  if ( *pCur == ' ' )
151  {
152  // read the number of properties
153  pCur++;
154  nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
155  nOutputs += nJust;
156  }
157  if ( *pCur == ' ' )
158  {
159  // read the number of properties
160  pCur++;
161  nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
162  nOutputs += nFair;
163  }
164  if ( *pCur != '\n' )
165  {
166  fprintf( stdout, "The parameter line is in a wrong format.\n" );
167  return NULL;
168  }
169  pCur++;
170 
171  // check the parameters
172  if ( nTotal != nInputs + nLatches + nAnds )
173  {
174  fprintf( stdout, "The number of objects does not match.\n" );
175  return NULL;
176  }
177  if ( nJust || nFair )
178  {
179  fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
180  return NULL;
181  }
182 
183  if ( nConstr )
184  {
185  if ( nConstr == 1 )
186  fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
187  else
188  fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
189  }
190 
191  // allocate the empty AIG
192  pNew = Aig_ManStart( nAnds );
193  pNew->nConstrs = nConstr;
194 
195  // prepare the array of nodes
196  vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
197  Vec_PtrPush( vNodes, Aig_ManConst0(pNew) );
198 
199  // create the PIs
200  for ( i = 0; i < nInputs + nLatches; i++ )
201  {
202  pObj = Aig_ObjCreateCi(pNew);
203  Vec_PtrPush( vNodes, pObj );
204  }
205 /*
206  // create the POs
207  for ( i = 0; i < nOutputs + nLatches; i++ )
208  {
209  pObj = Aig_ObjCreateCo(pNew);
210  }
211 */
212  // create the latches
213  pNew->nRegs = nLatches;
214 /*
215  nDigits = Ioa_Base10Log( nLatches );
216  for ( i = 0; i < nLatches; i++ )
217  {
218  pObj = Aig_ObjCreateLatch(pNew);
219  Aig_LatchSetInit0( pObj );
220  pNode0 = Aig_ObjCreateBi(pNew);
221  pNode1 = Aig_ObjCreateBo(pNew);
222  Aig_ObjAddFanin( pObj, pNode0 );
223  Aig_ObjAddFanin( pNode1, pObj );
224  Vec_PtrPush( vNodes, pNode1 );
225  // assign names to latch and its input
226 // Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
227 // printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id );
228  }
229 */
230 
231  // remember the beginning of latch/PO literals
232  pDrivers = pCur;
233  if ( pContents[3] == ' ' ) // standard AIGER
234  {
235  // scroll to the beginning of the binary data
236  for ( i = 0; i < nLatches + nOutputs; )
237  if ( *pCur++ == '\n' )
238  i++;
239  }
240  else // modified AIGER
241  {
242  vLits = Ioa_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
243  }
244 
245  // create the AND gates
246 // pProgress = Bar_ProgressStart( stdout, nAnds );
247  for ( i = 0; i < nAnds; i++ )
248  {
249 // Bar_ProgressUpdate( pProgress, i, NULL );
250  uLit = ((i + 1 + nInputs + nLatches) << 1);
251  uLit1 = uLit - Ioa_ReadAigerDecode( &pCur );
252  uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
253 // assert( uLit1 > uLit0 );
254  pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
255  pNode1 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
256  assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
257  Vec_PtrPush( vNodes, Aig_And(pNew, pNode0, pNode1) );
258  }
259 // Bar_ProgressStop( pProgress );
260 
261  // remember the place where symbols begin
262  pSymbols = pCur;
263 
264  // read the latch driver literals
265  vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
266  if ( pContents[3] == ' ' ) // standard AIGER
267  {
268  pCur = pDrivers;
269  for ( i = 0; i < nLatches; i++ )
270  {
271  uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
272  pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
273  Vec_PtrPush( vDrivers, pNode0 );
274  }
275  // read the PO driver literals
276  for ( i = 0; i < nOutputs; i++ )
277  {
278  uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
279  pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
280  Vec_PtrPush( vDrivers, pNode0 );
281  }
282 
283  }
284  else
285  {
286  // read the latch driver literals
287  for ( i = 0; i < nLatches; i++ )
288  {
289  uLit0 = Vec_IntEntry( vLits, i );
290  pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
291  Vec_PtrPush( vDrivers, pNode0 );
292  }
293  // read the PO driver literals
294  for ( i = 0; i < nOutputs; i++ )
295  {
296  uLit0 = Vec_IntEntry( vLits, i+nLatches );
297  pNode0 = Aig_NotCond( (Aig_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
298  Vec_PtrPush( vDrivers, pNode0 );
299  }
300  Vec_IntFree( vLits );
301  }
302 
303  // create the POs
304  for ( i = 0; i < nOutputs; i++ )
305  Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vDrivers, nLatches + i) );
306  for ( i = 0; i < nLatches; i++ )
307  Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vDrivers, i) );
308  Vec_PtrFree( vDrivers );
309 
310 /*
311  // read the names if present
312  pCur = pSymbols;
313  if ( *pCur != 'c' )
314  {
315  int Counter = 0;
316  while ( pCur < pContents + nFileSize && *pCur != 'c' )
317  {
318  // get the terminal type
319  pType = pCur;
320  if ( *pCur == 'i' )
321  vTerms = pNew->vPis;
322  else if ( *pCur == 'l' )
323  vTerms = pNew->vBoxes;
324  else if ( *pCur == 'o' )
325  vTerms = pNew->vPos;
326  else
327  {
328  fprintf( stdout, "Wrong terminal type.\n" );
329  return NULL;
330  }
331  // get the terminal number
332  iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
333  // get the node
334  if ( iTerm >= Vec_PtrSize(vTerms) )
335  {
336  fprintf( stdout, "The number of terminal is out of bound.\n" );
337  return NULL;
338  }
339  pObj = Vec_PtrEntry( vTerms, iTerm );
340  if ( *pType == 'l' )
341  pObj = Aig_ObjFanout0(pObj);
342  // assign the name
343  pName = pCur; while ( *pCur++ != '\n' );
344  // assign this name
345  *(pCur-1) = 0;
346  Aig_ObjAssignName( pObj, pName, NULL );
347  if ( *pType == 'l' )
348  {
349  Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
350  Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
351  }
352  // mark the node as named
353  pObj->pCopy = (Aig_Obj_t *)Aig_ObjName(pObj);
354  }
355 
356  // assign the remaining names
357  Aig_ManForEachCi( pNew, pObj, i )
358  {
359  if ( pObj->pCopy ) continue;
360  Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
361  Counter++;
362  }
363  Aig_ManForEachLatchOutput( pNew, pObj, i )
364  {
365  if ( pObj->pCopy ) continue;
366  Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
367  Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
368  Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
369  Counter++;
370  }
371  Aig_ManForEachCo( pNew, pObj, i )
372  {
373  if ( pObj->pCopy ) continue;
374  Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
375  Counter++;
376  }
377  if ( Counter )
378  printf( "Ioa_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
379  }
380  else
381  {
382 // printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
383  Aig_ManShortNames( pNew );
384  }
385 */
386  pCur = pSymbols;
387  if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
388  {
389  pCur++;
390  if ( *pCur == 'n' )
391  {
392  pCur++;
393  // read model name
394  ABC_FREE( pNew->pName );
395  pNew->pName = Abc_UtilStrsav( pCur );
396  }
397  }
398 
399  // skipping the comments
400  Vec_PtrFree( vNodes );
401 
402  // remove the extra nodes
403  Aig_ManCleanup( pNew );
404  Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
405 
406  // update polarity of the additional outputs
407  if ( nBad || nConstr || nJust || nFair )
408  Aig_ManInvertConstraints( pNew );
409 
410  // check the result
411  if ( fCheck && !Aig_ManCheck( pNew ) )
412  {
413  printf( "Ioa_ReadAiger: The network check has failed.\n" );
414  Aig_ManStop( pNew );
415  return NULL;
416  }
417  return pNew;
418 }
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_ManCheck
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ioa_ReadAigerDecode
ABC_NAMESPACE_IMPL_START unsigned Ioa_ReadAigerDecode(char **ppPos)
DECLARATIONS ///.
Definition: ioaReadAig.c:47
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_Obj_t_
Definition: aig.h:69
Ioa_WriteDecodeLiterals
Vec_Int_t * Ioa_WriteDecodeLiterals(char **ppPos, int nEntries)
Definition: ioaReadAig.c:70
Aig_ManInvertConstraints
void Aig_ManInvertConstraints(Aig_Man_t *pAig)
Definition: aigUtil.c:1543
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
strncmp
int strncmp()
assert
#define assert(ex)
Definition: util_old.h:213
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
nTotal
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
char* Ioa_TimeStamp ( )

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

Synopsis [Returns the time stamp.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 127 of file ioaUtil.c.

128 {
129  static char Buffer[100];
130  char * TimeStamp;
131  time_t ltime;
132  // get the current time
133  time( &ltime );
134  TimeStamp = asctime( localtime( &ltime ) );
135  TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
136  strcpy( Buffer, TimeStamp );
137  return Buffer;
138 }
strcpy
char * strcpy()
strlen
int strlen()
void Ioa_WriteAiger ( Aig_Man_t *  pMan,
char *  pFileName,
int  fWriteSymbols,
int  fCompact 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file ioaWriteAig.c.

447 {
448 // Bar_Progress_t * pProgress;
449  FILE * pFile;
450  Aig_Obj_t * pObj, * pDriver;
451  int i, nNodes, nBufferSize, Pos;
452  unsigned char * pBuffer;
453  unsigned uLit0, uLit1, uLit;
454 
455  if ( Aig_ManCoNum(pMan) == 0 )
456  {
457  printf( "AIG cannot be written because it has no POs.\n" );
458  return;
459  }
460 
461 // assert( Aig_ManIsStrash(pMan) );
462  // start the output stream
463  pFile = fopen( pFileName, "wb" );
464  if ( pFile == NULL )
465  {
466  fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
467  return;
468  }
469 /*
470  Aig_ManForEachLatch( pMan, pObj, i )
471  if ( !Aig_LatchIsInit0(pObj) )
472  {
473  fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
474  return;
475  }
476 */
477  // set the node numbers to be used in the output file
478  nNodes = 0;
479  Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
480  Aig_ManForEachCi( pMan, pObj, i )
481  Ioa_ObjSetAigerNum( pObj, nNodes++ );
482  Aig_ManForEachNode( pMan, pObj, i )
483  Ioa_ObjSetAigerNum( pObj, nNodes++ );
484 
485  // write the header "M I L O A" where M = I + L + A
486  fprintf( pFile, "aig%s %u %u %u %u %u",
487  fCompact? "2" : "",
488  Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan),
489  Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
490  Aig_ManRegNum(pMan),
491  Aig_ManConstrNum(pMan) ? 0 : Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
492  Aig_ManNodeNum(pMan) );
493  // write the extended header "B C J F"
494  if ( Aig_ManConstrNum(pMan) )
495  fprintf( pFile, " %u %u", Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
496  fprintf( pFile, "\n" );
497 
498  // if the driver node is a constant, we need to complement the literal below
499  // because, in the AIGER format, literal 0/1 is represented as number 0/1
500  // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
501 
502  Aig_ManInvertConstraints( pMan );
503  if ( !fCompact )
504  {
505  // write latch drivers
506  Aig_ManForEachLiSeq( pMan, pObj, i )
507  {
508  pDriver = Aig_ObjFanin0(pObj);
509  fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
510  }
511 
512  // write PO drivers
513  Aig_ManForEachPoSeq( pMan, pObj, i )
514  {
515  pDriver = Aig_ObjFanin0(pObj);
516  fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
517  }
518  }
519  else
520  {
521  Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan );
522  Vec_Str_t * vBinary = Ioa_WriteEncodeLiterals( vLits );
523  fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
524  Vec_StrFree( vBinary );
525  Vec_IntFree( vLits );
526  }
527  Aig_ManInvertConstraints( pMan );
528 
529  // write the nodes into the buffer
530  Pos = 0;
531  nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
532  pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
533 // pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
534  Aig_ManForEachNode( pMan, pObj, i )
535  {
536 // Bar_ProgressUpdate( pProgress, i, NULL );
537  uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
538  uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
539  uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
540  assert( uLit0 != uLit1 );
541  if ( uLit0 > uLit1 )
542  {
543  int Temp = uLit0;
544  uLit0 = uLit1;
545  uLit1 = Temp;
546  }
547  Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
548  Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
549  if ( Pos > nBufferSize - 10 )
550  {
551  printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
552  fclose( pFile );
553  return;
554  }
555  }
556  assert( Pos < nBufferSize );
557 // Bar_ProgressStop( pProgress );
558 
559  // write the buffer
560  fwrite( pBuffer, 1, Pos, pFile );
561  ABC_FREE( pBuffer );
562 /*
563  // write the symbol table
564  if ( fWriteSymbols )
565  {
566  int bads;
567  // write PIs
568  Aig_ManForEachPiSeq( pMan, pObj, i )
569  fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
570  // write latches
571  Aig_ManForEachLoSeq( pMan, pObj, i )
572  fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
573  // write POs
574  bads = Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan);
575  Aig_ManForEachPoSeq( pMan, pObj, i )
576  if ( !Aig_ManConstrNum(pMan) )
577  fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
578  else if ( i < bads )
579  fprintf( pFile, "b%d %s\n", i, Aig_ObjName(pObj) );
580  else
581  fprintf( pFile, "c%d %s\n", i - bads, Aig_ObjName(pObj) );
582  }
583 */
584  // write the comment
585  fprintf( pFile, "c" );
586  if ( pMan->pName )
587  fprintf( pFile, "n%s%c", pMan->pName, '\0' );
588  fprintf( pFile, "\nThis file was produced by the IOA package in ABC on %s\n", Ioa_TimeStamp() );
589  fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
590  fclose( pFile );
591 }
Aig_ManConstrNum
static int Aig_ManConstrNum(Aig_Man_t *p)
Definition: aig.h:261
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Pos
ush Pos
Definition: deflate.h:88
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ioa_WriteAigerLiterals
Vec_Int_t * Ioa_WriteAigerLiterals(Aig_Man_t *pMan)
Definition: ioaWriteAig.c:207
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Ioa_WriteAigerEncode
int Ioa_WriteAigerEncode(unsigned char *pBuffer, int Pos, unsigned x)
FUNCTION DEFINITIONS ///.
Definition: ioaWriteAig.c:151
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Ioa_ObjMakeLit
static ABC_NAMESPACE_IMPL_START int Ioa_ObjMakeLit(int Var, int fCompl)
DECLARATIONS ///.
Definition: ioaWriteAig.c:131
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Ioa_TimeStamp
char * Ioa_TimeStamp()
Definition: ioaUtil.c:127
Ioa_ObjAigerNum
static int Ioa_ObjAigerNum(Aig_Obj_t *pObj)
Definition: ioaWriteAig.c:132
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if
if(last==0)
Definition: sparse_int.h:34
Aig_Obj_t_
Definition: aig.h:69
Aig_ManInvertConstraints
void Aig_ManInvertConstraints(Aig_Man_t *pAig)
Definition: aigUtil.c:1543
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Ioa_ObjSetAigerNum
static void Ioa_ObjSetAigerNum(Aig_Obj_t *pObj, unsigned Num)
Definition: ioaWriteAig.c:133
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_Str_t_
Definition: bblif.c:47
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Ioa_WriteEncodeLiterals
Vec_Str_t * Ioa_WriteEncodeLiterals(Vec_Int_t *vLits)
Definition: ioaWriteAig.c:237
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
char* Ioa_WriteAigerIntoMemory ( Aig_Man_t *  pMan,
int *  pnSize 
)

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

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The returned size (pnSize) gives the number of bytes in the buffer. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 376 of file ioaWriteAig.c.

377 {
378  char * pBuffer;
379  Vec_Str_t * vBuffer;
380  vBuffer = Ioa_WriteAigerIntoMemoryStr( pMan );
381  if ( pMan->pName )
382  {
383  Vec_StrPrintStr( vBuffer, "n" );
384  Vec_StrPrintStr( vBuffer, pMan->pName );
385  Vec_StrPush( vBuffer, 0 );
386  }
387  // prepare the return values
388  *pnSize = Vec_StrSize( vBuffer );
389  pBuffer = Vec_StrReleaseArray( vBuffer );
390  Vec_StrFree( vBuffer );
391  return pBuffer;
392 }
Ioa_WriteAigerIntoMemoryStr
Vec_Str_t * Ioa_WriteAigerIntoMemoryStr(Aig_Man_t *pMan)
Definition: ioaWriteAig.c:286
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Vec_StrReleaseArray
static char * Vec_StrReleaseArray(Vec_Str_t *p)
Definition: vecStr.h:252
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Vec_Str_t_
Definition: bblif.c:47
Vec_StrPrintStr
static void Vec_StrPrintStr(Vec_Str_t *p, const char *pStr)
Definition: vecStr.h:627
Vec_Str_t* Ioa_WriteAigerIntoMemoryStr ( Aig_Man_t *  pMan)

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

Synopsis [Writes the AIG in into the memory buffer.]

Description [The resulting buffer constains the AIG in AIGER format. The returned size (pnSize) gives the number of bytes in the buffer. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 286 of file ioaWriteAig.c.

287 {
288  Vec_Str_t * vBuffer;
289  Aig_Obj_t * pObj, * pDriver;
290  int nNodes, i, uLit, uLit0, uLit1;
291  // set the node numbers to be used in the output file
292  nNodes = 0;
293  Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
294  Aig_ManForEachCi( pMan, pObj, i )
295  Ioa_ObjSetAigerNum( pObj, nNodes++ );
296  Aig_ManForEachNode( pMan, pObj, i )
297  Ioa_ObjSetAigerNum( pObj, nNodes++ );
298 
299  // write the header "M I L O A" where M = I + L + A
300 /*
301  fprintf( pFile, "aig%s %u %u %u %u %u\n",
302  fCompact? "2" : "",
303  Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan),
304  Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan),
305  Aig_ManRegNum(pMan),
306  Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan),
307  Aig_ManNodeNum(pMan) );
308 */
309  vBuffer = Vec_StrAlloc( 3*Aig_ManObjNum(pMan) );
310  Vec_StrPrintStr( vBuffer, "aig " );
311  Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) + Aig_ManNodeNum(pMan) );
312  Vec_StrPrintStr( vBuffer, " " );
313  Vec_StrPrintNum( vBuffer, Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
314  Vec_StrPrintStr( vBuffer, " " );
315  Vec_StrPrintNum( vBuffer, Aig_ManRegNum(pMan) );
316  Vec_StrPrintStr( vBuffer, " " );
317  Vec_StrPrintNum( vBuffer, Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
318  Vec_StrPrintStr( vBuffer, " " );
319  Vec_StrPrintNum( vBuffer, Aig_ManNodeNum(pMan) );
320  Vec_StrPrintStr( vBuffer, "\n" );
321 
322  // write latch drivers
323  Aig_ManForEachLiSeq( pMan, pObj, i )
324  {
325  pDriver = Aig_ObjFanin0(pObj);
326  uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) );
327 // fprintf( pFile, "%u\n", uLit );
328  Vec_StrPrintNum( vBuffer, uLit );
329  Vec_StrPrintStr( vBuffer, "\n" );
330  }
331 
332  // write PO drivers
333  Aig_ManForEachPoSeq( pMan, pObj, i )
334  {
335  pDriver = Aig_ObjFanin0(pObj);
336  uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) );
337 // fprintf( pFile, "%u\n", uLit );
338  Vec_StrPrintNum( vBuffer, uLit );
339  Vec_StrPrintStr( vBuffer, "\n" );
340  }
341  // write the nodes into the buffer
342  Aig_ManForEachNode( pMan, pObj, i )
343  {
344  uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
345  uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
346  uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
347  assert( uLit0 != uLit1 );
348  if ( uLit0 > uLit1 )
349  {
350  int Temp = uLit0;
351  uLit0 = uLit1;
352  uLit1 = Temp;
353  }
354 // Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
355 // Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
356  Ioa_WriteAigerEncodeStr( vBuffer, uLit - uLit1 );
357  Ioa_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
358  }
359  Vec_StrPrintStr( vBuffer, "c" );
360  return vBuffer;
361 }
Aig_ManObjNum
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Vec_StrPrintNum
static void Vec_StrPrintNum(Vec_Str_t *p, int Num)
Definition: vecStr.h:575
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Ioa_ObjMakeLit
static ABC_NAMESPACE_IMPL_START int Ioa_ObjMakeLit(int Var, int fCompl)
DECLARATIONS ///.
Definition: ioaWriteAig.c:131
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Ioa_ObjAigerNum
static int Ioa_ObjAigerNum(Aig_Obj_t *pObj)
Definition: ioaWriteAig.c:132
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Ioa_WriteAigerEncodeStr
void Ioa_WriteAigerEncodeStr(Vec_Str_t *vStr, unsigned x)
Definition: ioaWriteAig.c:179
Aig_Obj_t_
Definition: aig.h:69
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Ioa_ObjSetAigerNum
static void Ioa_ObjSetAigerNum(Aig_Obj_t *pObj, unsigned Num)
Definition: ioaWriteAig.c:133
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_Str_t_
Definition: bblif.c:47
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
Vec_StrPrintStr
static void Vec_StrPrintStr(Vec_Str_t *p, const char *pStr)
Definition: vecStr.h:627
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444