src/aig/dar/darPrec.c File Reference

#include "darInt.h"
Include dependency graph for darPrec.c:

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)

Function Documentation

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 [

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

] 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  ) 

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

Synopsis [Computes the factorial.]

Description []

SideEffects []

SeeAlso []

Definition at line 67 of file darPrec.c.

00068 {
00069     int i, Res = 1;
00070     for ( i = 1; i <= n; i++ )
00071         Res *= i;
00072     return Res;
00073 }

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 }

Generated on Tue Jan 5 12:18:18 2010 for abc70930 by  doxygen 1.6.1