ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
miniaig.h
Go to the documentation of this file.
1
20
21#ifndef MINI_AIG__mini_aig_h
22#define MINI_AIG__mini_aig_h
23
27
28#include <stdio.h>
29#include <stdlib.h>
30#include <string.h>
31#include <assert.h>
32
33#ifndef _VERIFIC_DATABASE_H_
34ABC_NAMESPACE_HEADER_START
35#endif
36
40
41#define MINI_AIG_NULL (0x7FFFFFFF)
42#define MINI_AIG_START_SIZE (0x000000FF)
43
47
48typedef struct Mini_Aig_t_ Mini_Aig_t;
49struct Mini_Aig_t_
50{
51 int nCap;
52 int nSize;
53 int nRegs;
54 int * pArray;
55};
56
60
61// memory management
62#define MINI_AIG_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
63#define MINI_AIG_CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
64#define MINI_AIG_FALLOC(type, num) ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
65#define MINI_AIG_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
66#define MINI_AIG_REALLOC(type, obj, num) \
67 ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
68 ((type *) malloc(sizeof(type) * (num))))
69
70// internal procedures
71static void Mini_AigGrow( Mini_Aig_t * p, int nCapMin )
72{
73 if ( p->nCap >= nCapMin )
74 return;
75 p->pArray = MINI_AIG_REALLOC( int, p->pArray, nCapMin );
76 assert( p->pArray );
77 p->nCap = nCapMin;
78}
79static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 )
80{
81 if ( p->nSize + 2 > p->nCap )
82 {
83 assert( p->nSize < MINI_AIG_NULL/4 );
84 if ( p->nCap < MINI_AIG_START_SIZE )
85 Mini_AigGrow( p, MINI_AIG_START_SIZE );
86 else
87 Mini_AigGrow( p, 2 * p->nCap );
88 }
89 p->pArray[p->nSize++] = Lit0;
90 p->pArray[p->nSize++] = Lit1;
91}
92
93// accessing fanins
94static int Mini_AigNodeFanin0( Mini_Aig_t * p, int Id )
95{
96 assert( Id >= 0 && 2*Id < p->nSize );
97 assert( p->pArray[2*Id] == MINI_AIG_NULL || p->pArray[2*Id] < 2*Id );
98 return p->pArray[2*Id];
99}
100static int Mini_AigNodeFanin1( Mini_Aig_t * p, int Id )
101{
102 assert( Id >= 0 && 2*Id < p->nSize );
103 assert( p->pArray[2*Id+1] == MINI_AIG_NULL || p->pArray[2*Id+1] < 2*Id );
104 return p->pArray[2*Id+1];
105}
106static void Mini_AigFlipLastPo( Mini_Aig_t * p )
107{
108 assert( p->pArray[p->nSize-1] == MINI_AIG_NULL );
109 assert( p->pArray[p->nSize-2] != MINI_AIG_NULL );
110 p->pArray[p->nSize-2] ^= 1;
111}
112
113// working with variables and literals
114static int Mini_AigVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
115static int Mini_AigLit2Var( int Lit ) { return Lit >> 1; }
116static int Mini_AigLitIsCompl( int Lit ) { return Lit & 1; }
117static int Mini_AigLitNot( int Lit ) { return Lit ^ 1; }
118static int Mini_AigLitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
119static int Mini_AigLitRegular( int Lit ) { return Lit & ~01; }
120
121static int Mini_AigLitConst0() { return 0; }
122static int Mini_AigLitConst1() { return 1; }
123static int Mini_AigLitIsConst0( int Lit ) { return Lit == 0; }
124static int Mini_AigLitIsConst1( int Lit ) { return Lit == 1; }
125static int Mini_AigLitIsConst( int Lit ) { return Lit == 0 || Lit == 1; }
126
127static int Mini_AigNodeNum( Mini_Aig_t * p ) { return p->nSize/2; }
128static int Mini_AigNodeIsConst( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id == 0; }
129static int Mini_AigNodeIsPi( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) == MINI_AIG_NULL; }
130static int Mini_AigNodeIsPo( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) == MINI_AIG_NULL; }
131static int Mini_AigNodeIsAnd( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) != MINI_AIG_NULL; }
132
133// working with sequential AIGs
134static int Mini_AigRegNum( Mini_Aig_t * p ) { return p->nRegs; }
135static void Mini_AigSetRegNum( Mini_Aig_t * p, int n ) { p->nRegs = n; }
136
137// iterators through objects
138#define Mini_AigForEachPi( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPi(p, i) ) {} else
139#define Mini_AigForEachPo( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPo(p, i) ) {} else
140#define Mini_AigForEachAnd( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsAnd(p, i) ) {} else
141
142
143// constructor/destructor
144static Mini_Aig_t * Mini_AigStart()
145{
146 Mini_Aig_t * p;
147 p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
148 p->nCap = MINI_AIG_START_SIZE;
149 p->pArray = MINI_AIG_ALLOC( int, p->nCap );
150 Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
151 return p;
152}
153static Mini_Aig_t * Mini_AigStartSupport( int nIns, int nObjsAlloc )
154{
155 Mini_Aig_t * p; int i;
156 assert( 1+nIns < nObjsAlloc );
157 p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
158 p->nCap = 2*nObjsAlloc;
159 p->nSize = 2*(1+nIns);
160 p->pArray = MINI_AIG_ALLOC( int, p->nCap );
161 for ( i = 0; i < p->nSize; i++ )
162 p->pArray[i] = MINI_AIG_NULL;
163 return p;
164}
165static Mini_Aig_t * Mini_AigStartArray( int nIns, int n0InAnds, int * p0InAnds, int nOuts, int * pOuts )
166{
167 Mini_Aig_t * p; int i;
168 assert( 1+nIns <= n0InAnds );
169 p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
170 p->nCap = 2*(n0InAnds + nOuts);
171 p->nSize = 2*(n0InAnds + nOuts);
172 p->pArray = MINI_AIG_ALLOC( int, p->nCap );
173 for ( i = 0; i < 2*(1 + nIns); i++ )
174 p->pArray[i] = MINI_AIG_NULL;
175 memcpy( p->pArray + 2*(1 + nIns), p0InAnds + 2*(1 + nIns), 2*(n0InAnds - 1 - nIns)*sizeof(int) );
176 for ( i = 0; i < nOuts; i++ )
177 {
178 p->pArray[2*(n0InAnds + i)+0] = pOuts[i];
179 p->pArray[2*(n0InAnds + i)+1] = MINI_AIG_NULL;
180 }
181 return p;
182}
183static Mini_Aig_t * Mini_AigDup( Mini_Aig_t * p )
184{
185 Mini_Aig_t * pNew;
186 pNew = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
187 pNew->nCap = p->nCap;
188 pNew->nSize = p->nSize;
189 pNew->pArray = MINI_AIG_ALLOC( int, p->nSize );
190 memcpy( pNew->pArray, p->pArray, p->nSize * sizeof(int) );
191 return pNew;
192}
193static void Mini_AigStop( Mini_Aig_t * p )
194{
195 MINI_AIG_FREE( p->pArray );
196 MINI_AIG_FREE( p );
197}
198static int Mini_AigPiNum( Mini_Aig_t * p )
199{
200 int i, nPis = 0;
201 Mini_AigForEachPi( p, i )
202 nPis++;
203 return nPis;
204}
205static int Mini_AigPoNum( Mini_Aig_t * p )
206{
207 int i, nPos = 0;
208 Mini_AigForEachPo( p, i )
209 nPos++;
210 return nPos;
211}
212static int Mini_AigAndNum( Mini_Aig_t * p )
213{
214 int i, nNodes = 0;
215 Mini_AigForEachAnd( p, i )
216 nNodes++;
217 return nNodes;
218}
219static int Mini_AigXorNum( Mini_Aig_t * p )
220{
221 int i, nNodes = 0;
222 Mini_AigForEachAnd( p, i )
223 nNodes += p->pArray[2*i] > p->pArray[2*i+1];
224 return nNodes;
225}
226static int Mini_AigLevelNum( Mini_Aig_t * p )
227{
228 int i, Level = 0;
229 int * pLevels = MINI_AIG_CALLOC( int, Mini_AigNodeNum(p) );
230 Mini_AigForEachAnd( p, i )
231 {
232 int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))];
233 int Lel1 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin1(p, i))];
234 pLevels[i] = 1 + (Lel0 > Lel1 ? Lel0 : Lel1);
235 }
236 Mini_AigForEachPo( p, i )
237 {
238 int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))];
239 Level = Level > Lel0 ? Level : Lel0;
240 }
241 MINI_AIG_FREE( pLevels );
242 return Level;
243}
244static void Mini_AigPrintStats( Mini_Aig_t * p )
245{
246 printf( "MiniAIG stats: PI = %d PO = %d FF = %d AND = %d\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigRegNum(p), Mini_AigAndNum(p) );
247}
248
249// serialization
250static void Mini_AigDump( Mini_Aig_t * p, char * pFileName )
251{
252 FILE * pFile;
253 int RetValue;
254 pFile = fopen( pFileName, "wb" );
255 if ( pFile == NULL )
256 {
257 printf( "Cannot open file for writing \"%s\".\n", pFileName );
258 return;
259 }
260 RetValue = (int)fwrite( &p->nSize, sizeof(int), 1, pFile );
261 RetValue = (int)fwrite( &p->nRegs, sizeof(int), 1, pFile );
262 RetValue = (int)fwrite( p->pArray, sizeof(int), p->nSize, pFile );
263 fclose( pFile );
264}
265static Mini_Aig_t * Mini_AigLoad( char * pFileName )
266{
267 Mini_Aig_t * p;
268 FILE * pFile;
269 int RetValue, nSize;
270 pFile = fopen( pFileName, "rb" );
271 if ( pFile == NULL )
272 {
273 printf( "Cannot open file for reading \"%s\".\n", pFileName );
274 return NULL;
275 }
276 RetValue = (int)fread( &nSize, sizeof(int), 1, pFile );
277 p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
278 p->nSize = p->nCap = nSize;
279 p->pArray = MINI_AIG_ALLOC( int, p->nCap );
280 RetValue = (int)fread( &p->nRegs, sizeof(int), 1, pFile );
281 RetValue = (int)fread( p->pArray, sizeof(int), p->nSize, pFile );
282 fclose( pFile );
283 return p;
284}
285
286
287// creating nodes
288// (constant node is created when AIG manager is created)
289static int Mini_AigCreatePi( Mini_Aig_t * p )
290{
291 int Lit = p->nSize;
292 Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
293 return Lit;
294}
295static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 )
296{
297 int Lit = p->nSize;
298 assert( Lit0 >= 0 && Lit0 < Lit );
299 Mini_AigPush( p, Lit0, MINI_AIG_NULL );
300 return Lit;
301}
302
303// boolean operations
304static int Mini_AigAnd( Mini_Aig_t * p, int Lit0, int Lit1 )
305{
306 int Lit = p->nSize;
307 assert( Lit0 >= 0 && Lit0 < Lit );
308 assert( Lit1 >= 0 && Lit1 < Lit );
309 if ( Lit0 < Lit1 )
310 Mini_AigPush( p, Lit0, Lit1 );
311 else
312 Mini_AigPush( p, Lit1, Lit0 );
313 return Lit;
314}
315static int Mini_AigOr( Mini_Aig_t * p, int Lit0, int Lit1 )
316{
317 return Mini_AigLitNot( Mini_AigAnd( p, Mini_AigLitNot(Lit0), Mini_AigLitNot(Lit1) ) );
318}
319static int Mini_AigMux( Mini_Aig_t * p, int LitC, int Lit1, int Lit0 )
320{
321 int Res0 = Mini_AigAnd( p, LitC, Lit1 );
322 int Res1 = Mini_AigAnd( p, Mini_AigLitNot(LitC), Lit0 );
323 return Mini_AigOr( p, Res0, Res1 );
324}
325static int Mini_AigXor( Mini_Aig_t * p, int Lit0, int Lit1 )
326{
327 return Mini_AigMux( p, Lit0, Mini_AigLitNot(Lit1), Lit1 );
328}
329static int Mini_AigXorSpecial( Mini_Aig_t * p, int Lit0, int Lit1 )
330{
331 int Lit = p->nSize;
332 assert( Lit0 >= 0 && Lit0 < Lit );
333 assert( Lit1 >= 0 && Lit1 < Lit );
334 if ( Lit0 > Lit1 )
335 Mini_AigPush( p, Lit0, Lit1 );
336 else
337 Mini_AigPush( p, Lit1, Lit0 );
338 return Lit;
339}
340static int Mini_AigAndMulti( Mini_Aig_t * p, int * pLits, int nLits )
341{
342 int i;
343 assert( nLits > 0 );
344 while ( nLits > 1 )
345 {
346 for ( i = 0; i < nLits/2; i++ )
347 pLits[i] = Mini_AigAnd(p, pLits[2*i], pLits[2*i+1]);
348 if ( nLits & 1 )
349 pLits[i++] = pLits[nLits-1];
350 nLits = i;
351 }
352 return pLits[0];
353}
354static int Mini_AigMuxMulti( Mini_Aig_t * p, int * pCtrl, int nCtrl, int * pData, int nData )
355{
356 int i, c;
357 assert( nData > 0 );
358 if ( nCtrl == 0 )
359 return pData[0];
360 assert( nData <= (1 << nCtrl) );
361 for ( c = 0; c < nCtrl; c++ )
362 {
363 for ( i = 0; i < nData/2; i++ )
364 pData[i] = Mini_AigMux( p, pCtrl[c], pData[2*i+1], pData[2*i] );
365 if ( nData & 1 )
366 pData[i++] = Mini_AigMux( p, pCtrl[c], 0, pData[nData-1] );
367 nData = i;
368 }
369 assert( nData == 1 );
370 return pData[0];
371}
372static int Mini_AigMuxMulti_rec( Mini_Aig_t * p, int * pCtrl, int * pData, int nData )
373{
374 int Res0, Res1;
375 assert( nData > 0 );
376 if ( nData == 1 )
377 return pData[0];
378 assert( nData % 2 == 0 );
379 Res0 = Mini_AigMuxMulti_rec( p, pCtrl+1, pData, nData/2 );
380 Res1 = Mini_AigMuxMulti_rec( p, pCtrl+1, pData+nData/2, nData/2 );
381 return Mini_AigMux( p, pCtrl[0], Res1, Res0 );
382}
383static Mini_Aig_t * Mini_AigTransformXor( Mini_Aig_t * p )
384{
385 Mini_Aig_t * pNew = Mini_AigStart();
386 int i, * pCopy = MINI_AIG_ALLOC( int, Mini_AigNodeNum(p) );
387 Mini_AigForEachPi( p, i )
388 pCopy[i] = Mini_AigCreatePi(pNew);
389 Mini_AigForEachAnd( p, i )
390 {
391 int iLit0 = Mini_AigNodeFanin0(p, i);
392 int iLit1 = Mini_AigNodeFanin1(p, i);
393 iLit0 = Mini_AigLitNotCond( pCopy[Mini_AigLit2Var(iLit0)], Mini_AigLitIsCompl(iLit0) );
394 iLit1 = Mini_AigLitNotCond( pCopy[Mini_AigLit2Var(iLit1)], Mini_AigLitIsCompl(iLit1) );
395 if ( iLit0 <= iLit1 )
396 pCopy[i] = Mini_AigAnd( pNew, iLit0, iLit1 );
397 else
398 pCopy[i] = Mini_AigXor( pNew, iLit0, iLit1 );
399 }
400 Mini_AigForEachPo( p, i )
401 {
402 int iLit0 = Mini_AigNodeFanin0( p, i );
403 iLit0 = Mini_AigLitNotCond( pCopy[Mini_AigLit2Var(iLit0)], Mini_AigLitIsCompl(iLit0) );
404 pCopy[i] = Mini_AigCreatePo( pNew, iLit0 );
405 }
406 MINI_AIG_FREE( pCopy );
407 return pNew;
408}
409
410
411static unsigned s_MiniTruths5[5] = {
412 0xAAAAAAAA,
413 0xCCCCCCCC,
414 0xF0F0F0F0,
415 0xFF00FF00,
416 0xFFFF0000,
417};
418static inline int Mini_AigTt5HasVar( unsigned t, int iVar )
419{
420 return ((t << (1<<iVar)) & s_MiniTruths5[iVar]) != (t & s_MiniTruths5[iVar]);
421}
422static inline unsigned Mini_AigTt5Cofactor0( unsigned t, int iVar )
423{
424 assert( iVar >= 0 && iVar < 6 );
425 return (t & ~s_MiniTruths5[iVar]) | ((t & ~s_MiniTruths5[iVar]) << (1<<iVar));
426}
427static inline unsigned Mini_AigTt5Cofactor1( unsigned t, int iVar )
428{
429 assert( iVar >= 0 && iVar < 6 );
430 return (t & s_MiniTruths5[iVar]) | ((t & s_MiniTruths5[iVar]) >> (1<<iVar));
431}
432static inline int Mini_AigAndProp( Mini_Aig_t * p, int iLit0, int iLit1 )
433{
434 if ( iLit0 < 2 )
435 return iLit0 ? iLit1 : 0;
436 if ( iLit1 < 2 )
437 return iLit1 ? iLit0 : 0;
438 if ( iLit0 == iLit1 )
439 return iLit1;
440 if ( iLit0 == Mini_AigLitNot(iLit1) )
441 return 0;
442 return Mini_AigAnd( p, iLit0, iLit1 );
443}
444static inline int Mini_AigMuxProp( Mini_Aig_t * p, int iCtrl, int iData1, int iData0 )
445{
446 int iTemp0 = Mini_AigAndProp( p, Mini_AigLitNot(iCtrl), iData0 );
447 int iTemp1 = Mini_AigAndProp( p, iCtrl, iData1 );
448 return Mini_AigLitNot( Mini_AigAndProp( p, Mini_AigLitNot(iTemp0), Mini_AigLitNot(iTemp1) ) );
449}
450static inline int Mini_AigTruth( Mini_Aig_t * p, int * pVarLits, int nVars, unsigned Truth )
451{
452 int Var, Lit0, Lit1;
453 if ( Truth == 0 )
454 return 0;
455 if ( ~Truth == 0 )
456 return 1;
457 assert( nVars > 0 );
458 // find the topmost var
459 for ( Var = nVars-1; Var >= 0; Var-- )
460 if ( Mini_AigTt5HasVar( Truth, Var ) )
461 break;
462 assert( Var >= 0 );
463 // cofactor
464 Lit0 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor0(Truth, Var) );
465 Lit1 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor1(Truth, Var) );
466 return Mini_AigMuxProp( p, pVarLits[Var], Lit1, Lit0 );
467}
468static char * Mini_AigPhase( Mini_Aig_t * p )
469{
470 char * pRes = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) );
471 int i;
472 Mini_AigForEachAnd( p, i )
473 {
474 int iFaninLit0 = Mini_AigNodeFanin0( p, i );
475 int iFaninLit1 = Mini_AigNodeFanin1( p, i );
476 int Phase0 = pRes[Mini_AigLit2Var(iFaninLit0)] ^ Mini_AigLitIsCompl(iFaninLit0);
477 int Phase1 = pRes[Mini_AigLit2Var(iFaninLit1)] ^ Mini_AigLitIsCompl(iFaninLit1);
478 pRes[i] = Phase0 & Phase1;
479 }
480 return pRes;
481}
482
483// procedure to check the topological order during AIG construction
484static int Mini_AigCheck( Mini_Aig_t * p )
485{
486 int status = 1;
487 int i, iFaninLit0, iFaninLit1;
488 Mini_AigForEachAnd( p, i )
489 {
490 // get the fanin literals of this AND node
491 iFaninLit0 = Mini_AigNodeFanin0( p, i );
492 iFaninLit1 = Mini_AigNodeFanin1( p, i );
493 // compare the fanin literals with the literal of the current node (2 * i)
494 if ( iFaninLit0 >= 2 * i )
495 printf( "Fanin0 of AND node %d is not in a topological order.\n", i ), status = 0;
496 if ( iFaninLit1 >= 2 * i )
497 printf( "Fanin0 of AND node %d is not in a topological order.\n", i ), status = 0;
498 }
499 Mini_AigForEachPo( p, i )
500 {
501 // get the fanin literal of this PO node
502 iFaninLit0 = Mini_AigNodeFanin0( p, i );
503 // compare the fanin literal with the literal of the current node (2 * i)
504 if ( iFaninLit0 >= 2 * i )
505 printf( "Fanin0 of PO node %d is not in a topological order.\n", i ), status = 0;
506 }
507 return status;
508}
509
510// procedure to dump MiniAIG into a Verilog file
511static void Mini_AigDumpVerilog( char * pFileName, char * pModuleName, Mini_Aig_t * p )
512{
513 int i, k, iFaninLit0, iFaninLit1, Length = strlen(pModuleName), nPos = Mini_AigPoNum(p);
514 char * pObjIsPi = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) );
515 FILE * pFile = fopen( pFileName, "wb" );
516 if ( pFile == NULL ) { printf( "Cannot open output file %s\n", pFileName ); MINI_AIG_FREE( pObjIsPi ); return; }
517 // write interface
518 //fprintf( pFile, "// This MiniAIG dump was produced by ABC on %s\n\n", Extra_TimeStamp() );
519 fprintf( pFile, "module %s (\n", pModuleName );
520 if ( Mini_AigPiNum(p) > 0 )
521 {
522 fprintf( pFile, "%*sinput wire", Length+10, "" );
523 k = 0;
524 Mini_AigForEachPi( p, i )
525 {
526 if ( k++ % 12 == 0 ) fprintf( pFile, "\n%*s", Length+10, "" );
527 fprintf( pFile, "i%d, ", i );
528 pObjIsPi[i] = 1;
529 }
530 }
531 fprintf( pFile, "\n%*soutput wire", Length+10, "" );
532 k = 0;
533 Mini_AigForEachPo( p, i )
534 {
535 if ( k++ % 12 == 0 ) fprintf( pFile, "\n%*s", Length+10, "" );
536 fprintf( pFile, "o%d%s", i, k==nPos ? "":", " );
537 }
538 fprintf( pFile, "\n%*s);\n\n", Length+8, "" );
539 // write LUTs
540 Mini_AigForEachAnd( p, i )
541 {
542 iFaninLit0 = Mini_AigNodeFanin0( p, i );
543 iFaninLit1 = Mini_AigNodeFanin1( p, i );
544 fprintf( pFile, " assign n%d = ", i );
545 fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", pObjIsPi[iFaninLit0 >> 1] ? 'i':'n', iFaninLit0 >> 1 );
546 fprintf( pFile, " & " );
547 fprintf( pFile, "%s%c%d", (iFaninLit1 & 1) ? "~":"", pObjIsPi[iFaninLit1 >> 1] ? 'i':'n', iFaninLit1 >> 1 );
548 fprintf( pFile, ";\n" );
549 }
550 // write assigns
551 fprintf( pFile, "\n" );
552 Mini_AigForEachPo( p, i )
553 {
554 iFaninLit0 = Mini_AigNodeFanin0( p, i );
555 fprintf( pFile, " assign o%d = ", i );
556 fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", pObjIsPi[iFaninLit0 >> 1] ? 'i':'n', iFaninLit0 >> 1 );
557 fprintf( pFile, ";\n" );
558 }
559 fprintf( pFile, "\nendmodule // %s \n\n\n", pModuleName );
560 MINI_AIG_FREE( pObjIsPi );
561 fclose( pFile );
562}
563
564// procedure to dump MiniAIG into a BLIF file
565static void Mini_AigDumpBlif( char * pFileName, char * pModuleName, Mini_Aig_t * p, int fVerbose )
566{
567 int i, k, iFaninLit0, iFaninLit1;
568 char * pObjIsPi = MINI_AIG_FALLOC( char, Mini_AigNodeNum(p) );
569 FILE * pFile = fopen( pFileName, "wb" );
570 assert( Mini_AigPiNum(p) <= 26 );
571 if ( pFile == NULL ) { printf( "Cannot open output file %s\n", pFileName ); MINI_AIG_FREE( pObjIsPi ); return; }
572 // write interface
573 //fprintf( pFile, "// This MiniAIG dump was produced by ABC on %s\n\n", Extra_TimeStamp() );
574 fprintf( pFile, ".model %s\n", pModuleName );
575 if ( Mini_AigPiNum(p) )
576 {
577 k = 0;
578 fprintf( pFile, ".inputs" );
579 Mini_AigForEachPi( p, i )
580 {
581 pObjIsPi[i] = k;
582 fprintf( pFile, " %c", (char)('a'+k++) );
583 }
584 }
585 k = 0;
586 fprintf( pFile, "\n.outputs" );
587 Mini_AigForEachPo( p, i )
588 fprintf( pFile, " o%d", k++ );
589 fprintf( pFile, "\n\n" );
590 // write LUTs
591 Mini_AigForEachAnd( p, i )
592 {
593 iFaninLit0 = Mini_AigNodeFanin0( p, i );
594 iFaninLit1 = Mini_AigNodeFanin1( p, i );
595 fprintf( pFile, ".names" );
596 if ( pObjIsPi[iFaninLit0 >> 1] >= 0 )
597 fprintf( pFile, " %c", (char)('a'+pObjIsPi[iFaninLit0 >> 1]) );
598 else
599 fprintf( pFile, " n%d", iFaninLit0 >> 1 );
600 if ( pObjIsPi[iFaninLit1 >> 1] >= 0 )
601 fprintf( pFile, " %c", (char)('a'+pObjIsPi[iFaninLit1 >> 1]) );
602 else
603 fprintf( pFile, " n%d", iFaninLit1 >> 1 );
604 fprintf( pFile, " n%d\n", i );
605 if ( iFaninLit0 < iFaninLit1 )
606 fprintf( pFile, "%d%d 1\n", !(iFaninLit0 & 1), !(iFaninLit1 & 1) );
607 else if ( !(iFaninLit0 & 1) == !(iFaninLit1 & 1) )
608 fprintf( pFile, "10 1\n01 1\n" );
609 else
610 fprintf( pFile, "00 1\n11 1\n" );
611 }
612 // write assigns
613 fprintf( pFile, "\n" );
614 k = 0;
615 Mini_AigForEachPo( p, i )
616 {
617 iFaninLit0 = Mini_AigNodeFanin0( p, i );
618 fprintf( pFile, ".names" );
619 if ( pObjIsPi[iFaninLit0 >> 1] >= 0 )
620 fprintf( pFile, " %c", (char)('a'+pObjIsPi[iFaninLit0 >> 1]) );
621 else
622 fprintf( pFile, " n%d", iFaninLit0 >> 1 );
623 fprintf( pFile, " o%d\n", k++ );
624 fprintf( pFile, "%d 1\n", !(iFaninLit0 & 1) );
625 }
626 fprintf( pFile, ".end\n\n" );
627 MINI_AIG_FREE( pObjIsPi );
628 fclose( pFile );
629 if ( fVerbose )
630 printf( "Written MiniAIG into the BLIF file \"%s\".\n", pFileName );
631}
632
633
634// checks if MiniAIG is normalized (first inputs, then internal nodes, then outputs)
635static int Mini_AigIsNormalized( Mini_Aig_t * p )
636{
637 int nCiNum = Mini_AigPiNum(p);
638 int nCoNum = Mini_AigPoNum(p);
639 int i, nOffset = 1;
640 for ( i = 0; i < nCiNum; i++ )
641 if ( !Mini_AigNodeIsPi( p, nOffset+i ) )
642 return 0;
643 nOffset = Mini_AigNodeNum(p) - nCoNum;
644 for ( i = 0; i < nCoNum; i++ )
645 if ( !Mini_AigNodeIsPo( p, nOffset+i ) )
646 return 0;
647 return 1;
648}
649
650
654
655static unsigned Mini_AigerReadUnsigned( FILE * pFile )
656{
657 unsigned x = 0, i = 0;
658 unsigned char ch;
659 while ((ch = fgetc(pFile)) & 0x80)
660 x |= (ch & 0x7f) << (7 * i++);
661 return x | (ch << (7 * i));
662}
663static void Mini_AigerWriteUnsigned( FILE * pFile, unsigned x )
664{
665 unsigned char ch;
666 while (x & ~0x7f)
667 {
668 ch = (x & 0x7f) | 0x80;
669 fputc( ch, pFile );
670 x >>= 7;
671 }
672 ch = x;
673 fputc( ch, pFile );
674}
675static int * Mini_AigerReadInt( char * pFileName, int * pnObjs, int * pnIns, int * pnLatches, int * pnOuts, int * pnAnds )
676{
677 int i, Temp, nTotal, nObjs, nIns, nLatches, nOuts, nAnds, * pObjs;
678 FILE * pFile = fopen( pFileName, "rb" );
679 if ( pFile == NULL )
680 {
681 fprintf( stdout, "Mini_AigerRead(): Cannot open the output file \"%s\".\n", pFileName );
682 return NULL;
683 }
684 if ( fgetc(pFile) != 'a' || fgetc(pFile) != 'i' || fgetc(pFile) != 'g' )
685 {
686 fprintf( stdout, "Mini_AigerRead(): Can only read binary AIGER.\n" );
687 fclose( pFile );
688 return NULL;
689 }
690 if ( fscanf(pFile, "%d %d %d %d %d", &nTotal, &nIns, &nLatches, &nOuts, &nAnds) != 5 )
691 {
692 fprintf( stdout, "Mini_AigerRead(): Cannot read the header line.\n" );
693 fclose( pFile );
694 return NULL;
695 }
696 if ( nTotal != nIns + nLatches + nAnds )
697 {
698 fprintf( stdout, "The number of objects does not match.\n" );
699 fclose( pFile );
700 return NULL;
701 }
702 nObjs = 1 + nIns + 2*nLatches + nOuts + nAnds;
703 pObjs = MINI_AIG_CALLOC( int, nObjs * 2 );
704 for ( i = 0; i <= nIns + nLatches; i++ )
705 pObjs[2*i] = pObjs[2*i+1] = MINI_AIG_NULL;
706 // read flop input literals
707 for ( i = 0; i < nLatches; i++ )
708 {
709 while ( fgetc(pFile) != '\n' );
710 fscanf( pFile, "%d", &Temp );
711 pObjs[2*(nObjs-nLatches+i)+0] = Temp;
712 pObjs[2*(nObjs-nLatches+i)+1] = MINI_AIG_NULL;
713 }
714 // read output literals
715 for ( i = 0; i < nOuts; i++ )
716 {
717 while ( fgetc(pFile) != '\n' );
718 fscanf( pFile, "%d", &Temp );
719 pObjs[2*(nObjs-nOuts-nLatches+i)+0] = Temp;
720 pObjs[2*(nObjs-nOuts-nLatches+i)+1] = MINI_AIG_NULL;
721 }
722 // read the binary part
723 while ( fgetc(pFile) != '\n' );
724 for ( i = 0; i < nAnds; i++ )
725 {
726 int uLit = 2*(1+nIns+nLatches+i);
727 int uLit1 = uLit - Mini_AigerReadUnsigned( pFile );
728 int uLit0 = uLit1 - Mini_AigerReadUnsigned( pFile );
729 pObjs[uLit+0] = uLit0;
730 pObjs[uLit+1] = uLit1;
731 }
732 fclose( pFile );
733 if ( pnObjs ) *pnObjs = nObjs;
734 if ( pnIns ) *pnIns = nIns;
735 if ( pnLatches ) *pnLatches = nLatches;
736 if ( pnOuts ) *pnOuts = nOuts;
737 if ( pnAnds ) *pnAnds = nAnds;
738 return pObjs;
739}
740static Mini_Aig_t * Mini_AigerRead( char * pFileName, int fVerbose )
741{
742 Mini_Aig_t * p;
743 int nObjs, nIns, nLatches, nOuts, nAnds, * pObjs = Mini_AigerReadInt( pFileName, &nObjs, &nIns, &nLatches, &nOuts, &nAnds );
744 if ( pObjs == NULL )
745 return NULL;
746 p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
747 p->nCap = 2*nObjs;
748 p->nSize = 2*nObjs;
749 p->nRegs = nLatches;
750 p->pArray = pObjs;
751 if ( fVerbose )
752 printf( "Loaded MiniAIG from the AIGER file \"%s\".\n", pFileName );
753 return p;
754}
755
756static void Mini_AigerWriteInt( char * pFileName, int * pObjs, int nObjs, int nIns, int nLatches, int nOuts, int nAnds )
757{
758 FILE * pFile = fopen( pFileName, "wb" ); int i;
759 if ( pFile == NULL )
760 {
761 fprintf( stdout, "Mini_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName );
762 return;
763 }
764 fprintf( pFile, "aig %d %d %d %d %d\n", nIns + nLatches + nAnds, nIns, nLatches, nOuts, nAnds );
765 for ( i = 0; i < nLatches; i++ )
766 fprintf( pFile, "%d\n", pObjs[2*(nObjs-nLatches+i)+0] );
767 for ( i = 0; i < nOuts; i++ )
768 fprintf( pFile, "%d\n", pObjs[2*(nObjs-nOuts-nLatches+i)+0] );
769 for ( i = 0; i < nAnds; i++ )
770 {
771 int uLit = 2*(1+nIns+nLatches+i);
772 int uLit0 = pObjs[uLit+0];
773 int uLit1 = pObjs[uLit+1];
774 Mini_AigerWriteUnsigned( pFile, uLit - uLit1 );
775 Mini_AigerWriteUnsigned( pFile, uLit1 - uLit0 );
776 }
777 fprintf( pFile, "c\n" );
778 fclose( pFile );
779}
780static void Mini_AigerWrite( char * pFileName, Mini_Aig_t * p, int fVerbose )
781{
782 int i, nIns = 0, nOuts = 0, nAnds = 0;
783 assert( Mini_AigIsNormalized(p) );
784 for ( i = 1; i < Mini_AigNodeNum(p); i++ )
785 {
786 if ( Mini_AigNodeIsPi(p, i) )
787 nIns++;
788 else if ( Mini_AigNodeIsPo(p, i) )
789 nOuts++;
790 else
791 nAnds++;
792 }
793 Mini_AigerWriteInt( pFileName, p->pArray, p->nSize/2, nIns - p->nRegs, p->nRegs, nOuts - p->nRegs, nAnds );
794 if ( fVerbose )
795 printf( "Written MiniAIG into the AIGER file \"%s\".\n", pFileName );
796}
797static void Mini_AigerTest( char * pFileNameIn, char * pFileNameOut )
798{
799 Mini_Aig_t * p = Mini_AigerRead( pFileNameIn, 1 );
800 if ( p == NULL )
801 return;
802 printf( "Finished reading input file \"%s\".\n", pFileNameIn );
803 Mini_AigerWrite( pFileNameOut, p, 1 );
804 printf( "Finished writing output file \"%s\".\n", pFileNameOut );
805 Mini_AigStop( p );
806}
807
808/*
809int main( int argc, char ** argv )
810{
811 if ( argc != 3 )
812 return 0;
813 Mini_AigerTest( argv[1], argv[2] );
814 return 1;
815}
816*/
817
818/*
819#include "aig/miniaig/miniaig.h"
820
821// this procedure creates a MiniAIG for function F = a*b + ~c and writes it into a file "test.aig"
822void Mini_AigTest()
823{
824 Mini_Aig_t * p = Mini_AigStart(); // create empty AIG manager (contains only const0 node)
825 int litApos = Mini_AigCreatePi( p ); // create input A (returns pos lit of A)
826 int litBpos = Mini_AigCreatePi( p ); // create input B (returns pos lit of B)
827 int litCpos = Mini_AigCreatePi( p ); // create input C (returns pos lit of C)
828 int litCneg = Mini_AigLitNot( litCpos ); // neg lit of C
829 int litAnd = Mini_AigAnd( p, litApos, litBpos ); // lit for a*b
830 int litOr = Mini_AigOr( p, litAnd, litCneg ); // lit for a*b + ~c
831 Mini_AigCreatePo( p, litOr ); // create primary output
832 Mini_AigerWrite( "test.aig", p, 1 ); // write the result into a file
833 Mini_AigStop( p ); // deallocate MiniAIG
834}
835*/
836
840
841#ifndef _VERIFIC_DATABASE_H_
842ABC_NAMESPACE_HEADER_END
843#endif
844
845#endif
846
850
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition abc_namespaces.h:51
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition abc_namespaces.h:50
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
MINI_AIG_ALLOC
#define MINI_AIG_ALLOC(type, num)
MACRO DEFINITIONS ///.
Definition miniaig.h:62
Mini_Aig_t
struct Mini_Aig_t_ Mini_Aig_t
BASIC TYPES ///.
Definition miniaig.h:48
MINI_AIG_FALLOC
#define MINI_AIG_FALLOC(type, num)
Definition miniaig.h:64
MINI_AIG_NULL
#define MINI_AIG_NULL
INCLUDES ///.
Definition miniaig.h:41
MINI_AIG_REALLOC
#define MINI_AIG_REALLOC(type, obj, num)
Definition miniaig.h:66
MINI_AIG_FREE
#define MINI_AIG_FREE(obj)
Definition miniaig.h:65
Mini_AigForEachPi
#define Mini_AigForEachPi(p, i)
Definition miniaig.h:138
Mini_AigForEachPo
#define Mini_AigForEachPo(p, i)
Definition miniaig.h:139
MINI_AIG_CALLOC
#define MINI_AIG_CALLOC(type, num)
Definition miniaig.h:63
Mini_AigForEachAnd
#define Mini_AigForEachAnd(p, i)
Definition miniaig.h:140
MINI_AIG_START_SIZE
#define MINI_AIG_START_SIZE
Definition miniaig.h:42
Mini_Aig_t_
Definition miniaig.h:50
Mini_Aig_t_::pArray
int * pArray
Definition miniaig.h:54
Mini_Aig_t_::nCap
int nCap
Definition miniaig.h:51
Mini_Aig_t_::nSize
int nSize
Definition miniaig.h:52
Mini_Aig_t_::nRegs
int nRegs
Definition miniaig.h:53
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
strlen
int strlen()