1 /**CFile****************************************************************
2
3 FileName [gia.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "misc/extra/extra.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis []
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Gia_ManPrintStateEncoding(Vec_Vec_t * vCodes,int nBits)46 void Gia_ManPrintStateEncoding( Vec_Vec_t * vCodes, int nBits )
47 {
48 char * pBuffer;
49 Vec_Int_t * vVec;
50 int i, k, Bit;
51 pBuffer = ABC_ALLOC( char, nBits + 1 );
52 pBuffer[nBits] = 0;
53 Vec_VecForEachLevelInt( vCodes, vVec, i )
54 {
55 printf( "%6d : ", i+1 );
56 memset( pBuffer, '-', (size_t)nBits );
57 Vec_IntForEachEntry( vVec, Bit, k )
58 {
59 assert( Bit < nBits );
60 pBuffer[Bit] = '1';
61 }
62 printf( "%s\n", pBuffer );
63 }
64 ABC_FREE( pBuffer );
65 }
66
67 /**Function*************************************************************
68
69 Synopsis []
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ***********************************************************************/
Gia_ManCreateOrGate(Gia_Man_t * p,Vec_Int_t * vLits)78 int Gia_ManCreateOrGate( Gia_Man_t * p, Vec_Int_t * vLits )
79 {
80 if ( Vec_IntSize(vLits) == 0 )
81 return 0;
82 while ( Vec_IntSize(vLits) > 1 )
83 {
84 int i, k = 0, Lit1, Lit2, LitRes;
85 Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i )
86 {
87 LitRes = Gia_ManHashOr( p, Lit1, Lit2 );
88 Vec_IntWriteEntry( vLits, k++, LitRes );
89 }
90 if ( Vec_IntSize(vLits) & 1 )
91 Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) );
92 Vec_IntShrink( vLits, k );
93 }
94 assert( Vec_IntSize(vLits) == 1 );
95 return Vec_IntEntry(vLits, 0);
96 }
97
98 /**Function*************************************************************
99
100 Synopsis []
101
102 Description []
103
104 SideEffects []
105
106 SeeAlso []
107
108 ***********************************************************************/
Gia_ManAssignCodes(int kHot,int nStates,int * pnBits)109 Vec_Vec_t * Gia_ManAssignCodes( int kHot, int nStates, int * pnBits )
110 {
111 Vec_Vec_t * vCodes;
112 int s, i1, i2, i3, i4, i5, nBits;
113 assert( nStates > 0 );
114 assert( kHot >= 1 && kHot <= 5 );
115 vCodes = Vec_VecStart( nStates );
116 *pnBits = -1;
117 if ( kHot == 1 )
118 {
119 for ( i1 = 0; i1 < nStates; i1++ )
120 Vec_VecPushInt( vCodes, i1, i1 );
121 *pnBits = nStates;
122 return vCodes;
123 }
124 if ( kHot == 2 )
125 {
126 for ( nBits = kHot; nBits < ABC_INFINITY; nBits++ )
127 if ( nBits * (nBits-1) / 2 >= nStates )
128 break;
129 *pnBits = nBits;
130 s = 0;
131 for ( i1 = 0; i1 < nBits; i1++ )
132 for ( i2 = i1 + 1; i2 < nBits; i2++ )
133 {
134 Vec_VecPushInt( vCodes, s, i1 );
135 Vec_VecPushInt( vCodes, s, i2 );
136 if ( ++s == nStates )
137 return vCodes;
138 }
139 }
140 if ( kHot == 3 )
141 {
142 for ( nBits = kHot; nBits < ABC_INFINITY; nBits++ )
143 if ( nBits * (nBits-1) * (nBits-2) / 6 >= nStates )
144 break;
145 *pnBits = nBits;
146 s = 0;
147 for ( i1 = 0; i1 < nBits; i1++ )
148 for ( i2 = i1 + 1; i2 < nBits; i2++ )
149 for ( i3 = i2 + 1; i3 < nBits; i3++ )
150 {
151 Vec_VecPushInt( vCodes, s, i1 );
152 Vec_VecPushInt( vCodes, s, i2 );
153 Vec_VecPushInt( vCodes, s, i3 );
154 if ( ++s == nStates )
155 return vCodes;
156 }
157 }
158 if ( kHot == 4 )
159 {
160 for ( nBits = kHot; nBits < ABC_INFINITY; nBits++ )
161 if ( nBits * (nBits-1) * (nBits-2) * (nBits-3) / 24 >= nStates )
162 break;
163 *pnBits = nBits;
164 s = 0;
165 for ( i1 = 0; i1 < nBits; i1++ )
166 for ( i2 = i1 + 1; i2 < nBits; i2++ )
167 for ( i3 = i2 + 1; i3 < nBits; i3++ )
168 for ( i4 = i3 + 1; i4 < nBits; i4++ )
169 {
170 Vec_VecPushInt( vCodes, s, i1 );
171 Vec_VecPushInt( vCodes, s, i2 );
172 Vec_VecPushInt( vCodes, s, i3 );
173 Vec_VecPushInt( vCodes, s, i4 );
174 if ( ++s == nStates )
175 return vCodes;
176 }
177 }
178 if ( kHot == 5 )
179 {
180 for ( nBits = kHot; nBits < ABC_INFINITY; nBits++ )
181 if ( nBits * (nBits-1) * (nBits-2) * (nBits-3) * (nBits-4) / 120 >= nStates )
182 break;
183 *pnBits = nBits;
184 s = 0;
185 for ( i1 = 0; i1 < nBits; i1++ )
186 for ( i2 = i1 + 1; i2 < nBits; i2++ )
187 for ( i3 = i2 + 1; i3 < nBits; i3++ )
188 for ( i4 = i3 + 1; i4 < nBits; i4++ )
189 for ( i5 = i4 + 1; i5 < nBits; i5++ )
190 {
191 Vec_VecPushInt( vCodes, s, i1 );
192 Vec_VecPushInt( vCodes, s, i2 );
193 Vec_VecPushInt( vCodes, s, i3 );
194 Vec_VecPushInt( vCodes, s, i4 );
195 Vec_VecPushInt( vCodes, s, i5 );
196 if ( ++s == nStates )
197 return vCodes;
198 }
199 }
200 assert( 0 );
201 return NULL;
202 }
203
204 /**Function*************************************************************
205
206 Synopsis []
207
208 Description []
209
210 SideEffects []
211
212 SeeAlso []
213
214 ***********************************************************************/
Gia_ManStgKHot(Vec_Int_t * vLines,int nIns,int nOuts,int nStates,int kHot,int fVerbose)215 Gia_Man_t * Gia_ManStgKHot( Vec_Int_t * vLines, int nIns, int nOuts, int nStates, int kHot, int fVerbose )
216 {
217 Gia_Man_t * p, * pTemp;
218 Vec_Int_t * vInMints, * vCurs, * vVec;
219 Vec_Vec_t * vLitsNext, * vLitsOuts, * vCodes;
220 int i, b, k, nBits, LitC, Lit;
221 assert( Vec_IntSize(vLines) % 4 == 0 );
222
223 // produce state encoding
224 vCodes = Gia_ManAssignCodes( kHot, nStates, &nBits );
225 assert( Vec_VecSize(vCodes) == nStates );
226 if ( fVerbose )
227 Gia_ManPrintStateEncoding( vCodes, nBits );
228
229 // start manager
230 p = Gia_ManStart( 10000 );
231 p->pName = Abc_UtilStrsav( "stg" );
232 for ( i = 0; i < nIns + nBits; i++ )
233 Gia_ManAppendCi(p);
234
235 // create input minterms
236 Gia_ManHashAlloc( p );
237 vInMints = Vec_IntAlloc( 1 << nIns );
238 for ( i = 0; i < (1 << nIns); i++ )
239 {
240 for ( Lit = 1, b = 0; b < nIns; b++ )
241 Lit = Gia_ManHashAnd( p, Lit, Abc_Var2Lit( b+1, !((i >> b) & 1) ) );
242 Vec_IntPush( vInMints, Lit );
243 }
244
245 // create current states
246 vCurs = Vec_IntAlloc( nStates );
247 Vec_VecForEachLevelInt( vCodes, vVec, i )
248 {
249 Lit = 1;
250 Vec_IntForEachEntry( vVec, b, k )
251 {
252 assert( b >= 0 && b < nBits );
253 Lit = Gia_ManHashAnd( p, Lit, Abc_Var2Lit(1+nIns+b, (b<kHot)) );
254 }
255 Vec_IntPush( vCurs, Lit );
256 }
257
258 // go through the lines
259 vLitsNext = Vec_VecStart( nBits );
260 vLitsOuts = Vec_VecStart( nOuts );
261 for ( i = 0; i < Vec_IntSize(vLines); )
262 {
263 int iMint = Vec_IntEntry(vLines, i++);
264 int iCur = Vec_IntEntry(vLines, i++);
265 int iNext = Vec_IntEntry(vLines, i++);
266 int iOut = Vec_IntEntry(vLines, i++);
267 assert( iMint >= 0 && iMint < (1<<nIns) );
268 assert( iCur >= 0 && iCur < nStates );
269 assert( iNext >= 0 && iNext < nStates );
270 assert( iOut >= 0 && iOut < (1<<nOuts) );
271 // create condition
272 LitC = Gia_ManHashAnd( p, Vec_IntEntry(vInMints, iMint), Vec_IntEntry(vCurs, iCur) );
273 // update next state
274 // Vec_VecPushInt( vLitsNext, iNext, LitC );
275 vVec = (Vec_Int_t *)Vec_VecEntryInt( vCodes, iNext );
276 Vec_IntForEachEntry( vVec, b, k )
277 Vec_VecPushInt( vLitsNext, b, LitC );
278 // update outputs
279 for ( b = 0; b < nOuts; b++ )
280 if ( (iOut >> b) & 1 )
281 Vec_VecPushInt( vLitsOuts, b, LitC );
282 }
283 Vec_IntFree( vInMints );
284 Vec_IntFree( vCurs );
285 Vec_VecFree( vCodes );
286
287 // create POs
288 Vec_VecForEachLevelInt( vLitsOuts, vVec, b )
289 Gia_ManAppendCo( p, Gia_ManCreateOrGate(p, vVec) );
290 Vec_VecFree( vLitsOuts );
291
292 // create next states
293 Vec_VecForEachLevelInt( vLitsNext, vVec, b )
294 Gia_ManAppendCo( p, Abc_LitNotCond( Gia_ManCreateOrGate(p, vVec), (b<kHot) ) );
295 Vec_VecFree( vLitsNext );
296
297 Gia_ManSetRegNum( p, nBits );
298 Gia_ManHashStop( p );
299
300 p = Gia_ManCleanup( pTemp = p );
301 Gia_ManStop( pTemp );
302 assert( !Gia_ManHasDangling(p) );
303 return p;
304 }
305
306 /**Function*************************************************************
307
308 Synopsis []
309
310 Description []
311
312 SideEffects []
313
314 SeeAlso []
315
316 ***********************************************************************/
Gia_ManStgOneHot(Vec_Int_t * vLines,int nIns,int nOuts,int nStates)317 Gia_Man_t * Gia_ManStgOneHot( Vec_Int_t * vLines, int nIns, int nOuts, int nStates )
318 {
319 Gia_Man_t * p, * pTemp;
320 Vec_Int_t * vInMints, * vCurs, * vVec;
321 Vec_Vec_t * vLitsNext, * vLitsOuts;
322 int i, b, LitC, Lit;
323 assert( Vec_IntSize(vLines) % 4 == 0 );
324
325 // start manager
326 p = Gia_ManStart( 10000 );
327 p->pName = Abc_UtilStrsav( "stg" );
328 for ( i = 0; i < nIns + nStates; i++ )
329 Gia_ManAppendCi(p);
330
331 // create input minterms
332 Gia_ManHashAlloc( p );
333 vInMints = Vec_IntAlloc( 1 << nIns );
334 for ( i = 0; i < (1 << nIns); i++ )
335 {
336 for ( Lit = 1, b = 0; b < nIns; b++ )
337 Lit = Gia_ManHashAnd( p, Lit, Abc_Var2Lit( b+1, !((i >> b) & 1) ) );
338 Vec_IntPush( vInMints, Lit );
339 }
340
341 // create current states
342 vCurs = Vec_IntAlloc( nStates );
343 for ( i = 0; i < nStates; i++ )
344 Vec_IntPush( vCurs, Abc_Var2Lit( 1+nIns+i, !i ) );
345
346 // go through the lines
347 vLitsNext = Vec_VecStart( nStates );
348 vLitsOuts = Vec_VecStart( nOuts );
349 for ( i = 0; i < Vec_IntSize(vLines); )
350 {
351 int iMint = Vec_IntEntry(vLines, i++);
352 int iCur = Vec_IntEntry(vLines, i++) - 1;
353 int iNext = Vec_IntEntry(vLines, i++) - 1;
354 int iOut = Vec_IntEntry(vLines, i++);
355 assert( iMint >= 0 && iMint < (1<<nIns) );
356 assert( iCur >= 0 && iCur < nStates );
357 assert( iNext >= 0 && iNext < nStates );
358 assert( iOut >= 0 && iOut < (1<<nOuts) );
359 // create condition
360 LitC = Gia_ManHashAnd( p, Vec_IntEntry(vInMints, iMint), Vec_IntEntry(vCurs, iCur) );
361 // update next state
362 // Lit = Gia_ManHashOr( p, LitC, Vec_IntEntry(vNexts, iNext) );
363 // Vec_IntWriteEntry( vNexts, iNext, Lit );
364 Vec_VecPushInt( vLitsNext, iNext, LitC );
365 // update outputs
366 for ( b = 0; b < nOuts; b++ )
367 if ( (iOut >> b) & 1 )
368 {
369 // Lit = Gia_ManHashOr( p, LitC, Vec_IntEntry(vOuts, b) );
370 // Vec_IntWriteEntry( vOuts, b, Lit );
371 Vec_VecPushInt( vLitsOuts, b, LitC );
372 }
373 }
374 Vec_IntFree( vInMints );
375 Vec_IntFree( vCurs );
376
377 // create POs
378 Vec_VecForEachLevelInt( vLitsOuts, vVec, i )
379 Gia_ManAppendCo( p, Gia_ManCreateOrGate(p, vVec) );
380 Vec_VecFree( vLitsOuts );
381
382 // create next states
383 Vec_VecForEachLevelInt( vLitsNext, vVec, i )
384 Gia_ManAppendCo( p, Abc_LitNotCond( Gia_ManCreateOrGate(p, vVec), !i ) );
385 Vec_VecFree( vLitsNext );
386
387 Gia_ManSetRegNum( p, nStates );
388 Gia_ManHashStop( p );
389
390 p = Gia_ManCleanup( pTemp = p );
391 Gia_ManStop( pTemp );
392 assert( !Gia_ManHasDangling(p) );
393 return p;
394 }
395
396 /**Function*************************************************************
397
398 Synopsis []
399
400 Description []
401
402 SideEffects []
403
404 SeeAlso []
405
406 ***********************************************************************/
Gia_ManStgPrint(FILE * pFile,Vec_Int_t * vLines,int nIns,int nOuts,int nStates)407 void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates )
408 {
409 int i, nDigits = Abc_Base10Log( nStates );
410 assert( Vec_IntSize(vLines) % 4 == 0 );
411 for ( i = 0; i < Vec_IntSize(vLines); i += 4 )
412 {
413 int iMint = Vec_IntEntry(vLines, i );
414 int iCur = Vec_IntEntry(vLines, i+1) - 1;
415 int iNext = Vec_IntEntry(vLines, i+2) - 1;
416 int iOut = Vec_IntEntry(vLines, i+3);
417 assert( iMint >= 0 && iMint < (1<<nIns) );
418 assert( iCur >= 0 && iCur < nStates );
419 assert( iNext >= 0 && iNext < nStates );
420 assert( iOut >= 0 && iOut < (1<<nOuts) );
421 Extra_PrintBinary( pFile, (unsigned *)Vec_IntEntryP(vLines, i), nIns );
422 fprintf( pFile, " %*d", nDigits, Vec_IntEntry(vLines, i+1) );
423 fprintf( pFile, " %*d ", nDigits, Vec_IntEntry(vLines, i+2) );
424 Extra_PrintBinary( pFile, (unsigned *)Vec_IntEntryP(vLines, i+3), nOuts );
425 fprintf( pFile, "\n" );
426 }
427 }
428
429 /**Function*************************************************************
430
431 Synopsis []
432
433 Description []
434
435 SideEffects []
436
437 SeeAlso []
438
439 ***********************************************************************/
Gia_ManStgReadLines(char * pFileName,int * pnIns,int * pnOuts,int * pnStates)440 Vec_Int_t * Gia_ManStgReadLines( char * pFileName, int * pnIns, int * pnOuts, int * pnStates )
441 {
442 Vec_Int_t * vLines;
443 char pBuffer[1000];
444 char * pToken;
445 int Number, nInputs = -1, nOutputs = -1, nStates = 1;
446 FILE * pFile;
447 if ( !strcmp(pFileName + strlen(pFileName) - 3, "aig") )
448 {
449 printf( "Input file \"%s\" has extension \"%s\".\n", pFileName, "aig" );
450 return NULL;
451 }
452 pFile = fopen( pFileName, "rb" );
453 if ( pFile == NULL )
454 {
455 printf( "Cannot open file \"%s\".\n", pFileName );
456 return NULL;
457 }
458 vLines = Vec_IntAlloc( 1000 );
459 while ( fgets( pBuffer, 1000, pFile ) != NULL )
460 {
461 if ( pBuffer[0] == '.' || pBuffer[0] == '#' )
462 continue;
463 // read condition
464 pToken = strtok( pBuffer, " \r\n" );
465 if ( nInputs == -1 )
466 nInputs = strlen(pToken);
467 else
468 assert( nInputs == (int)strlen(pToken) );
469 Number = Extra_ReadBinary( pToken );
470 Vec_IntPush( vLines, Number );
471 // read current state
472 pToken = strtok( NULL, " \r\n" );
473 Vec_IntPush( vLines, atoi(pToken) );
474 nStates = Abc_MaxInt( nStates, Vec_IntEntryLast(vLines)+1 );
475 // read next state
476 pToken = strtok( NULL, " \r\n" );
477 Vec_IntPush( vLines, atoi(pToken) );
478 // read output
479 pToken = strtok( NULL, " \r\n" );
480 if ( nOutputs == -1 )
481 nOutputs = strlen(pToken);
482 else
483 assert( nOutputs == (int)strlen(pToken) );
484 Number = Extra_ReadBinary( pToken );
485 Vec_IntPush( vLines, Number );
486 }
487 fclose( pFile );
488 if ( pnIns )
489 *pnIns = nInputs;
490 if ( pnOuts )
491 *pnOuts = nOutputs;
492 if ( pnStates )
493 *pnStates = nStates;
494 return vLines;
495 }
496
497 /**Function*************************************************************
498
499 Synopsis []
500
501 Description []
502
503 SideEffects []
504
505 SeeAlso []
506
507 ***********************************************************************/
Gia_ManStgRead(char * pFileName,int kHot,int fVerbose)508 Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose )
509 {
510 Gia_Man_t * p;
511 Vec_Int_t * vLines;
512 int nIns, nOuts, nStates;
513 vLines = Gia_ManStgReadLines( pFileName, &nIns, &nOuts, &nStates );
514 if ( vLines == NULL )
515 return NULL;
516 // p = Gia_ManStgOneHot( vLines, nIns, nOuts, nStates );
517 p = Gia_ManStgKHot( vLines, nIns, nOuts, nStates, kHot, fVerbose );
518 Vec_IntFree( vLines );
519 return p;
520 }
521
522 ////////////////////////////////////////////////////////////////////////
523 /// END OF FILE ///
524 ////////////////////////////////////////////////////////////////////////
525
526
527 ABC_NAMESPACE_IMPL_END
528
529