ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
luckySwap.c
Go to the documentation of this file.
1
16
17#include "luckyInt.h"
18
19
21
22
23static word mask0[6] = { ABC_CONST(0x5555555555555555),ABC_CONST(0x3333333333333333), ABC_CONST(0x0F0F0F0F0F0F0F0F),ABC_CONST(0x00FF00FF00FF00FF),ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x00000000FFFFFFFF)};
24/*
25static word mask1[6] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
26static word mask[6][2] = {
27 {0x5555555555555555,0xAAAAAAAAAAAAAAAA},
28 {0x3333333333333333,0xCCCCCCCCCCCCCCCC},
29 {0x0F0F0F0F0F0F0F0F,0xF0F0F0F0F0F0F0F0},
30 {0x00FF00FF00FF00FF,0xFF00FF00FF00FF00},
31 {0x0000FFFF0000FFFF,0xFFFF0000FFFF0000},
32 {0x00000000FFFFFFFF,0xFFFFFFFF00000000}
33};
34*/
35
36int Kit_TruthWordNum_64bit( int nVars ) { return nVars <= 6 ? 1 : (1 << (nVars - 6));}
37
39{
40 x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
41 x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
42 x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
43 x = x + (x >> 8);
44 x = x + (x >> 16);
45 x = x + (x >> 32);
46 return (int)(x & 0xFF);
47}
48
49int Kit_TruthCountOnes_64bit( word* pIn, int nVars )
50{
51 int w, Counter = 0;
52 for ( w = Kit_TruthWordNum_64bit(nVars)-1; w >= 0; w-- )
53 Counter += Kit_WordCountOnes_64bit(pIn[w]);
54 return Counter;
55}
56
57void Kit_TruthCountOnesInCofs_64bit( word * pTruth, int nVars, int * pStore )
58{
59 int nWords = Kit_TruthWordNum_64bit( nVars );
60 int i, k, Counter;
61 memset( pStore, 0, sizeof(int) * nVars );
62 if ( nVars <= 6 )
63 {
64 if ( nVars > 0 )
65 pStore[0] = Kit_WordCountOnes_64bit( pTruth[0] & ABC_CONST(0x5555555555555555) );
66 if ( nVars > 1 )
67 pStore[1] = Kit_WordCountOnes_64bit( pTruth[0] & ABC_CONST(0x3333333333333333) );
68 if ( nVars > 2 )
69 pStore[2] = Kit_WordCountOnes_64bit( pTruth[0] & ABC_CONST(0x0F0F0F0F0F0F0F0F) );
70 if ( nVars > 3 )
71 pStore[3] = Kit_WordCountOnes_64bit( pTruth[0] & ABC_CONST(0x00FF00FF00FF00FF) );
72 if ( nVars > 4 )
73 pStore[4] = Kit_WordCountOnes_64bit( pTruth[0] & ABC_CONST(0x0000FFFF0000FFFF) );
74 if ( nVars > 5 )
75 pStore[5] = Kit_WordCountOnes_64bit( pTruth[0] & ABC_CONST(0x00000000FFFFFFFF) );
76 return;
77 }
78 // nVars > 6
79 // count 1's for all other variables
80 for ( k = 0; k < nWords; k++ )
81 {
82 Counter = Kit_WordCountOnes_64bit( pTruth[k] );
83 for ( i = 6; i < nVars; i++ )
84 if ( (k & (1 << (i-6))) == 0)
85 pStore[i] += Counter;
86 }
87 // count 1's for the first six variables
88 for ( k = nWords/2; k>0; k-- )
89 {
90 pStore[0] += Kit_WordCountOnes_64bit( (pTruth[0] & ABC_CONST(0x5555555555555555)) | ((pTruth[1] & ABC_CONST(0x5555555555555555)) << 1) );
91 pStore[1] += Kit_WordCountOnes_64bit( (pTruth[0] & ABC_CONST(0x3333333333333333)) | ((pTruth[1] & ABC_CONST(0x3333333333333333)) << 2) );
92 pStore[2] += Kit_WordCountOnes_64bit( (pTruth[0] & ABC_CONST(0x0F0F0F0F0F0F0F0F)) | ((pTruth[1] & ABC_CONST(0x0F0F0F0F0F0F0F0F)) << 4) );
93 pStore[3] += Kit_WordCountOnes_64bit( (pTruth[0] & ABC_CONST(0x00FF00FF00FF00FF)) | ((pTruth[1] & ABC_CONST(0x00FF00FF00FF00FF)) << 8) );
94 pStore[4] += Kit_WordCountOnes_64bit( (pTruth[0] & ABC_CONST(0x0000FFFF0000FFFF)) | ((pTruth[1] & ABC_CONST(0x0000FFFF0000FFFF)) << 16) );
95 pStore[5] += Kit_WordCountOnes_64bit( (pTruth[0] & ABC_CONST(0x00000000FFFFFFFF)) | ((pTruth[1] & ABC_CONST(0x00000000FFFFFFFF)) << 32) );
96 pTruth += 2;
97 }
98}
99
100void Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar )
101{
102 int nWords = Kit_TruthWordNum_64bit( nVars );
103 int i, Step,SizeOfBlock;
104 word Temp[512];
105
106 assert( iVar < nVars );
107 if(iVar<=5)
108 {
109 for ( i = 0; i < nWords; i++ )
110 pInOut[i] = ((pInOut[i] & mask0[iVar]) << (1<<(iVar))) | ((pInOut[i] & ~mask0[iVar]) >> (1<<(iVar)));
111 }
112 else
113 {
114 Step = (1 << (iVar - 6));
115 SizeOfBlock = sizeof(word)*Step;
116 for ( i = 0; i < nWords; i += 2*Step )
117 {
118 memcpy(Temp,pInOut,(size_t)SizeOfBlock);
119 memcpy(pInOut,pInOut+Step,(size_t)SizeOfBlock);
120 memcpy(pInOut+Step,Temp,(size_t)SizeOfBlock);
121 // Temp = pInOut[i];
122 // pInOut[i] = pInOut[Step+i];
123 // pInOut[Step+i] = Temp;
124 pInOut += 2*Step;
125 }
126 }
127
128}
129
130void Kit_TruthNot_64bit(word * pIn, int nVars )
131{
132 int w;
133 for ( w = Kit_TruthWordNum_64bit(nVars)-1; w >= 0; w-- )
134 pIn[w] = ~pIn[w];
135}
136void Kit_TruthCopy_64bit( word * pOut, word * pIn, int nVars )
137{
138 memcpy(pOut,pIn,Kit_TruthWordNum_64bit(nVars)*sizeof(word));
139}
140
141void Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar )
142{
143 int i, Step, Shift, SizeOfBlock; //
144 word temp[256]; // to make only pInOut possible
145 static word PMasks[5][3] = {
146 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
147 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
148 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
149 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
150 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
151 };
152 int nWords = Kit_TruthWordNum_64bit( nVars );
153
154 assert( iVar < nVars - 1 );
155 if ( iVar < 5 )
156 {
157 Shift = (1 << iVar);
158 for ( i = 0; i < nWords; i++ )
159 pInOut[i] = (pInOut[i] & PMasks[iVar][0]) | ((pInOut[i] & PMasks[iVar][1]) << Shift) | ((pInOut[i] & PMasks[iVar][2]) >> Shift);
160 }
161 else if ( iVar > 5 )
162 {
163 Step = 1 << (iVar - 6);
164 SizeOfBlock = sizeof(word)*Step;
165 pInOut += 2*Step;
166 for(i=2*Step; i<nWords; i+=4*Step)
167 {
168 memcpy(temp,pInOut-Step,(size_t)SizeOfBlock);
169 memcpy(pInOut-Step,pInOut,(size_t)SizeOfBlock);
170 memcpy(pInOut,temp,(size_t)SizeOfBlock);
171 pInOut += 4*Step;
172 }
173 }
174 else // if ( iVar == 5 )
175 {
176 for ( i = 0; i < nWords; i += 2 )
177 {
178 temp[0] = pInOut[i+1] << 32;
179 pInOut[i+1] ^= (temp[0] ^ pInOut[i]) >> 32;
180 pInOut[i] = (pInOut[i] & 0x00000000FFFFFFFF) | temp[0];
181
182 }
183 }
184}
185
186unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm )
187{
188 int pStore[16];
189 int nWords = Kit_TruthWordNum_64bit( nVars );
190 int i, Temp, fChange, nOnes;
191 unsigned uCanonPhase=0;
192 assert( nVars <= 16 );
193
194 nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
195
196 if ( (nOnes > nWords * 32) )
197 {
198 uCanonPhase |= (1 << nVars);
199 Kit_TruthNot_64bit( pInOut, nVars );
200 nOnes = nWords*64 - nOnes;
201 }
202
203 // collect the minterm counts
204 Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
205
206 // canonicize phase
207 for ( i = 0; i < nVars; i++ )
208 {
209 if ( pStore[i] >= nOnes-pStore[i])
210 continue;
211 uCanonPhase |= (1 << i);
212 pStore[i] = nOnes-pStore[i];
213 Kit_TruthChangePhase_64bit( pInOut, nVars, i );
214 }
215
216 do {
217 fChange = 0;
218 for ( i = 0; i < nVars-1; i++ )
219 {
220 if ( pStore[i] <= pStore[i+1] )
221 continue;
222 fChange = 1;
223
224 Temp = pCanonPerm[i];
225 pCanonPerm[i] = pCanonPerm[i+1];
226 pCanonPerm[i+1] = Temp;
227
228 Temp = pStore[i];
229 pStore[i] = pStore[i+1];
230 pStore[i+1] = Temp;
231
232 // if the polarity of variables is different, swap them
233 if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
234 {
235 uCanonPhase ^= (1 << i);
236 uCanonPhase ^= (1 << (i+1));
237 }
238
239 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
240 }
241 } while ( fChange );
242 return uCanonPhase;
243}
244
245unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
246{
247 int nWords = Kit_TruthWordNum_64bit( nVars );
248 int i, fChange, nOnes;
249 int Temp;
250 unsigned uCanonPhase=0;
251 assert( nVars <= 16 );
252
253 nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
254 if ( nOnes == nWords * 32 )
255 uCanonPhase |= (1 << (nVars+2));
256
257 else if ( (nOnes > nWords * 32) )
258 {
259 uCanonPhase |= (1 << nVars);
260 Kit_TruthNot_64bit( pInOut, nVars );
261 nOnes = nWords*64 - nOnes;
262 }
263
264 // collect the minterm counts
265 Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
266
267 // canonicize phase
268 for ( i = 0; i < nVars; i++ )
269 {
270 if ( 2*pStore[i] == nOnes)
271 {
272 uCanonPhase |= (1 << (nVars+1));
273 continue;
274 }
275 if ( pStore[i] > nOnes-pStore[i])
276 continue;
277 uCanonPhase |= (1 << i);
278 pStore[i] = nOnes-pStore[i];
279 Kit_TruthChangePhase_64bit( pInOut, nVars, i );
280 }
281
282 do {
283 fChange = 0;
284 for ( i = 0; i < nVars-1; i++ )
285 {
286 if ( pStore[i] <= pStore[i+1] )
287 continue;
288 fChange = 1;
289
290 Temp = pCanonPerm[i];
291 pCanonPerm[i] = pCanonPerm[i+1];
292 pCanonPerm[i+1] = Temp;
293
294 Temp = pStore[i];
295 pStore[i] = pStore[i+1];
296 pStore[i+1] = Temp;
297
298 // if the polarity of variables is different, swap them
299 if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
300 {
301 uCanonPhase ^= (1 << i);
302 uCanonPhase ^= (1 << (i+1));
303 }
304
305 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
306 }
307 } while ( fChange );
308 return uCanonPhase;
309}
310
311
312// unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
313// {
314// unsigned uCanonPhase = 0;
315// int pStore[16];
316// int nWords = Kit_TruthWordNum_64bit( nVars );
317// int i, Temp, fChange, nOnes;
318// assert( nVars <= 16 );
319//
320// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
321//
322// if ( (nOnes > nWords * 32) )
323// {
324// Kit_TruthNot_64bit( pInOut, nVars );
325// nOnes = nWords*64 - nOnes;
326// }
327//
328// // collect the minterm counts
329// Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
330//
331// // canonicize phase
332// for ( i = 0; i < nVars; i++ )
333// {
334// if ( pStore[i] >= nOnes-pStore[i])
335// continue;
336// pStore[i] = nOnes-pStore[i];
337// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
338// }
339//
340// do {
341// fChange = 0;
342// for ( i = 0; i < nVars-1; i++ )
343// {
344// if ( pStore[i] <= pStore[i+1] )
345// continue;
346// fChange = 1;
347//
348// Temp = pStore[i];
349// pStore[i] = pStore[i+1];
350// pStore[i+1] = Temp;
351//
352// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
353// }
354// } while ( fChange );
355// return uCanonPhase;
356// }
357
358void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore )
359{
360 int nWords = Kit_TruthWordNum_64bit( nVars );
361 int i, Temp, fChange, nOnes;
362 assert( nVars <= 16 );
363
364 nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
365
366 if ( (nOnes > nWords * 32) )
367 {
368 Kit_TruthNot_64bit( pInOut, nVars );
369 nOnes = nWords*64 - nOnes;
370 }
371
372 // collect the minterm counts
373 Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
374
375 // canonicize phase
376 for ( i = 0; i < nVars; i++ )
377 {
378 if ( pStore[i] >= nOnes-pStore[i])
379 continue;
380 pStore[i] = nOnes-pStore[i];
381 Kit_TruthChangePhase_64bit( pInOut, nVars, i );
382 }
383
384 do {
385 fChange = 0;
386 for ( i = 0; i < nVars-1; i++ )
387 {
388 if ( pStore[i] <= pStore[i+1] )
389 continue;
390 fChange = 1;
391
392 Temp = pStore[i];
393 pStore[i] = pStore[i+1];
394 pStore[i+1] = Temp;
395
396 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
397 }
398 } while ( fChange );
399}
400
401
int nWords
Definition abcNpn.c:127
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
void Kit_TruthChangePhase_64bit(word *pInOut, int nVars, int iVar)
Definition luckySwap.c:100
void Kit_TruthSwapAdjacentVars_64bit(word *pInOut, int nVars, int iVar)
Definition luckySwap.c:141
int Kit_TruthCountOnes_64bit(word *pIn, int nVars)
Definition luckySwap.c:49
int Kit_TruthWordNum_64bit(int nVars)
Definition luckySwap.c:36
void Kit_TruthSemiCanonicize_Yasha_simple(word *pInOut, int nVars, int *pStore)
Definition luckySwap.c:358
void Kit_TruthNot_64bit(word *pIn, int nVars)
Definition luckySwap.c:130
unsigned Kit_TruthSemiCanonicize_Yasha1(word *pInOut, int nVars, char *pCanonPerm, int *pStore)
Definition luckySwap.c:245
void Kit_TruthCountOnesInCofs_64bit(word *pTruth, int nVars, int *pStore)
Definition luckySwap.c:57
void Kit_TruthCopy_64bit(word *pOut, word *pIn, int nVars)
Definition luckySwap.c:136
unsigned Kit_TruthSemiCanonicize_Yasha(word *pInOut, int nVars, char *pCanonPerm)
Definition luckySwap.c:186
int Kit_WordCountOnes_64bit(word x)
Definition luckySwap.c:38
#define assert(ex)
Definition util_old.h:213
char * memcpy()
char * memset()