1 /**CFile****************************************************************
2
3 FileName [bdcSpfd.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Truth-table-based bi-decomposition engine.]
8
9 Synopsis [The gateway to bi-decomposition.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - January 30, 2007.]
16
17 Revision [$Id: bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bdcInt.h"
22 #include "aig/aig/aig.h"
23 #include "misc/extra/extra.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 typedef struct Bdc_Nod_t_ Bdc_Nod_t;
33 struct Bdc_Nod_t_
34 {
35 unsigned iFan0g : 8;
36 unsigned iFan0n : 12;
37 unsigned Type : 12; // 0-3 = AND; 4 = XOR
38
39 unsigned iFan1g : 8;
40 unsigned iFan1n : 12;
41 unsigned Weight : 12;
42
43 word Truth;
44 };
45
46 static word Truths[6] = {
47 ABC_CONST(0xAAAAAAAAAAAAAAAA),
48 ABC_CONST(0xCCCCCCCCCCCCCCCC),
49 ABC_CONST(0xF0F0F0F0F0F0F0F0),
50 ABC_CONST(0xFF00FF00FF00FF00),
51 ABC_CONST(0xFFFF0000FFFF0000),
52 ABC_CONST(0xFFFFFFFF00000000)
53 };
54
Bdc_CountOnes(word t)55 static inline int Bdc_CountOnes( word t )
56 {
57 t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
58 t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
59 t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
60 t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
61 t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
62 return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
63 }
64
Bdc_CountSpfd(word t,word f)65 static inline int Bdc_CountSpfd( word t, word f )
66 {
67 int n00 = Bdc_CountOnes( ~t & ~f );
68 int n01 = Bdc_CountOnes( t & ~f );
69 int n10 = Bdc_CountOnes( ~t & f );
70 int n11 = Bdc_CountOnes( t & f );
71 return n00 * n11 + n10 * n01;
72 }
73
Bdc_Cof6(word t,int iVar,int fCof1)74 static inline word Bdc_Cof6( word t, int iVar, int fCof1 )
75 {
76 assert( iVar >= 0 && iVar < 6 );
77 if ( fCof1 )
78 return (t & Truths[iVar]) | ((t & Truths[iVar]) >> (1<<iVar));
79 else
80 return (t &~Truths[iVar]) | ((t &~Truths[iVar]) << (1<<iVar));
81 }
82
Bdc_SpfdAdjCost(word t)83 int Bdc_SpfdAdjCost( word t )
84 {
85 word c0, c1;
86 int v, Cost = 0;
87 for ( v = 0; v < 6; v++ )
88 {
89 c0 = Bdc_Cof6( t, v, 0 );
90 c1 = Bdc_Cof6( t, v, 1 );
91 Cost += Bdc_CountOnes( c0 ^ c1 );
92 }
93 return Cost;
94 }
95
96
97 extern void Abc_Show6VarFunc( word F0, word F1 );
98
99 ////////////////////////////////////////////////////////////////////////
100 /// FUNCTION DEFINITIONS ///
101 ////////////////////////////////////////////////////////////////////////
102
103 /**Function*************************************************************
104
105 Synopsis []
106
107 Description []
108
109 SideEffects []
110
111 SeeAlso []
112
113 ***********************************************************************/
Bdc_SpfdPrint_rec(Bdc_Nod_t * pNode,int Level,Vec_Ptr_t * vLevels)114 void Bdc_SpfdPrint_rec( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels )
115 {
116 assert( Level > 0 );
117 printf( "(" );
118
119 if ( pNode->Type & 1 )
120 printf( "!" );
121 if ( pNode->iFan0g == 0 )
122 printf( "%c", 'a' + pNode->iFan0n );
123 else
124 {
125 Bdc_Nod_t * pNode0 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan0g);
126 Bdc_SpfdPrint_rec( pNode0 + pNode->iFan0n, pNode->iFan0g, vLevels );
127 }
128
129 if ( pNode->Type & 4 )
130 printf( "+" );
131 else
132 printf( "*" );
133
134 if ( pNode->Type & 2 )
135 printf( "!" );
136 if ( pNode->iFan1g == 0 )
137 printf( "%c", 'a' + pNode->iFan1n );
138 else
139 {
140 Bdc_Nod_t * pNode1 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan1g);
141 Bdc_SpfdPrint_rec( pNode1 + pNode->iFan1n, pNode->iFan1g, vLevels );
142 }
143
144 printf( ")" );
145 }
146
147 /**Function*************************************************************
148
149 Synopsis []
150
151 Description []
152
153 SideEffects []
154
155 SeeAlso []
156
157 ***********************************************************************/
Bdc_SpfdPrint(Bdc_Nod_t * pNode,int Level,Vec_Ptr_t * vLevels,word Truth)158 void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels, word Truth )
159 {
160 word Diff = Truth ^ pNode->Truth;
161 Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( " " );
162 Extra_PrintHex( stdout, (unsigned *)&Diff, 6 ); printf( " " );
163 Bdc_SpfdPrint_rec( pNode, Level, vLevels );
164 printf( " %d\n", pNode->Weight );
165 }
166
167 /**Function*************************************************************
168
169 Synopsis []
170
171 Description []
172
173 SideEffects []
174
175 SeeAlso []
176
177 ***********************************************************************/
Bdc_SpfdDecompose(word Truth,int nVars,int nCands,int nGatesMax)178 void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
179 {
180 int nSize = nCands * nCands * (nGatesMax + 1) * 5;
181 Vec_Ptr_t * vLevels;
182 Vec_Int_t * vBegs, * vWeight;
183 Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2;
184 int Count0, Count1, * pPerm;
185 int i, j, k, c, n;
186 abctime clk;
187 assert( nGatesMax < (1<<8) );
188 assert( nCands < (1<<12) );
189 assert( (1<<(nVars-1))*(1<<(nVars-1)) < (1<<12) ); // max SPFD
190
191 printf( "Storage size = %d (%d * %d * %d * %d).\n", nSize, nCands, nCands, nGatesMax + 1, 5 );
192
193 printf( "SPFD = %d.\n", Bdc_CountOnes(Truth) * Bdc_CountOnes(~Truth) );
194
195 // consider elementary functions
196 if ( Truth == 0 || Truth == ~0 )
197 {
198 printf( "Function is a constant.\n" );
199 return;
200 }
201 for ( i = 0; i < nVars; i++ )
202 if ( Truth == Truths[i] || Truth == ~Truths[i] )
203 {
204 printf( "Function is an elementary variable.\n" );
205 return;
206 }
207
208 // allocate
209 vLevels = Vec_PtrAlloc( 100 );
210 vBegs = Vec_IntAlloc( 100 );
211 vWeight = Vec_IntAlloc( 100 );
212
213 // initialize elementary variables
214 pNode = ABC_CALLOC( Bdc_Nod_t, nVars );
215 for ( i = 0; i < nVars; i++ )
216 pNode[i].Truth = Truths[i];
217 for ( i = 0; i < nVars; i++ )
218 pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
219 Vec_PtrPush( vLevels, pNode );
220 Vec_IntPush( vBegs, nVars );
221
222 // the next level
223 clk = Abc_Clock();
224 pNode0 = pNode;
225 pNode = ABC_CALLOC( Bdc_Nod_t, 5 * nVars * (nVars - 1) / 2 );
226 for ( c = i = 0; i < nVars; i++ )
227 for ( j = i+1; j < nVars; j++ )
228 {
229 pNode[c].Truth = pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
230 pNode[c].Truth = ~pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
231 pNode[c].Truth = pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
232 pNode[c].Truth = ~pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
233 pNode[c].Truth = pNode0[i].Truth ^ pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
234 }
235 assert( c == 5 * nVars * (nVars - 1) / 2 );
236 Vec_PtrPush( vLevels, pNode );
237 Vec_IntPush( vBegs, c );
238 for ( i = 0; i < c; i++ )
239 {
240 pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
241 //Bdc_SpfdPrint( pNode + i, 1, vLevels );
242 if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
243 {
244 printf( "Function can be implemented using 1 gate.\n" );
245 pNode = NULL;
246 goto cleanup;
247 }
248 }
249 printf( "Selected %6d gates on level %2d. ", c, 1 );
250 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
251
252
253 // iterate through levels
254 pNode = ABC_CALLOC( Bdc_Nod_t, nSize );
255 for ( n = 2; n <= nGatesMax; n++ )
256 {
257 clk = Abc_Clock();
258 c = 0;
259 pNode1 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, n-1 );
260 Count1 = Vec_IntEntry( vBegs, n-1 );
261 // go through previous levels
262 for ( k = 0; k < n-1; k++ )
263 {
264 pNode0 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, k );
265 Count0 = Vec_IntEntry( vBegs, k );
266 for ( i = 0; i < Count0; i++ )
267 for ( j = 0; j < Count1; j++ )
268 {
269 pNode[c].Truth = pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
270 pNode[c].Truth = ~pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
271 pNode[c].Truth = pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
272 pNode[c].Truth = ~pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
273 pNode[c].Truth = pNode0[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
274 }
275 assert( c < nSize );
276 }
277 // go through current level
278 for ( i = 0; i < Count1; i++ )
279 for ( j = i+1; j < Count1; j++ )
280 {
281 pNode[c].Truth = pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
282 pNode[c].Truth = ~pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
283 pNode[c].Truth = pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
284 pNode[c].Truth = ~pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
285 pNode[c].Truth = pNode1[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
286 }
287 assert( c < nSize );
288 // sort
289 Vec_IntClear( vWeight );
290 for ( i = 0; i < c; i++ )
291 {
292 pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
293 if ( pNode[i].Weight > 300 )
294 Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
295 Vec_IntPush( vWeight, pNode[i].Weight );
296
297 if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
298 {
299 printf( "Function can be implemented using %d gates.\n", n );
300 Bdc_SpfdPrint( pNode + i, n, vLevels, Truth );
301 goto cleanup;
302 }
303 }
304 pPerm = Abc_MergeSortCost( Vec_IntArray(vWeight), c );
305 assert( Vec_IntEntry(vWeight, pPerm[0]) <= Vec_IntEntry(vWeight, pPerm[c-1]) );
306
307 printf( "Best SPFD = %d.\n", Vec_IntEntry(vWeight, pPerm[c-1]) );
308 // for ( i = 0; i < c; i++ )
309 //printf( "%d ", Vec_IntEntry(vWeight, pPerm[i]) );
310
311 // choose the best ones
312 pNode2 = ABC_CALLOC( Bdc_Nod_t, nCands );
313 for ( j = 0, i = c-1; i >= 0; i-- )
314 {
315 pNode2[j++] = pNode[pPerm[i]];
316 if ( j == nCands )
317 break;
318 }
319 ABC_FREE( pPerm );
320 Vec_PtrPush( vLevels, pNode2 );
321 Vec_IntPush( vBegs, j );
322
323 printf( "Selected %6d gates (out of %6d) on level %2d. ", j, c, n );
324 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
325
326 for ( i = 0; i < 10; i++ )
327 Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
328 }
329
330 cleanup:
331 ABC_FREE( pNode );
332 Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i )
333 ABC_FREE( pNode );
334 Vec_PtrFree( vLevels );
335 Vec_IntFree( vBegs );
336 Vec_IntFree( vWeight );
337 }
338
339
340 /**Function*************************************************************
341
342 Synopsis []
343
344 Description []
345
346 SideEffects []
347
348 SeeAlso []
349
350 ***********************************************************************/
Bdc_SpfdDecomposeTest_()351 void Bdc_SpfdDecomposeTest_()
352 {
353 int fTry = 0;
354 // word T[17];
355 // int i;
356
357 // word Truth = Truths[0] & ~Truths[3];
358 // word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]);
359 // word Truth = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5]));
360 // word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]);
361 // word Truth = 0x9ef7a8d9c7193a0f; // AAFFAAFF0A0F0A0F
362 // word Truth = 0x34080226CD163000;
363 word Truth = ABC_CONST(0x5052585a0002080a);
364 int nVars = 6;
365 int nCands = 200;// 75;
366 int nGatesMax = 20;
367
368 if ( fTry )
369 Bdc_SpfdDecompose( Truth, nVars, nCands, nGatesMax );
370 /*
371 for ( i = 0; i < 6; i++ )
372 T[i] = Truths[i];
373 T[7] = 0;
374 T[8] = ~T[1] & T[3];
375 T[9] = ~T[8] & T[0];
376 T[10] = T[1] & T[4];
377 T[11] = T[10] & T[2];
378 T[12] = T[11] & T[9];
379 T[13] = ~T[0] & T[5];
380 T[14] = T[2] & T[13];
381 T[15] = ~T[12] & ~T[14];
382 T[16] = ~T[15];
383 // if ( T[16] != Truth )
384 // printf( "Failed\n" );
385
386 for ( i = 0; i < 17; i++ )
387 {
388 // printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], Truth) );
389 printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], T[16]) );
390 Extra_PrintBinary( stdout, (unsigned *)&T[i], 64 ); printf( "\n" );
391 }
392 // Extra_PrintBinary( stdout, (unsigned *)&Truth, 64 ); printf( "\n" );
393 */
394 }
395
396
397
398
399 typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
400 struct Bdc_Ent_t_
401 {
402 unsigned iFan0 : 29;
403 unsigned fCompl0 : 1;
404 unsigned fCompl : 1;
405 unsigned fMark0 : 1;
406 unsigned iFan1 : 29;
407 unsigned fCompl1 : 1;
408 unsigned fExor : 1;
409 unsigned fMark1 : 1;
410 int iNext;
411 int iList;
412 word Truth;
413 };
414
415 #define BDC_TERM 0x1FFFFFFF
416
417
418 /**Function*************************************************************
419
420 Synopsis []
421
422 Description []
423
424 SideEffects []
425
426 SeeAlso []
427
428 ***********************************************************************/
Bdc_SpfdMark0(Bdc_Ent_t * p,Bdc_Ent_t * pEnt)429 int Bdc_SpfdMark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
430 {
431 if ( pEnt->iFan0 == BDC_TERM )
432 return 0;
433 if ( pEnt->fMark0 )
434 return 0;
435 pEnt->fMark0 = 1;
436 return pEnt->fMark1 +
437 Bdc_SpfdMark0(p, p + pEnt->iFan0) +
438 Bdc_SpfdMark0(p, p + pEnt->iFan1);
439 }
Bdc_SpfdMark1(Bdc_Ent_t * p,Bdc_Ent_t * pEnt)440 int Bdc_SpfdMark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
441 {
442 if ( pEnt->iFan0 == BDC_TERM )
443 return 0;
444 if ( pEnt->fMark1 )
445 return 0;
446 pEnt->fMark1 = 1;
447 return pEnt->fMark0 +
448 Bdc_SpfdMark1(p, p + pEnt->iFan0) +
449 Bdc_SpfdMark1(p, p + pEnt->iFan1);
450 }
Bdc_SpfdUnmark0(Bdc_Ent_t * p,Bdc_Ent_t * pEnt)451 void Bdc_SpfdUnmark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
452 {
453 if ( pEnt->iFan0 == BDC_TERM )
454 return;
455 pEnt->fMark0 = 0;
456 Bdc_SpfdUnmark0( p, p + pEnt->iFan0 );
457 Bdc_SpfdUnmark0( p, p + pEnt->iFan1 );
458 }
Bdc_SpfdUnmark1(Bdc_Ent_t * p,Bdc_Ent_t * pEnt)459 void Bdc_SpfdUnmark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
460 {
461 if ( pEnt->iFan0 == BDC_TERM )
462 return;
463 pEnt->fMark1 = 0;
464 Bdc_SpfdUnmark1( p, p + pEnt->iFan0 );
465 Bdc_SpfdUnmark1( p, p + pEnt->iFan1 );
466 }
467
468
469 /**Function*************************************************************
470
471 Synopsis []
472
473 Description []
474
475 SideEffects []
476
477 SeeAlso []
478
479 ***********************************************************************/
Bdc_SpfdCheckOverlap(Bdc_Ent_t * p,Bdc_Ent_t * pEnt0,Bdc_Ent_t * pEnt1)480 int Bdc_SpfdCheckOverlap( Bdc_Ent_t * p, Bdc_Ent_t * pEnt0, Bdc_Ent_t * pEnt1 )
481 {
482 int RetValue;
483 RetValue = Bdc_SpfdMark0( p, pEnt0 );
484 assert( RetValue == 0 );
485 RetValue = Bdc_SpfdMark1( p, pEnt1 );
486 Bdc_SpfdUnmark0( p, pEnt0 );
487 Bdc_SpfdUnmark1( p, pEnt1 );
488 return RetValue;
489 }
490
491 /**Function*************************************************************
492
493 Synopsis []
494
495 Description []
496
497 SideEffects []
498
499 SeeAlso []
500
501 ***********************************************************************/
Bdc_SpfdHashValue(word t,int Size)502 int Bdc_SpfdHashValue( word t, int Size )
503 {
504 // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html
505 // 53,
506 // 97,
507 // 193,
508 // 389,
509 // 769,
510 // 1543,
511 // 3079,
512 // 6151,
513 // 12289,
514 // 24593,
515 // 49157,
516 // 98317,
517 // 196613,
518 // 393241,
519 // 786433,
520 // 1572869,
521 // 3145739,
522 // 6291469,
523 // 12582917,
524 // 25165843,
525 // 50331653,
526 // 100663319,
527 // 201326611,
528 // 402653189,
529 // 805306457,
530 // 1610612741,
531 static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
532 unsigned char * s = (unsigned char *)&t;
533 unsigned i, Value = 0;
534 for ( i = 0; i < 8; i++ )
535 Value ^= BigPrimes[i] * s[i];
536 return Value % Size;
537 }
538
539 /**Function*************************************************************
540
541 Synopsis []
542
543 Description []
544
545 SideEffects []
546
547 SeeAlso []
548
549 ***********************************************************************/
Bdc_SpfdHashLookup(Bdc_Ent_t * p,int Size,word t)550 int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t )
551 {
552 Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size );
553 if ( pBin->iList == 0 )
554 return &pBin->iList;
555 for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext )
556 {
557 if ( pBin->Truth == t )
558 return NULL;
559 if ( pBin->iNext == 0 )
560 return &pBin->iNext;
561 }
562 assert( 0 );
563 return NULL;
564 }
565
566 /**Function*************************************************************
567
568 Synopsis []
569
570 Description []
571
572 SideEffects []
573
574 SeeAlso []
575
576 ***********************************************************************/
Bdc_SpfdDecomposeTest__(Vec_Int_t ** pvWeights)577 Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
578 {
579 // int nFuncs = 8000000; // the number of functions to compute
580 // int nSize = 2777111; // the hash table size to use
581 // int Limit = 6;
582
583 // int nFuncs = 51000000; // the number of functions to compute
584 // int nSize = 50331653; // the hash table size to use
585 // int Limit = 6;
586
587 int nFuncs = 250000000; // the number of functions to compute
588 int nSize = 201326611; // the hash table size to use
589 int Limit = 6;
590
591 int * pPlace, i, n, m, k, s, fCompl;
592 abctime clk = Abc_Clock(), clk2;
593 Vec_Int_t * vStops;
594 Vec_Wrd_t * vTruths;
595 Vec_Int_t * vWeights;
596 Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1;
597 word t0, t1, t;
598 assert( nSize <= nFuncs );
599
600 printf( "Allocating %.2f MB of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) );
601
602 p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) );
603 memset( p, 255, sizeof(Bdc_Ent_t) );
604 p->iList = 0;
605 for ( q = p; q < p+nFuncs; q++ )
606 q->iList = 0;
607 q = p + 1;
608 printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
609
610 vTruths = Vec_WrdStart( nFuncs );
611 vWeights = Vec_IntStart( nFuncs );
612 Vec_WrdClear( vTruths );
613 Vec_IntClear( vWeights );
614
615 // create elementary vars
616 vStops = Vec_IntAlloc( 10 );
617 Vec_IntPush( vStops, 1 );
618 for ( i = 0; i < 6; i++ )
619 {
620 q->iFan0 = BDC_TERM;
621 q->iFan1 = i;
622 q->Truth = Truths[i];
623 pPlace = Bdc_SpfdHashLookup( p, nSize, q->Truth );
624 *pPlace = q-p;
625 q++;
626 Vec_WrdPush( vTruths, Truths[i] );
627 Vec_IntPush( vWeights, 0 );
628 }
629 Vec_IntPush( vStops, 7 );
630 printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
631
632 // create gates
633 for ( n = 0; n < Limit; n++ )
634 {
635 // try previous
636 for ( k = 0; k < Limit; k++ )
637 for ( m = 0; m < Limit; m++ )
638 {
639 if ( k + m != n || k > m )
640 continue;
641 // set the start and stop
642 pBeg0 = p + Vec_IntEntry( vStops, k );
643 pEnd0 = p + Vec_IntEntry( vStops, k+1 );
644 // set the start and stop
645 pBeg1 = p + Vec_IntEntry( vStops, m );
646 pEnd1 = p + Vec_IntEntry( vStops, m+1 );
647
648 clk2 = Abc_Clock();
649 printf( "Trying %7d x %7d. ", (int)(pEnd0-pBeg0), (int)(pEnd1-pBeg1) );
650 for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
651 for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
652 if ( k < m || pThis1 > pThis0 )
653 // if ( n < 5 || Bdc_SpfdCheckOverlap(p, pThis0, pThis1) )
654 for ( s = 0; s < 5; s++ )
655 {
656 t0 = (s&1) ? ~pThis0->Truth : pThis0->Truth;
657 t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
658 t = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
659 fCompl = t & 1;
660 if ( fCompl )
661 t = ~t;
662 if ( t == 0 )
663 continue;
664 pPlace = Bdc_SpfdHashLookup( p, nSize, t );
665 if ( pPlace == NULL )
666 continue;
667 q->iFan0 = pThis0-p;
668 q->fCompl0 = s&1;
669 q->iFan1 = pThis1-p;
670 q->fCompl1 = (s>>1)&1;
671 q->fExor = (s>>2)&1;
672 q->Truth = t;
673 q->fCompl = fCompl;
674 *pPlace = q-p;
675 q++;
676 Vec_WrdPush( vTruths, t );
677 // Vec_IntPush( vWeights, n == 5 ? n : n+1 );
678 Vec_IntPush( vWeights, n+1 );
679 if ( q-p == nFuncs )
680 {
681 printf( "Reached limit of %d functions.\n", nFuncs );
682 goto finish;
683 }
684 }
685 printf( "Added %d + %d + 1 = %d. Total = %8d. ", k, m, n+1, (int)(q-p) );
686 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
687 }
688 Vec_IntPush( vStops, q-p );
689 }
690 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
691
692
693 {
694 FILE * pFile = fopen( "func6v6n_bin.txt", "wb" );
695 fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
696 fclose( pFile );
697 }
698 {
699 FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" );
700 fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
701 fclose( pFile );
702 }
703
704
705 finish:
706 Vec_IntFree( vStops );
707 free( p );
708
709 *pvWeights = vWeights;
710 // Vec_WrdFree( vTruths );
711 return vTruths;
712 }
713
714
715 /**Function*************************************************************
716
717 Synopsis []
718
719 Description []
720
721 SideEffects []
722
723 SeeAlso []
724
725 ***********************************************************************/
Bdc_SpfdReadFiles5(Vec_Int_t ** pvWeights)726 Vec_Wrd_t * Bdc_SpfdReadFiles5( Vec_Int_t ** pvWeights )
727 {
728 Vec_Int_t * vWeights;
729 Vec_Wrd_t * vDivs;
730 FILE * pFile;
731 int RetValue;
732
733 vDivs = Vec_WrdStart( 3863759 );
734 pFile = fopen( "func6v5n_bin.txt", "rb" );
735 RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
736 fclose( pFile );
737
738 vWeights = Vec_IntStart( 3863759 );
739 pFile = fopen( "func6v5nW_bin.txt", "rb" );
740 RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
741 fclose( pFile );
742
743 *pvWeights = vWeights;
744 return vDivs;
745 }
746
747 /**Function*************************************************************
748
749 Synopsis []
750
751 Description []
752
753 SideEffects []
754
755 SeeAlso []
756
757 ***********************************************************************/
Bdc_SpfdReadFiles6(Vec_Int_t ** pvWeights)758 Vec_Wrd_t * Bdc_SpfdReadFiles6( Vec_Int_t ** pvWeights )
759 {
760 Vec_Int_t * vWeights;
761 Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 );
762 FILE * pFile = fopen( "func6v6n_bin.txt", "rb" );
763 int RetValue;
764 RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
765 fclose( pFile );
766
767 vWeights = Vec_IntStart( 12776759 );
768 pFile = fopen( "func6v6nW_bin.txt", "rb" );
769 RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
770 fclose( pFile );
771
772 *pvWeights = vWeights;
773 return vDivs;
774 }
775
776 /**Function*************************************************************
777
778 Synopsis []
779
780 Description []
781
782 SideEffects []
783
784 SeeAlso []
785
786 ***********************************************************************/
Bdc_SpfdComputeCost(word f,int i,Vec_Int_t * vWeights)787 int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights )
788 {
789 int Ones = Bdc_CountOnes(f);
790 if ( Ones == 0 )
791 return -1;
792 return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i));
793 // return Bdc_CountOnes(f);
794 }
795
796 /**Function*************************************************************
797
798 Synopsis []
799
800 Description []
801
802 SideEffects []
803
804 SeeAlso []
805
806 ***********************************************************************/
Bdc_SpfdFindBest(Vec_Wrd_t * vDivs,Vec_Int_t * vWeights,word F0,word F1,int * pCost)807 word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost )
808 {
809 word Func, FuncBest;
810 int i, Cost, CostBest = -1, NumBest = -1;
811 Vec_WrdForEachEntry( vDivs, Func, i )
812 {
813 if ( (Func & F0) == 0 )
814 {
815 Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights);
816 if ( CostBest < Cost )
817 {
818 CostBest = Cost;
819 FuncBest = Func;
820 NumBest = i;
821 }
822 }
823 if ( (Func & F1) == 0 )
824 {
825 Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights);
826 if ( CostBest < Cost )
827 {
828 CostBest = Cost;
829 FuncBest = Func;
830 NumBest = i;
831 }
832 }
833 if ( (~Func & F0) == 0 )
834 {
835 Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights);
836 if ( CostBest < Cost )
837 {
838 CostBest = Cost;
839 FuncBest = ~Func;
840 NumBest = i;
841 }
842 }
843 if ( (~Func & F1) == 0 )
844 {
845 Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights);
846 if ( CostBest < Cost )
847 {
848 CostBest = Cost;
849 FuncBest = ~Func;
850 NumBest = i;
851 }
852 }
853 }
854 (*pCost) += Vec_IntEntry(vWeights, NumBest);
855 assert( CostBest > 0 );
856 printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) );
857 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
858 return FuncBest;
859 }
860
861 /**Function*************************************************************
862
863 Synopsis []
864
865 Description []
866
867 SideEffects []
868
869 SeeAlso []
870
871 ***********************************************************************/
Bdc_SpfdDecomposeTestOne(word t,Vec_Wrd_t * vDivs,Vec_Int_t * vWeights)872 int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
873 {
874 word F1 = t;
875 word F0 = ~F1;
876 word Func;
877 int i, Cost = 0;
878 printf( "Trying: " );
879 Extra_PrintHex( stdout, (unsigned *)&t, 6 ); printf( "\n" );
880 // Abc_Show6VarFunc( F0, F1 );
881 for ( i = 0; F0 && F1; i++ )
882 {
883 printf( "*** ITER %2d ", i );
884 Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost );
885 F0 &= ~Func;
886 F1 &= ~Func;
887 // Abc_Show6VarFunc( F0, F1 );
888 }
889 Cost += (i-1);
890 printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) );
891 return Cost;
892 }
893
894 /**Function*************************************************************
895
896 Synopsis []
897
898 Description []
899
900 SideEffects []
901
902 SeeAlso []
903
904 ***********************************************************************/
Bdc_SpfdDecomposeTest44()905 void Bdc_SpfdDecomposeTest44()
906 {
907 // word t = 0x5052585a0002080a;
908
909 word t = ABC_CONST(0x9ef7a8d9c7193a0f);
910 // word t = 0x6BFDA276C7193A0F;
911 // word t = 0xA3756AFE0B1DF60B;
912
913 // word t = 0xFEF7AEBFCE80AA0F;
914 // word t = 0x9EF7FDBFC77F6F0F;
915 // word t = 0xDEF7FDFF377F6FFF;
916
917 // word t = 0x345D02736DB390A5; // xor with var 0
918
919 // word t = 0x3EFDA2736D139A0F; // best solution after changes
920
921 Vec_Int_t * vWeights;
922 Vec_Wrd_t * vDivs;
923 word c0, c1, s, tt, tbest;
924 int i, j, Cost, CostBest = 100000;
925 abctime clk = Abc_Clock();
926
927 return;
928
929 // printf( "%d\n", RAND_MAX );
930
931 vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
932 // vDivs = Bdc_SpfdReadFiles5( &vWeights );
933
934 // Abc_Show6VarFunc( ~t, t );
935
936 // try function
937 tt = t;
938 Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
939 if ( CostBest > Cost )
940 {
941 CostBest = Cost;
942 tbest = tt;
943 }
944 printf( "\n" );
945
946 // try complemented output
947 for ( i = 0; i < 6; i++ )
948 {
949 tt = t ^ Truths[i];
950 Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
951 if ( CostBest > Cost )
952 {
953 CostBest = Cost;
954 tbest = tt;
955 }
956 }
957 printf( "\n" );
958
959 // try complemented input
960 for ( i = 0; i < 6; i++ )
961 for ( j = 0; j < 6; j++ )
962 {
963 if ( i == j )
964 continue;
965 c0 = Bdc_Cof6( t, i, 0 );
966 c1 = Bdc_Cof6( t, i, 1 );
967 s = Truths[i] ^ Truths[j];
968 tt = (~s & c0) | (s & c1);
969
970 Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
971 if ( CostBest > Cost )
972 {
973 CostBest = Cost;
974 tbest = tt;
975 }
976 }
977
978 /*
979 for ( i = 0; i < 6; i++ )
980 for ( j = 0; j < 6; j++ )
981 {
982 if ( i == j )
983 continue;
984 c0 = Bdc_Cof6( t, i, 0 );
985 c1 = Bdc_Cof6( t, i, 1 );
986 s = Truths[i] ^ Truths[j];
987 tt = (~s & c0) | (s & c1);
988
989 for ( k = 0; k < 6; k++ )
990 for ( n = 0; n < 6; n++ )
991 {
992 if ( k == n )
993 continue;
994 c0 = Bdc_Cof6( tt, k, 0 );
995 c1 = Bdc_Cof6( tt, k, 1 );
996 s = Truths[k] ^ Truths[n];
997 ttt= (~s & c0) | (s & c1);
998
999 Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights );
1000 if ( CostBest > Cost )
1001 {
1002 CostBest = Cost;
1003 tbest = ttt;
1004 }
1005 }
1006 }
1007 */
1008
1009 printf( "Best solution found with cost %d. ", CostBest );
1010 Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
1011 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1012
1013 Vec_WrdFree( vDivs );
1014 Vec_IntFree( vWeights );
1015 }
1016
1017 /**Function*************************************************************
1018
1019 Synopsis []
1020
1021 Description []
1022
1023 SideEffects []
1024
1025 SeeAlso []
1026
1027 ***********************************************************************/
Bdc_SpfdDecomposeTest3()1028 void Bdc_SpfdDecomposeTest3()
1029 {
1030 int nSizeM = (1 << 26);
1031 int nSizeK = (1 << 3);
1032 Vec_Wrd_t * v1M;
1033 Vec_Wrd_t * v1K;
1034 int i, k, Counter;
1035 abctime clk;
1036 // int EntryM, EntryK;
1037 Aig_ManRandom64( 1 );
1038
1039 v1M = Vec_WrdAlloc( nSizeM );
1040 for ( i = 0; i < nSizeM; i++ )
1041 Vec_WrdPush( v1M, Aig_ManRandom64(0) );
1042
1043 v1K = Vec_WrdAlloc( nSizeK );
1044 for ( i = 0; i < nSizeK; i++ )
1045 Vec_WrdPush( v1K, Aig_ManRandom64(0) );
1046
1047 clk = Abc_Clock();
1048 Counter = 0;
1049 for ( i = 0; i < nSizeM; i++ )
1050 for ( k = 0; k < nSizeK; k++ )
1051 Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1052 // Vec_WrdForEachEntry( v1M, EntryM, i )
1053 // Vec_WrdForEachEntry( v1K, EntryK, k )
1054 // Counter += ((EntryM & EntryK) == EntryK);
1055
1056 printf( "Total = %8d. ", Counter );
1057 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1058
1059 clk = Abc_Clock();
1060 Counter = 0;
1061 for ( k = 0; k < nSizeK; k++ )
1062 for ( i = 0; i < nSizeM; i++ )
1063 Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1064 printf( "Total = %8d. ", Counter );
1065 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1066
1067 }
1068
1069 /**Function*************************************************************
1070
1071 Synopsis []
1072
1073 Description []
1074
1075 SideEffects []
1076
1077 SeeAlso []
1078
1079 ***********************************************************************/
Bdc_SpfdDecomposeTest8()1080 void Bdc_SpfdDecomposeTest8()
1081 {
1082 // word t = 0x9ef7a8d9c7193a0f;
1083 // word t = 0x9EF7FDBFC77F6F0F;
1084 word t = ABC_CONST(0x513B57150819050F);
1085
1086 Vec_Int_t * vWeights;
1087 Vec_Wrd_t * vDivs;
1088 word Func, FuncBest;
1089 int Cost, CostBest = ABC_INFINITY;
1090 int i;
1091 abctime clk = Abc_Clock();
1092
1093 // return;
1094
1095 vDivs = Bdc_SpfdReadFiles5( &vWeights );
1096
1097 printf( "Best init = %4d. ", Bdc_SpfdAdjCost(t) );
1098 Extra_PrintHex( stdout, (unsigned *)&t, 6 ); //printf( "\n" );
1099 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1100
1101 Vec_WrdForEachEntry( vDivs, Func, i )
1102 {
1103 Cost = Bdc_SpfdAdjCost( t ^ Func );
1104 if ( CostBest > Cost )
1105 {
1106 CostBest = Cost;
1107 FuncBest = Func;
1108 }
1109 }
1110
1111 printf( "Best cost = %4d. ", CostBest );
1112 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); //printf( "\n" );
1113 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1114
1115 Abc_Show6VarFunc( 0, t );
1116 Abc_Show6VarFunc( 0, FuncBest );
1117 Abc_Show6VarFunc( 0, (FuncBest ^ t) );
1118
1119 FuncBest ^= t;
1120 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
1121
1122 }
1123
1124 /**Function*************************************************************
1125
1126 Synopsis []
1127
1128 Description []
1129
1130 SideEffects []
1131
1132 SeeAlso []
1133
1134 ***********************************************************************/
Bdc_SpfdDecomposeTest()1135 void Bdc_SpfdDecomposeTest()
1136 {
1137 int nSizeM = (1 << 26); // big array size
1138 int nSizeK = (1 << 3); // small array size
1139 Vec_Wrd_t * v1M, * v1K;
1140 int EntryM, EntryK;
1141 int i, k, Counter;
1142 abctime clk;
1143
1144 Aig_ManRandom64( 1 );
1145
1146 v1M = Vec_WrdAlloc( nSizeM );
1147 for ( i = 0; i < nSizeM; i++ )
1148 Vec_WrdPush( v1M, Aig_ManRandom64(0) );
1149
1150 v1K = Vec_WrdAlloc( nSizeK );
1151 for ( i = 0; i < nSizeK; i++ )
1152 Vec_WrdPush( v1K, Aig_ManRandom64(0) );
1153
1154 clk = Abc_Clock();
1155 Counter = 0;
1156 // for ( i = 0; i < nSizeM; i++ )
1157 // for ( k = 0; k < nSizeK; k++ )
1158 // Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1159 Vec_WrdForEachEntry( v1M, EntryM, i )
1160 Vec_WrdForEachEntry( v1K, EntryK, k )
1161 Counter += ((EntryM & EntryK) == EntryK);
1162 printf( "Total = %8d. ", Counter );
1163 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1164
1165 clk = Abc_Clock();
1166 Counter = 0;
1167 // for ( k = 0; k < nSizeK; k++ )
1168 // for ( i = 0; i < nSizeM; i++ )
1169 // Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1170 Vec_WrdForEachEntry( v1K, EntryK, k )
1171 Vec_WrdForEachEntry( v1M, EntryM, i )
1172 Counter += ((EntryM & EntryK) == EntryK);
1173 printf( "Total = %8d. ", Counter );
1174 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1175 }
1176
1177
1178 ////////////////////////////////////////////////////////////////////////
1179 /// END OF FILE ///
1180 ////////////////////////////////////////////////////////////////////////
1181
1182
1183 ABC_NAMESPACE_IMPL_END
1184
1185