abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ifDec10.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ifDec10.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: ifDec10.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 Truth10[10][16] = {
61  {ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA)},
62  {ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC)},
63  {ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0)},
64  {ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00)},
65  {ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000)},
66  {ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000)},
67  {ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
68  {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
69  {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
70  {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)}
71 };
72 
73 ////////////////////////////////////////////////////////////////////////
74 /// FUNCTION DEFINITIONS ///
75 ////////////////////////////////////////////////////////////////////////
76 
77 static inline int If_Dec10WordNum( int nVars )
78 {
79  return nVars <= 6 ? 1 : 1 << (nVars-6);
80 }
81 static void If_Dec10PrintConfigOne( unsigned z )
82 {
83  unsigned t;
84  t = (z & 0xffff) | ((z & 0xffff) << 16);
85  Extra_PrintBinary( stdout, &t, 16 );
86  printf( " " );
87  Kit_DsdPrintFromTruth( &t, 4 );
88  printf( " " );
89  printf( " %d", (z >> 16) & 7 );
90  printf( " %d", (z >> 20) & 7 );
91  printf( " %d", (z >> 24) & 7 );
92  printf( " %d", (z >> 28) & 7 );
93  printf( "\n" );
94 }
95 void If_Dec10PrintConfig( unsigned * pZ )
96 {
97  while ( *pZ )
98  If_Dec10PrintConfigOne( *pZ++ );
99 }
100 static inline void If_Dec10ComposeLut4( int t, word ** pF, word * pR, int nVars )
101 {
102  word pC[16];
103  int m, w, v, nWords;
104  assert( nVars <= 10 );
105  nWords = If_Dec10WordNum( nVars );
106  for ( w = 0; w < nWords; w++ )
107  pR[w] = 0;
108  for ( m = 0; m < 16; m++ )
109  {
110  if ( !((t >> m) & 1) )
111  continue;
112  for ( w = 0; w < nWords; w++ )
113  pC[w] = ~(word)0;
114  for ( v = 0; v < 4; v++ )
115  for ( w = 0; w < nWords; w++ )
116  pC[w] &= ((m >> v) & 1) ? pF[v][w] : ~pF[v][w];
117  for ( w = 0; w < nWords; w++ )
118  pR[w] |= pC[w];
119  }
120 }
121 void If_Dec10Verify( word * pF, int nVars, unsigned * pZ )
122 {
123  word pN[16][16], * pG[4];
124  int i, w, v, k, nWords;
125  unsigned z;
126  nWords = If_Dec10WordNum( nVars );
127  for ( k = 0; k < nVars; k++ )
128  for ( w = 0; w < nWords; w++ )
129  pN[k][w] = Truth10[k][w];
130  for ( i = 0; (z = pZ[i]); i++, k++ )
131  {
132  for ( v = 0; v < 4; v++ )
133  pG[v] = pN[ (z >> (16+(v<<2))) & 7 ];
134  If_Dec10ComposeLut4( (int)(z & 0xffff), pG, pN[k], nVars );
135  }
136  k--;
137  for ( w = 0; w < nWords; w++ )
138  if ( pN[k][w] != pF[w] )
139  {
140  If_Dec10PrintConfig( pZ );
141  Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
142  Kit_DsdPrintFromTruth( (unsigned*)pN[k], nVars ); printf( "\n" );
143  printf( "Verification failed!\n" );
144  break;
145  }
146 }
147 
148 
149 // count the number of unique cofactors
150 static inline int If_Dec10CofCount2( word * pF, int nVars )
151 {
152  int nShift = (1 << (nVars - 4));
153  word Mask = (((word)1) << nShift) - 1;
154  word iCof0 = pF[0] & Mask;
155  word iCof1 = iCof0, iCof;
156  int i;
157  assert( nVars > 6 && nVars <= 10 );
158  if ( nVars == 10 )
159  Mask = ~(word)0;
160  for ( i = 1; i < 16; i++ )
161  {
162  iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
163  if ( iCof == iCof0 )
164  continue;
165  if ( iCof1 == iCof0 )
166  iCof1 = iCof;
167  else if ( iCof != iCof1 )
168  return 3;
169  }
170  return 2;
171 }
172 static inline int If_Dec10CofCount( word * pF, int nVars )
173 {
174  int nShift = (1 << (nVars - 4));
175  word Mask = (((word)1) << nShift) - 1;
176  word iCofs[16], iCof;
177  int i, c, nCofs = 1;
178  if ( nVars == 10 )
179  Mask = ~(word)0;
180  iCofs[0] = pF[0] & Mask;
181  for ( i = 1; i < 16; i++ )
182  {
183  iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
184  for ( c = 0; c < nCofs; c++ )
185  if ( iCof == iCofs[c] )
186  break;
187  if ( c == nCofs )
188  iCofs[nCofs++] = iCof;
189  }
190  return nCofs;
191 }
192 
193 
194 // variable permutation for large functions
195 static inline void If_Dec10Copy( word * pOut, word * pIn, int nVars )
196 {
197  int w, nWords = If_Dec10WordNum( nVars );
198  for ( w = 0; w < nWords; w++ )
199  pOut[w] = pIn[w];
200 }
201 static inline void If_Dec10SwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
202 {
203  int i, k, nWords = If_Dec10WordNum( nVars );
204  assert( iVar < nVars - 1 );
205  if ( iVar < 5 )
206  {
207  int Shift = (1 << iVar);
208  for ( i = 0; i < nWords; i++ )
209  pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
210  }
211  else if ( iVar > 5 )
212  {
213  int Step = (1 << (iVar - 6));
214  for ( k = 0; k < nWords; k += 4*Step )
215  {
216  for ( i = 0; i < Step; i++ )
217  pOut[i] = pIn[i];
218  for ( i = 0; i < Step; i++ )
219  pOut[Step+i] = pIn[2*Step+i];
220  for ( i = 0; i < Step; i++ )
221  pOut[2*Step+i] = pIn[Step+i];
222  for ( i = 0; i < Step; i++ )
223  pOut[3*Step+i] = pIn[3*Step+i];
224  pIn += 4*Step;
225  pOut += 4*Step;
226  }
227  }
228  else // if ( iVar == 5 )
229  {
230  for ( i = 0; i < nWords; i += 2 )
231  {
232  pOut[i] = (pIn[i] & ABC_CONST(0x00000000FFFFFFFF)) | ((pIn[i+1] & ABC_CONST(0x00000000FFFFFFFF)) << 32);
233  pOut[i+1] = (pIn[i+1] & ABC_CONST(0xFFFFFFFF00000000)) | ((pIn[i] & ABC_CONST(0xFFFFFFFF00000000)) >> 32);
234  }
235  }
236 }
237 static inline void If_Dec10MoveTo( word * pF, int nVars, int v, int p, int Pla2Var[], int Var2Pla[] )
238 {
239  word pG[16], * pIn = pF, * pOut = pG, * pTemp;
240  int iPlace0, iPlace1, Count = 0;
241  assert( Var2Pla[v] <= p );
242  while ( Var2Pla[v] != p )
243  {
244  iPlace0 = Var2Pla[v];
245  iPlace1 = Var2Pla[v]+1;
246  If_Dec10SwapAdjacent( pOut, pIn, iPlace0, nVars );
247  pTemp = pIn; pIn = pOut, pOut = pTemp;
248  Var2Pla[Pla2Var[iPlace0]]++;
249  Var2Pla[Pla2Var[iPlace1]]--;
250  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
251  Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
252  Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
253  Count++;
254  }
255  if ( Count & 1 )
256  If_Dec10Copy( pF, pIn, nVars );
257  assert( Pla2Var[p] == v );
258 }
259 /*
260 // derive binary function
261 static inline int If_Dec10DeriveCount2( word * pF, word * pRes, int nVars )
262 {
263  int nShift = (1 << (nVars - 4));
264  word Mask = (((word)1) << nShift) - 1;
265  int i, MaskDec = 0;
266  word iCof0 = pF[0] & Mask;
267  word iCof1 = pF[0] & Mask;
268  word iCof, * pCof0, * pCof1;
269  if ( nVars == 10 )
270  Mask = ~(word)0;
271  for ( i = 1; i < 16; i++ )
272  {
273  iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
274  if ( *pCof0 != iCof )
275  {
276  *pCof1 = iCof;
277  MaskDec |= (1 << i);
278  }
279  }
280  *pRes = ((iCof1 << nShift) | iCof0);
281  return MaskDec;
282 }
283 static inline word If_DecTruthStretch( word t, int nVars )
284 {
285  assert( nVars > 1 );
286  if ( nVars == 1 )
287  nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
288  if ( nVars == 2 )
289  nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
290  if ( nVars == 3 )
291  nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
292  if ( nVars == 4 )
293  nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
294  if ( nVars == 5 )
295  nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
296  assert( nVars >= 6 );
297 }
298 */
299 
300 // support minimization
301 static inline int If_DecSuppIsMinBase( int Supp )
302 {
303  return (Supp & (Supp+1)) == 0;
304 }
305 static inline int If_Dec10HasVar( word * t, int nVars, int iVar )
306 {
307  int nWords = If_Dec10WordNum( nVars );
308  assert( iVar < nVars );
309  if ( iVar < 6 )
310  {
311  int i, Shift = (1 << iVar);
312  for ( i = 0; i < nWords; i++ )
313  if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
314  return 1;
315  return 0;
316  }
317  else
318  {
319  int i, k, Step = (1 << (iVar - 6));
320  for ( k = 0; k < nWords; k += 2*Step )
321  {
322  for ( i = 0; i < Step; i++ )
323  if ( t[i] != t[Step+i] )
324  return 1;
325  t += 2*Step;
326  }
327  return 0;
328  }
329 }
330 static inline int If_Dec10Support( word * t, int nVars )
331 {
332  int v, Supp = 0;
333  for ( v = 0; v < nVars; v++ )
334  if ( If_Dec10HasVar( t, nVars, v ) )
335  Supp |= (1 << v);
336  return Supp;
337 }
338 
339 // checks
340 void If_Dec10Cofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 )
341 {
342  int nWords = If_Dec10WordNum( nVars );
343  assert( iVar < nVars );
344  if ( iVar < 6 )
345  {
346  int i, Shift = (1 << iVar);
347  for ( i = 0; i < nWords; i++ )
348  {
349  pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift);
350  pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift);
351  }
352  return;
353  }
354  else
355  {
356  int i, k, Step = (1 << (iVar - 6));
357  for ( k = 0; k < nWords; k += 2*Step )
358  {
359  for ( i = 0; i < Step; i++ )
360  {
361  pCof0[i] = pCof0[Step+i] = pF[i];
362  pCof1[i] = pCof1[Step+i] = pF[Step+i];
363  }
364  pF += 2*Step;
365  pCof0 += 2*Step;
366  pCof1 += 2*Step;
367  }
368  return;
369  }
370 }
371 static inline int If_Dec10Count16( int Num16 )
372 {
373  assert( Num16 < (1<<16)-1 );
374  return BitCount8[Num16 & 255] + BitCount8[(Num16 >> 8) & 255];
375 }
376 static inline void If_DecVerifyPerm( int Pla2Var[10], int Var2Pla[10], int nVars )
377 {
378  int i;
379  for ( i = 0; i < nVars; i++ )
380  assert( Pla2Var[Var2Pla[i]] == i );
381 }
382 int If_Dec10Perform( word * pF, int nVars, int fDerive )
383 {
384 // static int Cnt = 0;
385  word pCof0[16], pCof1[16];
386  int Pla2Var[10], Var2Pla[10], Count[210], Masks[210];
387  int i, i0,i1,i2,i3, v, x;
388  assert( nVars >= 6 && nVars <= 10 );
389  // start arrays
390  for ( i = 0; i < nVars; i++ )
391  {
392  assert( If_Dec10HasVar( pF, nVars, i ) );
393  Pla2Var[i] = Var2Pla[i] = i;
394  }
395 /*
396  Cnt++;
397 //if ( Cnt == 108 )
398 {
399 printf( "%d\n", Cnt );
400 //Extra_PrintHex( stdout, (unsigned *)pF, nVars );
401 //printf( "\n" );
402 Kit_DsdPrintFromTruth( (unsigned *)pF, nVars );
403 printf( "\n" );
404 printf( "\n" );
405 }
406 */
407  // generate permutations
408  v = 0;
409  for ( i0 = 0; i0 < nVars; i0++ )
410  for ( i1 = i0+1; i1 < nVars; i1++ )
411  for ( i2 = i1+1; i2 < nVars; i2++ )
412  for ( i3 = i2+1; i3 < nVars; i3++, v++ )
413  {
414  If_Dec10MoveTo( pF, nVars, i0, nVars-1, Pla2Var, Var2Pla );
415  If_Dec10MoveTo( pF, nVars, i1, nVars-2, Pla2Var, Var2Pla );
416  If_Dec10MoveTo( pF, nVars, i2, nVars-3, Pla2Var, Var2Pla );
417  If_Dec10MoveTo( pF, nVars, i3, nVars-4, Pla2Var, Var2Pla );
418  If_DecVerifyPerm( Pla2Var, Var2Pla, nVars );
419  Count[v] = If_Dec10CofCount( pF, nVars );
420  Masks[v] = (1 << i0) | (1 << i1) | (1 << i2) | (1 << i3);
421  assert( Count[v] > 1 );
422 //printf( "%d ", Count[v] );
423  if ( Count[v] == 2 || Count[v] > 5 )
424  continue;
425  for ( x = 0; x < 4; x++ )
426  {
427  If_Dec10Cofactors( pF, nVars, nVars-1-x, pCof0, pCof1 );
428  if ( If_Dec10CofCount2(pCof0, nVars) <= 2 && If_Dec10CofCount2(pCof1, nVars) <= 2 )
429  {
430  Count[v] = -Count[v];
431  break;
432  }
433  }
434  }
435 //printf( "\n" );
436  assert( v <= 210 );
437  // check if there are compatible bound sets
438  for ( i0 = 0; i0 < v; i0++ )
439  for ( i1 = i0+1; i1 < v; i1++ )
440  {
441  if ( If_Dec10Count16(Masks[i0] & Masks[i1]) > 10 - nVars )
442  continue;
443  if ( nVars == 10 )
444  {
445  if ( Count[i0] == 2 && Count[i1] == 2 )
446  return 1;
447  }
448  else if ( nVars == 9 )
449  {
450  if ( (Count[i0] == 2 && Count[i1] == 2) ||
451  (Count[i0] == 2 && Count[i1] < 0) ||
452  (Count[i0] < 0 && Count[i1] == 2) )
453  return 1;
454  }
455  else
456  {
457  if ( (Count[i0] == 2 && Count[i1] == 2) ||
458  (Count[i0] == 2 && Count[i1] < 0) ||
459  (Count[i0] < 0 && Count[i1] == 2) ||
460  (Count[i0] < 0 && Count[i1] < 0) )
461  return 1;
462  }
463  }
464 // printf( "not found\n" );
465  return 0;
466 }
467 
468 
469 /**Function*************************************************************
470 
471  Synopsis [Performs additional check.]
472 
473  Description []
474 
475  SideEffects []
476 
477  SeeAlso []
478 
479 ***********************************************************************/
480 int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
481 {
482  int nSupp, fDerive = 0;
483  word pF[16];
484  if ( nLeaves <= 6 )
485  return 1;
486  If_Dec10Copy( pF, (word *)pTruth, nVars );
487  nSupp = If_Dec10Support( pF, nLeaves );
488  if ( !nSupp || !If_DecSuppIsMinBase(nSupp) )
489  return 0;
490  if ( If_Dec10Perform( pF, nLeaves, fDerive ) )
491  {
492 // printf( "1" );
493  return 1;
494 // If_Dec10Verify( t, nLeaves, NULL );
495  }
496 // printf( "0" );
497  return 0;
498 }
499 
500 ////////////////////////////////////////////////////////////////////////
501 /// END OF FILE ///
502 ////////////////////////////////////////////////////////////////////////
503 
504 
505 ABC_NAMESPACE_IMPL_END
506 
If_Dec10CofCount
static int If_Dec10CofCount(word *pF, int nVars)
Definition: ifDec10.c:172
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
If_DecVerifyPerm
static void If_DecVerifyPerm(int Pla2Var[10], int Var2Pla[10], int nVars)
Definition: ifDec10.c:376
If_Dec10SwapAdjacent
static void If_Dec10SwapAdjacent(word *pOut, word *pIn, int iVar, int nVars)
Definition: ifDec10.c:201
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition: kitDsd.c:490
nWords
int nWords
Definition: abcNpn.c:127
If_Dec10WordNum
static int If_Dec10WordNum(int nVars)
FUNCTION DEFINITIONS ///.
Definition: ifDec10.c:77
If_Dec10Count16
static int If_Dec10Count16(int Num16)
Definition: ifDec10.c:371
PMasks
static word PMasks[5][3]
Definition: ifDec10.c:44
If_Dec10Support
static int If_Dec10Support(word *t, int nVars)
Definition: ifDec10.c:330
If_Dec10Cofactors
void If_Dec10Cofactors(word *pF, int nVars, int iVar, word *pCof0, word *pCof1)
Definition: ifDec10.c:340
If_Dec10ComposeLut4
static void If_Dec10ComposeLut4(int t, word **pF, word *pR, int nVars)
Definition: ifDec10.c:100
If_Man_t_
Definition: if.h:180
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Truth6
static word Truth6[6]
Definition: ifDec10.c:52
If_DecSuppIsMinBase
static int If_DecSuppIsMinBase(int Supp)
Definition: ifDec10.c:301
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
BitCount8
static ABC_NAMESPACE_IMPL_START int BitCount8[256]
DECLARATIONS ///.
Definition: ifDec10.c:33
If_Dec10Perform
int If_Dec10Perform(word *pF, int nVars, int fDerive)
Definition: ifDec10.c:382
If_Dec10PrintConfig
void If_Dec10PrintConfig(unsigned *pZ)
Definition: ifDec10.c:95
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
If_Dec10HasVar
static int If_Dec10HasVar(word *t, int nVars, int iVar)
Definition: ifDec10.c:305
If_Dec10CofCount2
static int If_Dec10CofCount2(word *pF, int nVars)
Definition: ifDec10.c:150
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition: extraUtilFile.c:497
Truth10
static word Truth10[10][16]
Definition: ifDec10.c:60
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
If_Dec10Verify
void If_Dec10Verify(word *pF, int nVars, unsigned *pZ)
Definition: ifDec10.c:121
If_CutPerformCheck10
int If_CutPerformCheck10(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition: ifDec10.c:480
assert
#define assert(ex)
Definition: util_old.h:213
If_Dec10Copy
static void If_Dec10Copy(word *pOut, word *pIn, int nVars)
Definition: ifDec10.c:195
If_Dec10MoveTo
static void If_Dec10MoveTo(word *pF, int nVars, int v, int p, int Pla2Var[], int Var2Pla[])
Definition: ifDec10.c:237
If_Dec10PrintConfigOne
static void If_Dec10PrintConfigOne(unsigned z)
Definition: ifDec10.c:81