abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
darPrec.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [darPrec.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [DAG-aware AIG rewriting.]
8 
9  Synopsis [Truth table precomputation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: darPrec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "darInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Allocated one-memory-chunk array.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 char ** Dar_ArrayAlloc( int nCols, int nRows, int Size )
46 {
47  char ** pRes;
48  char * pBuffer;
49  int i;
50  assert( nCols > 0 && nRows > 0 && Size > 0 );
51  pBuffer = ABC_ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
52  pRes = (char **)pBuffer;
53  pRes[0] = pBuffer + nCols * sizeof(void *);
54  for ( i = 1; i < nCols; i++ )
55  pRes[i] = pRes[0] + i * nRows * Size;
56  return pRes;
57 }
58 
59 /**Function********************************************************************
60 
61  Synopsis [Computes the factorial.]
62 
63  Description []
64 
65  SideEffects []
66 
67  SeeAlso []
68 
69 ******************************************************************************/
70 int Dar_Factorial( int n )
71 {
72  int i, Res = 1;
73  for ( i = 1; i <= n; i++ )
74  Res *= i;
75  return Res;
76 }
77 
78 /**Function********************************************************************
79 
80  Synopsis [Fills in the array of permutations.]
81 
82  Description []
83 
84  SideEffects []
85 
86  SeeAlso []
87 
88 ******************************************************************************/
89 void Dar_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
90 {
91  char ** pNext;
92  int nFactNext;
93  int iTemp, iCur, iLast, k;
94 
95  if ( n == 1 )
96  {
97  pRes[0][0] = Array[0];
98  return;
99  }
100 
101  // get the next factorial
102  nFactNext = nFact / n;
103  // get the last entry
104  iLast = n - 1;
105 
106  for ( iCur = 0; iCur < n; iCur++ )
107  {
108  // swap Cur and Last
109  iTemp = Array[iCur];
110  Array[iCur] = Array[iLast];
111  Array[iLast] = iTemp;
112 
113  // get the pointer to the current section
114  pNext = pRes + (n - 1 - iCur) * nFactNext;
115 
116  // set the last entry
117  for ( k = 0; k < nFactNext; k++ )
118  pNext[k][iLast] = Array[iLast];
119 
120  // call recursively for this part
121  Dar_Permutations_rec( pNext, nFactNext, n - 1, Array );
122 
123  // swap them back
124  iTemp = Array[iCur];
125  Array[iCur] = Array[iLast];
126  Array[iLast] = iTemp;
127  }
128 }
129 
130 /**Function********************************************************************
131 
132  Synopsis [Computes the set of all permutations.]
133 
134  Description [The number of permutations in the array is n!. The number of
135  entries in each permutation is n. Therefore, the resulting array is a
136  two-dimentional array of the size: n! x n. To free the resulting array,
137  call ABC_FREE() on the pointer returned by this procedure.]
138 
139  SideEffects []
140 
141  SeeAlso []
142 
143 ******************************************************************************/
144 char ** Dar_Permutations( int n )
145 {
146  char Array[50];
147  char ** pRes;
148  int nFact, i;
149  // allocate memory
150  nFact = Dar_Factorial( n );
151  pRes = Dar_ArrayAlloc( nFact, n, sizeof(char) );
152  // fill in the permutations
153  for ( i = 0; i < n; i++ )
154  Array[i] = i;
155  Dar_Permutations_rec( pRes, nFact, n, Array );
156  // print the permutations
157 /*
158  {
159  int i, k;
160  for ( i = 0; i < nFact; i++ )
161  {
162  printf( "{" );
163  for ( k = 0; k < n; k++ )
164  printf( " %d", pRes[i][k] );
165  printf( " }\n" );
166  }
167  }
168 */
169  return pRes;
170 }
171 
172 /**Function*************************************************************
173 
174  Synopsis [Permutes the given vector of minterms.]
175 
176  Description []
177 
178  SideEffects []
179 
180  SeeAlso []
181 
182 ***********************************************************************/
183 void Dar_TruthPermute_int( int * pMints, int nMints, char * pPerm, int nVars, int * pMintsP )
184 {
185  int m, v;
186  // clean the storage for minterms
187  memset( pMintsP, 0, sizeof(int) * nMints );
188  // go through minterms and add the variables
189  for ( m = 0; m < nMints; m++ )
190  for ( v = 0; v < nVars; v++ )
191  if ( pMints[m] & (1 << v) )
192  pMintsP[m] |= (1 << pPerm[v]);
193 }
194 
195 /**Function*************************************************************
196 
197  Synopsis [Permutes the function.]
198 
199  Description []
200 
201  SideEffects []
202 
203  SeeAlso []
204 
205 ***********************************************************************/
206 unsigned Dar_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse )
207 {
208  unsigned Result;
209  int * pMints;
210  int * pMintsP;
211  int nMints;
212  int i, m;
213 
214  assert( nVars < 6 );
215  nMints = (1 << nVars);
216  pMints = ABC_ALLOC( int, nMints );
217  pMintsP = ABC_ALLOC( int, nMints );
218  for ( i = 0; i < nMints; i++ )
219  pMints[i] = i;
220 
221  Dar_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP );
222 
223  Result = 0;
224  if ( fReverse )
225  {
226  for ( m = 0; m < nMints; m++ )
227  if ( Truth & (1 << pMintsP[m]) )
228  Result |= (1 << m);
229  }
230  else
231  {
232  for ( m = 0; m < nMints; m++ )
233  if ( Truth & (1 << m) )
234  Result |= (1 << pMintsP[m]);
235  }
236 
237  ABC_FREE( pMints );
238  ABC_FREE( pMintsP );
239 
240  return Result;
241 }
242 
243 /**Function*************************************************************
244 
245  Synopsis [Changes the phase of the function.]
246 
247  Description []
248 
249  SideEffects []
250 
251  SeeAlso []
252 
253 ***********************************************************************/
254 unsigned Dar_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
255 {
256  // elementary truth tables
257  static unsigned Signs[5] = {
258  0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010
259  0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010
260  0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000
261  0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000
262  0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000
263  };
264  unsigned uTruthRes, uCof0, uCof1;
265  int nMints, Shift, v;
266  assert( nVars < 6 );
267  nMints = (1 << nVars);
268  uTruthRes = uTruth;
269  for ( v = 0; v < nVars; v++ )
270  if ( Polarity & (1 << v) )
271  {
272  uCof0 = uTruth & ~Signs[v];
273  uCof1 = uTruth & Signs[v];
274  Shift = (1 << v);
275  uCof0 <<= Shift;
276  uCof1 >>= Shift;
277  uTruth = uCof0 | uCof1;
278  }
279  return uTruth;
280 }
281 
282 /**Function*************************************************************
283 
284  Synopsis [Computes NPN canonical forms for 4-variable functions.]
285 
286  Description []
287 
288  SideEffects []
289 
290  SeeAlso []
291 
292 ***********************************************************************/
293 void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap )
294 {
295  unsigned short * uCanons;
296  unsigned char * uMap;
297  unsigned uTruth, uPhase, uPerm;
298  char ** pPerms4, * uPhases, * uPerms;
299  int nFuncs, nClasses;
300  int i, k;
301 
302  nFuncs = (1 << 16);
303  uCanons = ABC_CALLOC( unsigned short, nFuncs );
304  uPhases = ABC_CALLOC( char, nFuncs );
305  uPerms = ABC_CALLOC( char, nFuncs );
306  uMap = ABC_CALLOC( unsigned char, nFuncs );
307  pPerms4 = Dar_Permutations( 4 );
308 
309  nClasses = 1;
310  nFuncs = (1 << 15);
311  for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
312  {
313  // skip already assigned
314  if ( uCanons[uTruth] )
315  {
316  assert( uTruth > uCanons[uTruth] );
317  uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
318  continue;
319  }
320  uMap[uTruth] = nClasses++;
321  for ( i = 0; i < 16; i++ )
322  {
323  uPhase = Dar_TruthPolarize( uTruth, i, 4 );
324  for ( k = 0; k < 24; k++ )
325  {
326  uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
327  if ( uCanons[uPerm] == 0 )
328  {
329  uCanons[uPerm] = uTruth;
330  uPhases[uPerm] = i;
331  uPerms[uPerm] = k;
332  uMap[uPerm] = uMap[uTruth];
333 
334  uPerm = ~uPerm & 0xFFFF;
335  uCanons[uPerm] = uTruth;
336  uPhases[uPerm] = i | 16;
337  uPerms[uPerm] = k;
338  uMap[uPerm] = uMap[uTruth];
339  }
340  else
341  assert( uCanons[uPerm] == uTruth );
342  }
343  uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 );
344  for ( k = 0; k < 24; k++ )
345  {
346  uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
347  if ( uCanons[uPerm] == 0 )
348  {
349  uCanons[uPerm] = uTruth;
350  uPhases[uPerm] = i;
351  uPerms[uPerm] = k;
352  uMap[uPerm] = uMap[uTruth];
353 
354  uPerm = ~uPerm & 0xFFFF;
355  uCanons[uPerm] = uTruth;
356  uPhases[uPerm] = i | 16;
357  uPerms[uPerm] = k;
358  uMap[uPerm] = uMap[uTruth];
359  }
360  else
361  assert( uCanons[uPerm] == uTruth );
362  }
363  }
364  }
365  for ( uTruth = 1; uTruth < 0xffff; uTruth++ )
366  assert( uMap[uTruth] != 0 );
367  uPhases[(1<<16)-1] = 16;
368  assert( nClasses == 222 );
369  ABC_FREE( pPerms4 );
370  if ( puCanons )
371  *puCanons = uCanons;
372  else
373  ABC_FREE( uCanons );
374  if ( puPhases )
375  *puPhases = uPhases;
376  else
377  ABC_FREE( uPhases );
378  if ( puPerms )
379  *puPerms = uPerms;
380  else
381  ABC_FREE( uPerms );
382  if ( puMap )
383  *puMap = uMap;
384  else
385  ABC_FREE( uMap );
386 }
387 
388 ////////////////////////////////////////////////////////////////////////
389 /// END OF FILE ///
390 ////////////////////////////////////////////////////////////////////////
391 
392 
393 ABC_NAMESPACE_IMPL_END
394 
memset
char * memset()
Dar_ArrayAlloc
ABC_NAMESPACE_IMPL_START char ** Dar_ArrayAlloc(int nCols, int nRows, int Size)
DECLARATIONS ///.
Definition: darPrec.c:45
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Dar_TruthPolarize
unsigned Dar_TruthPolarize(unsigned uTruth, int Polarity, int nVars)
Definition: darPrec.c:254
Dar_Permutations_rec
void Dar_Permutations_rec(char **pRes, int nFact, int n, char Array[])
Definition: darPrec.c:89
Dar_TruthPermute
unsigned Dar_TruthPermute(unsigned Truth, char *pPerms, int nVars, int fReverse)
Definition: darPrec.c:206
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Dar_Truth4VarNPN
void Dar_Truth4VarNPN(unsigned short **puCanons, char **puPhases, char **puPerms, unsigned char **puMap)
Definition: darPrec.c:293
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Dar_Permutations
char ** Dar_Permutations(int n)
Definition: darPrec.c:144
Dar_Factorial
int Dar_Factorial(int n)
Definition: darPrec.c:70
assert
#define assert(ex)
Definition: util_old.h:213
Dar_TruthPermute_int
void Dar_TruthPermute_int(int *pMints, int nMints, char *pPerm, int nVars, int *pMintsP)
Definition: darPrec.c:183