ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
exorBits.c
Go to the documentation of this file.
1
20
40
41#include "exor.h"
42
43#ifdef _MSC_VER
44# include <intrin.h>
45# define __builtin_popcount __popcnt
46#endif
47
49
53
57
58// information about the cube cover
59// the number of cubes is constantly updated when the cube cover is processed
60// in this module, only the number of variables (nVarsIn) and integers (nWordsIn)
61// is used, which do not change
62extern cinfo g_CoverInfo;
63
67
68int GetDistance( Cube * pC1, Cube * pC2 );
69// return the distance between two cubes
70int GetDistancePlus( Cube * pC1, Cube * pC2 );
71
72int FindDiffVars( int * pDiffVars, Cube * pC1, Cube * pC2 );
73// determine different variables in cubes from pCubes[] and writes them into pDiffVars
74// returns the number of different variables
75
76void InsertVars( Cube * pC, int * pVars, int nVarsIn, int * pVarValues );
77
78//inline int VarWord( int element );
79//inline int VarBit( int element );
80varvalue GetVar( Cube * pC, int Var );
81
82void ExorVar( Cube * pC, int Var, varvalue Val );
83
87
88static int SparseNumbers[163] = {
89 0,1,4,5,16,17,20,21,64,65,68,69,80,81,84,85,256,257,260,
90 261,272,273,276,277,320,321,324,325,336,337,340,1024,1025,
91 1028,1029,1040,1041,1044,1045,1088,1089,1092,1093,1104,1105,
92 1108,1280,1281,1284,1285,1296,1297,1300,1344,1345,1348,1360,
93 4096,4097,4100,4101,4112,4113,4116,4117,4160,4161,4164,4165,
94 4176,4177,4180,4352,4353,4356,4357,4368,4369,4372,4416,4417,
95 4420,4432,5120,5121,5124,5125,5136,5137,5140,5184,5185,5188,
96 5200,5376,5377,5380,5392,5440,16384,16385,16388,16389,16400,
97 16401,16404,16405,16448,16449,16452,16453,16464,16465,16468,
98 16640,16641,16644,16645,16656,16657,16660,16704,16705,16708,
99 16720,17408,17409,17412,17413,17424,17425,17428,17472,17473,
100 17476,17488,17664,17665,17668,17680,17728,20480,20481,20484,
101 20485,20496,20497,20500,20544,20545,20548,20560,20736,20737,
102 20740,20752,20800,21504,21505,21508,21520,21568,21760
103};
104
105static unsigned char GroupLiterals[163][4] = {
106 {0}, {0}, {1}, {0,1}, {2}, {0,2}, {1,2}, {0,1,2}, {3}, {0,3},
107 {1,3}, {0,1,3}, {2,3}, {0,2,3}, {1,2,3}, {0,1,2,3}, {4}, {0,4},
108 {1,4}, {0,1,4}, {2,4}, {0,2,4}, {1,2,4}, {0,1,2,4}, {3,4},
109 {0,3,4}, {1,3,4}, {0,1,3,4}, {2,3,4}, {0,2,3,4}, {1,2,3,4}, {5},
110 {0,5}, {1,5}, {0,1,5}, {2,5}, {0,2,5}, {1,2,5}, {0,1,2,5}, {3,5},
111 {0,3,5}, {1,3,5}, {0,1,3,5}, {2,3,5}, {0,2,3,5}, {1,2,3,5},
112 {4,5}, {0,4,5}, {1,4,5}, {0,1,4,5}, {2,4,5}, {0,2,4,5},
113 {1,2,4,5}, {3,4,5}, {0,3,4,5}, {1,3,4,5}, {2,3,4,5}, {6}, {0,6},
114 {1,6}, {0,1,6}, {2,6}, {0,2,6}, {1,2,6}, {0,1,2,6}, {3,6},
115 {0,3,6}, {1,3,6}, {0,1,3,6}, {2,3,6}, {0,2,3,6}, {1,2,3,6},
116 {4,6}, {0,4,6}, {1,4,6}, {0,1,4,6}, {2,4,6}, {0,2,4,6},
117 {1,2,4,6}, {3,4,6}, {0,3,4,6}, {1,3,4,6}, {2,3,4,6}, {5,6},
118 {0,5,6}, {1,5,6}, {0,1,5,6}, {2,5,6}, {0,2,5,6}, {1,2,5,6},
119 {3,5,6}, {0,3,5,6}, {1,3,5,6}, {2,3,5,6}, {4,5,6}, {0,4,5,6},
120 {1,4,5,6}, {2,4,5,6}, {3,4,5,6}, {7}, {0,7}, {1,7}, {0,1,7},
121 {2,7}, {0,2,7}, {1,2,7}, {0,1,2,7}, {3,7}, {0,3,7}, {1,3,7},
122 {0,1,3,7}, {2,3,7}, {0,2,3,7}, {1,2,3,7}, {4,7}, {0,4,7},
123 {1,4,7}, {0,1,4,7}, {2,4,7}, {0,2,4,7}, {1,2,4,7}, {3,4,7},
124 {0,3,4,7}, {1,3,4,7}, {2,3,4,7}, {5,7}, {0,5,7}, {1,5,7},
125 {0,1,5,7}, {2,5,7}, {0,2,5,7}, {1,2,5,7}, {3,5,7}, {0,3,5,7},
126 {1,3,5,7}, {2,3,5,7}, {4,5,7}, {0,4,5,7}, {1,4,5,7}, {2,4,5,7},
127 {3,4,5,7}, {6,7}, {0,6,7}, {1,6,7}, {0,1,6,7}, {2,6,7},
128 {0,2,6,7}, {1,2,6,7}, {3,6,7}, {0,3,6,7}, {1,3,6,7}, {2,3,6,7},
129 {4,6,7}, {0,4,6,7}, {1,4,6,7}, {2,4,6,7}, {3,4,6,7}, {5,6,7},
130 {0,5,6,7}, {1,5,6,7}, {2,5,6,7}, {3,5,6,7}, {4,5,6,7}
131};
132
133// the bit count to 16-bit numbers
134#define FULL16BITS 0x10000
135#define MARKNUMBER 200
136
137static unsigned char BitGroupNumbers[FULL16BITS];
138unsigned char BitCount[FULL16BITS];
139
143
145// this function should be called before anything is done with the cube cover
146{
147 // prepare bit count
148 int i, k;
149 int nLimit;
150
151 nLimit = FULL16BITS;
152 for ( i = 0; i < nLimit; i++ )
153 {
154 BitCount[i] = __builtin_popcount( i & 0xffff );
155 BitGroupNumbers[i] = MARKNUMBER;
156 }
157 // prepare bit groups
158 for ( k = 0; k < 163; k++ )
159 BitGroupNumbers[ SparseNumbers[k] ] = k;
160/*
161 // verify bit groups
162 int n = 4368;
163 char Buff[100];
164 cout << "The number is " << n << endl;
165 cout << "The binary is " << itoa(n,Buff,2) << endl;
166 cout << "BitGroupNumbers[n] is " << (int)BitGroupNumbers[n] << endl;
167 cout << "The group literals are ";
168 for ( int g = 0; g < 4; g++ )
169 cout << " " << (int)GroupLiterals[BitGroupNumbers[n]][g];
170*/
171}
172
176/*
177int VarWord( int element )
178{
179 return ( element >> LOGBPI );
180}
181
182int VarBit( int element )
183{
184 return ( element & BPIMASK );
185}
186*/
187
189// returns VAR_NEG if var is neg, VAR_POS if var is pos, VAR_ABS if var is absent
190{
191 int Bit = (Var<<1);
192 int Value = ((pC->pCubeDataIn[VarWord(Bit)] >> VarBit(Bit)) & 3);
193 assert( Value == VAR_NEG || Value == VAR_POS || Value == VAR_ABS );
194 return (varvalue)Value;
195}
196
197void ExorVar( Cube * pC, int Var, varvalue Val )
198// EXORs the value Val with the value of variable Var in the given cube
199// ((cube[VAR_WORD((v)<<1)]) ^ ( (pol)<<VAR_BIT((v)<<1) ))
200{
201 int Bit = (Var<<1);
202 pC->pCubeDataIn[VarWord(Bit)] ^= ( Val << VarBit(Bit) );
203}
204
208
209static int DiffVarCounter, cVars;
210static drow Temp1, Temp2, Temp;
211static drow LastNonZeroWord;
212static int LastNonZeroWordNum;
213
214int GetDistance( Cube * pC1, Cube * pC2 )
215// finds and returns the distance between two cubes pC1 and pC2
216{
217 int i;
218 DiffVarCounter = 0;
219
220 for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
221 {
222 Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i];
223 Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT;
224
225 // count how many bits are one in this var difference
226 DiffVarCounter += BIT_COUNT(Temp2);
227 if ( DiffVarCounter > 4 )
228 return 5;
229 }
230 // check whether the output parts are different
231 for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
232 if ( pC1->pCubeDataOut[i] ^ pC2->pCubeDataOut[i] )
233 {
234 DiffVarCounter++;
235 break;
236 }
237 return DiffVarCounter;
238}
239
240// place to put the number of the different variable and its value in the second cube
241extern int s_DiffVarNum;
242extern int s_DiffVarValueP_old;
243extern int s_DiffVarValueP_new;
244extern int s_DiffVarValueQ;
245
246int GetDistancePlus( Cube * pC1, Cube * pC2 )
247// finds and returns the distance between two cubes pC1 and pC2
248// if the distance is 1, returns the number of diff variable in VarNum
249{
250 int i;
251
252 DiffVarCounter = 0;
253 LastNonZeroWordNum = -1;
254 for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
255 {
256 Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i];
257 Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT;
258
259 // save the value of var difference, in case
260 // the distance is one and we need to return the var number
261 if ( Temp2 )
262 {
263 LastNonZeroWordNum = i;
264 LastNonZeroWord = Temp2;
265 }
266
267 // count how many bits are one in this var difference
268 DiffVarCounter += BIT_COUNT(Temp2);
269 if ( DiffVarCounter > 4 )
270 return 5;
271 }
272 // check whether the output parts are different
273 for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
274 if ( pC1->pCubeDataOut[i] ^ pC2->pCubeDataOut[i] )
275 {
276 DiffVarCounter++;
277 break;
278 }
279
280 if ( DiffVarCounter == 1 )
281 {
282 if ( LastNonZeroWordNum == -1 ) // the output is the only different variable
283 s_DiffVarNum = -1;
284 else
285 {
286 Temp = (LastNonZeroWord>>2);
287 for ( i = 0; Temp; Temp>>=2, i++ );
288 s_DiffVarNum = LastNonZeroWordNum*BPI/2 + i;
289
290 // save the old var value
293
294 // EXOR this value with the corresponding value in p cube
296
298 }
299 }
300
301 return DiffVarCounter;
302}
303
304int FindDiffVars( int * pDiffVars, Cube * pC1, Cube * pC2 )
305// determine different variables in two cubes and
306// writes them into pDiffVars[]
307// -1 is written into pDiffVars[0] if the cubes have different outputs
308// returns the number of different variables (including the output)
309{
310 int i, v;
311 DiffVarCounter = 0;
312 // check whether the output parts of the cubes are different
313
314 for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
315 if ( pC1->pCubeDataOut[i] != pC2->pCubeDataOut[i] )
316 { // they are different
317 pDiffVars[0] = -1;
318 DiffVarCounter = 1;
319 break;
320 }
321
322 for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
323 {
324
325 Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i];
326 Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT;
327
328 // check the first part of this word
329 Temp = Temp2 & 0xffff;
330 cVars = BitCount[ Temp ];
331 if ( cVars )
332 {
333 if ( cVars < 5 )
334 for ( v = 0; v < cVars; v++ )
335 {
336 assert( BitGroupNumbers[Temp] != MARKNUMBER );
337 pDiffVars[ DiffVarCounter++ ] = i*16 + GroupLiterals[ BitGroupNumbers[Temp] ][v];
338 }
339 else
340 return 5;
341 }
342 if ( DiffVarCounter > 4 )
343 return 5;
344
345 // check the second part of this word
346 Temp = Temp2 >> 16;
347 cVars = BitCount[ Temp ];
348 if ( cVars )
349 {
350 if ( cVars < 5 )
351 for ( v = 0; v < cVars; v++ )
352 {
353 assert( BitGroupNumbers[Temp] != MARKNUMBER );
354 pDiffVars[ DiffVarCounter++ ] = i*16 + 8 + GroupLiterals[ BitGroupNumbers[Temp] ][v];
355 }
356 else
357 return 5;
358 }
359 if ( DiffVarCounter > 4 )
360 return 5;
361 }
362 return DiffVarCounter;
363}
364
365void InsertVars( Cube * pC, int * pVars, int nVarsIn, int * pVarValues )
366// corrects the given number of variables (nVarsIn) in pC->pCubeDataIn[]
367// variable numbers are given in pVarNumbers[], their values are in pVarValues[]
368// arrays pVarNumbers[] and pVarValues[] are provided by the user
369{
370 int GlobalBit;
371 int LocalWord;
372 int LocalBit;
373 int i;
374 assert( nVarsIn > 0 && nVarsIn <= g_CoverInfo.nVarsIn );
375 for ( i = 0; i < nVarsIn; i++ )
376 {
377 assert( pVars[i] >= 0 && pVars[i] < g_CoverInfo.nVarsIn );
378 assert( pVarValues[i] == VAR_NEG || pVarValues[i] == VAR_POS || pVarValues[i] == VAR_ABS );
379 GlobalBit = (pVars[i]<<1);
380 LocalWord = VarWord(GlobalBit);
381 LocalBit = VarBit(GlobalBit);
382
383 // correct this variables
384 pC->pCubeDataIn[LocalWord] = ((pC->pCubeDataIn[LocalWord]&(~(3<<LocalBit)))|(pVarValues[i]<<LocalBit));
385 }
386}
387
388void InsertVarsWithoutClearing( Cube * pC, int * pVars, int nVarsIn, int * pVarValues, int Output )
389// corrects the given number of variables (nVarsIn) in pC->pCubeDataIn[]
390// variable numbers are given in pVarNumbers[], their values are in pVarValues[]
391// arrays pVarNumbers[] and pVarValues[] are provided by the user
392{
393 int GlobalBit;
394 int LocalWord;
395 int LocalBit;
396 int i;
397 assert( nVarsIn > 0 && nVarsIn <= g_CoverInfo.nVarsIn );
398 for ( i = 0; i < nVarsIn; i++ )
399 {
400 assert( pVars[i] >= 0 && pVars[i] < g_CoverInfo.nVarsIn );
401 assert( pVarValues[i] == VAR_NEG || pVarValues[i] == VAR_POS || pVarValues[i] == VAR_ABS );
402 GlobalBit = (pVars[i]<<1);
403 LocalWord = VarWord(GlobalBit);
404 LocalBit = VarBit(GlobalBit);
405
406 // correct this variables
407 pC->pCubeDataIn[LocalWord] |= ( pVarValues[i] << LocalBit );
408 }
409 // insert the output bit
410 pC->pCubeDataOut[VarWord(Output)] |= ( 1 << VarBit(Output) );
411}
412
416
417
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
int FindDiffVars(int *pDiffVars, Cube *pC1, Cube *pC2)
Definition exorBits.c:304
int s_DiffVarValueP_new
Definition exorList.c:640
void PrepareBitSetModule()
FUNCTION DEFINITIONS ///.
Definition exorBits.c:144
#define MARKNUMBER
Definition exorBits.c:135
int s_DiffVarValueQ
Definition exorList.c:641
#define FULL16BITS
Definition exorBits.c:134
int s_DiffVarNum
Definition exorList.c:638
void InsertVars(Cube *pC, int *pVars, int nVarsIn, int *pVarValues)
Definition exorBits.c:365
void InsertVarsWithoutClearing(Cube *pC, int *pVars, int nVarsIn, int *pVarValues, int Output)
Definition exorBits.c:388
varvalue GetVar(Cube *pC, int Var)
INLINE FUNCTION DEFINITIONS ///.
Definition exorBits.c:188
void ExorVar(Cube *pC, int Var, varvalue Val)
Definition exorBits.c:197
int s_DiffVarValueP_old
Definition exorList.c:639
int GetDistance(Cube *pC1, Cube *pC2)
FUNCTIONS OF THIS MODULE ///.
Definition exorBits.c:214
int GetDistancePlus(Cube *pC1, Cube *pC2)
Definition exorBits.c:246
int Var
Definition exorList.c:228
ABC_NAMESPACE_IMPL_START cinfo g_CoverInfo
GLOBAL VARIABLES ///.
Definition exor.c:58
unsigned char BitCount[]
Definition exorBits.c:138
unsigned int drow
Definition exor.h:120
struct cube Cube
@ BPI
Definition exor.h:59
@ DIFFERENT
Definition exor.h:74
struct cinfo_tag cinfo
varvalue
VARVALUE and CUBEDIST enum typedefs ///.
Definition exor.h:178
@ VAR_POS
Definition exor.h:178
@ VAR_NEG
Definition exor.h:178
@ VAR_ABS
Definition exor.h:178
drow * pCubeDataOut
Definition exor.h:130
drow * pCubeDataIn
Definition exor.h:129
#define assert(ex)
Definition util_old.h:213