ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
darPrec.c File Reference
#include "darInt.h"
Include dependency graph for darPrec.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START char ** Dar_ArrayAlloc (int nCols, int nRows, int Size)
 DECLARATIONS ///.
 
int Dar_Factorial (int n)
 
void Dar_Permutations_rec (char **pRes, int nFact, int n, char Array[])
 
char ** Dar_Permutations (int n)
 
void Dar_TruthPermute_int (int *pMints, int nMints, char *pPerm, int nVars, int *pMintsP)
 
unsigned Dar_TruthPermute (unsigned Truth, char *pPerms, int nVars, int fReverse)
 
unsigned Dar_TruthPolarize (unsigned uTruth, int Polarity, int nVars)
 
void Dar_Truth4VarNPN (unsigned short **puCanons, char **puPhases, char **puPerms, unsigned char **puMap)
 

Function Documentation

◆ Dar_ArrayAlloc()

ABC_NAMESPACE_IMPL_START char ** Dar_ArrayAlloc ( int nCols,
int nRows,
int Size )

DECLARATIONS ///.

CFile****************************************************************

FileName [darPrec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Truth table precomputation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
darPrec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Allocated one-memory-chunk array.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file darPrec.c.

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}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Dar_Factorial()

int Dar_Factorial ( int n)

Function********************************************************************

Synopsis [Computes the factorial.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file darPrec.c.

71{
72 int i, Res = 1;
73 for ( i = 1; i <= n; i++ )
74 Res *= i;
75 return Res;
76}
Here is the caller graph for this function:

◆ Dar_Permutations()

char ** Dar_Permutations ( int n)

Function********************************************************************

Synopsis [Computes the set of all permutations.]

Description [The number of permutations in the array is n!. The number of entries in each permutation is n. Therefore, the resulting array is a two-dimentional array of the size: n! x n. To free the resulting array, call ABC_FREE() on the pointer returned by this procedure.]

SideEffects []

SeeAlso []

Definition at line 144 of file darPrec.c.

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}
Dar_Permutations_rec
void Dar_Permutations_rec(char **pRes, int nFact, int n, char Array[])
Definition darPrec.c:89
Dar_Factorial
int Dar_Factorial(int n)
Definition darPrec.c:70
Dar_ArrayAlloc
ABC_NAMESPACE_IMPL_START char ** Dar_ArrayAlloc(int nCols, int nRows, int Size)
DECLARATIONS ///.
Definition darPrec.c:45
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_Permutations_rec()

void Dar_Permutations_rec ( char ** pRes,
int nFact,
int n,
char Array[] )

Function********************************************************************

Synopsis [Fills in the array of permutations.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file darPrec.c.

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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_Truth4VarNPN()

void Dar_Truth4VarNPN ( unsigned short ** puCanons,
char ** puPhases,
char ** puPerms,
unsigned char ** puMap )

Function*************************************************************

Synopsis [Computes NPN canonical forms for 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 293 of file darPrec.c.

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}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Dar_TruthPolarize
unsigned Dar_TruthPolarize(unsigned uTruth, int Polarity, int nVars)
Definition darPrec.c:254
Dar_TruthPermute
unsigned Dar_TruthPermute(unsigned Truth, char *pPerms, int nVars, int fReverse)
Definition darPrec.c:206
Dar_Permutations
char ** Dar_Permutations(int n)
Definition darPrec.c:144
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_TruthPermute()

unsigned Dar_TruthPermute ( unsigned Truth,
char * pPerms,
int nVars,
int fReverse )

Function*************************************************************

Synopsis [Permutes the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file darPrec.c.

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}
Dar_TruthPermute_int
void Dar_TruthPermute_int(int *pMints, int nMints, char *pPerm, int nVars, int *pMintsP)
Definition darPrec.c:183
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_TruthPermute_int()

void Dar_TruthPermute_int ( int * pMints,
int nMints,
char * pPerm,
int nVars,
int * pMintsP )

Function*************************************************************

Synopsis [Permutes the given vector of minterms.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file darPrec.c.

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}
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_TruthPolarize()

unsigned Dar_TruthPolarize ( unsigned uTruth,
int Polarity,
int nVars )

Function*************************************************************

Synopsis [Changes the phase of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file darPrec.c.

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}
Here is the caller graph for this function: