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
If_Dec10WordNum(int nVars)77 static inline int If_Dec10WordNum( int nVars )
78 {
79 return nVars <= 6 ? 1 : 1 << (nVars-6);
80 }
If_Dec10PrintConfigOne(unsigned z)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 }
If_Dec10PrintConfig(unsigned * pZ)95 void If_Dec10PrintConfig( unsigned * pZ )
96 {
97 while ( *pZ )
98 If_Dec10PrintConfigOne( *pZ++ );
99 }
If_Dec10ComposeLut4(int t,word ** pF,word * pR,int nVars)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 }
If_Dec10Verify(word * pF,int nVars,unsigned * pZ)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
If_Dec10CofCount2(word * pF,int nVars)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 }
If_Dec10CofCount(word * pF,int nVars)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
If_Dec10Copy(word * pOut,word * pIn,int nVars)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 }
If_Dec10SwapAdjacent(word * pOut,word * pIn,int iVar,int nVars)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 }
If_Dec10MoveTo(word * pF,int nVars,int v,int p,int Pla2Var[],int Var2Pla[])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
If_DecSuppIsMinBase(int Supp)301 static inline int If_DecSuppIsMinBase( int Supp )
302 {
303 return (Supp & (Supp+1)) == 0;
304 }
If_Dec10HasVar(word * t,int nVars,int iVar)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 }
If_Dec10Support(word * t,int nVars)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
If_Dec10Cofactors(word * pF,int nVars,int iVar,word * pCof0,word * pCof1)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 }
If_Dec10Count16(int Num16)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 }
If_DecVerifyPerm(int Pla2Var[10],int Var2Pla[10],int nVars)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 }
If_Dec10Perform(word * pF,int nVars,int fDerive)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 ***********************************************************************/
If_CutPerformCheck10(If_Man_t * p,unsigned * pTruth,int nVars,int nLeaves,char * pStr)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
507