ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaStg.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "misc/extra/extra.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
34
46void 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
78int 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
109Vec_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
215Gia_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
317Gia_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
407void 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
440Vec_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
508Gia_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
525
526
527ABC_NAMESPACE_IMPL_END
528
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
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
Extra_ReadBinary
unsigned Extra_ReadBinary(char *Buffer)
Definition extraUtilFile.c:489
Gia_ManAssignCodes
Vec_Vec_t * Gia_ManAssignCodes(int kHot, int nStates, int *pnBits)
Definition giaStg.c:109
Gia_ManPrintStateEncoding
ABC_NAMESPACE_IMPL_START void Gia_ManPrintStateEncoding(Vec_Vec_t *vCodes, int nBits)
DECLARATIONS ///.
Definition giaStg.c:46
Gia_ManStgKHot
Gia_Man_t * Gia_ManStgKHot(Vec_Int_t *vLines, int nIns, int nOuts, int nStates, int kHot, int fVerbose)
Definition giaStg.c:215
Gia_ManStgOneHot
Gia_Man_t * Gia_ManStgOneHot(Vec_Int_t *vLines, int nIns, int nOuts, int nStates)
Definition giaStg.c:317
Gia_ManStgReadLines
Vec_Int_t * Gia_ManStgReadLines(char *pFileName, int *pnIns, int *pnOuts, int *pnStates)
Definition giaStg.c:440
Gia_ManStgPrint
void Gia_ManStgPrint(FILE *pFile, Vec_Int_t *vLines, int nIns, int nOuts, int nStates)
Definition giaStg.c:407
Gia_ManStgRead
Gia_Man_t * Gia_ManStgRead(char *pFileName, int kHot, int fVerbose)
Definition giaStg.c:508
Gia_ManCreateOrGate
int Gia_ManCreateOrGate(Gia_Man_t *p, Vec_Int_t *vLits)
Definition giaStg.c:78
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
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_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:621
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
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_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
strlen
int strlen()
strcmp
int strcmp()
strtok
char * strtok()
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_VecForEachLevelInt
#define Vec_VecForEachLevelInt(vGlob, vVec, i)
Definition vecVec.h:71
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42