ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
giaAiger.c File Reference
#include "gia.h"
#include "misc/tim/tim.h"
#include "base/main/main.h"
Include dependency graph for giaAiger.c:

Go to the source code of this file.

Macros

#define XAIG_VERBOSE   0
 

Functions

void Gia_FileFixName (char *pFileName)
 DECLARATIONS ///.
 
char * Gia_FileNameGeneric (char *FileName)
 
int Gia_FileSize (char *pFileName)
 FUNCTION DECLARATIONS ///.
 
void Gia_FileWriteBufferSize (FILE *pFile, int nSize)
 
Vec_Int_t * Gia_AigerCollectLiterals (Gia_Man_t *p)
 
Vec_Int_t * Gia_AigerReadLiterals (unsigned char **ppPos, int nEntries)
 
Vec_Str_t * Gia_AigerWriteLiterals (Vec_Int_t *vLits)
 
Gia_Man_t * Gia_AigerReadFromMemory (char *pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck)
 
Gia_Man_t * Gia_AigerRead (char *pFileName, int fGiaSimple, int fSkipStrash, int fCheck)
 
Vec_Str_t * Gia_AigerWriteIntoMemoryStr (Gia_Man_t *p)
 
Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart (Gia_Man_t *p, Vec_Int_t *vCis, Vec_Int_t *vAnds, Vec_Int_t *vCos, int nRegs)
 
void Gia_AigerWriteS (Gia_Man_t *pInit, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine, int fSkipComment)
 
void Gia_AigerWrite (Gia_Man_t *pInit, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
 
void Gia_DumpAiger (Gia_Man_t *p, char *pFilePrefix, int iFileNum, int nFileNumDigits)
 
void Gia_AigerWriteSimple (Gia_Man_t *pInit, char *pFileName)
 
int * Aiger_Read (char *pFileName, int *pnObjs, int *pnIns, int *pnLats, int *pnOuts, int *pnAnds)
 
void Aiger_Write (char *pFileName, int *pObjs, int nObjs, int nIns, int nLats, int nOuts, int nAnds)
 
void Aiger_Test (char *pFileNameIn, char *pFileNameOut)
 

Macro Definition Documentation

◆ XAIG_VERBOSE

#define XAIG_VERBOSE   0

CFile****************************************************************

FileName [giaAiger.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Procedures to read/write 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 - June 20, 2005.]

Revision [

Id
giaAiger.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 28 of file giaAiger.c.

Function Documentation

◆ Aiger_Read()

int * Aiger_Read ( char * pFileName,
int * pnObjs,
int * pnIns,
int * pnLats,
int * pnOuts,
int * pnAnds )

Definition at line 1685 of file giaAiger.c.

1686{
1687 int i, Temp, Value = 0, nTotal, nObjs, nIns, nLats, nOuts, nAnds, * pObjs;
1688 FILE * pFile = fopen( pFileName, "rb" );
1689 if ( pFile == NULL )
1690 {
1691 fprintf( stdout, "Aiger_Read(): Cannot open the output file \"%s\".\n", pFileName );
1692 return NULL;
1693 }
1694 if ( fgetc(pFile) != 'a' || fgetc(pFile) != 'i' || fgetc(pFile) != 'g' )
1695 {
1696 fprintf( stdout, "Aiger_Read(): Can only read binary AIGER.\n" );
1697 fclose( pFile );
1698 return NULL;
1699 }
1700 if ( fscanf(pFile, "%d %d %d %d %d", &nTotal, &nIns, &nLats, &nOuts, &nAnds) != 5 )
1701 {
1702 fprintf( stdout, "Aiger_Read(): Cannot read the header line.\n" );
1703 fclose( pFile );
1704 return NULL;
1705 }
1706 if ( nTotal != nIns + nLats + nAnds )
1707 {
1708 fprintf( stdout, "The number of objects does not match.\n" );
1709 fclose( pFile );
1710 return NULL;
1711 }
1712 nObjs = 1 + nIns + 2*nLats + nOuts + nAnds;
1713 pObjs = ABC_CALLOC( int, nObjs * 2 );
1714 // read flop input literals
1715 for ( i = 0; i < nLats; i++ )
1716 {
1717 while ( fgetc(pFile) != '\n' );
1718 Value += fscanf( pFile, "%d", &Temp );
1719 pObjs[2*(nObjs-nLats+i)+0] = Temp;
1720 pObjs[2*(nObjs-nLats+i)+1] = Temp;
1721 }
1722 // read output literals
1723 for ( i = 0; i < nOuts; i++ )
1724 {
1725 while ( fgetc(pFile) != '\n' );
1726 Value += fscanf( pFile, "%d", &Temp );
1727 pObjs[2*(nObjs-nOuts-nLats+i)+0] = Temp;
1728 pObjs[2*(nObjs-nOuts-nLats+i)+1] = Temp;
1729 }
1730 assert( Value == nLats + nOuts );
1731 // read the binary part
1732 while ( fgetc(pFile) != '\n' );
1733 for ( i = 0; i < nAnds; i++ )
1734 {
1735 int uLit = 2*(1 + nIns + nLats + i);
1736 int uLit1 = uLit - Aiger_ReadUnsigned( pFile );
1737 int uLit0 = uLit1 - Aiger_ReadUnsigned( pFile );
1738 pObjs[2*(1+nIns+nLats+i)+0] = uLit0;
1739 pObjs[2*(1+nIns+nLats+i)+1] = uLit1;
1740 }
1741 fclose( pFile );
1742 if ( pnObjs ) *pnObjs = nObjs;
1743 if ( pnIns ) *pnIns = nIns;
1744 if ( pnLats ) *pnLats = nLats;
1745 if ( pnOuts ) *pnOuts = nOuts;
1746 if ( pnAnds ) *pnAnds = nAnds;
1747 return pObjs;
1748}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Aiger_Test()

void Aiger_Test ( char * pFileNameIn,
char * pFileNameOut )

Definition at line 1773 of file giaAiger.c.

1774{
1775 int nObjs, nIns, nLats, nOuts, nAnds, * pObjs = Aiger_Read( pFileNameIn, &nObjs, &nIns, &nLats, &nOuts, &nAnds );
1776 if ( pObjs == NULL )
1777 return;
1778 printf( "Read input file \"%s\".\n", pFileNameIn );
1779 Aiger_Write( pFileNameOut, pObjs, nObjs, nIns, nLats, nOuts, nAnds );
1780 printf( "Written output file \"%s\".\n", pFileNameOut );
1781 ABC_FREE( pObjs );
1782}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aiger_Read
int * Aiger_Read(char *pFileName, int *pnObjs, int *pnIns, int *pnLats, int *pnOuts, int *pnAnds)
Definition giaAiger.c:1685
Aiger_Write
void Aiger_Write(char *pFileName, int *pObjs, int nObjs, int nIns, int nLats, int nOuts, int nAnds)
Definition giaAiger.c:1749
Here is the call graph for this function:

◆ Aiger_Write()

void Aiger_Write ( char * pFileName,
int * pObjs,
int nObjs,
int nIns,
int nLats,
int nOuts,
int nAnds )

Definition at line 1749 of file giaAiger.c.

1750{
1751 FILE * pFile = fopen( pFileName, "wb" ); int i;
1752 if ( pFile == NULL )
1753 {
1754 fprintf( stdout, "Aiger_Write(): Cannot open the output file \"%s\".\n", pFileName );
1755 return;
1756 }
1757 fprintf( pFile, "aig %d %d %d %d %d\n", nIns + nLats + nAnds, nIns, nLats, nOuts, nAnds );
1758 for ( i = 0; i < nLats; i++ )
1759 fprintf( pFile, "%d\n", pObjs[2*(nObjs-nLats+i)+0] );
1760 for ( i = 0; i < nOuts; i++ )
1761 fprintf( pFile, "%d\n", pObjs[2*(nObjs-nOuts-nLats+i)+0] );
1762 for ( i = 0; i < nAnds; i++ )
1763 {
1764 int uLit = 2*(1 + nIns + nLats + i);
1765 int uLit0 = pObjs[2*(1+nIns+nLats+i)+0];
1766 int uLit1 = pObjs[2*(1+nIns+nLats+i)+1];
1767 Aiger_WriteUnsigned( pFile, uLit - uLit1 );
1768 Aiger_WriteUnsigned( pFile, uLit1 - uLit0 );
1769 }
1770 fprintf( pFile, "c\n" );
1771 fclose( pFile );
1772}
Here is the caller graph for this function:

◆ Gia_AigerCollectLiterals()

Vec_Int_t * Gia_AigerCollectLiterals ( Gia_Man_t * p)

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

Synopsis [Create the array of literals to be written.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file giaAiger.c.

98{
99 Vec_Int_t * vLits;
100 Gia_Obj_t * pObj;
101 int i;
102 vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
103 Gia_ManForEachRi( p, pObj, i )
104 Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
105 Gia_ManForEachPo( p, pObj, i )
106 Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
107 return vLits;
108}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Here is the caller graph for this function:

◆ Gia_AigerRead()

Gia_Man_t * Gia_AigerRead ( char * pFileName,
int fGiaSimple,
int fSkipStrash,
int fCheck )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1017 of file giaAiger.c.

1018{
1019 FILE * pFile;
1020 Gia_Man_t * pNew;
1021 char * pName, * pContents;
1022 int nFileSize;
1023 int RetValue;
1024
1025 // read the file into the buffer
1026 Gia_FileFixName( pFileName );
1027 nFileSize = Gia_FileSize( pFileName );
1028 pFile = fopen( pFileName, "rb" );
1029 pContents = ABC_ALLOC( char, nFileSize );
1030 RetValue = fread( pContents, nFileSize, 1, pFile );
1031 fclose( pFile );
1032
1033 pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fGiaSimple, fSkipStrash, fCheck );
1034 ABC_FREE( pContents );
1035 if ( pNew )
1036 {
1037 ABC_FREE( pNew->pName );
1038 pName = Gia_FileNameGeneric( pFileName );
1039 pNew->pName = Abc_UtilStrsav( pName );
1040 ABC_FREE( pName );
1041
1042 assert( pNew->pSpec == NULL );
1043 pNew->pSpec = Abc_UtilStrsav( pFileName );
1044 }
1045 return pNew;
1046}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Gia_FileSize
int Gia_FileSize(char *pFileName)
FUNCTION DECLARATIONS ///.
Definition giaAiger.c:64
Gia_FileFixName
void Gia_FileFixName(char *pFileName)
DECLARATIONS ///.
Definition giaAiger.c:49
Gia_FileNameGeneric
char * Gia_FileNameGeneric(char *FileName)
Definition giaAiger.c:56
Gia_AigerReadFromMemory
Gia_Man_t * Gia_AigerReadFromMemory(char *pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck)
Definition giaAiger.c:176
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_AigerReadFromMemory()

Gia_Man_t * Gia_AigerReadFromMemory ( char * pContents,
int nFileSize,
int fGiaSimple,
int fSkipStrash,
int fCheck )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file giaAiger.c.

177{
178 Gia_Man_t * pNew, * pTemp;
179 Vec_Ptr_t * vNamesIn = NULL, * vNamesOut = NULL, * vNamesRegIn = NULL, * vNamesRegOut = NULL, * vNamesNode = NULL;
180 Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
181 Vec_Int_t * vNodes, * vDrivers, * vInits = NULL;
182 int iObj, iNode0, iNode1, fHieOnly = 0;
183 int nTotal, nInputs, nOutputs, nLatches, nAnds, i;
184 int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
185 unsigned char * pDrivers, * pSymbols, * pCur;
186 unsigned uLit0, uLit1, uLit;
187
188 // read the parameters (M I L O A + B C J F)
189 pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++;
190 // read the number of objects
191 nTotal = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
192 // read the number of inputs
193 nInputs = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
194 // read the number of latches
195 nLatches = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
196 // read the number of outputs
197 nOutputs = atoi( (const char *)pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
198 // read the number of nodes
199 nAnds = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
200 if ( *pCur == ' ' )
201 {
202// assert( nOutputs == 0 );
203 // read the number of properties
204 pCur++;
205 nBad = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
206 nOutputs += nBad;
207 }
208 if ( *pCur == ' ' )
209 {
210 // read the number of properties
211 pCur++;
212 nConstr = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
213 nOutputs += nConstr;
214 }
215 if ( *pCur == ' ' )
216 {
217 // read the number of properties
218 pCur++;
219 nJust = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
220 nOutputs += nJust;
221 }
222 if ( *pCur == ' ' )
223 {
224 // read the number of properties
225 pCur++;
226 nFair = atoi( (const char *)pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
227 nOutputs += nFair;
228 }
229 if ( *pCur != '\n' )
230 {
231 fprintf( stdout, "The parameter line is in a wrong format.\n" );
232 return NULL;
233 }
234 pCur++;
235
236 // check the parameters
237 if ( nTotal != nInputs + nLatches + nAnds )
238 {
239 fprintf( stdout, "The number of objects does not match.\n" );
240 return NULL;
241 }
242 if ( nJust || nFair )
243 {
244 fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
245 return NULL;
246 }
247
248 if ( nConstr )
249 {
250 if ( nConstr == 1 )
251 fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
252 else
253 fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
254 }
255
256 // allocate the empty AIG
257 pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
258 pNew->nConstrs = nConstr;
259 pNew->fGiaSimple = fGiaSimple;
260
261 // prepare the array of nodes
262 vNodes = Vec_IntAlloc( 1 + nTotal );
263 Vec_IntPush( vNodes, 0 );
264
265 // create the PIs
266 for ( i = 0; i < nInputs + nLatches; i++ )
267 {
268 iObj = Gia_ManAppendCi(pNew);
269 Vec_IntPush( vNodes, iObj );
270 }
271
272 // remember the beginning of latch/PO literals
273 pDrivers = pCur;
274 if ( pContents[3] == ' ' ) // standard AIGER
275 {
276 // scroll to the beginning of the binary data
277 for ( i = 0; i < nLatches + nOutputs; )
278 if ( *pCur++ == '\n' )
279 i++;
280 }
281 else // modified AIGER
282 {
283 vLits = Gia_AigerReadLiterals( &pCur, nLatches + nOutputs );
284 }
285
286 // create the AND gates
287 if ( !fGiaSimple && !fSkipStrash )
288 Gia_ManHashAlloc( pNew );
289 for ( i = 0; i < nAnds; i++ )
290 {
291 uLit = ((i + 1 + nInputs + nLatches) << 1);
292 uLit1 = uLit - Gia_AigerReadUnsigned( &pCur );
293 uLit0 = uLit1 - Gia_AigerReadUnsigned( &pCur );
294// assert( uLit1 > uLit0 );
295 iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
296 iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
297 assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
298 if ( !fGiaSimple && fSkipStrash )
299 {
300 if ( iNode0 == iNode1 )
301 Vec_IntPush( vNodes, Gia_ManAppendBuf(pNew, iNode0) );
302 else
303 Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
304 }
305 else
306 Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
307 }
308 if ( !fGiaSimple && !fSkipStrash )
309 Gia_ManHashStop( pNew );
310
311 // remember the place where symbols begin
312 pSymbols = pCur;
313
314 // read the latch driver literals
315 vDrivers = Vec_IntAlloc( nLatches + nOutputs );
316 if ( pContents[3] == ' ' ) // standard AIGER
317 {
318 vInits = Vec_IntAlloc( nLatches );
319 pCur = pDrivers;
320 for ( i = 0; i < nLatches; i++ )
321 {
322 uLit0 = atoi( (char *)pCur );
323 while ( *pCur != ' ' && *pCur != '\n' )
324 pCur++;
325 if ( *pCur == ' ' )
326 {
327 pCur++;
328 Vec_IntPush( vInits, atoi( (char *)pCur ) );
329 while ( *pCur++ != '\n' );
330 }
331 else
332 {
333 pCur++;
334 Vec_IntPush( vInits, 0 );
335 }
336 iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
337 Vec_IntPush( vDrivers, iNode0 );
338 }
339 // read the PO driver literals
340 for ( i = 0; i < nOutputs; i++ )
341 {
342 uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
343 iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
344 Vec_IntPush( vDrivers, iNode0 );
345 }
346
347 }
348 else
349 {
350 // read the latch driver literals
351 for ( i = 0; i < nLatches; i++ )
352 {
353 uLit0 = Vec_IntEntry( vLits, i );
354 iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
355 Vec_IntPush( vDrivers, iNode0 );
356 }
357 // read the PO driver literals
358 for ( i = 0; i < nOutputs; i++ )
359 {
360 uLit0 = Vec_IntEntry( vLits, i+nLatches );
361 iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
362 Vec_IntPush( vDrivers, iNode0 );
363 }
364 Vec_IntFree( vLits );
365 }
366
367 // create the POs
368 for ( i = 0; i < nOutputs; i++ )
369 Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
370 for ( i = 0; i < nLatches; i++ )
371 Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
372 Vec_IntFree( vDrivers );
373
374 // create the latches
375 Gia_ManSetRegNum( pNew, nLatches );
376
377 // read signal names if they are of the special type
378 pCur = pSymbols;
379 if ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
380 {
381 int fReadNames = 1;
382 if ( fReadNames )
383 {
384 int fError = 0;
385 while ( !fError && pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
386 {
387 int iTerm;
388 char * pType = (char *)pCur;
389 char * pName = NULL;
390 // check terminal type
391 if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l' && *pCur != 'n' )
392 {
393 fError = 1;
394 break;
395 }
396 // get terminal number
397 iTerm = atoi( (char *)++pCur ); while ( *pCur++ != ' ' );
398 // skip spaces
399 while ( *pCur == ' ' )
400 pCur++;
401 // skip till the end of line
402 for ( pName = (char *)pCur; *pCur && *pCur != '\n'; pCur++ );
403 if ( *pCur == '\n' )
404 *pCur = 0;
405 // save the name
406 if ( *pType == 'i' )
407 {
408 if ( vNamesIn == NULL )
409 vNamesIn = Vec_PtrStart( nInputs );
410 if ( Vec_PtrSize(vNamesIn) <= iTerm )
411 {
412 fError = 1;
413 break;
414 }
415 Vec_PtrWriteEntry( vNamesIn, iTerm, Abc_UtilStrsav(pName) );
416 }
417 else if ( *pType == 'o' )
418 {
419 if ( vNamesOut == NULL )
420 vNamesOut = Vec_PtrStart( nOutputs );
421 if ( Vec_PtrSize(vNamesOut) <= iTerm )
422 {
423 fError = 1;
424 break;
425 }
426 Vec_PtrWriteEntry( vNamesOut, iTerm, Abc_UtilStrsav(pName) );
427 }
428 else if ( *pType == 'l' )
429 {
430 char Buffer[1000];
431 assert( strlen(pName) < 995 );
432 sprintf( Buffer, "%s_in", pName );
433 if ( vNamesRegIn == NULL )
434 vNamesRegIn = Vec_PtrStart( nLatches );
435 if ( vNamesRegOut == NULL )
436 vNamesRegOut = Vec_PtrStart( nLatches );
437 if ( Vec_PtrSize(vNamesRegIn) <= iTerm )
438 {
439 fError = 1;
440 break;
441 }
442 Vec_PtrWriteEntry( vNamesRegIn, iTerm, Abc_UtilStrsav(Buffer) );
443 Vec_PtrWriteEntry( vNamesRegOut, iTerm, Abc_UtilStrsav(pName) );
444 }
445 else if ( *pType == 'n' )
446 {
447 if ( Vec_IntSize(&pNew->vHTable) != 0 )
448 {
449 printf( "Structural hashing should be disabled to read internal nodes names.\n" );
450 fError = 1;
451 break;
452 }
453 if ( vNamesNode == NULL )
454 vNamesNode = Vec_PtrStart( Gia_ManObjNum(pNew) );
455 Vec_PtrWriteEntry( vNamesNode, iTerm, Abc_UtilStrsav(pName) );
456 }
457 else
458 {
459 fError = 1;
460 break;
461 }
462 pCur++;
463 }
464 if ( fError )
465 {
466 printf( "Error occurred when reading signal names. Signal names ignored.\n" );
467 if ( vNamesIn ) Vec_PtrFreeFree( vNamesIn ), vNamesIn = NULL;
468 if ( vNamesOut ) Vec_PtrFreeFree( vNamesOut ), vNamesOut = NULL;
469 if ( vNamesRegIn ) Vec_PtrFreeFree( vNamesRegIn ), vNamesRegIn = NULL;
470 if ( vNamesRegOut ) Vec_PtrFreeFree( vNamesRegOut ), vNamesRegOut = NULL;
471 if ( vNamesNode ) Vec_PtrFreeFree( vNamesNode ), vNamesNode = NULL;
472 }
473 }
474 else
475 {
476 int fBreakUsed = 0;
477 unsigned char * pCurOld = pCur;
478 pNew->vUserPiIds = Vec_IntStartFull( nInputs );
479 pNew->vUserPoIds = Vec_IntStartFull( nOutputs );
480 pNew->vUserFfIds = Vec_IntStartFull( nLatches );
481 while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
482 {
483 int iTerm;
484 char * pType = (char *)pCur;
485 // check terminal type
486 if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l' )
487 {
488// fprintf( stdout, "Wrong terminal type.\n" );
489 fBreakUsed = 1;
490 break;
491 }
492 // get terminal number
493 iTerm = atoi( (char *)++pCur ); while ( *pCur++ != ' ' );
494 // skip spaces
495 while ( *pCur == ' ' )
496 pCur++;
497 // decode the user numbers:
498 // flops are named: @l<num>
499 // PIs are named: @i<num>
500 // POs are named: @o<num>
501 if ( *pCur++ != '@' )
502 {
503 fBreakUsed = 1;
504 break;
505 }
506 if ( *pCur == 'i' && *pType == 'i' )
507 Vec_IntWriteEntry( pNew->vUserPiIds, iTerm, atoi((char *)pCur+1) );
508 else if ( *pCur == 'o' && *pType == 'o' )
509 Vec_IntWriteEntry( pNew->vUserPoIds, iTerm, atoi((char *)pCur+1) );
510 else if ( *pCur == 'l' && *pType == 'l' )
511 Vec_IntWriteEntry( pNew->vUserFfIds, iTerm, atoi((char *)pCur+1) );
512 else
513 {
514 fprintf( stdout, "Wrong name format.\n" );
515 fBreakUsed = 1;
516 break;
517 }
518 // skip digits
519 while ( *pCur++ != '\n' );
520 }
521 // in case of abnormal termination, remove the arrays
522 if ( fBreakUsed )
523 {
524 unsigned char * pName;
525 int Entry, nInvars, nConstr, iTerm;
526
527 Vec_Int_t * vPoNames = Vec_IntStartFull( nOutputs );
528
529 Vec_IntFreeP( &pNew->vUserPiIds );
530 Vec_IntFreeP( &pNew->vUserPoIds );
531 Vec_IntFreeP( &pNew->vUserFfIds );
532
533 // try to figure out signal names
534 fBreakUsed = 0;
535 pCur = (unsigned char *)pCurOld;
536 while ( pCur < (unsigned char *)pContents + nFileSize && *pCur != 'c' )
537 {
538 // get the terminal type
539 if ( *pCur == 'i' || *pCur == 'l' )
540 {
541 // skip till the end of the line
542 while ( *pCur++ != '\n' );
543 *(pCur-1) = 0;
544 continue;
545 }
546 if ( *pCur != 'o' )
547 {
548// fprintf( stdout, "Wrong terminal type.\n" );
549 fBreakUsed = 1;
550 break;
551 }
552 // get the terminal number
553 iTerm = atoi( (char *)++pCur ); while ( *pCur++ != ' ' );
554 // get the node
555 if ( iTerm < 0 || iTerm >= nOutputs )
556 {
557 fprintf( stdout, "The output number (%d) is out of range.\n", iTerm );
558 fBreakUsed = 1;
559 break;
560 }
561 if ( Vec_IntEntry(vPoNames, iTerm) != ~0 )
562 {
563 fprintf( stdout, "The output number (%d) is listed twice.\n", iTerm );
564 fBreakUsed = 1;
565 break;
566 }
567
568 // get the name
569 pName = pCur; while ( *pCur++ != '\n' );
570 *(pCur-1) = 0;
571 // assign the name
572 Vec_IntWriteEntry( vPoNames, iTerm, pName - (unsigned char *)pContents );
573 }
574
575 // check that all names are assigned
576 if ( !fBreakUsed )
577 {
578 nInvars = nConstr = 0;
579 vPoTypes = Vec_IntStart( Gia_ManPoNum(pNew) );
580 Vec_IntForEachEntry( vPoNames, Entry, i )
581 {
582 if ( Entry == ~0 )
583 continue;
584 if ( strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
585 {
586 Vec_IntWriteEntry( vPoTypes, i, 1 );
587 nConstr++;
588 }
589 if ( strncmp( pContents+Entry, "invariant:", 10 ) == 0 )
590 {
591 Vec_IntWriteEntry( vPoTypes, i, 2 );
592 nInvars++;
593 }
594 }
595 if ( nConstr )
596 fprintf( stdout, "Recognized and added %d constraints.\n", nConstr );
597 if ( nInvars )
598 fprintf( stdout, "Recognized and skipped %d invariants.\n", nInvars );
599 if ( nConstr == 0 && nInvars == 0 )
600 Vec_IntFreeP( &vPoTypes );
601 }
602 Vec_IntFree( vPoNames );
603 }
604 }
605 }
606
607
608 // check if there are other types of information to read
609 if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
610 {
611 int fVerbose = XAIG_VERBOSE;
612 Vec_Str_t * vStr;
613 unsigned char * pCurTemp;
614 pCur++;
615 // skip new line if present
616// if ( *pCur == '\n' )
617// pCur++;
618 while ( pCur < (unsigned char *)pContents + nFileSize )
619 {
620 // read extra AIG
621 if ( *pCur == 'a' )
622 {
623 pCur++;
624 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
625 memcpy( Vec_StrArray(vStr), pCur, (size_t)Vec_StrSize(vStr) );
626 pCur += Vec_StrSize(vStr);
627 pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0, 0 );
628 Vec_StrFree( vStr );
629 if ( fVerbose ) printf( "Finished reading extension \"a\".\n" );
630 }
631 // read number of constraints
632 else if ( *pCur == 'c' )
633 {
634 pCur++;
635 assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4;
636 pNew->nConstrs = Gia_AigerReadInt( pCur ); pCur += 4;
637 if ( fVerbose ) printf( "Finished reading extension \"c\".\n" );
638 }
639 // read delay information
640 else if ( *pCur == 'd' )
641 {
642 pCur++;
643 assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4;
644 pNew->nAnd2Delay = Gia_AigerReadInt(pCur); pCur += 4;
645 if ( fVerbose ) printf( "Finished reading extension \"d\".\n" );
646 }
647 else if ( *pCur == 'i' )
648 {
649 pCur++;
650 nInputs = Gia_AigerReadInt(pCur)/4; pCur += 4;
651 pNew->vInArrs = Vec_FltStart( nInputs );
652 memcpy( Vec_FltArray(pNew->vInArrs), pCur, (size_t)4*nInputs ); pCur += 4*nInputs;
653 if ( fVerbose ) printf( "Finished reading extension \"i\".\n" );
654 }
655 else if ( *pCur == 'o' )
656 {
657 pCur++;
658 nOutputs = Gia_AigerReadInt(pCur)/4; pCur += 4;
659 pNew->vOutReqs = Vec_FltStart( nOutputs );
660 memcpy( Vec_FltArray(pNew->vOutReqs), pCur, (size_t)4*nOutputs ); pCur += 4*nOutputs;
661 if ( fVerbose ) printf( "Finished reading extension \"o\".\n" );
662 }
663 // read equivalence classes
664 else if ( *pCur == 'e' )
665 {
666 extern Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize );
667 pCur++;
668 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
669 pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
670 pNew->pNexts = Gia_ManDeriveNexts( pNew );
671 assert( pCur == pCurTemp );
672 if ( fVerbose ) printf( "Finished reading extension \"e\".\n" );
673 }
674 // read flop classes
675 else if ( *pCur == 'f' )
676 {
677 pCur++;
678 assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) ); pCur += 4;
679 pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
680 memcpy( Vec_IntArray(pNew->vFlopClasses), pCur, (size_t)4*Gia_ManRegNum(pNew) ); pCur += 4*Gia_ManRegNum(pNew);
681 if ( fVerbose ) printf( "Finished reading extension \"f\".\n" );
682 }
683 // read gate classes
684 else if ( *pCur == 'g' )
685 {
686 pCur++;
687 assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) ); pCur += 4;
688 pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) );
689 memcpy( Vec_IntArray(pNew->vGateClasses), pCur, (size_t)4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew);
690 if ( fVerbose ) printf( "Finished reading extension \"g\".\n" );
691 }
692 // read hierarchy information
693 else if ( *pCur == 'h' )
694 {
695 pCur++;
696 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
697 memcpy( Vec_StrArray(vStr), pCur, (size_t)Vec_StrSize(vStr) );
698 pCur += Vec_StrSize(vStr);
699 pNew->pManTime = Tim_ManLoad( vStr, 1 );
700 Vec_StrFree( vStr );
701 fHieOnly = 1;
702 if ( fVerbose ) printf( "Finished reading extension \"h\".\n" );
703 }
704 // read packing
705 else if ( *pCur == 'k' )
706 {
707 extern Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize );
708 int nSize;
709 pCur++;
710 nSize = Gia_AigerReadInt(pCur);
711 pCurTemp = pCur + nSize + 4; pCur += 4;
712 pNew->vPacking = Gia_AigerReadPacking( &pCur, nSize );
713 assert( pCur == pCurTemp );
714 if ( fVerbose ) printf( "Finished reading extension \"k\".\n" );
715 }
716 // read mapping
717 else if ( *pCur == 'm' )
718 {
719 extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
720 extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize );
721 extern Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs );
722 int nSize;
723 pCur++;
724 nSize = Gia_AigerReadInt(pCur);
725 pCurTemp = pCur + nSize + 4; pCur += 4;
726 pNew->vMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew) );
727 assert( pCur == pCurTemp );
728 if ( fVerbose ) printf( "Finished reading extension \"m\".\n" );
729 }
730 // read model name
731 else if ( *pCur == 'n' )
732 {
733 pCur++;
734 if ( (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z') || (*pCur >= '0' && *pCur <= '9') )
735 {
736 ABC_FREE( pNew->pName );
737 pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1;
738 }
739 else
740 {
741 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
742 ABC_FREE( pNew->pName );
743 pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1;
744 assert( pCur == pCurTemp );
745 }
746 }
747 // read placement
748 else if ( *pCur == 'p' )
749 {
750 Gia_Plc_t * pPlacement;
751 pCur++;
752 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
753 pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) );
754 memcpy( pPlacement, pCur, (size_t)4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew);
755 assert( pCur == pCurTemp );
756 pNew->pPlacement = pPlacement;
757 if ( fVerbose ) printf( "Finished reading extension \"p\".\n" );
758 }
759 // read register classes
760 else if ( *pCur == 'r' )
761 {
762 int i, nRegs;
763 pCur++;
764 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
765 nRegs = Gia_AigerReadInt(pCur); pCur += 4;
766 //nRegs = (pCurTemp - pCur)/4;
767 pNew->vRegClasses = Vec_IntAlloc( nRegs );
768 for ( i = 0; i < nRegs; i++ )
769 Vec_IntPush( pNew->vRegClasses, Gia_AigerReadInt(pCur) ), pCur += 4;
770 assert( pCur == pCurTemp );
771 if ( fVerbose ) printf( "Finished reading extension \"r\".\n" );
772 }
773 // read register inits
774 else if ( *pCur == 's' )
775 {
776 int i, nRegs;
777 pCur++;
778 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
779 nRegs = Gia_AigerReadInt(pCur); pCur += 4;
780 pNew->vRegInits = Vec_IntAlloc( nRegs );
781 for ( i = 0; i < nRegs; i++ )
782 Vec_IntPush( pNew->vRegInits, Gia_AigerReadInt(pCur) ), pCur += 4;
783 assert( pCur == pCurTemp );
784 if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
785 }
786 // read configuration data
787 else if ( *pCur == 'b' )
788 {
789 int nSize;
790 pCur++;
791 nSize = Gia_AigerReadInt(pCur);
792 pCurTemp = pCur + nSize + 4; pCur += 4;
793 pNew->pCellStr = Abc_UtilStrsav( (char*)pCur ); pCur += strlen((char*)pCur) + 1;
794 nSize = nSize - strlen(pNew->pCellStr) - 1;
795 assert( nSize % 4 == 0 );
796 pNew->vConfigs = Vec_IntAlloc(nSize / 4);
797// memcpy(Vec_IntArray(pNew->vConfigs), pCur, (size_t)nSize); pCur += nSize;
798 for ( i = 0; i < nSize / 4; i++ )
799 Vec_IntPush( pNew->vConfigs, Gia_AigerReadInt(pCur) ), pCur += 4;
800 assert( pCur == pCurTemp );
801 if ( fVerbose ) printf( "Finished reading extension \"b\".\n" );
802 }
803 // read choices
804 else if ( *pCur == 'q' )
805 {
806 int i, nPairs, iRepr, iNode;
807 assert( !Gia_ManHasChoices(pNew) );
808 pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(pNew) );
809 pCur++;
810 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
811 nPairs = Gia_AigerReadInt(pCur); pCur += 4;
812 for ( i = 0; i < nPairs; i++ )
813 {
814 iRepr = Gia_AigerReadInt(pCur); pCur += 4;
815 iNode = Gia_AigerReadInt(pCur); pCur += 4;
816 pNew->pSibls[iRepr] = iNode;
817 assert( iRepr > iNode );
818 }
819 assert( pCur == pCurTemp );
820 if ( fVerbose ) printf( "Finished reading extension \"q\".\n" );
821 }
822 // read switching activity
823 else if ( *pCur == 'u' )
824 {
825 unsigned char * pSwitching;
826 pCur++;
827 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
828 pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) );
829 memcpy( pSwitching, pCur, (size_t)Gia_ManObjNum(pNew) ); pCur += Gia_ManObjNum(pNew);
830 assert( pCur == pCurTemp );
831 if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
832 }
833 // read timing manager
834 else if ( *pCur == 't' )
835 {
836 pCur++;
837 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
838 memcpy( Vec_StrArray(vStr), pCur, (size_t)Vec_StrSize(vStr) ); pCur += Vec_StrSize(vStr);
839 pNew->pManTime = Tim_ManLoad( vStr, 0 );
840 Vec_StrFree( vStr );
841 if ( fVerbose ) printf( "Finished reading extension \"t\".\n" );
842 }
843 // read object classes
844 else if ( *pCur == 'v' )
845 {
846 pCur++;
847 pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4;
848 memcpy( Vec_IntArray(pNew->vObjClasses), pCur, (size_t)4*Vec_IntSize(pNew->vObjClasses) );
849 pCur += 4*Vec_IntSize(pNew->vObjClasses);
850 if ( fVerbose ) printf( "Finished reading extension \"v\".\n" );
851 }
852 // read edge information
853 else if ( *pCur == 'w' )
854 {
855 Vec_Int_t * vPairs;
856 int i, nPairs;
857 pCur++;
858 pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
859 nPairs = Gia_AigerReadInt(pCur); pCur += 4;
860 vPairs = Vec_IntAlloc( 2*nPairs );
861 for ( i = 0; i < 2*nPairs; i++ )
862 Vec_IntPush( vPairs, Gia_AigerReadInt(pCur) ), pCur += 4;
863 assert( pCur == pCurTemp );
864 if ( fSkipStrash )
865 {
866 Gia_ManEdgeFromArray( pNew, vPairs );
867 if ( fVerbose ) printf( "Finished reading extension \"w\".\n" );
868 }
869 else
870 printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
871 Vec_IntFree( vPairs );
872 }
873 else break;
874 }
875 }
876
877 // skipping the comments
878 Vec_IntFree( vNodes );
879
880 // update polarity of the additional outputs
881 if ( nBad || nConstr || nJust || nFair )
882 Gia_ManInvertConstraints( pNew );
883
884 // clean the PO drivers
885 if ( vPoTypes )
886 {
887 pNew = Gia_ManDupWithConstraints( pTemp = pNew, vPoTypes );
888 Gia_ManStop( pTemp );
889 Vec_IntFreeP( &vPoTypes );
890 }
891
892 if ( !fGiaSimple && !fSkipStrash && Gia_ManHasDangling(pNew) )
893 {
894 Tim_Man_t * pManTime;
895 Gia_Man_t * pAigExtra;
896 Vec_Int_t * vFlopMap, * vGateMap, * vObjMap, * vRegClasses, * vRegInits;
897 vRegClasses = pNew->vRegClasses; pNew->vRegClasses = NULL;
898 vRegInits = pNew->vRegInits; pNew->vRegInits = NULL;
899 vFlopMap = pNew->vFlopClasses; pNew->vFlopClasses = NULL;
900 vGateMap = pNew->vGateClasses; pNew->vGateClasses = NULL;
901 vObjMap = pNew->vObjClasses; pNew->vObjClasses = NULL;
902 pManTime = (Tim_Man_t *)pNew->pManTime; pNew->pManTime = NULL;
903 pAigExtra = pNew->pAigExtra; pNew->pAigExtra = NULL;
904 pNew = Gia_ManCleanup( pTemp = pNew );
905 if ( (vGateMap || vObjMap) && (Gia_ManObjNum(pNew) < Gia_ManObjNum(pTemp)) )
906 printf( "Cleanup removed objects after reading. Old gate/object abstraction maps are invalid!\n" );
907 Gia_ManStop( pTemp );
908 pNew->vRegClasses = vRegClasses;
909 pNew->vRegInits = vRegInits;
910 pNew->vFlopClasses = vFlopMap;
911 pNew->vGateClasses = vGateMap;
912 pNew->vObjClasses = vObjMap;
913 pNew->pManTime = pManTime;
914 pNew->pAigExtra = pAigExtra;
915 }
916
917 if ( fHieOnly )
918 {
919// Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
920 if ( Abc_FrameReadLibBox() == NULL )
921 printf( "Warning: Creating unit-delay box delay tables because box library is not available.\n" );
922 Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs );
923 }
924 Vec_FltFreeP( &pNew->vInArrs );
925 Vec_FltFreeP( &pNew->vOutReqs );
926/*
927 // check the result
928 if ( fCheck && !Gia_ManCheck( pNew ) )
929 {
930 printf( "Gia_AigerRead: The network check has failed.\n" );
931 Gia_ManStop( pNew );
932 return NULL;
933 }
934*/
935
936 if ( vInits && Vec_IntSum(vInits) )
937 {
938 char * pInit = ABC_ALLOC( char, Vec_IntSize(vInits) + 1 );
939 Gia_Obj_t * pObj;
940 int i;
941 assert( Vec_IntSize(vInits) == Gia_ManRegNum(pNew) );
942 Gia_ManForEachRo( pNew, pObj, i )
943 {
944 if ( Vec_IntEntry(vInits, i) == 0 )
945 pInit[i] = '0';
946 else if ( Vec_IntEntry(vInits, i) == 1 )
947 pInit[i] = '1';
948 else
949 {
950 assert( Vec_IntEntry(vInits, i) == Abc_Var2Lit(Gia_ObjId(pNew, pObj), 0) );
951 // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf
952 pInit[i] = 'X';
953 }
954 }
955 pInit[i] = 0;
956 if ( !fSkipStrash )
957 {
958 pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 );
959 pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
960 Gia_ManStop( pTemp );
961 }
962 ABC_FREE( pInit );
963 }
964 Vec_IntFreeP( &vInits );
965 if ( !fGiaSimple && !fSkipStrash && pNew->vMapping )
966 {
967 Abc_Print( 0, "Structural hashing enabled while reading AIGER invalidated the mapping. Consider using \"&r -s\".\n" );
968 Vec_IntFreeP( &pNew->vMapping );
969 }
970 if ( vNamesIn && Gia_ManPiNum(pNew) != Vec_PtrSize(vNamesIn) )
971 Abc_Print( 0, "The number of inputs does not match the number of input names.\n" );
972 else if ( vNamesOut && Gia_ManPoNum(pNew) != Vec_PtrSize(vNamesOut) )
973 Abc_Print( 0, "The number of output does not match the number of output names.\n" );
974 else if ( vNamesRegOut && Gia_ManRegNum(pNew) != Vec_PtrSize(vNamesRegOut) )
975 Abc_Print( 0, "The number of inputs does not match the number of flop names.\n" );
976 else if ( vNamesIn && vNamesOut )
977 {
978 pNew->vNamesIn = vNamesIn; vNamesIn = NULL;
979 pNew->vNamesOut = vNamesOut; vNamesOut = NULL;
980 if ( vNamesRegOut )
981 {
982 Vec_PtrAppend( pNew->vNamesIn, vNamesRegOut );
983 Vec_PtrClear( vNamesRegOut );
984 Vec_PtrFree( vNamesRegOut );
985 vNamesRegOut = NULL;
986 }
987 if ( vNamesRegIn )
988 {
989 Vec_PtrAppend( pNew->vNamesOut, vNamesRegIn );
990 Vec_PtrClear( vNamesRegIn );
991 Vec_PtrFree( vNamesRegIn );
992 vNamesRegIn = NULL;
993 }
994 }
995 if ( vNamesNode && Gia_ManObjNum(pNew) != Vec_PtrSize(vNamesNode) )
996 Abc_Print( 0, "The size of the node name array does not match the number of objects. Names are not entered.\n" );
997 else if ( vNamesNode )
998 pNew->vNamesNode = vNamesNode, vNamesNode = NULL;
999 if ( vNamesIn ) Vec_PtrFreeFree( vNamesIn );
1000 if ( vNamesOut ) Vec_PtrFreeFree( vNamesOut );
1001 if ( vNamesRegIn ) Vec_PtrFreeFree( vNamesRegIn );
1002 if ( vNamesRegOut ) Vec_PtrFreeFree( vNamesRegOut );
1003 return pNew;
1004}
Abc_FrameReadLibBox
ABC_DLL void * Abc_FrameReadLibBox()
Definition mainFrame.c:58
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Gia_AigerReadEquivClasses
ABC_NAMESPACE_IMPL_START Gia_Rpr_t * Gia_AigerReadEquivClasses(unsigned char **ppPos, int nSize)
DECLARATIONS ///.
Definition giaAigerExt.c:48
Gia_AigerReadMappingSimple
int * Gia_AigerReadMappingSimple(unsigned char **ppPos, int nSize)
Definition giaAigerExt.c:222
Gia_AigerReadMappingDoc
Vec_Int_t * Gia_AigerReadMappingDoc(unsigned char **ppPos, int nObjs)
Definition giaAigerExt.c:248
Gia_AigerReadMapping
int * Gia_AigerReadMapping(unsigned char **ppPos, int nSize)
Definition giaAigerExt.c:146
Gia_AigerReadPacking
Vec_Int_t * Gia_AigerReadPacking(unsigned char **ppPos, int nSize)
Definition giaAigerExt.c:400
XAIG_VERBOSE
#define XAIG_VERBOSE
Definition giaAiger.c:28
Gia_AigerReadLiterals
Vec_Int_t * Gia_AigerReadLiterals(unsigned char **ppPos, int nEntries)
Definition giaAiger.c:109
Gia_Rpr_t
struct Gia_Rpr_t_ Gia_Rpr_t
Definition gia.h:57
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManHasDangling
int Gia_ManHasDangling(Gia_Man_t *p)
Definition giaUtil.c:1353
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManDeriveNexts
int * Gia_ManDeriveNexts(Gia_Man_t *p)
Definition giaEquiv.c:260
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_Plc_t
struct Gia_Plc_t_ Gia_Plc_t
Definition gia.h:67
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManDupWithConstraints
Gia_Man_t * Gia_ManDupWithConstraints(Gia_Man_t *p, Vec_Int_t *vPoTypes)
Definition giaDup.c:3816
Gia_ManEdgeFromArray
void Gia_ManEdgeFromArray(Gia_Man_t *p, Vec_Int_t *vArray)
FUNCTION DEFINITIONS ///.
Definition giaEdge.c:72
Gia_ManInvertConstraints
void Gia_ManInvertConstraints(Gia_Man_t *pAig)
Definition giaUtil.c:1641
Gia_ManDupZeroUndc
Gia_Man_t * Gia_ManDupZeroUndc(Gia_Man_t *p, char *pInit, int nNewPis, int fGiaSimple, int fVerbose)
Definition giaDup.c:3569
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_Man_t_::pAigExtra
Gia_Man_t * pAigExtra
Definition gia.h:167
Gia_Man_t_::vNamesIn
Vec_Ptr_t * vNamesIn
Definition gia.h:181
Gia_Man_t_::pSibls
int * pSibls
Definition gia.h:128
Gia_Man_t_::nAnd2Delay
int nAnd2Delay
Definition gia.h:202
Gia_Man_t_::pPlacement
Gia_Plc_t * pPlacement
Definition gia.h:166
Gia_Man_t_::vOutReqs
Vec_Flt_t * vOutReqs
Definition gia.h:169
Gia_Man_t_::vInArrs
Vec_Flt_t * vInArrs
Definition gia.h:168
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition gia.h:126
Gia_Man_t_::vRegInits
Vec_Int_t * vRegInits
Definition gia.h:161
Gia_Man_t_::vUserPoIds
Vec_Int_t * vUserPoIds
Definition gia.h:185
Gia_Man_t_::vPacking
Vec_Int_t * vPacking
Definition gia.h:141
Gia_Man_t_::pNexts
int * pNexts
Definition gia.h:127
Gia_Man_t_::vHTable
Vec_Int_t vHTable
Definition gia.h:113
Gia_Man_t_::vNamesOut
Vec_Ptr_t * vNamesOut
Definition gia.h:182
Gia_Man_t_::fGiaSimple
int fGiaSimple
Definition gia.h:116
Gia_Man_t_::vMapping
Vec_Int_t * vMapping
Definition gia.h:136
Gia_Man_t_::vRegClasses
Vec_Int_t * vRegClasses
Definition gia.h:160
Gia_Man_t_::pManTime
void * pManTime
Definition gia.h:194
Gia_Man_t_::vObjClasses
Vec_Int_t * vObjClasses
Definition gia.h:158
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition gia.h:157
Gia_Man_t_::vFlopClasses
Vec_Int_t * vFlopClasses
Definition gia.h:156
Gia_Man_t_::vNamesNode
Vec_Ptr_t * vNamesNode
Definition gia.h:183
Gia_Man_t_::vUserPiIds
Vec_Int_t * vUserPiIds
Definition gia.h:184
Gia_Man_t_::pCellStr
char * pCellStr
Definition gia.h:143
Gia_Man_t_::vUserFfIds
Vec_Int_t * vUserFfIds
Definition gia.h:186
Gia_Man_t_::nConstrs
int nConstrs
Definition gia.h:122
Gia_Man_t_::vConfigs
Vec_Int_t * vConfigs
Definition gia.h:142
Tim_Man_t
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition tim.h:92
Tim_ManLoad
Tim_Man_t * Tim_ManLoad(Vec_Str_t *p, int fHieOnly)
Definition timDump.c:113
Tim_ManCreate
void Tim_ManCreate(Tim_Man_t *p, void *pLib, Vec_Flt_t *vInArrs, Vec_Flt_t *vOutReqs)
Definition timMan.c:406
strncmp
int strncmp()
memcpy
char * memcpy()
strlen
int strlen()
sprintf
char * sprintf()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
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:

◆ Gia_AigerReadLiterals()

Vec_Int_t * Gia_AigerReadLiterals ( unsigned char ** ppPos,
int nEntries )

Definition at line 109 of file giaAiger.c.

110{
111 Vec_Int_t * vLits;
112 int Lit, LitPrev, Diff, i;
113 vLits = Vec_IntAlloc( nEntries );
114 LitPrev = Gia_AigerReadUnsigned( ppPos );
115 Vec_IntPush( vLits, LitPrev );
116 for ( i = 1; i < nEntries; i++ )
117 {
118// Diff = Lit - LitPrev;
119// Diff = (Lit < LitPrev)? -Diff : Diff;
120// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
121 Diff = Gia_AigerReadUnsigned( ppPos );
122 Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
123 Lit = Diff + LitPrev;
124 Vec_IntPush( vLits, Lit );
125 LitPrev = Lit;
126 }
127 return vLits;
128}
Here is the caller graph for this function:

◆ Gia_AigerWrite()

void Gia_AigerWrite ( Gia_Man_t * pInit,
char * pFileName,
int fWriteSymbols,
int fCompact,
int fWriteNewLine )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1595 of file giaAiger.c.

1596{
1597 Gia_AigerWriteS( pInit, pFileName, fWriteSymbols, fCompact, fWriteNewLine, 0 );
1598}
Gia_AigerWriteS
void Gia_AigerWriteS(Gia_Man_t *pInit, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine, int fSkipComment)
Definition giaAiger.c:1220
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_AigerWriteIntoMemoryStr()

Vec_Str_t * Gia_AigerWriteIntoMemoryStr ( Gia_Man_t * p)

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

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

Description [The resulting buffer constains the AIG in AIGER format. The resulting buffer should be deallocated by the user.]

SideEffects []

SeeAlso []

Definition at line 1062 of file giaAiger.c.

1063{
1064 Vec_Str_t * vBuffer;
1065 Gia_Obj_t * pObj;
1066 int nNodes = 0, i, uLit, uLit0, uLit1;
1067 // set the node numbers to be used in the output file
1068 Gia_ManConst0(p)->Value = nNodes++;
1069 Gia_ManForEachCi( p, pObj, i )
1070 pObj->Value = nNodes++;
1071 Gia_ManForEachAnd( p, pObj, i )
1072 pObj->Value = nNodes++;
1073
1074 // write the header "M I L O A" where M = I + L + A
1075 vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
1076 Vec_StrPrintStr( vBuffer, "aig " );
1077 Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
1078 Vec_StrPrintStr( vBuffer, " " );
1079 Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
1080 Vec_StrPrintStr( vBuffer, " " );
1081 Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
1082 Vec_StrPrintStr( vBuffer, " " );
1083 Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
1084 Vec_StrPrintStr( vBuffer, " " );
1085 Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
1086 Vec_StrPrintStr( vBuffer, "\n" );
1087
1088 // write latch drivers
1089 Gia_ManForEachRi( p, pObj, i )
1090 {
1091 uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1092 Vec_StrPrintNum( vBuffer, uLit );
1093 Vec_StrPrintStr( vBuffer, "\n" );
1094 }
1095
1096 // write PO drivers
1097 Gia_ManForEachPo( p, pObj, i )
1098 {
1099 uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1100 Vec_StrPrintNum( vBuffer, uLit );
1101 Vec_StrPrintStr( vBuffer, "\n" );
1102 }
1103 // write the nodes into the buffer
1104 Gia_ManForEachAnd( p, pObj, i )
1105 {
1106 uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
1107 uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1108 uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
1109 assert( uLit0 != uLit1 );
1110 if ( uLit0 > uLit1 )
1111 {
1112 int Temp = uLit0;
1113 uLit0 = uLit1;
1114 uLit1 = Temp;
1115 }
1116 Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 );
1117 Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
1118 }
1119 Vec_StrPrintStr( vBuffer, "c" );
1120 return vBuffer;
1121}
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Here is the caller graph for this function:

◆ Gia_AigerWriteIntoMemoryStrPart()

Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart ( Gia_Man_t * p,
Vec_Int_t * vCis,
Vec_Int_t * vAnds,
Vec_Int_t * vCos,
int nRegs )

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

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

Description [The resulting buffer constains the AIG in AIGER format. The CI/CO/AND nodes are assumed to be ordered according to some rule. The resulting buffer should be deallocated by the user.]

SideEffects [Note that in vCos, PIs are order first, followed by latches!]

SeeAlso []

Definition at line 1136 of file giaAiger.c.

1137{
1138 Vec_Str_t * vBuffer;
1139 Gia_Obj_t * pObj;
1140 int nNodes = 0, i, uLit, uLit0, uLit1;
1141 // set the node numbers to be used in the output file
1142 Gia_ManConst0(p)->Value = nNodes++;
1143 Gia_ManForEachObjVec( vCis, p, pObj, i )
1144 {
1145 assert( Gia_ObjIsCi(pObj) );
1146 pObj->Value = nNodes++;
1147 }
1148 Gia_ManForEachObjVec( vAnds, p, pObj, i )
1149 {
1150 assert( Gia_ObjIsAnd(pObj) );
1151 pObj->Value = nNodes++;
1152 }
1153
1154 // write the header "M I L O A" where M = I + L + A
1155 vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
1156 Vec_StrPrintStr( vBuffer, "aig " );
1157 Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) );
1158 Vec_StrPrintStr( vBuffer, " " );
1159 Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs );
1160 Vec_StrPrintStr( vBuffer, " " );
1161 Vec_StrPrintNum( vBuffer, nRegs );
1162 Vec_StrPrintStr( vBuffer, " " );
1163 Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs );
1164 Vec_StrPrintStr( vBuffer, " " );
1165 Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) );
1166 Vec_StrPrintStr( vBuffer, "\n" );
1167
1168 // write latch drivers
1169 Gia_ManForEachObjVec( vCos, p, pObj, i )
1170 {
1171 assert( Gia_ObjIsCo(pObj) );
1172 if ( i < Vec_IntSize(vCos) - nRegs )
1173 continue;
1174 uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1175 Vec_StrPrintNum( vBuffer, uLit );
1176 Vec_StrPrintStr( vBuffer, "\n" );
1177 }
1178 // write output drivers
1179 Gia_ManForEachObjVec( vCos, p, pObj, i )
1180 {
1181 assert( Gia_ObjIsCo(pObj) );
1182 if ( i >= Vec_IntSize(vCos) - nRegs )
1183 continue;
1184 uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1185 Vec_StrPrintNum( vBuffer, uLit );
1186 Vec_StrPrintStr( vBuffer, "\n" );
1187 }
1188
1189 // write the nodes into the buffer
1190 Gia_ManForEachObjVec( vAnds, p, pObj, i )
1191 {
1192 uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
1193 uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
1194 uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
1195 assert( uLit0 != uLit1 );
1196 if ( uLit0 > uLit1 )
1197 {
1198 int Temp = uLit0;
1199 uLit0 = uLit1;
1200 uLit1 = Temp;
1201 }
1202 Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 );
1203 Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
1204 }
1205 Vec_StrPrintStr( vBuffer, "c" );
1206 return vBuffer;
1207}
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Here is the caller graph for this function:

◆ Gia_AigerWriteLiterals()

Vec_Str_t * Gia_AigerWriteLiterals ( Vec_Int_t * vLits)

Definition at line 129 of file giaAiger.c.

130{
131 Vec_Str_t * vBinary;
132 int Pos = 0, Lit, LitPrev, Diff, i;
133 vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
134 LitPrev = Vec_IntEntry( vLits, 0 );
135 Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev );
136 Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
137 {
138 Diff = Lit - LitPrev;
139 Diff = (Lit < LitPrev)? -Diff : Diff;
140 Diff = (Diff << 1) | (int)(Lit < LitPrev);
141 Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
142 LitPrev = Lit;
143 if ( Pos + 10 > vBinary->nCap )
144 Vec_StrGrow( vBinary, vBinary->nCap+1 );
145 }
146 vBinary->nSize = Pos;
147/*
148 // verify
149 {
150 extern Vec_Int_t * Gia_AigerReadLiterals( char ** ppPos, int nEntries );
151 char * pPos = Vec_StrArray( vBinary );
152 Vec_Int_t * vTemp = Gia_AigerReadLiterals( &pPos, Vec_IntSize(vLits) );
153 for ( i = 0; i < Vec_IntSize(vLits); i++ )
154 {
155 int Entry1 = Vec_IntEntry(vLits,i);
156 int Entry2 = Vec_IntEntry(vTemp,i);
157 assert( Entry1 == Entry2 );
158 }
159 Vec_IntFree( vTemp );
160 }
161*/
162 return vBinary;
163}
Pos
ush Pos
Definition deflate.h:88
Vec_Str_t_::nCap
int nCap
Definition bblif.c:49
Vec_Str_t_::nSize
int nSize
Definition bblif.c:50
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the caller graph for this function:

◆ Gia_AigerWriteS()

void Gia_AigerWriteS ( Gia_Man_t * pInit,
char * pFileName,
int fWriteSymbols,
int fCompact,
int fWriteNewLine,
int fSkipComment )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1220 of file giaAiger.c.

1221{
1222 int fVerbose = XAIG_VERBOSE;
1223 FILE * pFile;
1224 Gia_Man_t * p;
1225 Gia_Obj_t * pObj;
1226 Vec_Str_t * vStrExt;
1227 int i, nBufferSize, Pos;
1228 unsigned char * pBuffer;
1229 unsigned uLit0, uLit1, uLit;
1230 assert( pInit->nXors == 0 && pInit->nMuxes == 0 );
1231
1232 if ( Gia_ManCoNum(pInit) == 0 )
1233 {
1234 printf( "AIG cannot be written because it has no POs.\n" );
1235 return;
1236 }
1237
1238 // start the output stream
1239 pFile = fopen( pFileName, "wb" );
1240 if ( pFile == NULL )
1241 {
1242 fprintf( stdout, "Gia_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName );
1243 return;
1244 }
1245
1246 // create normalized AIG
1247 if ( !Gia_ManIsNormalized(pInit) )
1248 {
1249// printf( "Gia_AigerWrite(): Normalizing AIG for writing.\n" );
1250 p = Gia_ManDupNormalize( pInit, 0 );
1251 Gia_ManTransferMapping( p, pInit );
1252 Gia_ManTransferPacking( p, pInit );
1253 Gia_ManTransferTiming( p, pInit );
1254 p->nConstrs = pInit->nConstrs;
1255 }
1256 else
1257 p = pInit;
1258
1259 // write the header "M I L O A" where M = I + L + A
1260 fprintf( pFile, "aig%s %u %u %u %u %u",
1261 fCompact? "2" : "",
1262 Gia_ManCiNum(p) + Gia_ManAndNum(p),
1263 Gia_ManPiNum(p),
1264 Gia_ManRegNum(p),
1265 Gia_ManConstrNum(p) ? 0 : Gia_ManPoNum(p),
1266 Gia_ManAndNum(p) );
1267 // write the extended header "B C J F"
1268 if ( Gia_ManConstrNum(p) )
1269 fprintf( pFile, " %u %u", Gia_ManPoNum(p) - Gia_ManConstrNum(p), Gia_ManConstrNum(p) );
1270 fprintf( pFile, "\n" );
1271
1272 Gia_ManInvertConstraints( p );
1273 if ( !fCompact )
1274 {
1275 // write latch drivers
1276 Gia_ManForEachRi( p, pObj, i )
1277 fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) );
1278 // write PO drivers
1279 Gia_ManForEachPo( p, pObj, i )
1280 fprintf( pFile, "%u\n", Gia_ObjFaninLit0p(p, pObj) );
1281 }
1282 else
1283 {
1284 Vec_Int_t * vLits = Gia_AigerCollectLiterals( p );
1285 Vec_Str_t * vBinary = Gia_AigerWriteLiterals( vLits );
1286 fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
1287 Vec_StrFree( vBinary );
1288 Vec_IntFree( vLits );
1289 }
1290 Gia_ManInvertConstraints( p );
1291
1292 // write the nodes into the buffer
1293 Pos = 0;
1294 nBufferSize = 8 * Gia_ManAndNum(p) + 100; // skeptically assuming 3 chars per one AIG edge
1295 pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
1296 Gia_ManForEachAnd( p, pObj, i )
1297 {
1298 uLit = Abc_Var2Lit( i, 0 );
1299 uLit0 = Gia_ObjFaninLit0( pObj, i );
1300 uLit1 = Gia_ObjFaninLit1( pObj, i );
1301 assert( p->fGiaSimple || Gia_ManBufNum(p) || uLit0 < uLit1 );
1302 Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit - uLit1 );
1303 Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit1 - uLit0 );
1304 if ( Pos > nBufferSize - 10 )
1305 {
1306 printf( "Gia_AigerWrite(): AIGER generation has failed because the allocated buffer is too small.\n" );
1307 fclose( pFile );
1308 if ( p != pInit )
1309 Gia_ManStop( p );
1310 return;
1311 }
1312 }
1313 assert( Pos < nBufferSize );
1314
1315 // write the buffer
1316 fwrite( pBuffer, 1, Pos, pFile );
1317 ABC_FREE( pBuffer );
1318
1319 // write the symbol table
1320 if ( p->vNamesIn && p->vNamesOut )
1321 {
1322 assert( Vec_PtrSize(p->vNamesIn) == Gia_ManCiNum(p) );
1323 assert( Vec_PtrSize(p->vNamesOut) == Gia_ManCoNum(p) );
1324 // write PIs
1325 Gia_ManForEachPi( p, pObj, i )
1326 fprintf( pFile, "i%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, i) );
1327 // write latches
1328 Gia_ManForEachRo( p, pObj, i )
1329 fprintf( pFile, "l%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, Gia_ManPiNum(p) + i) );
1330 // write POs
1331 Gia_ManForEachPo( p, pObj, i )
1332 fprintf( pFile, "o%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesOut, i) );
1333 }
1334 if ( p->vNamesNode && Vec_PtrSize(p->vNamesNode) != Gia_ManObjNum(p) )
1335 Abc_Print( 0, "The size of the node name array does not match the number of objects. Names are not written.\n" );
1336 else if ( p->vNamesNode )
1337 {
1338 Gia_ManForEachAnd( p, pObj, i )
1339 if ( Vec_PtrEntry(p->vNamesNode, i) )
1340 fprintf( pFile, "n%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesNode, i) );
1341 }
1342
1343 // write the comment
1344 if ( fWriteNewLine )
1345 fprintf( pFile, "c\n" );
1346 else
1347 fprintf( pFile, "c" );
1348
1349 // write additional AIG
1350 if ( p->pAigExtra )
1351 {
1352 fprintf( pFile, "a" );
1353 vStrExt = Gia_AigerWriteIntoMemoryStr( p->pAigExtra );
1354 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1355 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1356 Vec_StrFree( vStrExt );
1357 if ( fVerbose ) printf( "Finished writing extension \"a\".\n" );
1358 }
1359 // write constraints
1360 if ( p->nConstrs )
1361 {
1362 fprintf( pFile, "c" );
1363 Gia_FileWriteBufferSize( pFile, 4 );
1364 Gia_FileWriteBufferSize( pFile, p->nConstrs );
1365 }
1366 // write timing information
1367 if ( p->nAnd2Delay )
1368 {
1369 fprintf( pFile, "d" );
1370 Gia_FileWriteBufferSize( pFile, 4 );
1371 Gia_FileWriteBufferSize( pFile, p->nAnd2Delay );
1372 }
1373 if ( p->pManTime )
1374 {
1375 float * pTimes;
1376 pTimes = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime );
1377 if ( pTimes )
1378 {
1379 fprintf( pFile, "i" );
1380 Gia_FileWriteBufferSize( pFile, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
1381 fwrite( pTimes, 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
1382 ABC_FREE( pTimes );
1383 if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
1384 }
1385 pTimes = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime );
1386 if ( pTimes )
1387 {
1388 fprintf( pFile, "o" );
1389 Gia_FileWriteBufferSize( pFile, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
1390 fwrite( pTimes, 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
1391 ABC_FREE( pTimes );
1392 if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
1393 }
1394 }
1395 // write equivalences
1396 if ( p->pReprs && p->pNexts )
1397 {
1398 extern Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p );
1399 fprintf( pFile, "e" );
1400 vStrExt = Gia_WriteEquivClasses( p );
1401 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1402 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1403 Vec_StrFree( vStrExt );
1404 }
1405 // write flop classes
1406 if ( p->vFlopClasses )
1407 {
1408 fprintf( pFile, "f" );
1409 Gia_FileWriteBufferSize( pFile, 4*Gia_ManRegNum(p) );
1410 assert( Vec_IntSize(p->vFlopClasses) == Gia_ManRegNum(p) );
1411 fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile );
1412 }
1413 // write gate classes
1414 if ( p->vGateClasses )
1415 {
1416 fprintf( pFile, "g" );
1417 Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1418 assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
1419 fwrite( Vec_IntArray(p->vGateClasses), 1, 4*Gia_ManObjNum(p), pFile );
1420 }
1421 // write hierarchy info
1422 if ( p->pManTime )
1423 {
1424 fprintf( pFile, "h" );
1425 vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 1 );
1426 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1427 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1428 Vec_StrFree( vStrExt );
1429 if ( fVerbose ) printf( "Finished writing extension \"h\".\n" );
1430 }
1431 // write packing
1432 if ( p->vPacking )
1433 {
1434 extern Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking );
1435 fprintf( pFile, "k" );
1436 vStrExt = Gia_WritePacking( p->vPacking );
1437 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1438 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1439 Vec_StrFree( vStrExt );
1440 if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
1441 }
1442 // write edges
1443 if ( p->vEdge1 )
1444 {
1445 Vec_Int_t * vPairs = Gia_ManEdgeToArray( p );
1446 int i;
1447 fprintf( pFile, "w" );
1448 Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(vPairs)+1) );
1449 Gia_FileWriteBufferSize( pFile, Vec_IntSize(vPairs)/2 );
1450 for ( i = 0; i < Vec_IntSize(vPairs); i++ )
1451 Gia_FileWriteBufferSize( pFile, Vec_IntEntry(vPairs, i) );
1452 Vec_IntFree( vPairs );
1453 }
1454 // write mapping
1455 if ( Gia_ManHasMapping(p) )
1456 {
1457 extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
1458 extern Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p );
1459 extern Vec_Str_t * Gia_AigerWriteMappingDoc( Gia_Man_t * p );
1460 fprintf( pFile, "m" );
1461 vStrExt = Gia_AigerWriteMappingDoc( p );
1462 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1463 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1464 Vec_StrFree( vStrExt );
1465 if ( fVerbose ) printf( "Finished writing extension \"m\".\n" );
1466 }
1467 // write cell mapping
1468 if ( Gia_ManHasCellMapping(p) )
1469 {
1470 extern Vec_Str_t * Gia_AigerWriteCellMappingDoc( Gia_Man_t * p );
1471 fprintf( pFile, "M" );
1472 vStrExt = Gia_AigerWriteCellMappingDoc( p );
1473 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1474 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1475 Vec_StrFree( vStrExt );
1476 if ( fVerbose ) printf( "Finished writing extension \"M\".\n" );
1477
1478 }
1479 // write placement
1480 if ( p->pPlacement )
1481 {
1482 fprintf( pFile, "p" );
1483 Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1484 fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile );
1485 }
1486 // write register classes
1487 if ( p->vRegClasses )
1488 {
1489 int i;
1490 fprintf( pFile, "r" );
1491 Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(p->vRegClasses)+1) );
1492 Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegClasses) );
1493 for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
1494 Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
1495 }
1496 // write register inits
1497 if ( p->vRegInits )
1498 {
1499 int i;
1500 fprintf( pFile, "s" );
1501 Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(p->vRegInits)+1) );
1502 Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegInits) );
1503 for ( i = 0; i < Vec_IntSize(p->vRegInits); i++ )
1504 Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegInits, i) );
1505 }
1506 // write configuration data
1507 if ( p->vConfigs )
1508 {
1509 fprintf( pFile, "b" );
1510 assert( p->pCellStr != NULL );
1511 Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(p->vConfigs) + strlen(p->pCellStr) + 1 );
1512 fwrite( p->pCellStr, 1, strlen(p->pCellStr) + 1, pFile );
1513// fwrite( Vec_IntArray(p->vConfigs), 1, 4*Vec_IntSize(p->vConfigs), pFile );
1514 for ( i = 0; i < Vec_IntSize(p->vConfigs); i++ )
1515 Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vConfigs, i) );
1516 }
1517 // write choices
1518 if ( Gia_ManHasChoices(p) )
1519 {
1520 int i, nPairs = 0;
1521 fprintf( pFile, "q" );
1522 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1523 nPairs += (Gia_ObjSibl(p, i) > 0);
1524 Gia_FileWriteBufferSize( pFile, 4*(nPairs * 2 + 1) );
1525 Gia_FileWriteBufferSize( pFile, nPairs );
1526 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1527 if ( Gia_ObjSibl(p, i) )
1528 {
1529 assert( i > Gia_ObjSibl(p, i) );
1530 Gia_FileWriteBufferSize( pFile, i );
1531 Gia_FileWriteBufferSize( pFile, Gia_ObjSibl(p, i) );
1532 }
1533 if ( fVerbose ) printf( "Finished writing extension \"q\".\n" );
1534 }
1535 // write switching activity
1536 if ( p->pSwitching )
1537 {
1538 fprintf( pFile, "u" );
1539 Gia_FileWriteBufferSize( pFile, Gia_ManObjNum(p) );
1540 fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile );
1541 }
1542/*
1543 // write timing information
1544 if ( p->pManTime )
1545 {
1546 fprintf( pFile, "t" );
1547 vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 0 );
1548 Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
1549 fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
1550 Vec_StrFree( vStrExt );
1551 }
1552*/
1553 // write object classes
1554 if ( p->vObjClasses )
1555 {
1556 fprintf( pFile, "v" );
1557 Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1558 assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
1559 fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
1560 }
1561 // write name
1562 if ( p->pName )
1563 {
1564 fprintf( pFile, "n" );
1565 Gia_FileWriteBufferSize( pFile, strlen(p->pName)+1 );
1566 fwrite( p->pName, 1, strlen(p->pName), pFile );
1567 fprintf( pFile, "%c", '\0' );
1568 }
1569 // write comments
1570 if ( fWriteNewLine )
1571 fprintf( pFile, "c\n" );
1572 if ( !fSkipComment ) {
1573 fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
1574 fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
1575 }
1576 fclose( pFile );
1577 if ( p != pInit )
1578 {
1579 Gia_ManTransferTiming( pInit, p );
1580 Gia_ManStop( p );
1581 }
1582}
Gia_AigerWriteMappingSimple
Vec_Str_t * Gia_AigerWriteMappingSimple(Gia_Man_t *p)
Definition giaAigerExt.c:229
Gia_AigerWriteMapping
Vec_Str_t * Gia_AigerWriteMapping(Gia_Man_t *p)
Definition giaAigerExt.c:204
Gia_WritePacking
Vec_Str_t * Gia_WritePacking(Vec_Int_t *vPacking)
Definition giaAigerExt.c:409
Gia_AigerWriteCellMappingDoc
Vec_Str_t * Gia_AigerWriteCellMappingDoc(Gia_Man_t *p)
Definition giaAigerExt.c:314
Gia_AigerWriteMappingDoc
Vec_Str_t * Gia_AigerWriteMappingDoc(Gia_Man_t *p)
Definition giaAigerExt.c:270
Gia_WriteEquivClasses
Vec_Str_t * Gia_WriteEquivClasses(Gia_Man_t *p)
Definition giaAigerExt.c:121
Gia_AigerWriteIntoMemoryStr
Vec_Str_t * Gia_AigerWriteIntoMemoryStr(Gia_Man_t *p)
Definition giaAiger.c:1062
Gia_AigerCollectLiterals
Vec_Int_t * Gia_AigerCollectLiterals(Gia_Man_t *p)
Definition giaAiger.c:97
Gia_FileWriteBufferSize
void Gia_FileWriteBufferSize(FILE *pFile, int nSize)
Definition giaAiger.c:79
Gia_AigerWriteLiterals
Vec_Str_t * Gia_AigerWriteLiterals(Vec_Int_t *vLits)
Definition giaAiger.c:129
Gia_ManIsNormalized
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition giaTim.c:114
Gia_ManEdgeToArray
Vec_Int_t * Gia_ManEdgeToArray(Gia_Man_t *p)
Definition giaEdge.c:88
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_TimeStamp
char * Gia_TimeStamp()
Definition giaUtil.c:106
Gia_ManTransferTiming
void Gia_ManTransferTiming(Gia_Man_t *p, Gia_Man_t *pGia)
Definition giaIf.c:2370
Gia_ManDupNormalize
Gia_Man_t * Gia_ManDupNormalize(Gia_Man_t *p, int fHashMapping)
Definition giaTim.c:139
Gia_ManTransferMapping
void Gia_ManTransferMapping(Gia_Man_t *p, Gia_Man_t *pGia)
Definition giaIf.c:2305
Gia_ManTransferPacking
void Gia_ManTransferPacking(Gia_Man_t *p, Gia_Man_t *pGia)
Definition giaIf.c:2336
Gia_Man_t_::nMuxes
int nMuxes
Definition gia.h:108
Gia_Man_t_::nXors
int nXors
Definition gia.h:107
Tim_ManSave
Vec_Str_t * Tim_ManSave(Tim_Man_t *p, int fHieOnly)
FUNCTION DEFINITIONS ///.
Definition timDump.c:46
Tim_ManGetArrTimes
float * Tim_ManGetArrTimes(Tim_Man_t *p)
Definition timMan.c:482
Tim_ManPoNum
int Tim_ManPoNum(Tim_Man_t *p)
Definition timMan.c:714
Tim_ManGetReqTimes
float * Tim_ManGetReqTimes(Tim_Man_t *p)
Definition timMan.c:497
Tim_ManPiNum
int Tim_ManPiNum(Tim_Man_t *p)
Definition timMan.c:708
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_AigerWriteSimple()

void Gia_AigerWriteSimple ( Gia_Man_t * pInit,
char * pFileName )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1629 of file giaAiger.c.

1630{
1631 FILE * pFile;
1632 Vec_Str_t * vStr;
1633 if ( Gia_ManPoNum(pInit) == 0 )
1634 {
1635 printf( "Gia_AigerWriteSimple(): AIG cannot be written because it has no POs.\n" );
1636 return;
1637 }
1638 // start the output stream
1639 pFile = fopen( pFileName, "wb" );
1640 if ( pFile == NULL )
1641 {
1642 fprintf( stdout, "Gia_AigerWriteSimple(): Cannot open the output file \"%s\".\n", pFileName );
1643 return;
1644 }
1645 // write the buffer
1646 vStr = Gia_AigerWriteIntoMemoryStr( pInit );
1647 fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
1648 Vec_StrFree( vStr );
1649 fclose( pFile );
1650}
Here is the call graph for this function:

◆ Gia_DumpAiger()

void Gia_DumpAiger ( Gia_Man_t * p,
char * pFilePrefix,
int iFileNum,
int nFileNumDigits )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1611 of file giaAiger.c.

1612{
1613 char Buffer[100];
1614 sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
1615 Gia_AigerWrite( p, Buffer, 0, 0, 0 );
1616}
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *pInit, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_FileFixName()

void Gia_FileFixName ( char * pFileName)

DECLARATIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file giaAiger.c.

50{
51 char * pName;
52 for ( pName = pFileName; *pName; pName++ )
53 if ( *pName == '>' )
54 *pName = '\\';
55}
Here is the caller graph for this function:

◆ Gia_FileNameGeneric()

char * Gia_FileNameGeneric ( char * FileName)

Definition at line 56 of file giaAiger.c.

57{
58 char * pDot, * pRes;
59 pRes = Abc_UtilStrsav( FileName );
60 if ( (pDot = strrchr( pRes, '.' )) )
61 *pDot = 0;
62 return pRes;
63}
strrchr
char * strrchr()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_FileSize()

int Gia_FileSize ( char * pFileName)

FUNCTION DECLARATIONS ///.

Definition at line 64 of file giaAiger.c.

65{
66 FILE * pFile;
67 int nFileSize;
68 pFile = fopen( pFileName, "r" );
69 if ( pFile == NULL )
70 {
71 printf( "Gia_FileSize(): The file is unavailable (absent or open).\n" );
72 return 0;
73 }
74 fseek( pFile, 0, SEEK_END );
75 nFileSize = ftell( pFile );
76 fclose( pFile );
77 return nFileSize;
78}
SEEK_END
#define SEEK_END
Definition zconf.h:392
Here is the caller graph for this function:

◆ Gia_FileWriteBufferSize()

void Gia_FileWriteBufferSize ( FILE * pFile,
int nSize )

Definition at line 79 of file giaAiger.c.

80{
81 unsigned char Buffer[5];
82 Gia_AigerWriteInt( Buffer, nSize );
83 fwrite( Buffer, 1, 4, pFile );
84}
Here is the caller graph for this function: