1 /**CFile****************************************************************
2
3 FileName [dau.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware unmapping.]
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: dau.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "dauInt.h"
22 #include "misc/util/utilTruth.h"
23 #include "misc/extra/extra.h"
24 #include "bool/lucky/lucky.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis []
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Dau_TruthEnum(int nVars)48 void Dau_TruthEnum(int nVars)
49 {
50 int fUseTable = 1;
51 abctime clk = Abc_Clock();
52 int nSizeLog = (1<<nVars) -2;
53 int nSizeW = 1 << nSizeLog;
54 int nPerms = Extra_Factorial( nVars );
55 int nMints = 1 << nVars;
56 int * pPerm = Extra_PermSchedule( nVars );
57 int * pComp = Extra_GreyCodeSchedule( nVars );
58 word nFuncs = ((word)1 << (((word)1 << nVars)-1));
59 word * pPres = ABC_CALLOC( word, 1 << ((1<<nVars)-7) );
60 unsigned * pTable = fUseTable ? (unsigned *)ABC_CALLOC(word, nSizeW) : NULL;
61 Vec_Int_t * vNpns = Vec_IntAlloc( 1000 );
62 word tMask = Abc_Tt6Mask( 1 << nVars );
63 word tTemp, tCur;
64 int i, k;
65 if ( pPres == NULL )
66 {
67 printf( "Cannot alloc memory for marks.\n" );
68 return;
69 }
70 if ( pTable == NULL )
71 printf( "Cannot alloc memory for table.\n" );
72 for ( tCur = 0; tCur < nFuncs; tCur++ )
73 {
74 if ( (tCur & 0x3FFFF) == 0 )
75 {
76 printf( "Finished %08x. Classes = %6d. ", (int)tCur, Vec_IntSize(vNpns) );
77 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
78 fflush(stdout);
79 }
80 if ( Abc_TtGetBit(pPres, (int)tCur) )
81 continue;
82 //Extra_PrintBinary( stdout, (unsigned *)&tCur, 16 ); printf( " %04x\n", (int)tCur );
83 //Dau_DsdPrintFromTruth( &tCur, 4 ); printf( "\n" );
84 Vec_IntPush( vNpns, (int)tCur );
85 tTemp = tCur;
86 for ( i = 0; i < nPerms; i++ )
87 {
88 for ( k = 0; k < nMints; k++ )
89 {
90 if ( tCur < nFuncs )
91 {
92 if ( pTable ) pTable[(int)tCur] = tTemp;
93 Abc_TtSetBit( pPres, (int)tCur );
94 }
95 if ( (tMask & ~tCur) < nFuncs )
96 {
97 if ( pTable ) pTable[(int)(tMask & ~tCur)] = tTemp;
98 Abc_TtSetBit( pPres, (int)(tMask & ~tCur) );
99 }
100 tCur = Abc_Tt6Flip( tCur, pComp[k] );
101 }
102 tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[i] );
103 }
104 assert( tTemp == tCur );
105 }
106 printf( "Computed %d NPN classes of %d variables. ", Vec_IntSize(vNpns), nVars );
107 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
108 fflush(stdout);
109 Vec_IntFree( vNpns );
110 ABC_FREE( pPres );
111 ABC_FREE( pPerm );
112 ABC_FREE( pComp );
113 // write into file
114 if ( pTable )
115 {
116 FILE * pFile;
117 int RetValue;
118 char pFileName[200];
119 sprintf( pFileName, "tableW%d.data", nSizeLog );
120 pFile = fopen( pFileName, "wb" );
121 RetValue = fwrite( pTable, 8, nSizeW, pFile );
122 RetValue = 0;
123 fclose( pFile );
124 ABC_FREE( pTable );
125 }
126 }
127
128
129 /**Function*************************************************************
130
131 Synopsis []
132
133 Description []
134
135 SideEffects []
136
137 SeeAlso []
138
139 ***********************************************************************/
Dau_ReadFile(char * pFileName,int nSizeW)140 unsigned * Dau_ReadFile( char * pFileName, int nSizeW )
141 {
142 abctime clk = Abc_Clock();
143 FILE * pFile = fopen( pFileName, "rb" );
144 unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW);
145 int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
146 RetValue = 0;
147 if ( pFile )
148 {
149 printf( "Finished reading file \"%s\".\n", pFileName );
150 fclose( pFile );
151 }
152 else
153 printf( "Cannot open input file \"%s\".\n", pFileName );
154 Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
155 return p;
156 }
Dau_AddFunction(word tCur,int nVars,unsigned * pTable,Vec_Int_t * vNpns,Vec_Int_t * vNpns_)157 int Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns, Vec_Int_t * vNpns_ )
158 {
159 int Digit = (1 << nVars)-1;
160 word tMask = Abc_Tt6Mask( 1 << nVars );
161 word tNorm = (tCur >> Digit) & 1 ? ~tCur : tCur;
162 unsigned t = (unsigned)(tNorm & tMask);
163 unsigned tRep = pTable[t] & 0x7FFFFFFF;
164 unsigned tRep2 = pTable[tRep];
165 assert( ((tNorm >> Digit) & 1) == 0 );
166 if ( (tRep2 >> 31) == 0 ) // first time
167 {
168 Vec_IntPush( vNpns, tRep2 );
169 if ( Abc_TtSupportSize(&tCur, nVars) < nVars )
170 Vec_IntPush( vNpns_, tRep2 );
171 pTable[tRep] = tRep2 | (1 << 31);
172 return tRep2;
173 }
174 return 0;
175 }
Dau_NetworkEnum(int nVars)176 void Dau_NetworkEnum(int nVars)
177 {
178 abctime clk = Abc_Clock();
179 int Limit = 2;
180 int UseTwo = 0;
181 int nSizeLog = (1<<nVars) -2;
182 int nSizeW = 1 << nSizeLog;
183 char pFileName[200];
184 unsigned * pTable;
185 Vec_Wec_t * vNpns = Vec_WecStart( 32 );
186 Vec_Wec_t * vNpns_ = Vec_WecStart( 32 );
187 int i, v, u, g, k, m, n, Res, Entry;
188 unsigned Inv = (unsigned)Abc_Tt6Mask(1 << (nVars-1));
189 sprintf( pFileName, "tableW%d.data", nSizeLog );
190 pTable = Dau_ReadFile( pFileName, nSizeW );
191 // create constant function and buffer/inverter function
192 pTable[0] |= (1 << 31);
193 pTable[Inv] |= (1 << 31);
194 Vec_IntPushTwo( Vec_WecEntry(vNpns, 0), 0, Inv );
195 Vec_IntPushTwo( Vec_WecEntry(vNpns_, 0), 0, Inv );
196 printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
197 0, Vec_IntSize(Vec_WecEntry(vNpns, 0)), Vec_WecSizeSize(vNpns),
198 Vec_IntSize(Vec_WecEntry(vNpns_, 0)), Vec_WecSizeSize(vNpns_) );
199 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
200 // numerate other functions based on how many nodes they have
201 for ( n = 1; n < 32; n++ )
202 {
203 Vec_Int_t * vFuncsN2 = n > 1 ? Vec_WecEntry( vNpns, n-2 ) : NULL;
204 Vec_Int_t * vFuncsN1 = Vec_WecEntry( vNpns, n-1 );
205 Vec_Int_t * vFuncsN = Vec_WecEntry( vNpns, n );
206 Vec_Int_t * vFuncsN_ = Vec_WecEntry( vNpns_,n );
207 Vec_IntForEachEntry( vFuncsN1, Entry, i )
208 {
209 word uTruth = (((word)Entry) << 32) | (word)Entry;
210 int nSupp = Abc_TtSupportSize( &uTruth, nVars );
211 assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
212 //printf( "Exploring function %4d with %d vars: ", i, nSupp );
213 //printf( " %04x\n", (int)uTruth );
214 //Dau_DsdPrintFromTruth( &uTruth, 4 );
215 for ( v = 0; v < nSupp; v++ )
216 {
217 word tGate, tCur;
218 word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
219 word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
220 for ( g = 0; g < Limit; g++ )
221 {
222 if ( nSupp < nVars )
223 {
224 if ( g == 0 )
225 {
226 tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
227 tCur = (tGate & Cof1) | (~tGate & Cof0);
228 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
229
230 tCur = (tGate & Cof0) | (~tGate & Cof1);
231 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
232 }
233 else
234 {
235 tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
236 tCur = (tGate & Cof1) | (~tGate & Cof0);
237 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
238 }
239 }
240 }
241 for ( g = 0; g < Limit; g++ )
242 {
243 // add one cross bar
244 for ( k = 0; k < nSupp; k++ ) if ( k != v )
245 {
246 if ( g == 0 )
247 {
248 tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
249 tCur = (tGate & Cof1) | (~tGate & Cof0);
250 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
251
252 tCur = (tGate & Cof0) | (~tGate & Cof1);
253 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
254
255 tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
256 tCur = (tGate & Cof1) | (~tGate & Cof0);
257 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
258
259 tCur = (tGate & Cof0) | (~tGate & Cof1);
260 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
261 }
262 else
263 {
264 tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
265 tCur = (tGate & Cof1) | (~tGate & Cof0);
266 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
267 }
268 }
269 }
270 for ( g = 0; g < Limit; g++ )
271 {
272 // add two cross bars
273 for ( k = 0; k < nSupp; k++ ) if ( k != v )
274 for ( m = k+1; m < nSupp; m++ ) if ( m != v )
275 {
276 if ( g == 0 )
277 {
278 tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
279 tCur = (tGate & Cof1) | (~tGate & Cof0);
280 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
281
282 tCur = (tGate & Cof0) | (~tGate & Cof1);
283 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
284
285 tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
286 tCur = (tGate & Cof1) | (~tGate & Cof0);
287 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
288
289 tCur = (tGate & Cof0) | (~tGate & Cof1);
290 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
291
292 tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
293 tCur = (tGate & Cof1) | (~tGate & Cof0);
294 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
295
296 tCur = (tGate & Cof0) | (~tGate & Cof1);
297 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
298
299 tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
300 tCur = (tGate & Cof1) | (~tGate & Cof0);
301 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
302
303 tCur = (tGate & Cof0) | (~tGate & Cof1);
304 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
305 }
306 else
307 {
308 tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
309 tCur = (tGate & Cof1) | (~tGate & Cof0);
310 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
311 }
312 }
313 }
314 }
315 }
316 if ( UseTwo && vFuncsN2 )
317 Vec_IntForEachEntry( vFuncsN2, Entry, i )
318 {
319 word uTruth = (((word)Entry) << 32) | (word)Entry;
320 int nSupp = Abc_TtSupportSize( &uTruth, nVars );
321 assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
322 //printf( "Exploring function %4d with %d vars: ", i, nSupp );
323 //printf( " %04x\n", (int)uTruth );
324 //Dau_DsdPrintFromTruth( &uTruth, 4 );
325 for ( v = 0; v < nSupp; v++ )
326 // for ( u = v+1; u < nSupp; u++ ) if ( u != v )
327 for ( u = 0; u < nSupp; u++ ) if ( u != v )
328 {
329 word tGate1, tGate2, tCur;
330 word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
331 word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
332
333 word Cof00 = Abc_Tt6Cofactor0( Cof0, nVars-1-u );
334 word Cof01 = Abc_Tt6Cofactor1( Cof0, nVars-1-u );
335 word Cof10 = Abc_Tt6Cofactor0( Cof1, nVars-1-u );
336 word Cof11 = Abc_Tt6Cofactor1( Cof1, nVars-1-u );
337
338 tGate1 = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-u];
339 tGate2 = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-u];
340
341 Cof0 = (tGate2 & Cof00) | (~tGate2 & Cof01);
342 Cof1 = (tGate2 & Cof10) | (~tGate2 & Cof11);
343
344 tCur = (tGate1 & Cof1) | (~tGate1 & Cof0);
345 Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
346 if ( Res )
347 printf( "Found function %d\n", Res );
348
349 tCur = (tGate1 & Cof0) | (~tGate1 & Cof1);
350 Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
351 if ( Res )
352 printf( "Found function %d\n", Res );
353 }
354 }
355 printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
356 n, Vec_IntSize(vFuncsN), Vec_WecSizeSize(vNpns), Vec_IntSize(vFuncsN_), Vec_WecSizeSize(vNpns_) );
357 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
358 fflush(stdout);
359 if ( Vec_IntSize(vFuncsN) == 0 )
360 break;
361 }
362 // printf( "Functions with 7 nodes:\n" );
363 // Vec_IntForEachEntry( Vec_WecEntry(vNpns_,7), Entry, i )
364 // printf( "%04x ", Entry );
365 // printf( "\n" );
366
367 Vec_WecFree( vNpns );
368 Vec_WecFree( vNpns_ );
369 ABC_FREE( pTable );
370 Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
371 fflush(stdout);
372 }
Dau_NetworkEnumTest()373 void Dau_NetworkEnumTest()
374 {
375 //Dau_TruthEnum(3);
376 Dau_NetworkEnum(4);
377 }
378
379
380
381 /**Function*************************************************************
382
383 Synopsis [Count the number of symmetric pairs.]
384
385 Description []
386
387 SideEffects []
388
389 SeeAlso []
390
391 ***********************************************************************/
Dau_CountSymms(word t,int nVars)392 int Dau_CountSymms( word t, int nVars )
393 {
394 word Cof0, Cof1;
395 int i, j, nPairs = 0;
396 for ( i = 0; i < nVars; i++ )
397 for ( j = i+1; j < nVars; j++ )
398 nPairs += Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1);
399 return nPairs;
400 }
Dau_CountSymms2(word t,int nVars)401 int Dau_CountSymms2( word t, int nVars )
402 {
403 word Cof0, Cof1;
404 int i, j, SymVars = 0;
405 for ( i = 0; i < nVars; i++ )
406 for ( j = i+1; j < nVars; j++ )
407 if ( Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1) )
408 SymVars |= (1 << j);
409 return SymVars;
410 }
Dau_CountCompl1(word t,int v,int nVars)411 int Dau_CountCompl1( word t, int v, int nVars )
412 {
413 word tNew = Abc_Tt6Flip(t, v);
414 int k;
415 if ( tNew == ~t )
416 return 1;
417 for ( k = 0; k < nVars; k++ ) if ( k != v )
418 if ( tNew == Abc_Tt6Flip(t, k) )
419 return 1;
420 return 0;
421 }
Dau_CountCompl(word t,int nVars)422 int Dau_CountCompl( word t, int nVars )
423 {
424 int i, nPairs = 0;
425 for ( i = 0; i < nVars; i++ )
426 nPairs += Dau_CountCompl1(t, i, nVars);
427 return nPairs;
428 }
429
430 /**Function*************************************************************
431
432 Synopsis [Performs exact canonicization of semi-canonical classes.]
433
434 Description []
435
436 SideEffects []
437
438 SeeAlso []
439
440 ***********************************************************************/
Dau_ExactNpnForClasses(Vec_Mem_t * vTtMem,Vec_Int_t * vNodSup,int nVars,int nInputs)441 Vec_Wrd_t * Dau_ExactNpnForClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs )
442 {
443 Vec_Wrd_t * vCanons = Vec_WrdStart( Vec_IntSize(vNodSup) );
444 word pAuxWord[1024], pAuxWord1[1024];
445 word uTruth; int i, Entry;
446 permInfo * pi = setPermInfoPtr(nVars);
447 Vec_IntForEachEntry( vNodSup, Entry, i )
448 {
449 if ( (Entry & 0xF) > nVars )
450 continue;
451 uTruth = *Vec_MemReadEntry( vTtMem, i );
452 simpleMinimal(&uTruth, pAuxWord, pAuxWord1, pi, nVars);
453 Vec_WrdWriteEntry( vCanons, i, uTruth );
454 }
455 freePermInfoPtr(pi);
456 return vCanons;
457 }
Dau_ExactNpnPrint(Vec_Mem_t * vTtMem,Vec_Int_t * vNodSup,int nVars,int nInputs,int nNodesMax)458 void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs, int nNodesMax )
459 {
460 abctime clk = Abc_Clock(); int n, nTotal = 0;
461 Vec_Wrd_t * vCanons = Dau_ExactNpnForClasses( vTtMem, vNodSup, nVars, nInputs );
462 Vec_Mem_t * vTtMem2 = Vec_MemAlloc( Vec_MemEntrySize(vTtMem), 10 );
463 Vec_MemHashAlloc( vTtMem2, 1<<10 );
464 Abc_PrintTime( 1, "Exact NPN computation time", Abc_Clock() - clk );
465 printf( "Final results:\n" );
466 for ( n = 0; n <= nNodesMax; n++ )
467 {
468 int i, Entry, Entry2, nEntries2, Counter = 0, Counter2 = 0;
469 Vec_IntForEachEntry( vNodSup, Entry, i )
470 {
471 if ( (Entry & 0xF) > nVars || (Entry >> 16) != n )
472 continue;
473 Counter++;
474 nEntries2 = Vec_MemEntryNum(vTtMem2);
475 Entry2 = Vec_MemHashInsert( vTtMem2, Vec_WrdEntryP(vCanons, i) );
476 if ( nEntries2 == Vec_MemEntryNum(vTtMem2) ) // found in the table - not new
477 continue;
478 Counter2++;
479 }
480 nTotal += Counter2;
481 printf( "Nodes = %2d. ", n );
482 printf( "Semi-canonical = %8d. ", Counter );
483 printf( "Canonical = %8d. ", Counter2 );
484 printf( "Total = %8d.", nTotal );
485 printf( "\n" );
486 }
487 Vec_MemHashFree( vTtMem2 );
488 Vec_MemFreeP( &vTtMem2 );
489 Vec_WrdFree( vCanons );
490 fflush(stdout);
491 }
492
493 /**Function*************************************************************
494
495 Synopsis [Saving hash tables.]
496
497 Description []
498
499 SideEffects []
500
501 SeeAlso []
502
503 ***********************************************************************/
Dau_TablesSave(int nInputs,int nVars,Vec_Mem_t * vTtMem,Vec_Int_t * vNodSup,int nFronts,abctime clk)504 void Dau_TablesSave( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
505 {
506 FILE * pFile;
507 char FileName[100];
508 int i, nWords = Abc_TtWordNum(nInputs);
509 // NPN classes
510 sprintf( FileName, "npn%d%d.ttd", nInputs, nVars );
511 pFile = fopen( FileName, "wb" );
512 for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
513 fwrite( Vec_MemReadEntry(vTtMem, i), 8, nWords, pFile );
514 fwrite( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile );
515 fclose( pFile );
516 // printf( "Dumped files with %10d classes after exploring %10d frontiers.\n",
517 // Vec_IntSize(vNodSup), nFronts );
518 printf( "Dumped file \"%s\" with %10d classes after exploring %10d frontiers. ",
519 FileName, Vec_IntSize(vNodSup), nFronts );
520 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
521 fflush(stdout);
522 }
523
524 /**Function*************************************************************
525
526 Synopsis [Dump functions by the number of nodes.]
527
528 Description []
529
530 SideEffects []
531
532 SeeAlso []
533
534 ***********************************************************************/
Dau_DumpFuncs(Vec_Mem_t * vTtMem,Vec_Int_t * vNodSup,int nVars,int nMax)535 void Dau_DumpFuncs( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nMax )
536 {
537 FILE * pFile[20];
538 int Counters[20] = {0};
539 int n, i;
540 assert( nVars == 4 || nVars == 5 );
541 for ( n = 0; n <= nMax; n++ )
542 {
543 char FileName[100];
544 sprintf( FileName, "func%d_min%d.tt", nVars, n );
545 pFile[n] = fopen( FileName, "wb" );
546 }
547 for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
548 {
549 word * pTruth = Vec_MemReadEntry( vTtMem, i );
550 int NodSup = Vec_IntEntry( vNodSup, i );
551 if ( (NodSup & 0xF) != nVars )
552 continue;
553 Counters[NodSup >> 16]++;
554 if ( nVars == 4 )
555 fprintf( pFile[NodSup >> 16], "%04x\n", (int)(0xFFFF & pTruth[0]) );
556 else if ( nVars == 5 )
557 fprintf( pFile[NodSup >> 16], "%08x\n", (int)(0xFFFFFFFF & pTruth[0]) );
558 }
559 for ( n = 0; n <= nMax; n++ )
560 {
561 printf( "Dumped %8d %d-node %d-input functions into file.\n", Counters[n], n, nVars );
562 fclose( pFile[n] );
563 }
564 }
565
566 /**Function*************************************************************
567
568 Synopsis [Function enumeration.]
569
570 Description []
571
572 SideEffects []
573
574 SeeAlso []
575
576 ***********************************************************************/
Dau_CountFuncs(Vec_Int_t * vNodSup,int iStart,int iStop,int nVars)577 int Dau_CountFuncs( Vec_Int_t * vNodSup, int iStart, int iStop, int nVars )
578 {
579 int i, Entry, Count = 0;
580 Vec_IntForEachEntryStartStop( vNodSup, Entry, i, iStart, iStop )
581 Count += ((Entry & 0xF) <= nVars);
582 return Count;
583 }
Dau_PrintStats(int nNodes,int nInputs,int nVars,Vec_Int_t * vNodSup,int iStart,int iStop,word nSteps,int Count2,abctime clk)584 int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int iStart, int iStop, word nSteps, int Count2, abctime clk )
585 {
586 int nNew;
587 printf("N =%2d | ", nNodes );
588 printf("C =%12.0f ", (double)(iword)nSteps );
589 printf("New%d =%10d ", nInputs, iStop-iStart );
590 printf("All%d =%10d | ", nInputs, iStop );
591 printf("New%d =%8d ", nVars, nNew = Dau_CountFuncs(vNodSup, iStart, iStop, nVars) );
592 printf("All%d =%8d ", nVars, Dau_CountFuncs(vNodSup, 0, iStop, nVars) );
593 printf("Two =%6d ", Count2 );
594 //Abc_PrintTime( 1, "T", Abc_Clock() - clk );
595 Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
596 fflush(stdout);
597 return nNew;
598 }
599
600
Dau_InsertFunction(Abc_TtHieMan_t * pMan,word * pCur,int nNodes,int nInputs,int nVars0,int nVars,Vec_Mem_t * vTtMem,Vec_Int_t * vNodSup,int nFronts,abctime clk)601 int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars0, int nVars,
602 Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
603 {
604 int DumpDelta = 1000000;
605 char Perm[16] = {0};
606 int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
607 //unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 );
608 unsigned Phase = Abc_TtCanonicizeWrap( Abc_TtCanonicizeAda, pMan, pCur, nVarsNew, Perm, 99 );
609 int nEntries = Vec_MemEntryNum(vTtMem);
610 int Entry = Vec_MemHashInsert( vTtMem, pCur );
611 if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new
612 return 0;
613 Entry = 0;
614 Phase = 0;
615 // this is a new class
616 Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
617 assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
618 if ( Vec_IntSize(vNodSup) % DumpDelta == 0 )
619 Dau_TablesSave( nInputs, nVars0, vTtMem, vNodSup, nFronts, clk );
620 return 1;
621 }
Dau_FunctionEnum(int nInputs,int nVars,int nNodeMax,int fUseTwo,int fReduce,int fVerbose)622 void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose )
623 {
624 abctime clk = Abc_Clock();
625 int nWords = Abc_TtWordNum(nInputs); word nSteps = 0;
626 Abc_TtHieMan_t * pMan = Abc_TtHieManStart( nInputs, 5 );
627 Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 16 );
628 Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 );
629 int v, u, k, m, n, Entry, nNew, Limit[32] = {1, 2};
630 word Truth[4] = {0};
631 assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 );
632 Vec_MemHashAlloc( vTtMem, 1<<16 );
633 // add constant 0
634 Vec_MemHashInsert( vTtMem, Truth );
635 Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0
636 // add buffer/inverter
637 Abc_TtIthVar( Truth, 0, nInputs );
638 Abc_TtNot( Truth, nWords );
639 Vec_MemHashInsert( vTtMem, Truth );
640 Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1
641 Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, nSteps, 0, clk );
642 // numerate other functions based on how many nodes they have
643 for ( n = 1; n <= nNodeMax; n++ )
644 {
645 int Count2 = 0;
646 int fExpand = !(fReduce && n == nNodeMax);
647 for ( Entry = Limit[n-1]; Entry < Limit[n]; Entry++ )
648 {
649 word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
650 int NodSup = Vec_IntEntry(vNodSup, Entry);
651 int nSupp = 0xF & NodSup;
652 int SymVars = Dau_CountSymms2( pTruth[0], nSupp );
653 assert( n-1 == (NodSup >> 16) );
654 assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
655 //printf( "Exploring function %4d with %d vars: ", i, nSupp );
656 //printf( " %04x\n", (int)uTruth );
657 //Dau_DsdPrintFromTruth( &uTruth, 4 );
658 for ( v = 0; v < nSupp; v++ ) if ( (SymVars & (1 << v)) == 0 )
659 {
660 word tGate, tCur;
661 word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
662 word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
663 // add one extra variable to support
664 if ( nSupp < nInputs && fExpand )
665 {
666 tGate = s_Truths6[v] & s_Truths6[nSupp];
667 tCur = (tGate & Cof1) | (~tGate & Cof0);
668 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
669
670 tCur = (tGate & Cof0) | (~tGate & Cof1);
671 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
672
673
674 tGate = s_Truths6[v] ^ s_Truths6[nSupp];
675 tCur = (tGate & Cof1) | (~tGate & Cof0);
676 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
677
678 nSteps += 3;
679 }
680 // add one cross bar
681 if ( fExpand )
682 for ( k = 0; k < nSupp; k++ ) if ( k != v && ((SymVars & (1 << k)) == 0 || k == v+1) )
683 {
684 tGate = s_Truths6[v] & s_Truths6[k];
685 tCur = (tGate & Cof1) | (~tGate & Cof0);
686 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
687
688 tCur = (tGate & Cof0) | (~tGate & Cof1);
689 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
690
691 tGate = s_Truths6[v] & ~s_Truths6[k];
692 tCur = (tGate & Cof1) | (~tGate & Cof0);
693 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
694
695 tCur = (tGate & Cof0) | (~tGate & Cof1);
696 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
697
698
699 tGate = s_Truths6[v] ^ s_Truths6[k];
700 tCur = (tGate & Cof1) | (~tGate & Cof0);
701 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
702
703 nSteps += 5;
704 }
705 // add two cross bars
706 for ( k = 0; k < nSupp; k++ ) if ( k != v )//&& ((SymVars & (1 << k)) == 0) )
707 for ( m = k+1; m < nSupp; m++ ) if ( m != v )//&& ((SymVars & (1 << m)) == 0 || m == k+1) )
708 {
709 tGate = s_Truths6[m] & s_Truths6[k];
710 tCur = (tGate & Cof1) | (~tGate & Cof0);
711 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
712
713 tCur = (tGate & Cof0) | (~tGate & Cof1);
714 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
715
716 tGate = s_Truths6[m] & ~s_Truths6[k];
717 tCur = (tGate & Cof1) | (~tGate & Cof0);
718 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
719
720 tCur = (tGate & Cof0) | (~tGate & Cof1);
721 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
722
723 tGate = ~s_Truths6[m] & s_Truths6[k];
724 tCur = (tGate & Cof1) | (~tGate & Cof0);
725 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
726
727 tCur = (tGate & Cof0) | (~tGate & Cof1);
728 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
729
730 tGate = ~s_Truths6[m] & ~s_Truths6[k];
731 tCur = (tGate & Cof1) | (~tGate & Cof0);
732 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
733
734 tCur = (tGate & Cof0) | (~tGate & Cof1);
735 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
736
737
738 tGate = s_Truths6[m] ^ s_Truths6[k];
739 tCur = (tGate & Cof1) | (~tGate & Cof0);
740 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
741
742 tGate = s_Truths6[m] ^ s_Truths6[k];
743 tCur = (tGate & Cof0) | (~tGate & Cof1);
744 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
745
746 nSteps += 10;
747 }
748 }
749 }
750 if ( fUseTwo && n > 2 && fExpand )
751 for ( Entry = Limit[n-2]; Entry < Limit[n-1]; Entry++ )
752 {
753 word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
754 int NodSup = Vec_IntEntry(vNodSup, Entry);
755 int nSupp = 0xF & NodSup; int g1, g2;
756 assert( n-2 == (NodSup >> 16) );
757 assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
758 for ( v = 0; v < nSupp; v++ )
759 for ( u = 0; u < nSupp; u++ ) if ( u != v )
760 {
761 word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
762 word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
763
764 word Cof00 = Abc_Tt6Cofactor0( Cof0, u );
765 word Cof01 = Abc_Tt6Cofactor1( Cof0, u );
766 word Cof10 = Abc_Tt6Cofactor0( Cof1, u );
767 word Cof11 = Abc_Tt6Cofactor1( Cof1, u );
768
769 word tGates[5], tCur;
770 tGates[0] = s_Truths6[v] & s_Truths6[u];
771 tGates[1] = s_Truths6[v] & ~s_Truths6[u];
772 tGates[2] = ~s_Truths6[v] & s_Truths6[u];
773 tGates[3] = s_Truths6[v] | s_Truths6[u];
774 tGates[4] = s_Truths6[v] ^ s_Truths6[u];
775
776 for ( g1 = 0; g1 < 5; g1++ )
777 for ( g2 = g1+1; g2 < 5; g2++ )
778 {
779 Cof0 = (tGates[g1] & Cof01) | (~tGates[g1] & Cof00);
780 Cof1 = (tGates[g1] & Cof11) | (~tGates[g1] & Cof10);
781
782 tCur = (tGates[g2] & Cof1) | (~tGates[g2] & Cof0);
783 Count2 += Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
784 }
785 }
786 }
787 Limit[n+1] = Vec_IntSize(vNodSup);
788 nNew = Dau_PrintStats( n, nInputs, nVars, vNodSup, Limit[n], Limit[n+1], nSteps, Count2, clk );
789 if ( nNew == 0 )
790 break;
791 }
792 Dau_TablesSave( nInputs, nVars, vTtMem, vNodSup, Vec_IntSize(vNodSup), clk );
793 Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
794 //Dau_DumpFuncs( vTtMem, vNodSup, nVars, nNodeMax );
795 //Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n );
796 Abc_TtHieManStop( pMan );
797 Vec_MemHashFree( vTtMem );
798 Vec_MemFreeP( &vTtMem );
799 Vec_IntFree( vNodSup );
800 fflush(stdout);
801 }
802
803 ////////////////////////////////////////////////////////////////////////
804 /// END OF FILE ///
805 ////////////////////////////////////////////////////////////////////////
806
807 ABC_NAMESPACE_IMPL_END
808
809