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