ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ifDec07.c
Go to the documentation of this file.
1
20
21#include "if.h"
22#include "misc/extra/extra.h"
23#include "bool/kit/kit.h"
24
25ABC_NAMESPACE_IMPL_START
26
27
31
32// variable swapping code
33static word PMasks[5][3] = {
34 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
35 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
36 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
37 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
38 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
39};
40// elementary truth tables
41static word Truth6[6] = {
42 ABC_CONST(0xAAAAAAAAAAAAAAAA),
43 ABC_CONST(0xCCCCCCCCCCCCCCCC),
44 ABC_CONST(0xF0F0F0F0F0F0F0F0),
45 ABC_CONST(0xFF00FF00FF00FF00),
46 ABC_CONST(0xFFFF0000FFFF0000),
47 ABC_CONST(0xFFFFFFFF00000000)
48};
49static word Truth7[7][2] = {
50 {ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA)},
51 {ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC)},
52 {ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0)},
53 {ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00)},
54 {ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000)},
55 {ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000)},
56 {ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF)}
57};
58
59extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
60extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
61
65
66void If_DecPrintConfig( word z )
67{
68 unsigned S[1];
69 S[0] = (z & 0xffff) | ((z & 0xffff) << 16);
70 Extra_PrintBinary( stdout, S, 16 );
71 printf( " " );
72 Kit_DsdPrintFromTruth( S, 4 );
73 printf( " " );
74 printf( " %d", (int)((z >> 16) & 7) );
75 printf( " %d", (int)((z >> 20) & 7) );
76 printf( " %d", (int)((z >> 24) & 7) );
77 printf( " %d", (int)((z >> 28) & 7) );
78 printf( " " );
79 S[0] = ((z >> 32) & 0xffff) | (((z >> 32) & 0xffff) << 16);
80 Extra_PrintBinary( stdout, S, 16 );
81 printf( " " );
82 Kit_DsdPrintFromTruth( S, 4 );
83 printf( " " );
84 printf( " %d", (int)((z >> 48) & 7) );
85 printf( " %d", (int)((z >> 52) & 7) );
86 printf( " %d", (int)((z >> 56) & 7) );
87 printf( " %d", (int)((z >> 60) & 7) );
88 printf( "\n" );
89}
90
91// verification for 6-input function
92static word If_Dec6ComposeLut4( int t, word f[4] )
93{
94 int m, v;
95 word c, r = 0;
96 for ( m = 0; m < 16; m++ )
97 {
98 if ( !((t >> m) & 1) )
99 continue;
100 c = ~(word)0;
101 for ( v = 0; v < 4; v++ )
102 c &= ((m >> v) & 1) ? f[v] : ~f[v];
103 r |= c;
104 }
105 return r;
106}
107word If_Dec6Truth( word z )
108{
109 word r, q, f[4];
110 int i, v;
111 assert( z );
112 for ( i = 0; i < 4; i++ )
113 {
114 v = (z >> (16+(i<<2))) & 7;
115 assert( v != 7 );
116 if ( v == 6 )
117 continue;
118 f[i] = Truth6[v];
119 }
120 q = If_Dec6ComposeLut4( (int)(z & 0xffff), f );
121 for ( i = 0; i < 4; i++ )
122 {
123 v = (z >> (48+(i<<2))) & 7;
124 if ( v == 6 )
125 continue;
126 f[i] = (v == 7) ? q : Truth6[v];
127 }
128 r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f );
129 return r;
130}
131void If_Dec6Verify( word t, word z )
132{
133 word r = If_Dec6Truth( z );
134 if ( r != t )
135 {
136 If_DecPrintConfig( z );
137 Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" );
138// Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" );
139 Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" );
140 printf( "Verification failed!\n" );
141 }
142}
143// verification for 7-input function
144static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] )
145{
146 int m, v;
147 word c[2];
148 r[0] = r[1] = 0;
149 for ( m = 0; m < 16; m++ )
150 {
151 if ( !((t >> m) & 1) )
152 continue;
153 c[0] = c[1] = ~(word)0;
154 for ( v = 0; v < 4; v++ )
155 {
156 c[0] &= ((m >> v) & 1) ? f[v][0] : ~f[v][0];
157 c[1] &= ((m >> v) & 1) ? f[v][1] : ~f[v][1];
158 }
159 r[0] |= c[0];
160 r[1] |= c[1];
161 }
162}
163void If_Dec7Verify( word t[2], word z )
164{
165 word f[4][2], r[2];
166 int i, v;
167 assert( z );
168 for ( i = 0; i < 4; i++ )
169 {
170 v = (z >> (16+(i<<2))) & 7;
171 f[i][0] = Truth7[v][0];
172 f[i][1] = Truth7[v][1];
173 }
174 If_Dec7ComposeLut4( (int)(z & 0xffff), f, r );
175 f[3][0] = r[0];
176 f[3][1] = r[1];
177 for ( i = 0; i < 3; i++ )
178 {
179 v = (z >> (48+(i<<2))) & 7;
180 f[i][0] = Truth7[v][0];
181 f[i][1] = Truth7[v][1];
182 }
183 If_Dec7ComposeLut4( (int)((z >> 32) & 0xffff), f, r );
184 if ( r[0] != t[0] || r[1] != t[1] )
185 {
186 If_DecPrintConfig( z );
187 Kit_DsdPrintFromTruth( (unsigned*)t, 7 ); printf( "\n" );
188 Kit_DsdPrintFromTruth( (unsigned*)r, 7 ); printf( "\n" );
189 printf( "Verification failed!\n" );
190 }
191}
192
193
194// count the number of unique cofactors
195static inline int If_Dec6CofCount2( word t )
196{
197 int i, Mask = 0;
198 for ( i = 0; i < 16; i++ )
199 Mask |= (1 << ((t >> (i<<2)) & 15));
200 return __builtin_popcount( Mask & 0xffff );
201}
202// count the number of unique cofactors (up to 3)
203static inline int If_Dec7CofCount3( word t[2] )
204{
205 unsigned char * pTruth = (unsigned char *)t;
206 int i, iCof2 = 0;
207 for ( i = 1; i < 16; i++ )
208 {
209 if ( pTruth[i] == pTruth[0] )
210 continue;
211 if ( iCof2 == 0 )
212 iCof2 = i;
213 else if ( pTruth[i] != pTruth[iCof2] )
214 return 3;
215 }
216 assert( iCof2 );
217 return 2;
218}
219
220// permute 6-input function
221static inline word If_Dec6SwapAdjacent( word t, int v )
222{
223 assert( v < 5 );
224 return (t & PMasks[v][0]) | ((t & PMasks[v][1]) << (1 << v)) | ((t & PMasks[v][2]) >> (1 << v));
225}
226static inline word If_Dec6MoveTo( word t, int v, int p, int Pla2Var[6], int Var2Pla[6] )
227{
228 int iPlace0, iPlace1;
229 assert( Var2Pla[v] >= p );
230 while ( Var2Pla[v] != p )
231 {
232 iPlace0 = Var2Pla[v]-1;
233 iPlace1 = Var2Pla[v];
234 t = If_Dec6SwapAdjacent( t, iPlace0 );
235 Var2Pla[Pla2Var[iPlace0]]++;
236 Var2Pla[Pla2Var[iPlace1]]--;
237 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
238 Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
239 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
240 }
241 assert( Pla2Var[p] == v );
242 return t;
243}
244
245// permute 7-input function
246static inline void If_Dec7SwapAdjacent( word t[2], int v )
247{
248 if ( v == 5 )
249 {
250 unsigned Temp = (t[0] >> 32);
251 t[0] = (t[0] & 0xFFFFFFFF) | ((t[1] & 0xFFFFFFFF) << 32);
252 t[1] ^= (t[1] & 0xFFFFFFFF) ^ Temp;
253 return;
254 }
255 assert( v < 5 );
256 t[0] = If_Dec6SwapAdjacent( t[0], v );
257 t[1] = If_Dec6SwapAdjacent( t[1], v );
258}
259static inline void If_Dec7MoveTo( word t[2], int v, int p, int Pla2Var[7], int Var2Pla[7] )
260{
261 int iPlace0, iPlace1;
262 assert( Var2Pla[v] >= p );
263 while ( Var2Pla[v] != p )
264 {
265 iPlace0 = Var2Pla[v]-1;
266 iPlace1 = Var2Pla[v];
267 If_Dec7SwapAdjacent( t, iPlace0 );
268 Var2Pla[Pla2Var[iPlace0]]++;
269 Var2Pla[Pla2Var[iPlace1]]--;
270 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
271 Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
272 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
273 }
274 assert( Pla2Var[p] == v );
275}
276
277// derive binary function
278static inline int If_Dec6DeriveCount2( word t, int * pCof0, int * pCof1 )
279{
280 int i, Mask = 0;
281 *pCof0 = (t & 15);
282 *pCof1 = (t & 15);
283 for ( i = 1; i < 16; i++ )
284 if ( *pCof0 != ((t >> (i<<2)) & 15) )
285 {
286 *pCof1 = ((t >> (i<<2)) & 15);
287 Mask |= (1 << i);
288 }
289 return Mask;
290}
291static inline int If_Dec7DeriveCount3( word t[2], int * pCof0, int * pCof1 )
292{
293 unsigned char * pTruth = (unsigned char *)t;
294 int i, Mask = 0;
295 *pCof0 = pTruth[0];
296 *pCof1 = pTruth[0];
297 for ( i = 1; i < 16; i++ )
298 if ( *pCof0 != pTruth[i] )
299 {
300 *pCof1 = pTruth[i];
301 Mask |= (1 << i);
302 }
303 return Mask;
304}
305
306// derives decomposition
307static inline word If_Dec6Cofactor( word t, int iVar, int fCof1 )
308{
309 assert( iVar >= 0 && iVar < 6 );
310 if ( fCof1 )
311 return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<<iVar));
312 else
313 return (t &~Truth6[iVar]) | ((t &~Truth6[iVar]) << (1<<iVar));
314}
315static word If_Dec6DeriveDisjoint( word t, int Pla2Var[6], int Var2Pla[6] )
316{
317 int i, Cof0, Cof1;
318 word z = If_Dec6DeriveCount2( t, &Cof0, &Cof1 );
319 for ( i = 0; i < 4; i++ )
320 z |= (((word)Pla2Var[i+2]) << (16 + 4*i));
321 z |= ((word)((Cof1 << 4) | Cof0) << 32);
322 z |= ((word)((Cof1 << 4) | Cof0) << 40);
323 for ( i = 0; i < 2; i++ )
324 z |= (((word)Pla2Var[i]) << (48 + 4*i));
325 z |= (((word)7) << (48 + 4*i++));
326 assert( i == 3 );
327 return z;
328}
329static word If_Dec6DeriveNonDisjoint( word t, int s, int Pla2Var0[6], int Var2Pla0[6] )
330{
331 word z, c0, c1;
332 int Cof0[2], Cof1[2];
333 int Truth0, Truth1, i;
334 int Pla2Var[6], Var2Pla[6];
335 assert( s >= 2 && s <= 5 );
336 for ( i = 0; i < 6; i++ )
337 {
338 Pla2Var[i] = Pla2Var0[i];
339 Var2Pla[i] = Var2Pla0[i];
340 }
341 for ( i = s; i < 5; i++ )
342 {
343 t = If_Dec6SwapAdjacent( t, i );
344 Var2Pla[Pla2Var[i]]++;
345 Var2Pla[Pla2Var[i+1]]--;
346 Pla2Var[i] ^= Pla2Var[i+1];
347 Pla2Var[i+1] ^= Pla2Var[i];
348 Pla2Var[i] ^= Pla2Var[i+1];
349 }
350 c0 = If_Dec6Cofactor( t, 5, 0 );
351 c1 = If_Dec6Cofactor( t, 5, 1 );
352 assert( 2 >= If_Dec6CofCount2(c0) );
353 assert( 2 >= If_Dec6CofCount2(c1) );
354 Truth0 = If_Dec6DeriveCount2( c0, &Cof0[0], &Cof0[1] );
355 Truth1 = If_Dec6DeriveCount2( c1, &Cof1[0], &Cof1[1] );
356 z = ((Truth1 & 0xFF) << 8) | (Truth0 & 0xFF);
357 for ( i = 0; i < 4; i++ )
358 z |= (((word)Pla2Var[i+2]) << (16 + 4*i));
359 z |= ((word)((Cof0[1] << 4) | Cof0[0]) << 32);
360 z |= ((word)((Cof1[1] << 4) | Cof1[0]) << 40);
361 for ( i = 0; i < 2; i++ )
362 z |= (((word)Pla2Var[i]) << (48 + 4*i));
363 z |= (((word)7) << (48 + 4*i++));
364 z |= (((word)Pla2Var[5]) << (48 + 4*i++));
365 assert( i == 4 );
366 return z;
367}
368static word If_Dec7DeriveDisjoint( word t[2], int Pla2Var[7], int Var2Pla[7] )
369{
370 int i, Cof0, Cof1;
371 word z = If_Dec7DeriveCount3( t, &Cof0, &Cof1 );
372 for ( i = 0; i < 4; i++ )
373 z |= (((word)Pla2Var[i+3]) << (16 + 4*i));
374 z |= ((word)((Cof1 << 8) | Cof0) << 32);
375 for ( i = 0; i < 3; i++ )
376 z |= (((word)Pla2Var[i]) << (48 + 4*i));
377 z |= (((word)7) << (48 + 4*i));
378 return z;
379}
380
381static inline int If_Dec6CountOnes( word t )
382{
383 t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
384 t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
385 t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
386 t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
387 t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
388 return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
389}
390static inline int If_Dec6HasVar( word t, int v )
391{
392 return ((t & Truth6[v]) >> (1<<v)) != (t & ~Truth6[v]);
393}
394static inline int If_Dec7HasVar( word t[2], int v )
395{
396 assert( v >= 0 && v < 7 );
397 if ( v == 6 )
398 return t[0] != t[1];
399 return ((t[0] & Truth6[v]) >> (1<<v)) != (t[0] & ~Truth6[v])
400 || ((t[1] & Truth6[v]) >> (1<<v)) != (t[1] & ~Truth6[v]);
401}
402
403static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
404{
405 int i;
406 for ( i = 0; i < 6; i++ )
407 assert( Pla2Var[Var2Pla[i]] == i );
408}
409word If_Dec6Perform( word t, int fDerive )
410{
411 word r = 0;
412 int i, v, u, x, Count, Pla2Var[6], Var2Pla[6];
413 // start arrays
414 for ( i = 0; i < 6; i++ )
415 {
416 assert( If_Dec6HasVar( t, i ) );
417 Pla2Var[i] = Var2Pla[i] = i;
418 }
419 // generate permutations
420 i = 0;
421 for ( v = 0; v < 6; v++ )
422 for ( u = v+1; u < 6; u++, i++ )
423 {
424 t = If_Dec6MoveTo( t, v, 0, Pla2Var, Var2Pla );
425 t = If_Dec6MoveTo( t, u, 1, Pla2Var, Var2Pla );
426// If_DecVerifyPerm( Pla2Var, Var2Pla );
427 Count = If_Dec6CofCount2( t );
428 assert( Count > 1 );
429 if ( Count == 2 )
430 return !fDerive ? 1 : If_Dec6DeriveDisjoint( t, Pla2Var, Var2Pla );
431 // check non-disjoint decomposition
432 if ( !r && (Count == 3 || Count == 4) )
433 {
434 for ( x = 0; x < 4; x++ )
435 {
436 word c0 = If_Dec6Cofactor( t, x+2, 0 );
437 word c1 = If_Dec6Cofactor( t, x+2, 1 );
438 if ( If_Dec6CofCount2( c0 ) <= 2 && If_Dec6CofCount2( c1 ) <= 2 )
439 {
440 r = !fDerive ? 1 : If_Dec6DeriveNonDisjoint( t, x+2, Pla2Var, Var2Pla );
441 break;
442 }
443 }
444 }
445 }
446 assert( i == 15 );
447 return r;
448}
449word If_Dec7Perform( word t0[2], int fDerive )
450{
451 word t[2] = {t0[0], t0[1]};
452 int i, v, u, y, Pla2Var[7], Var2Pla[7];
453 // start arrays
454 for ( i = 0; i < 7; i++ )
455 {
456/*
457 if ( i < 6 )
458 assert( If_Dec6HasVar( t[0], i ) || If_Dec6HasVar( t[1], i ) );
459 else
460 assert( t[0] != t[1] );
461*/
462 Pla2Var[i] = Var2Pla[i] = i;
463 }
464 // generate permutations
465 for ( v = 0; v < 7; v++ )
466 for ( u = v+1; u < 7; u++ )
467 for ( y = u+1; y < 7; y++ )
468 {
469 If_Dec7MoveTo( t, v, 0, Pla2Var, Var2Pla );
470 If_Dec7MoveTo( t, u, 1, Pla2Var, Var2Pla );
471 If_Dec7MoveTo( t, y, 2, Pla2Var, Var2Pla );
472// If_DecVerifyPerm( Pla2Var, Var2Pla );
473 if ( If_Dec7CofCount3( t ) == 2 )
474 {
475 return !fDerive ? 1 : If_Dec7DeriveDisjoint( t, Pla2Var, Var2Pla );
476 }
477 }
478 return 0;
479}
480
481
482// support minimization
483static inline int If_DecSuppIsMinBase( int Supp )
484{
485 return (Supp & (Supp+1)) == 0;
486}
487static inline word If_Dec6TruthShrink( word uTruth, int nVars, int nVarsAll, unsigned Phase )
488{
489 int i, k, Var = 0;
490 assert( nVarsAll <= 6 );
491 for ( i = 0; i < nVarsAll; i++ )
492 if ( Phase & (1 << i) )
493 {
494 for ( k = i-1; k >= Var; k-- )
495 uTruth = If_Dec6SwapAdjacent( uTruth, k );
496 Var++;
497 }
498 assert( Var == nVars );
499 return uTruth;
500}
501word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars )
502{
503 int v, iVar = 0, uSupp = 0;
504 assert( nVarsAll <= 6 );
505 for ( v = 0; v < nVarsAll; v++ )
506 if ( If_Dec6HasVar( uTruth, v ) )
507 {
508 uSupp |= (1 << v);
509 if ( pSupp )
510 pSupp[iVar] = pSupp[v];
511 iVar++;
512 }
513 if ( pnVars )
514 *pnVars = iVar;
515 if ( If_DecSuppIsMinBase( uSupp ) )
516 return uTruth;
517 return If_Dec6TruthShrink( uTruth, iVar, nVarsAll, uSupp );
518}
519
520static inline void If_Dec7TruthShrink( word uTruth[2], int nVars, int nVarsAll, unsigned Phase )
521{
522 int i, k, Var = 0;
523 assert( nVarsAll <= 7 );
524 for ( i = 0; i < nVarsAll; i++ )
525 if ( Phase & (1 << i) )
526 {
527 for ( k = i-1; k >= Var; k-- )
528 If_Dec7SwapAdjacent( uTruth, k );
529 Var++;
530 }
531 assert( Var == nVars );
532}
533void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars )
534{
535 int v, iVar = 0, uSupp = 0;
536 assert( nVarsAll <= 7 );
537 for ( v = 0; v < nVarsAll; v++ )
538 if ( If_Dec7HasVar( uTruth, v ) )
539 {
540 uSupp |= (1 << v);
541 if ( pSupp )
542 pSupp[iVar] = pSupp[v];
543 iVar++;
544 }
545 if ( pnVars )
546 *pnVars = iVar;
547 if ( If_DecSuppIsMinBase( uSupp ) )
548 return;
549 If_Dec7TruthShrink( uTruth, iVar, nVarsAll, uSupp );
550}
551
552
553
554// check for MUX decomposition
555static inline int If_Dec6SuppSize( word t )
556{
557 int v, Count = 0;
558 for ( v = 0; v < 6; v++ )
559 if ( If_Dec6Cofactor(t, v, 0) != If_Dec6Cofactor(t, v, 1) )
560 Count++;
561 return Count;
562}
563static inline int If_Dec6CheckMux( word t )
564{
565 int v;
566 for ( v = 0; v < 6; v++ )
567 if ( If_Dec6SuppSize(If_Dec6Cofactor(t, v, 0)) < 5 &&
568 If_Dec6SuppSize(If_Dec6Cofactor(t, v, 1)) < 5 )
569 return v;
570 return -1;
571}
572
573// check for MUX decomposition
574static inline void If_Dec7Cofactor( word t[2], int iVar, int fCof1, word r[2] )
575{
576 assert( iVar >= 0 && iVar < 7 );
577 if ( iVar == 6 )
578 {
579 if ( fCof1 )
580 r[0] = r[1] = t[1];
581 else
582 r[0] = r[1] = t[0];
583 }
584 else
585 {
586 if ( fCof1 )
587 {
588 r[0] = (t[0] & Truth6[iVar]) | ((t[0] & Truth6[iVar]) >> (1<<iVar));
589 r[1] = (t[1] & Truth6[iVar]) | ((t[1] & Truth6[iVar]) >> (1<<iVar));
590 }
591 else
592 {
593 r[0] = (t[0] &~Truth6[iVar]) | ((t[0] &~Truth6[iVar]) << (1<<iVar));
594 r[1] = (t[1] &~Truth6[iVar]) | ((t[1] &~Truth6[iVar]) << (1<<iVar));
595 }
596 }
597}
598static inline int If_Dec7SuppSize( word t[2] )
599{
600 word c0[2], c1[2];
601 int v, Count = 0;
602 for ( v = 0; v < 7; v++ )
603 {
604 If_Dec7Cofactor( t, v, 0, c0 );
605 If_Dec7Cofactor( t, v, 1, c1 );
606 if ( c0[0] != c1[0] || c0[1] != c1[1] )
607 Count++;
608 }
609 return Count;
610}
611static inline int If_Dec7CheckMux( word t[2] )
612{
613 word c0[2], c1[2];
614 int v;
615 for ( v = 0; v < 7; v++ )
616 {
617 If_Dec7Cofactor( t, v, 0, c0 );
618 If_Dec7Cofactor( t, v, 1, c1 );
619 if ( If_Dec7SuppSize(c0) < 5 && If_Dec7SuppSize(c1) < 5 )
620 return v;
621 }
622 return -1;
623}
624
625// find the best MUX decomposition
626int If_Dec6PickBestMux( word t, word Cofs[2] )
627{
628 int v, vBest = -1, Count0, Count1, CountBest = 1000;
629 for ( v = 0; v < 6; v++ )
630 {
631 Count0 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 0) );
632 Count1 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 1) );
633 if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
634 {
635 CountBest = Count0 + Count1;
636 vBest = v;
637 Cofs[0] = If_Dec6Cofactor(t, v, 0);
638 Cofs[1] = If_Dec6Cofactor(t, v, 1);
639 }
640 }
641 return vBest;
642}
643int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
644{
645 word c0[2], c1[2];
646 int v, vBest = -1, Count0, Count1, CountBest = 1000;
647 for ( v = 0; v < 7; v++ )
648 {
649 If_Dec7Cofactor( t, v, 0, c0 );
650 If_Dec7Cofactor( t, v, 1, c1 );
651 Count0 = If_Dec7SuppSize(c0);
652 Count1 = If_Dec7SuppSize(c1);
653 if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
654 {
655 CountBest = Count0 + Count1;
656 vBest = v;
657 c0r[0] = c0[0]; c0r[1] = c0[1];
658 c1r[0] = c1[0]; c1r[1] = c1[1];
659 }
660 }
661 return vBest;
662}
663
664
665
677// count the number of unique cofactors
678static inline word If_Dec5CofCount2( word t, int x, int y, int * Pla2Var, word t0, int fDerive )
679{
680 int m, i, Mask;
681 assert( x >= 0 && x < 4 );
682 assert( y >= 0 && y < 4 );
683 for ( m = 0; m < 4; m++ )
684 {
685 for ( Mask = i = 0; i < 16; i++ )
686 if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) )
687 Mask |= (1 << ((t >> (i<<1)) & 3));
688 if ( __builtin_popcount( Mask & 0xF ) > 2 )
689 return 0;
690 }
691// Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
692 if ( !fDerive )
693 return 1;
694 else
695 {
696 int fHas2, fHas3;
697 // composition function C depends on {x, y, Out, v[0]}
698 // decomposed function D depends on {x, y, z1, z2}
699 word F[4] = { 0, ABC_CONST(0x5555555555555555), ABC_CONST(0xAAAAAAAAAAAAAAAA), ~((word)0) };
700 word C2[4], D2[4] = {0}, C1[2], D1[2], C, D, z;
701 int v, zz1 = -1, zz2 = -1;
702 // find two variables
703 for ( v = 0; v < 4; v++ )
704 if ( v != x && v != y )
705 { zz1 = v; break; }
706 for ( v = 1; v < 4; v++ )
707 if ( v != x && v != y && v != zz1 )
708 { zz2 = v; break; }
709 assert( zz1 != -1 && zz2 != -1 );
710 // find the cofactors
711 for ( m = 0; m < 4; m++ )
712 {
713 // for each cofactor, derive C2 and D2
714 for ( Mask = i = 0; i < 16; i++ )
715 if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) )
716 Mask |= (1 << ((t >> (i<<1)) & 3));
717 // find the values
718 if ( __builtin_popcount( Mask & 0xF ) == 1 )
719 {
720 C2[m] = F[Abc_Tt6FirstBit( Mask )];
721 D2[m] = ~(word)0;
722 }
723 else if ( __builtin_popcount( Mask & 0xF ) == 2 )
724 {
725 int Bit0 = Abc_Tt6FirstBit( Mask );
726 int Bit1 = Abc_Tt6FirstBit( Mask ^ (((word)1)<<Bit0) );
727 C2[m] = (F[Bit1] & Truth6[1]) | (F[Bit0] & ~Truth6[1]);
728 // find Bit1 appears
729 for ( Mask = i = 0; i < 16; i++ )
730 if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) )
731 if ( Bit1 == ((t >> (i<<1)) & 3) )
732 D2[m] |= (((word)1) << ( (((i >> zz2) & 1) << 1) | ((i >> zz1) & 1) ));
733 }
734 else assert( 0 );
735 D2[m] = Abc_Tt6Stretch( D2[m], 2 );
736 }
737
738 // combine
739 C1[0] = (C2[1] & Truth6[2]) | (C2[0] & ~Truth6[2]);
740 C1[1] = (C2[3] & Truth6[2]) | (C2[2] & ~Truth6[2]);
741 C = (C1[1] & Truth6[3]) | (C1[0] & ~Truth6[3]);
742
743 // combine
744 D1[0] = (D2[1] & Truth6[2]) | (D2[0] & ~Truth6[2]);
745 D1[1] = (D2[3] & Truth6[2]) | (D2[2] & ~Truth6[2]);
746 D = (D1[1] & Truth6[3]) | (D1[0] & ~Truth6[3]);
747
748// printf( "\n" );
749// Kit_DsdPrintFromTruth( (unsigned *)&C, 5 ); printf("\n");
750// Kit_DsdPrintFromTruth( (unsigned *)&D, 5 ); printf("\n");
751
752 // create configuration
753 // find one
754 fHas2 = Abc_TtHasVar(&D, 5, 2);
755 fHas3 = Abc_TtHasVar(&D, 5, 3);
756 if ( fHas2 && fHas3 )
757 {
758 z = D & 0xFFFF;
759 z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
760 z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
761 z |= (((word)Pla2Var[x+1]) << (16 + 4*2));
762 z |= (((word)Pla2Var[y+1]) << (16 + 4*3));
763 }
764 else if ( fHas2 && !fHas3 )
765 {
766 z = D & 0xFFFF;
767 z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
768 z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
769 z |= (((word)Pla2Var[x+1]) << (16 + 4*2));
770 z |= (((word)6) << (16 + 4*3));
771 }
772 else if ( !fHas2 && fHas3 )
773 {
774 Abc_TtSwapVars( &D, 5, 2, 3 );
775 z = D & 0xFFFF;
776 z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
777 z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
778 z |= (((word)Pla2Var[y+1]) << (16 + 4*2));
779 z |= (((word)6) << (16 + 4*3));
780 }
781 else
782 {
783 z = D & 0xFFFF;
784 z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0));
785 z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1));
786 z |= (((word)6) << (16 + 4*2));
787 z |= (((word)6) << (16 + 4*3));
788 }
789
790 // second one
791 fHas2 = Abc_TtHasVar(&C, 5, 2);
792 fHas3 = Abc_TtHasVar(&C, 5, 3);
793 if ( fHas2 && fHas3 )
794 {
795 z |= ((C & 0xFFFF) << 32);
796 z |= (((word)Pla2Var[0]) << (48 + 4*0));
797 z |= (((word)7) << (48 + 4*1));
798 z |= (((word)Pla2Var[x+1]) << (48 + 4*2));
799 z |= (((word)Pla2Var[y+1]) << (48 + 4*3));
800 }
801 else if ( fHas2 && !fHas3 )
802 {
803 z |= ((C & 0xFFFF) << 32);
804 z |= (((word)Pla2Var[0]) << (48 + 4*0));
805 z |= (((word)7) << (48 + 4*1));
806 z |= (((word)Pla2Var[x+1]) << (48 + 4*2));
807 z |= (((word)6) << (48 + 4*3));
808 }
809 else if ( !fHas2 && fHas3 )
810 {
811 Abc_TtSwapVars( &C, 5, 2, 3 );
812 z |= ((C & 0xFFFF) << 32);
813 z |= (((word)Pla2Var[0]) << (48 + 4*0));
814 z |= (((word)7) << (48 + 4*1));
815 z |= (((word)Pla2Var[y+1]) << (48 + 4*2));
816 z |= (((word)6) << (48 + 4*3));
817 }
818 else
819 {
820 z |= ((C & 0xFFFF) << 32);
821 z |= (((word)Pla2Var[0]) << (48 + 4*0));
822 z |= (((word)7) << (48 + 4*1));
823 z |= (((word)6) << (48 + 4*2));
824 z |= (((word)6) << (48 + 4*3));
825 }
826
827 // verify
828 {
829 word t1 = If_Dec6Truth( z );
830 if ( t1 != t0 )
831 {
832 printf( "\n" );
833 Kit_DsdPrintFromTruth( (unsigned *)&C2[0], 5 ); printf("\n");
834 Kit_DsdPrintFromTruth( (unsigned *)&C2[1], 5 ); printf("\n");
835 Kit_DsdPrintFromTruth( (unsigned *)&C2[2], 5 ); printf("\n");
836 Kit_DsdPrintFromTruth( (unsigned *)&C2[3], 5 ); printf("\n");
837
838 printf( "\n" );
839 Kit_DsdPrintFromTruth( (unsigned *)&D2[0], 5 ); printf("\n");
840 Kit_DsdPrintFromTruth( (unsigned *)&D2[1], 5 ); printf("\n");
841 Kit_DsdPrintFromTruth( (unsigned *)&D2[2], 5 ); printf("\n");
842 Kit_DsdPrintFromTruth( (unsigned *)&D2[3], 5 ); printf("\n");
843
844 printf( "\n" );
845 Kit_DsdPrintFromTruth( (unsigned *)&C, 5 ); printf("\n");
846 Kit_DsdPrintFromTruth( (unsigned *)&D, 5 ); printf("\n");
847
848 printf( "\n" );
849 Kit_DsdPrintFromTruth( (unsigned *)&t1, 5 ); printf("\n");
850 Kit_DsdPrintFromTruth( (unsigned *)&t0, 5 ); printf("\n");
851 }
852 assert( t1 == t0 );
853 }
854 return z;
855 }
856}
857word If_Dec5Perform( word t, int fDerive )
858{
859 int Pla2Var[7], Var2Pla[7];
860 int i, j, v;
861 word t0 = t;
862/*
863 word c0, c1, c00, c01, c10, c11;
864 for ( i = 0; i < 5; i++ )
865 {
866 c0 = If_Dec6Cofactor( t, i, 0 );
867 c1 = If_Dec6Cofactor( t, i, 1 );
868 if ( c0 == 0 )
869 return 1;
870 if ( ~c0 == 0 )
871 return 1;
872 if ( c1 == 0 )
873 return 1;
874 if ( ~c1 == 0 )
875 return 1;
876 if ( c0 == ~c1 )
877 return 1;
878 }
879 for ( i = 0; i < 4; i++ )
880 {
881 c0 = If_Dec6Cofactor( t, i, 0 );
882 c1 = If_Dec6Cofactor( t, i, 1 );
883 for ( j = i + 1; j < 5; j++ )
884 {
885 c00 = If_Dec6Cofactor( c0, j, 0 );
886 c01 = If_Dec6Cofactor( c0, j, 1 );
887 c10 = If_Dec6Cofactor( c1, j, 0 );
888 c11 = If_Dec6Cofactor( c1, j, 1 );
889 if ( c00 == c01 && c00 == c10 )
890 return 1;
891 if ( c11 == c01 && c11 == c10 )
892 return 1;
893 if ( c11 == c00 && c11 == c01 )
894 return 1;
895 if ( c11 == c00 && c11 == c10 )
896 return 1;
897 if ( c00 == c11 && c01 == c10 )
898 return 1;
899 }
900 }
901*/
902 // start arrays
903 for ( i = 0; i < 7; i++ )
904 Pla2Var[i] = Var2Pla[i] = i;
905 // generate permutations
906 for ( v = 0; v < 5; v++ )
907 {
908 t = If_Dec6MoveTo( t, v, 0, Pla2Var, Var2Pla );
909 If_DecVerifyPerm( Pla2Var, Var2Pla );
910 for ( i = 0; i < 4; i++ )
911 for ( j = i + 1; j < 4; j++ )
912 {
913 word z = If_Dec5CofCount2( t, i, j, Pla2Var, t0, fDerive );
914 if ( z )
915 {
916/*
917 if ( v == 0 && i == 1 && j == 2 )
918 {
919 Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
920 }
921*/
922 return z;
923 }
924 }
925 }
926
927/*
928 // start arrays
929 for ( i = 0; i < 7; i++ )
930 Pla2Var[i] = Var2Pla[i] = i;
931
932 t = t0;
933 for ( v = 0; v < 5; v++ )
934 {
935 int x, y;
936
937 t = If_Dec6MoveTo( t, v, 0, Pla2Var, Var2Pla );
938 If_DecVerifyPerm( Pla2Var, Var2Pla );
939
940 for ( i = 0; i < 16; i++ )
941 printf( "%d ", ((t >> (i<<1)) & 3) );
942 printf( "\n" );
943
944 for ( x = 0; x < 4; x++ )
945 for ( y = x + 1; y < 4; y++ )
946 {
947 for ( i = 0; i < 16; i++ )
948 if ( !((i >> x) & 1) && !((i >> y) & 1) )
949 printf( "%d ", ((t >> (i<<1)) & 3) );
950 printf( "\n" );
951
952 for ( i = 0; i < 16; i++ )
953 if ( ((i >> x) & 1) && !((i >> y) & 1) )
954 printf( "%d ", ((t >> (i<<1)) & 3) );
955 printf( "\n" );
956
957 for ( i = 0; i < 16; i++ )
958 if ( !((i >> x) & 1) && ((i >> y) & 1) )
959 printf( "%d ", ((t >> (i<<1)) & 3) );
960 printf( "\n" );
961
962 for ( i = 0; i < 16; i++ )
963 if ( ((i >> x) & 1) && ((i >> y) & 1) )
964 printf( "%d ", ((t >> (i<<1)) & 3) );
965 printf( "\n" );
966 printf( "\n" );
967 }
968 }
969*/
970
971// Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" );
972 return 0;
973}
974
975word If_Dec5PerformEx()
976{
977 word z;
978 // find one
979 z = (word)(0x17ac & 0xFFFF);
980 z |= (((word)3) << (16 + 4*0));
981 z |= (((word)4) << (16 + 4*1));
982 z |= (((word)1) << (16 + 4*2));
983 z |= (((word)2) << (16 + 4*3));
984 // second one
985 z |= (((word)(0x179a & 0xFFFF)) << 32);
986 z |= (((word)0) << (48 + 4*0));
987 z |= (((word)7) << (48 + 4*1));
988 z |= (((word)1) << (48 + 4*2));
989 z |= (((word)2) << (48 + 4*3));
990 return z;
991}
992void If_Dec5PerformTest()
993{
994 word z, t, t1;
995// s = If_Dec5PerformEx();
996// t = If_Dec6Truth( s );
997 t = ABC_CONST(0xB0F3B0FFB0F3B0FF);
998
999 Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf("\n");
1000
1001 z = If_Dec5Perform( t, 1 );
1002 t1 = If_Dec6Truth( z );
1003 assert( t == t1 );
1004}
1005
1006
1018word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
1019{
1020 if ( nLeaves < 5 )
1021 return 1;
1022 if ( nLeaves == 5 )
1023 {
1024 word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0];
1025 z = If_Dec5Perform( t, 1 );
1026 If_Dec6Verify( t, z );
1027 return z;
1028 }
1029 if ( nLeaves == 6 )
1030 {
1031 word z, t = ((word *)pTruth)[0];
1032 z = If_Dec6Perform( t, 1 );
1033 If_Dec6Verify( t, z );
1034 return z;
1035 }
1036 if ( nLeaves == 7 )
1037 {
1038 word z, t[2];
1039 t[0] = ((word *)pTruth)[0];
1040 t[1] = ((word *)pTruth)[1];
1041 z = If_Dec7Perform( t, 1 );
1042 If_Dec7Verify( t, z );
1043 return z;
1044 }
1045 assert( 0 );
1046 return 0;
1047}
1048
1060int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
1061{
1062 int fDerive = 0;
1063 int v;
1064 // skip non-support minimal
1065 for ( v = 0; v < nLeaves; v++ )
1066 if ( !Abc_TtHasVar( (word *)pTruth, nVars, v ) )
1067 return 0;
1068 // check
1069 if ( nLeaves < 5 )
1070 return 1;
1071 if ( nLeaves == 5 )
1072 {
1073 word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0];
1074 z = If_Dec5Perform( t, fDerive );
1075 if ( fDerive && z )
1076 If_Dec6Verify( t, z );
1077 return z != 0;
1078 }
1079 if ( nLeaves == 6 )
1080 {
1081 word z, t = ((word *)pTruth)[0];
1082 z = If_Dec6Perform( t, fDerive );
1083 if ( fDerive && z )
1084 {
1085// If_DecPrintConfig( z );
1086 If_Dec6Verify( t, z );
1087 }
1088// if ( z == 0 )
1089// Extra_PrintHex(stdout, (unsigned *)&t, 6), printf( " " ), Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
1090 return z != 0;
1091 }
1092 if ( nLeaves == 7 )
1093 {
1094 word z, t[2];
1095 t[0] = ((word *)pTruth)[0];
1096 t[1] = ((word *)pTruth)[1];
1097// if ( If_Dec7CheckMux(t) >= 0 )
1098// return 1;
1099 z = If_Dec7Perform( t, fDerive );
1100 if ( fDerive && z )
1101 If_Dec7Verify( t, z );
1102 return z != 0;
1103 }
1104 assert( 0 );
1105 return 0;
1106}
1107
1119int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
1120{
1121 if ( nLeaves < nVars )
1122 return 1;
1123 assert( nLeaves == nVars );
1124 if ( Abc_Tt6Check1( ((word *)pTruth)[0], nLeaves ) )
1125 return 1;
1126 return 0;
1127}
1128int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
1129{
1130 if ( nLeaves < nVars )
1131 return 1;
1132 assert( nLeaves == nVars );
1133 if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) )
1134 return 1;
1135 return 0;
1136}
1137
1141
1142
1143ABC_NAMESPACE_IMPL_END
1144
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
If_Dec7Verify
void If_Dec7Verify(word t[2], word z)
Definition ifDec07.c:163
If_MatchCheck1
int If_MatchCheck1(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition ifDec07.c:1119
If_Dec7PickBestMux
int If_Dec7PickBestMux(word t[2], word c0r[2], word c1r[2])
Definition ifDec07.c:643
If_Dec6PickBestMux
int If_Dec6PickBestMux(word t, word Cofs[2])
Definition ifDec07.c:626
If_Dec6Perform
word If_Dec6Perform(word t, int fDerive)
Definition ifDec07.c:409
If_Dec6Verify
void If_Dec6Verify(word t, word z)
Definition ifDec07.c:131
If_MatchCheck2
int If_MatchCheck2(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition ifDec07.c:1128
If_CutPerformCheck07
int If_CutPerformCheck07(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition ifDec07.c:1060
If_Dec6Truth
word If_Dec6Truth(word z)
Definition ifDec07.c:107
If_CutPerformDerive07
word If_CutPerformDerive07(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition ifDec07.c:1018
If_Dec7Perform
word If_Dec7Perform(word t0[2], int fDerive)
Definition ifDec07.c:449
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
If_DecPrintConfig
void If_DecPrintConfig(word z)
FUNCTION DEFINITIONS ///.
Definition ifDec07.c:66
If_Dec6MinimumBase
word If_Dec6MinimumBase(word uTruth, int *pSupp, int nVarsAll, int *pnVars)
Definition ifDec07.c:501
If_Dec5Perform
word If_Dec5Perform(word t, int fDerive)
Definition ifDec07.c:857
If_Dec5PerformEx
word If_Dec5PerformEx()
Definition ifDec07.c:975
If_Dec5PerformTest
void If_Dec5PerformTest()
Definition ifDec07.c:992
If_Dec7MinimumBase
void If_Dec7MinimumBase(word uTruth[2], int *pSupp, int nVarsAll, int *pnVars)
Definition ifDec07.c:533
If_Man_t
struct If_Man_t_ If_Man_t
BASIC TYPES ///.
Definition if.h:77
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213