#include "darInt.h"
Go to the source code of this file.
Functions | |
char ** | Dar_ArrayAlloc (int nCols, int nRows, int Size) |
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) |
char** Dar_ArrayAlloc | ( | int | nCols, | |
int | nRows, | |||
int | Size | |||
) |
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 [
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Allocated one-memory-chunk array.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file darPrec.c.
00043 { 00044 char ** pRes; 00045 char * pBuffer; 00046 int i; 00047 assert( nCols > 0 && nRows > 0 && Size > 0 ); 00048 pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) ); 00049 pRes = (char **)pBuffer; 00050 pRes[0] = pBuffer + nCols * sizeof(void *); 00051 for ( i = 1; i < nCols; i++ ) 00052 pRes[i] = pRes[0] + i * nRows * Size; 00053 return pRes; 00054 }
int Dar_Factorial | ( | int | n | ) |
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 free() on the pointer returned by this procedure.]
SideEffects []
SeeAlso []
Definition at line 141 of file darPrec.c.
00142 { 00143 char Array[50]; 00144 char ** pRes; 00145 int nFact, i; 00146 // allocate memory 00147 nFact = Dar_Factorial( n ); 00148 pRes = Dar_ArrayAlloc( nFact, n, sizeof(char) ); 00149 // fill in the permutations 00150 for ( i = 0; i < n; i++ ) 00151 Array[i] = i; 00152 Dar_Permutations_rec( pRes, nFact, n, Array ); 00153 // print the permutations 00154 /* 00155 { 00156 int i, k; 00157 for ( i = 0; i < nFact; i++ ) 00158 { 00159 printf( "{" ); 00160 for ( k = 0; k < n; k++ ) 00161 printf( " %d", pRes[i][k] ); 00162 printf( " }\n" ); 00163 } 00164 } 00165 */ 00166 return pRes; 00167 }
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 86 of file darPrec.c.
00087 { 00088 char ** pNext; 00089 int nFactNext; 00090 int iTemp, iCur, iLast, k; 00091 00092 if ( n == 1 ) 00093 { 00094 pRes[0][0] = Array[0]; 00095 return; 00096 } 00097 00098 // get the next factorial 00099 nFactNext = nFact / n; 00100 // get the last entry 00101 iLast = n - 1; 00102 00103 for ( iCur = 0; iCur < n; iCur++ ) 00104 { 00105 // swap Cur and Last 00106 iTemp = Array[iCur]; 00107 Array[iCur] = Array[iLast]; 00108 Array[iLast] = iTemp; 00109 00110 // get the pointer to the current section 00111 pNext = pRes + (n - 1 - iCur) * nFactNext; 00112 00113 // set the last entry 00114 for ( k = 0; k < nFactNext; k++ ) 00115 pNext[k][iLast] = Array[iLast]; 00116 00117 // call recursively for this part 00118 Dar_Permutations_rec( pNext, nFactNext, n - 1, Array ); 00119 00120 // swap them back 00121 iTemp = Array[iCur]; 00122 Array[iCur] = Array[iLast]; 00123 Array[iLast] = iTemp; 00124 } 00125 }
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 290 of file darPrec.c.
00291 { 00292 unsigned short * uCanons; 00293 unsigned char * uMap; 00294 unsigned uTruth, uPhase, uPerm; 00295 char ** pPerms4, * uPhases, * uPerms; 00296 int nFuncs, nClasses; 00297 int i, k; 00298 00299 nFuncs = (1 << 16); 00300 uCanons = ALLOC( unsigned short, nFuncs ); 00301 uPhases = ALLOC( char, nFuncs ); 00302 uPerms = ALLOC( char, nFuncs ); 00303 uMap = ALLOC( unsigned char, nFuncs ); 00304 memset( uCanons, 0, sizeof(unsigned short) * nFuncs ); 00305 memset( uPhases, 0, sizeof(char) * nFuncs ); 00306 memset( uPerms, 0, sizeof(char) * nFuncs ); 00307 memset( uMap, 0, sizeof(unsigned char) * nFuncs ); 00308 pPerms4 = Dar_Permutations( 4 ); 00309 00310 nClasses = 1; 00311 nFuncs = (1 << 15); 00312 for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ ) 00313 { 00314 // skip already assigned 00315 if ( uCanons[uTruth] ) 00316 { 00317 assert( uTruth > uCanons[uTruth] ); 00318 uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]]; 00319 continue; 00320 } 00321 uMap[uTruth] = nClasses++; 00322 for ( i = 0; i < 16; i++ ) 00323 { 00324 uPhase = Dar_TruthPolarize( uTruth, i, 4 ); 00325 for ( k = 0; k < 24; k++ ) 00326 { 00327 uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 ); 00328 if ( uCanons[uPerm] == 0 ) 00329 { 00330 uCanons[uPerm] = uTruth; 00331 uPhases[uPerm] = i; 00332 uPerms[uPerm] = k; 00333 00334 uPerm = ~uPerm & 0xFFFF; 00335 uCanons[uPerm] = uTruth; 00336 uPhases[uPerm] = i | 16; 00337 uPerms[uPerm] = k; 00338 } 00339 else 00340 assert( uCanons[uPerm] == uTruth ); 00341 } 00342 uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 ); 00343 for ( k = 0; k < 24; k++ ) 00344 { 00345 uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 ); 00346 if ( uCanons[uPerm] == 0 ) 00347 { 00348 uCanons[uPerm] = uTruth; 00349 uPhases[uPerm] = i; 00350 uPerms[uPerm] = k; 00351 00352 uPerm = ~uPerm & 0xFFFF; 00353 uCanons[uPerm] = uTruth; 00354 uPhases[uPerm] = i | 16; 00355 uPerms[uPerm] = k; 00356 } 00357 else 00358 assert( uCanons[uPerm] == uTruth ); 00359 } 00360 } 00361 } 00362 uPhases[(1<<16)-1] = 16; 00363 assert( nClasses == 222 ); 00364 free( pPerms4 ); 00365 if ( puCanons ) 00366 *puCanons = uCanons; 00367 else 00368 free( uCanons ); 00369 if ( puPhases ) 00370 *puPhases = uPhases; 00371 else 00372 free( uPhases ); 00373 if ( puPerms ) 00374 *puPerms = uPerms; 00375 else 00376 free( uPerms ); 00377 if ( puMap ) 00378 *puMap = uMap; 00379 else 00380 free( uMap ); 00381 }
unsigned Dar_TruthPermute | ( | unsigned | Truth, | |
char * | pPerms, | |||
int | nVars, | |||
int | fReverse | |||
) |
Function*************************************************************
Synopsis [Permutes the function.]
Description []
SideEffects []
SeeAlso []
Definition at line 203 of file darPrec.c.
00204 { 00205 unsigned Result; 00206 int * pMints; 00207 int * pMintsP; 00208 int nMints; 00209 int i, m; 00210 00211 assert( nVars < 6 ); 00212 nMints = (1 << nVars); 00213 pMints = ALLOC( int, nMints ); 00214 pMintsP = ALLOC( int, nMints ); 00215 for ( i = 0; i < nMints; i++ ) 00216 pMints[i] = i; 00217 00218 Dar_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP ); 00219 00220 Result = 0; 00221 if ( fReverse ) 00222 { 00223 for ( m = 0; m < nMints; m++ ) 00224 if ( Truth & (1 << pMintsP[m]) ) 00225 Result |= (1 << m); 00226 } 00227 else 00228 { 00229 for ( m = 0; m < nMints; m++ ) 00230 if ( Truth & (1 << m) ) 00231 Result |= (1 << pMintsP[m]); 00232 } 00233 00234 free( pMints ); 00235 free( pMintsP ); 00236 00237 return Result; 00238 }
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 180 of file darPrec.c.
00181 { 00182 int m, v; 00183 // clean the storage for minterms 00184 memset( pMintsP, 0, sizeof(int) * nMints ); 00185 // go through minterms and add the variables 00186 for ( m = 0; m < nMints; m++ ) 00187 for ( v = 0; v < nVars; v++ ) 00188 if ( pMints[m] & (1 << v) ) 00189 pMintsP[m] |= (1 << pPerm[v]); 00190 }
unsigned Dar_TruthPolarize | ( | unsigned | uTruth, | |
int | Polarity, | |||
int | nVars | |||
) |
Function*************************************************************
Synopsis [Changes the phase of the function.]
Description []
SideEffects []
SeeAlso []
Definition at line 251 of file darPrec.c.
00252 { 00253 // elementary truth tables 00254 static unsigned Signs[5] = { 00255 0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010 00256 0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010 00257 0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000 00258 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000 00259 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000 00260 }; 00261 unsigned uTruthRes, uCof0, uCof1; 00262 int nMints, Shift, v; 00263 assert( nVars < 6 ); 00264 nMints = (1 << nVars); 00265 uTruthRes = uTruth; 00266 for ( v = 0; v < nVars; v++ ) 00267 if ( Polarity & (1 << v) ) 00268 { 00269 uCof0 = uTruth & ~Signs[v]; 00270 uCof1 = uTruth & Signs[v]; 00271 Shift = (1 << v); 00272 uCof0 <<= Shift; 00273 uCof1 >>= Shift; 00274 uTruth = uCof0 | uCof1; 00275 } 00276 return uTruth; 00277 }