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