ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bdcSpfd.c
Go to the documentation of this file.
1
20
21#include "bdcInt.h"
22#include "aig/aig/aig.h"
23#include "misc/extra/extra.h"
24
26
27
31
32typedef struct Bdc_Nod_t_ 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
44};
45
46static 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
55static 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
65static 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
74static 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
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
97extern void Abc_Show6VarFunc( word F0, word F1 );
98
102
114void 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
158void 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
178void 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, (unsigned char)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
223clk = 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 }
249printf( "Selected %6d gates on level %2d. ", c, 1 );
250Abc_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 {
257clk = 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 );
293if ( pNode[i].Weight > 300 )
294Bdc_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
323printf( "Selected %6d gates (out of %6d) on level %2d. ", j, c, n );
324Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
325
326 for ( i = 0; i < 10; i++ )
327 Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
328 }
329
330cleanup:
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
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
399typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
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;
413};
414
415#define BDC_TERM 0x1FFFFFFF
416
417
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}
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}
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}
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
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
502int 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
550int * 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
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
705finish:
706 Vec_IntFree( vStops );
707 free( p );
708
709 *pvWeights = vWeights;
710// Vec_WrdFree( vTruths );
711 return vTruths;
712}
713
714
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
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
787int 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
807word 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
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
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
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
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
1115Abc_Show6VarFunc( 0, t );
1116Abc_Show6VarFunc( 0, FuncBest );
1117Abc_Show6VarFunc( 0, (FuncBest ^ t) );
1118
1119 FuncBest ^= t;
1120 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
1121
1122}
1123
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
1181
1182
1184
ABC_INT64_T abctime
Definition abc_global.h:332
int * Abc_MergeSortCost(int *pCosts, int nSize)
Definition utilSort.c:442
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
word Aig_ManRandom64(int fReset)
Definition aigUtil.c:1200
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
void Bdc_SpfdDecomposeTest8()
Definition bdcSpfd.c:1080
int Bdc_SpfdComputeCost(word f, int i, Vec_Int_t *vWeights)
Definition bdcSpfd.c:787
void Bdc_SpfdUnmark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:459
void Bdc_SpfdDecomposeTest44()
Definition bdcSpfd.c:905
void Bdc_SpfdPrint_rec(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
FUNCTION DEFINITIONS ///.
Definition bdcSpfd.c:114
#define BDC_TERM
Definition bdcSpfd.c:415
void Bdc_SpfdPrint(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels, word Truth)
Definition bdcSpfd.c:158
Vec_Wrd_t * Bdc_SpfdReadFiles6(Vec_Int_t **pvWeights)
Definition bdcSpfd.c:758
Vec_Wrd_t * Bdc_SpfdReadFiles5(Vec_Int_t **pvWeights)
Definition bdcSpfd.c:726
int Bdc_SpfdMark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:429
int Bdc_SpfdAdjCost(word t)
Definition bdcSpfd.c:83
int Bdc_SpfdHashValue(word t, int Size)
Definition bdcSpfd.c:502
int * Bdc_SpfdHashLookup(Bdc_Ent_t *p, int Size, word t)
Definition bdcSpfd.c:550
struct Bdc_Ent_t_ Bdc_Ent_t
Definition bdcSpfd.c:399
int Bdc_SpfdCheckOverlap(Bdc_Ent_t *p, Bdc_Ent_t *pEnt0, Bdc_Ent_t *pEnt1)
Definition bdcSpfd.c:480
Vec_Wrd_t * Bdc_SpfdDecomposeTest__(Vec_Int_t **pvWeights)
Definition bdcSpfd.c:577
void Bdc_SpfdDecomposeTest3()
Definition bdcSpfd.c:1028
void Bdc_SpfdDecomposeTest()
Definition bdcSpfd.c:1135
void Bdc_SpfdDecompose(word Truth, int nVars, int nCands, int nGatesMax)
Definition bdcSpfd.c:178
void Abc_Show6VarFunc(word F0, word F1)
Definition abcPrint.c:2007
typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t
DECLARATIONS ///.
Definition bdcSpfd.c:32
void Bdc_SpfdUnmark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:451
word Bdc_SpfdFindBest(Vec_Wrd_t *vDivs, Vec_Int_t *vWeights, word F0, word F1, int *pCost)
Definition bdcSpfd.c:807
int Bdc_SpfdDecomposeTestOne(word t, Vec_Wrd_t *vDivs, Vec_Int_t *vWeights)
Definition bdcSpfd.c:872
void Bdc_SpfdDecomposeTest_()
Definition bdcSpfd.c:351
int Bdc_SpfdMark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:440
Cube * p
Definition exorList.c:222
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
int iList
Definition bdcSpfd.c:411
unsigned fCompl1
Definition bdcSpfd.c:407
unsigned fCompl0
Definition bdcSpfd.c:403
word Truth
Definition bdcSpfd.c:412
unsigned fExor
Definition bdcSpfd.c:408
unsigned fCompl
Definition bdcSpfd.c:404
unsigned iFan0
Definition bdcSpfd.c:402
unsigned fMark1
Definition bdcSpfd.c:409
int iNext
Definition bdcSpfd.c:410
unsigned fMark0
Definition bdcSpfd.c:405
unsigned iFan1
Definition bdcSpfd.c:406
unsigned iFan1n
Definition bdcSpfd.c:40
unsigned Weight
Definition bdcSpfd.c:41
unsigned iFan1g
Definition bdcSpfd.c:39
unsigned iFan0n
Definition bdcSpfd.c:36
unsigned Type
Definition bdcSpfd.c:37
word Truth
Definition bdcSpfd.c:43
unsigned iFan0g
Definition bdcSpfd.c:35
#define assert(ex)
Definition util_old.h:213
char * calloc()
char * memset()
VOID_HACK free()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42