/**CFile****************************************************************
FileName [ifDec16.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [FPGA mapping based on priority cuts.]
Synopsis [Fast checking procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifDec16.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
#include "if.h"
#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
//#define IF_USE_CASE3
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define CLU_VAR_MAX 16
#define CLU_WRD_MAX (1 << ((CLU_VAR_MAX)-6))
#define CLU_MEM_MAX 1000 // 1 GB
#define CLU_UNUSED 0xff
// decomposition
typedef struct If_Grp_t_ If_Grp_t;
struct If_Grp_t_
{
char nVars;
char nMyu;
char pVars[CLU_VAR_MAX];
};
// hash table entry
typedef struct If_Hte_t_ If_Hte_t;
struct If_Hte_t_
{
If_Hte_t * pNext;
unsigned Group;
unsigned Counter;
word pTruth[1];
};
// variable swapping code
static word PMasks[5][3] = {
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
{ 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
{ 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
};
// elementary truth tables
static word Truth6[6] = {
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX] = {{0}};
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
extern int If_CluSupportSize( word * t, int nVars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline unsigned If_CluGrp2Uns( If_Grp_t * pG )
{
char * pChar = (char *)pG;
unsigned Res = 0;
int i;
for ( i = 0; i < 8; i++ )
Res |= ((pChar[i] & 15) << (i << 2));
return Res;
}
static inline void If_CluUns2Grp( unsigned Group, If_Grp_t * pG )
{
char * pChar = (char *)pG;
int i;
for ( i = 0; i < 8; i++ )
pChar[i] = ((Group >> (i << 2)) & 15);
}
unsigned int If_CluPrimeCudd( unsigned int p )
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
// hash table
static inline int If_CluWordNum( int nVars )
{
return nVars <= 6 ? 1 : 1 << (nVars-6);
}
static inline int If_CluCountOnes( word t )
{
t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555);
t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333);
t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F);
t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF);
t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF);
return (t & 0x00000000FFFFFFFF) + (t>>32);
}
void If_CluHashTableCheck( If_Man_t * p )
{
int t = 1;
If_Hte_t * pEntry;
int i, RetValue, Status;
for ( i = 0; i < p->nTableSize[t]; i++ )
{
for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext )
{
Status = ((pEntry->Group & 15) > 0);
RetValue = If_CutPerformCheck16( NULL, (unsigned *)pEntry->pTruth, 13, If_CluSupportSize(pEntry->pTruth, 13), "555" );
if ( RetValue != Status )
{
Kit_DsdPrintFromTruth( (unsigned*)pEntry->pTruth, 13 ); printf( "\n" );
RetValue = If_CutPerformCheck16( NULL, (unsigned *)pEntry->pTruth, 13, If_CluSupportSize(pEntry->pTruth, 13), "555" );
printf( "Hash table problem!!!\n" );
}
}
}
}
void If_CluHashPrintStats( If_Man_t * p, int t )
{
If_Hte_t * pEntry;
int i, Counter;
for ( i = 0; i < p->nTableSize[t]; i++ )
{
Counter = 0;
for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext )
Counter++;
if ( Counter == 0 )
continue;
if ( Counter < 10 )
continue;
printf( "%d=%d ", i, Counter );
}
}
int If_CluHashFindMedian( If_Man_t * p, int t )
{
If_Hte_t * pEntry;
Vec_Int_t * vCounters;
int i, Max = 0, Total = 0, Half = 0;
vCounters = Vec_IntStart( 1000 );
for ( i = 0; i < p->nTableSize[t]; i++ )
{
for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext )
{
if ( Max < (int)pEntry->Counter )
{
Max = pEntry->Counter;
Vec_IntSetEntry( vCounters, pEntry->Counter, 0 );
}
Vec_IntAddToEntry( vCounters, pEntry->Counter, 1 );
Total++;
}
}
for ( i = Max; i > 0; i-- )
{
Half += Vec_IntEntry( vCounters, i );
if ( Half > Total/2 )
break;
}
/*
printf( "total = %d ", Total );
printf( "half = %d ", Half );
printf( "i = %d ", i );
printf( "Max = %d.\n", Max );
*/
Vec_IntFree( vCounters );
return Abc_MaxInt( i, 1 );
}
int If_CluHashKey( word * pTruth, int nWords, int Size )
{
static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
unsigned Value = 0;
int i;
if ( nWords < 4 )
{
unsigned char * s = (unsigned char *)pTruth;
for ( i = 0; i < 8 * nWords; i++ )
Value ^= BigPrimes[i % 7] * s[i];
}
else
{
unsigned * s = (unsigned *)pTruth;
for ( i = 0; i < 2 * nWords; i++ )
Value ^= BigPrimes[i % 7] * s[i];
}
return Value % Size;
}
unsigned * If_CluHashLookup( If_Man_t * p, word * pTruth, int t )
{
If_Hte_t * pEntry, * pPrev;
int nWords, HashKey;
if ( p == NULL )
return NULL;
nWords = If_CluWordNum(p->pPars->nLutSize);
if ( p->pMemEntries == NULL )
p->pMemEntries = Mem_FixedStart( sizeof(If_Hte_t) + sizeof(word) * (If_CluWordNum(p->pPars->nLutSize) - 1) );
if ( p->pHashTable[t] == NULL )
{
// decide how large should be the table
int nEntriesMax1 = 4 * If_CluPrimeCudd( Vec_PtrSize(p->vObjs) * p->pPars->nCutsMax );
int nEntriesMax2 = (int)(((double)CLU_MEM_MAX * (1 << 20)) / If_CluWordNum(p->pPars->nLutSize) / 8);
// int nEntriesMax2 = 10000;
// create table
p->nTableSize[t] = If_CluPrimeCudd( Abc_MinInt(nEntriesMax1, nEntriesMax2)/2 );
p->pHashTable[t] = ABC_CALLOC( void *, p->nTableSize[t] );
}
// check if this entry exists
HashKey = If_CluHashKey( pTruth, nWords, p->nTableSize[t] );
for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[HashKey]; pEntry; pEntry = pEntry->pNext )
if ( memcmp(pEntry->pTruth, pTruth, sizeof(word) * nWords) == 0 )
{
pEntry->Counter++;
return &pEntry->Group;
}
// resize the hash table
if ( p->nTableEntries[t] >= 2 * p->nTableSize[t] )
{
// collect useful entries
If_Hte_t * pPrev;
Vec_Ptr_t * vUseful = Vec_PtrAlloc( p->nTableEntries[t] );
int i, Median = If_CluHashFindMedian( p, t );
for ( i = 0; i < p->nTableSize[t]; i++ )
{
for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; )
{
if ( (int)pEntry->Counter > Median )
{
Vec_PtrPush( vUseful, pEntry );
pEntry = pEntry->pNext;
}
else
{
pPrev = pEntry->pNext;
Mem_FixedEntryRecycle( p->pMemEntries, (char *)pEntry );
pEntry = pPrev;
}
}
}
// add useful entries
memset( p->pHashTable[t], 0, sizeof(void *) * p->nTableSize[t] );
Vec_PtrForEachEntry( If_Hte_t *, vUseful, pEntry, i )
{
HashKey = If_CluHashKey( pEntry->pTruth, nWords, p->nTableSize[t] );
pPrev = ((If_Hte_t **)p->pHashTable[t])[HashKey];
if ( pPrev == NULL || pEntry->Counter >= pPrev->Counter )
{
pEntry->pNext = pPrev;
((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry;
}
else
{
while ( pPrev->pNext && pEntry->Counter < pPrev->pNext->Counter )
pPrev = pPrev->pNext;
pEntry->pNext = pPrev->pNext;
pPrev->pNext = pEntry;
}
}
p->nTableEntries[t] = Vec_PtrSize( vUseful );
Vec_PtrFree( vUseful );
}
// create entry
p->nTableEntries[t]++;
pEntry = (If_Hte_t *)Mem_FixedEntryFetch( p->pMemEntries );
memcpy( pEntry->pTruth, pTruth, sizeof(word) * nWords );
pEntry->Group = CLU_UNUSED;
pEntry->Counter = 1;
// insert at the beginning
// pEntry->pNext = ((If_Hte_t **)p->pHashTable[t])[HashKey];
// ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry;
// insert at the end
pEntry->pNext = NULL;
for ( pPrev = ((If_Hte_t **)p->pHashTable[t])[HashKey]; pPrev && pPrev->pNext; pPrev = pPrev->pNext );
if ( pPrev == NULL )
((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry;
else
pPrev->pNext = pEntry;
return &pEntry->Group;
}
// variable permutation for large functions
static inline void If_CluClear( word * pIn, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
pIn[w] = 0;
}
static inline void If_CluFill( word * pIn, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
pIn[w] = ~0;
}
static inline void If_CluCopy( word * pOut, word * pIn, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn[w];
}
static inline int If_CluEqual( word * pOut, word * pIn, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
if ( pOut[w] != pIn[w] )
return 0;
return 1;
}
static inline void If_CluAnd( word * pRes, word * pIn1, word * pIn2, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
pRes[w] = pIn1[w] & pIn2[w];
}
static inline void If_CluSharp( word * pRes, word * pIn1, word * pIn2, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
pRes[w] = pIn1[w] & ~pIn2[w];
}
static inline void If_CluOr( word * pRes, word * pIn1, word * pIn2, int nVars )
{
int w, nWords = If_CluWordNum( nVars );
for ( w = 0; w < nWords; w++ )
pRes[w] = pIn1[w] | pIn2[w];
}
static inline word If_CluAdjust( word t, int nVars )
{
assert( nVars >= 0 && nVars <= 6 );
if ( nVars == 6 )
return t;
t &= (((word)1) << (1 << nVars)) - 1;
if ( nVars == 0 )
t |= t << (1<<nVars++);
if ( nVars == 1 )
t |= t << (1<<nVars++);
if ( nVars == 2 )
t |= t << (1<<nVars++);
if ( nVars == 3 )
t |= t << (1<<nVars++);
if ( nVars == 4 )
t |= t << (1<<nVars++);
if ( nVars == 5 )
t |= t << (1<<nVars++);
return t;
}
static inline void If_CluAdjustBig( word * pF, int nVarsCur, int nVarsMax )
{
int v, nWords;
if ( nVarsCur == nVarsMax )
return;
assert( nVarsCur < nVarsMax );
for ( v = Abc_MaxInt( nVarsCur, 6 ); v < nVarsMax; v++ )
{
nWords = If_CluWordNum( v );
If_CluCopy( pF + nWords, pF, v );
}
}
static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
{
int i, k, nWords = If_CluWordNum( nVars );
assert( iVar < nVars - 1 );
if ( iVar < 5 )
{
int Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
}
else if ( iVar > 5 )
{
int Step = (1 << (iVar - 6));
for ( k = 0; k < nWords; k += 4*Step )
{
for ( i = 0; i < Step; i++ )
pOut[i] = pIn[i];
for ( i = 0; i < Step; i++ )
pOut[Step+i] = pIn[2*Step+i];
for ( i = 0; i < Step; i++ )
pOut[2*Step+i] = pIn[Step+i];
for ( i = 0; i < Step; i++ )
pOut[3*Step+i] = pIn[3*Step+i];
pIn += 4*Step;
pOut += 4*Step;
}
}
else // if ( iVar == 5 )
{
for ( i = 0; i < nWords; i += 2 )
{
pOut[i] = (pIn[i] & 0x00000000FFFFFFFF) | ((pIn[i+1] & 0x00000000FFFFFFFF) << 32);
pOut[i+1] = (pIn[i+1] & 0xFFFFFFFF00000000) | ((pIn[i] & 0xFFFFFFFF00000000) >> 32);
}
}
}
void If_CluChangePhase( word * pF, int nVars, int iVar )
{
int nWords = If_CluWordNum( nVars );
assert( iVar < nVars );
if ( iVar < 6 )
{
int i, Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
pF[i] = ((pF[i] & ~Truth6[iVar]) << Shift) | ((pF[i] & Truth6[iVar]) >> Shift);
}
else
{
word Temp;
int i, k, Step = (1 << (iVar - 6));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
Temp = pF[i];
pF[i] = pF[Step+i];
pF[Step+i] = Temp;
}
pF += 2*Step;
}
}
}
void If_CluCountOnesInCofs( word * pTruth, int nVars, int * pStore )
{
int nWords = If_CluWordNum( nVars );
int i, k, nOnes = 0, Limit = Abc_MinInt( nVars, 6 );
memset( pStore, 0, sizeof(int) * 2 * nVars );
// compute positive cofactors
for ( k = 0; k < nWords; k++ )
for ( i = 0; i < Limit; i++ )
pStore[2*i+1] += If_CluCountOnes( pTruth[k] & Truth6[i] );
if ( nVars > 6 )
for ( k = 0; k < nWords; k++ )
for ( i = 6; i < nVars; i++ )
if ( k & (1 << (i-6)) )
pStore[2*i+1] += If_CluCountOnes( pTruth[k] );
// compute negative cofactors
for ( k = 0; k < nWords; k++ )
nOnes += If_CluCountOnes( pTruth[k] );
for ( i = 0; i < nVars; i++ )
pStore[2*i] = nOnes - pStore[2*i+1];
}
unsigned If_CluSemiCanonicize( word * pTruth, int nVars, int * pCanonPerm )
{
word pFunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp;
int pStore[CLU_VAR_MAX*2];
unsigned uCanonPhase = 0;
int i, Temp, fChange, Counter = 0;
//Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
// collect signatures
If_CluCountOnesInCofs( pTruth, nVars, pStore );
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
if ( pStore[2*i+0] <= pStore[2*i+1] )
continue;
uCanonPhase |= (1 << i);
Temp = pStore[2*i+0];
pStore[2*i+0] = pStore[2*i+1];
pStore[2*i+1] = Temp;
If_CluChangePhase( pIn, nVars, i );
}
// compute permutation
for ( i = 0; i < nVars; i++ )
pCanonPerm[i] = i;
do {
fChange = 0;
for ( i = 0; i < nVars-1; i++ )
{
if ( pStore[2*i] <= pStore[2*(i+1)] )
continue;
Counter++;
fChange = 1;
Temp = pCanonPerm[i];
pCanonPerm[i] = pCanonPerm[i+1];
pCanonPerm[i+1] = Temp;
Temp = pStore[2*i];
pStore[2*i] = pStore[2*(i+1)];
pStore[2*(i+1)] = Temp;
Temp = pStore[2*i+1];
pStore[2*i+1] = pStore[2*(i+1)+1];
pStore[2*(i+1)+1] = Temp;
If_CluSwapAdjacent( pOut, pIn, i, nVars );
pTemp = pIn; pIn = pOut; pOut = pTemp;
}
} while ( fChange );
// swap if it was moved an odd number of times
if ( Counter & 1 )
If_CluCopy( pOut, pIn, nVars );
return uCanonPhase;
}
void If_CluSemiCanonicizeVerify( word * pTruth, word * pTruth0, int nVars, int * pCanonPerm, unsigned uCanonPhase )
{
word pFunc[CLU_WRD_MAX], pGunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp;
int i, Temp, fChange, Counter = 0;
If_CluCopy( pGunc, pTruth, nVars );
// undo permutation
do {
fChange = 0;
for ( i = 0; i < nVars-1; i++ )
{
if ( pCanonPerm[i] < pCanonPerm[i+1] )
continue;
Counter++;
fChange = 1;
Temp = pCanonPerm[i];
pCanonPerm[i] = pCanonPerm[i+1];
pCanonPerm[i+1] = Temp;
If_CluSwapAdjacent( pOut, pIn, i, nVars );
pTemp = pIn; pIn = pOut; pOut = pTemp;
}
} while ( fChange );
if ( Counter & 1 )
If_CluCopy( pOut, pIn, nVars );
// undo phase
for ( i = 0; i < nVars; i++ )
if ( (uCanonPhase >> i) & 1 )
If_CluChangePhase( pTruth, nVars, i );
// compare
if ( !If_CluEqual(pTruth0, pTruth, nVars) )
{
Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pGunc, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
printf( "SemiCanonical verification FAILED!\n" );
}
}
void If_CluPrintGroup( If_Grp_t * g )
{
int i;
printf( "Vars = %d ", g->nVars );
printf( "Myu = %d {", g->nMyu );
for ( i = 0; i < g->nVars; i++ )
printf( " %c", 'a' + g->pVars[i] );
printf( " }\n" );
}
void If_CluPrintConfig( int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth )
{
assert( r->nVars == nVars - g->nVars + 1 + (g->nMyu > 2) );
If_CluPrintGroup( g );
if ( g->nVars < 6 )
BStruth = If_CluAdjust( BStruth, g->nVars );
Kit_DsdPrintFromTruth( (unsigned *)&BStruth, g->nVars );
printf( "\n" );
If_CluPrintGroup( r );
if ( r->nVars < 6 )
pFStruth[0] = If_CluAdjust( pFStruth[0], r->nVars );
Kit_DsdPrintFromTruth( (unsigned *)pFStruth, r->nVars );
printf( "\n" );
}
void If_CluInitTruthTables()
{
int i, k;
assert( CLU_VAR_MAX <= 16 );
for ( i = 0; i < 6; i++ )
for ( k = 0; k < CLU_WRD_MAX; k++ )
TruthAll[i][k] = Truth6[i];
for ( i = 6; i < CLU_VAR_MAX; i++ )
for ( k = 0; k < CLU_WRD_MAX; k++ )
TruthAll[i][k] = ((k >> (i-6)) & 1) ? ~0 : 0;
// Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" );
// Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" );
}
// verification
static void If_CluComposeLut( int nVars, If_Grp_t * g, word * t, word f[6][CLU_WRD_MAX], word * r )
{
word c[CLU_WRD_MAX];
int m, v;
If_CluClear( r, nVars );
for ( m = 0; m < (1<<g->nVars); m++ )
{
if ( !((t[m >> 6] >> (m & 63)) & 1) )
continue;
If_CluFill( c, nVars );
for ( v = 0; v < g->nVars; v++ )
if ( (m >> v) & 1 )
If_CluAnd( c, c, f[v], nVars );
else
If_CluSharp( c, c, f[v], nVars );
If_CluOr( r, r, c, nVars );
}
}
void If_CluVerify( word * pF, int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth )
{
word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX];
int i;
assert( g->nVars <= 6 && r->nVars <= 6 );
if ( TruthAll[0][0] == 0 )
If_CluInitTruthTables();
for ( i = 0; i < g->nVars; i++ )
If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars );
If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire );
for ( i = 0; i < r->nVars; i++ )
if ( r->pVars[i] == nVars )
If_CluCopy( pTTFans[i], pTTWire, nVars );
else
If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars );
If_CluComposeLut( nVars, r, pFStruth, pTTFans, pTTRes );
if ( !If_CluEqual(pTTRes, pF, nVars) )
{
printf( "\n" );
If_CluPrintConfig( nVars, g, r, BStruth, pFStruth );
Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
printf( "Verification FAILED!\n" );
}
// else
// printf( "Verification succeed!\n" );
}
void If_CluVerify3( word * pF, int nVars, If_Grp_t * g, If_Grp_t * g2, If_Grp_t * r, word BStruth, word BStruth2, word FStruth )
{
word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTWire2[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX];
int i;
assert( g->nVars >= 2 && g2->nVars >= 2 && r->nVars >= 2 );
assert( g->nVars <= 6 && g2->nVars <= 6 && r->nVars <= 6 );
if ( TruthAll[0][0] == 0 )
If_CluInitTruthTables();
for ( i = 0; i < g->nVars; i++ )
If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars );
If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire );
for ( i = 0; i < g2->nVars; i++ )
If_CluCopy( pTTFans[i], TruthAll[(int)g2->pVars[i]], nVars );
If_CluComposeLut( nVars, g2, &BStruth2, pTTFans, pTTWire2 );
for ( i = 0; i < r->nVars; i++ )
if ( r->pVars[i] == nVars )
If_CluCopy( pTTFans[i], pTTWire, nVars );
else if ( r->pVars[i] == nVars + 1 )
If_CluCopy( pTTFans[i], pTTWire2, nVars );
else
If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars );
If_CluComposeLut( nVars, r, &FStruth, pTTFans, pTTRes );
if ( !If_CluEqual(pTTRes, pF, nVars) )
{
printf( "%d\n", nVars );
// If_CluPrintConfig( nVars, g, r, BStruth, pFStruth );
// Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)&BStruth, g->nVars ); printf( " " ); If_CluPrintGroup(g); // printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)&BStruth2, g2->nVars ); printf( " " ); If_CluPrintGroup(g2); // printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)&FStruth, r->nVars ); printf( " " ); If_CluPrintGroup(r); // printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pTTWire, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pTTWire2, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
printf( "Verification FAILED!\n" );
}
// else
// printf( "Verification succeed!\n" );
}
void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar )
{
word low2High, high2Low, temp;
int nWords = If_CluWordNum(nVars);
int shift, step, iStep, jStep;
int w = 0, i = 0, j = 0;
static word PPMasks[6][6] = {
{ 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
{ 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
{ 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 },
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 },
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 },
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 }
};
if( iVar == jVar )
return;
if( jVar < iVar )
{
int varTemp = jVar;
jVar = iVar;
iVar = varTemp;
}
if ( iVar <= 5 && jVar <= 5 )
{
shift = (1 << jVar) - (1 << iVar);
for ( w = 0; w < nWords; w++ )
{
low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift;
pTruth[w] &= ~PPMasks[iVar][jVar - 1];
high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
pTruth[w] &= ~ (PPMasks[iVar][jVar - 1] << shift);
pTruth[w] = pTruth[w] | low2High | high2Low;
}
}
else if( iVar <= 5 && jVar > 5 )
{
step = If_CluWordNum(jVar + 1)/2;
shift = 1 << iVar;
for ( w = 0; w < nWords; w += 2*step )
{
for (j = 0; j < step; j++)
{
low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift;
pTruth[w + j] &= ~PPMasks[iVar][5];
high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift;
pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift);
pTruth[w + j] |= high2Low;
pTruth[w + step + j] |= low2High;
}
}
}
else
{
iStep = If_CluWordNum(iVar + 1)/2;
jStep = If_CluWordNum(jVar + 1)/2;
for (w = 0; w < nWords; w += 2*jStep)
{
for (i = 0; i < jStep; i += 2*iStep)
{
for (j = 0; j < iStep; j++)
{
temp = pTruth[w + iStep + i + j];
pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j];
pTruth[w + jStep + i + j] = temp;
}
}
}
}
if ( V2P && P2V )
{
V2P[P2V[iVar]] = jVar;
V2P[P2V[jVar]] = iVar;
P2V[iVar] ^= P2V[jVar];
P2V[jVar] ^= P2V[iVar];
P2V[iVar] ^= P2V[jVar];
}
}
void If_CluReverseOrder( word * pTruth, int nVars, int * V2P, int * P2V, int iVarStart )
{
int i, j, k;
for ( k = 0; k < (nVars-iVarStart)/2 ; k++ )
{
i = iVarStart + k;
j = nVars - 1 - k;
If_CluSwapVars( pTruth, nVars, V2P, P2V, i, j );
}
}
// moves one var (v) to the given position (p)
void If_CluMoveVar2( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p )
{
If_CluSwapVars( pF, nVars, Var2Pla, Pla2Var, Var2Pla[v], p );
}
// moves one var (v) to the given position (p)
void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p )
{
word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp;
int iPlace0, iPlace1, Count = 0;
assert( v >= 0 && v < nVars );
while ( Var2Pla[v] < p )
{
iPlace0 = Var2Pla[v];
iPlace1 = Var2Pla[v]+1;
If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars );
pTemp = pIn; pIn = pOut, pOut = pTemp;
Var2Pla[Pla2Var[iPlace0]]++;
Var2Pla[Pla2Var[iPlace1]]--;
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Count++;
}
while ( Var2Pla[v] > p )
{
iPlace0 = Var2Pla[v]-1;
iPlace1 = Var2Pla[v];
If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars );
pTemp = pIn; pIn = pOut, pOut = pTemp;
Var2Pla[Pla2Var[iPlace0]]++;
Var2Pla[Pla2Var[iPlace1]]--;
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Count++;
}
if ( Count & 1 )
If_CluCopy( pF, pIn, nVars );
assert( Pla2Var[p] == v );
}
// moves vars to be the most signiticant ones (Group[0] is MSB)
void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g )
{
int v;
for ( v = 0; v < g->nVars; v++ )
If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[g->nVars - 1 - v], nVars - 1 - v );
}
// reverses the variable order
void If_CluReverseOrder_old( word * pF, int nVars, int * V2P, int * P2V, int iVarStart )
{
word pG[CLU_WRD_MAX];
int v;
If_CluCopy( pG, pF, nVars );
// for ( v = 0; v < nVars; v++ )
// printf( "%c ", 'a' + P2V[v] );
// printf( " --- " );
for ( v = iVarStart; v < nVars; v++ )
If_CluMoveVar( pF, nVars, V2P, P2V, P2V[iVarStart], nVars - 1 - (v - iVarStart) );
// for ( v = 0; v < nVars; v++ )
// printf( "%c ", 'a' + P2V[v] );
// printf( "\n" );
// if ( iVarStart > 0 )
// return;
If_CluReverseOrder( pG, nVars, NULL, NULL, iVarStart );
if ( If_CluEqual( pG, pF, nVars ) )
{
// printf( "+" );
}
else
{
/*
printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned*)pG, nVars );
printf( "\n" );
*/
printf( "%d ", nVars );
}
}
// return the number of cofactors w.r.t. the topmost vars (nBSsize)
int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift, word pCofs[3][CLU_WRD_MAX/4] )
{
word iCofs[128], iCof, Result = 0;
word * pCofA, * pCofB;
int nMints = (1 << nBSsize);
int i, c, w, nCofs;
assert( nBSsize >= 2 && nBSsize <= 7 && nBSsize < nVars );
if ( nVars - nBSsize < 6 )
{
int nShift = (1 << (nVars - nBSsize));
word Mask = ((((word)1) << nShift) - 1);
for ( nCofs = i = 0; i < nMints; i++ )
{
iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask;
for ( c = 0; c < nCofs; c++ )
if ( iCof == iCofs[c] )
break;
if ( c == nCofs )
iCofs[nCofs++] = iCof;
if ( pCofs && iCof != iCofs[0] )
Result |= (((word)1) << i);
if ( nCofs == 5 )
break;
}
if ( nCofs <= 2 && pCofs )
{
assert( nBSsize <= 6 );
pCofs[0][0] = iCofs[0];
pCofs[1][0] = (nCofs == 2) ? iCofs[1] : iCofs[0];
pCofs[2][0] = Result;
}
}
else
{
int nWords = If_CluWordNum( nVars - nBSsize );
assert( nWords * nMints == If_CluWordNum(nVars) );
for ( nCofs = i = 0; i < nMints; i++ )
{
pCofA = pF + i * nWords;
for ( c = 0; c < nCofs; c++ )
{
pCofB = pF + iCofs[c] * nWords;
for ( w = 0; w < nWords; w++ )
if ( pCofA[w] != pCofB[w] )
break;
if ( w == nWords )
break;
}
if ( c == nCofs )
iCofs[nCofs++] = i;
if ( pCofs )
{
assert( nBSsize <= 6 );
pCofB = pF + iCofs[0] * nWords;
for ( w = 0; w < nWords; w++ )
if ( pCofA[w] != pCofB[w] )
break;
if ( w != nWords )
Result |= (((word)1) << i);
}
if ( nCofs == 5 )
break;
}
if ( nCofs <= 2 && pCofs )
{
If_CluCopy( pCofs[0], pF + iCofs[0] * nWords, nVars - nBSsize );
If_CluCopy( pCofs[1], pF + ((nCofs == 2) ? iCofs[1] : iCofs[0]) * nWords, nVars - nBSsize );
pCofs[2][0] = Result;
}
}
assert( nCofs >= 1 && nCofs <= 5 );
return nCofs;
}
// return the number of cofactors w.r.t. the topmost vars (nBSsize)
int If_CluCountCofs4( word * pF, int nVars, int nBSsize, word pCofs[6][CLU_WRD_MAX/4] )
{
word iCofs[128], iCof, Result0 = 0, Result1 = 0;
int nMints = (1 << nBSsize);
int i, c, nCofs;
assert( pCofs );
assert( nBSsize >= 2 && nBSsize <= 6 && nBSsize < nVars );
if ( nVars - nBSsize < 6 )
{
int nShift = (1 << (nVars - nBSsize));
word Mask = ((((word)1) << nShift) - 1);
for ( nCofs = i = 0; i < nMints; i++ )
{
iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
for ( c = 0; c < nCofs; c++ )
if ( iCof == iCofs[c] )
break;
if ( c == nCofs )
iCofs[nCofs++] = iCof;
if ( c == 1 || c == 3 )
Result0 |= (((word)1) << i);
if ( c == 2 || c == 3 )
Result1 |= (((word)1) << i);
}
assert( nCofs >= 3 && nCofs <= 4 );
pCofs[0][0] = iCofs[0];
pCofs[1][0] = iCofs[1];
pCofs[2][0] = iCofs[2];
pCofs[3][0] = (nCofs == 4) ? iCofs[3] : iCofs[2];
pCofs[4][0] = Result0;
pCofs[5][0] = Result1;
}
else
assert( 0 );
return nCofs;
}
void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 )
{
int nWords = If_CluWordNum( nVars );
assert( iVar < nVars );
if ( iVar < 6 )
{
int i, Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
{
pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift);
pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift);
}
}
else
{
int i, k, Step = (1 << (iVar - 6));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
pCof0[i] = pCof0[Step+i] = pF[i];
pCof1[i] = pCof1[Step+i] = pF[Step+i];
}
pF += 2*Step;
pCof0 += 2*Step;
pCof1 += 2*Step;
}
}
}
// returns 1 if we have special case of cofactors; otherwise, returns 0
int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar )
{
word Cof0, Cof1;
int State[6] = {0};
int i, nWords = If_CluWordNum( nVars );
assert( iVar < nVars );
if ( iVar < 6 )
{
int Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
{
Cof0 = (pF[i] & ~Truth6[iVar]);
Cof1 = ((pF[i] & Truth6[iVar]) >> Shift);
if ( Cof0 == 0 )
State[0]++;
else if ( Cof0 == ~Truth6[iVar] )
State[1]++;
else if ( Cof1 == 0 )
State[2]++;
else if ( Cof1 == ~Truth6[iVar] )
State[3]++;
else if ( Cof0 == ~Cof1 )
State[4]++;
else if ( Cof0 == Cof1 )
State[5]++;
}
}
else
{
int k, Step = (1 << (iVar - 6));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
Cof0 = pF[i];
Cof1 = pF[Step+i];
if ( Cof0 == 0 )
State[0]++;
else if ( Cof0 == ~0 )
State[1]++;
else if ( Cof1 == 0 )
State[2]++;
else if ( Cof1 == ~0 )
State[3]++;
else if ( Cof0 == ~Cof1 )
State[4]++;
else if ( Cof0 == Cof1 )
State[5]++;
}
pF += 2*Step;
}
nWords /= 2;
}
assert( State[5] != nWords );
for ( i = 0; i < 5; i++ )
{
assert( State[i] <= nWords );
if ( State[i] == nWords )
return i;
}
return -1;
}
// returns 1 if we have special case of cofactors; otherwise, returns 0
If_Grp_t If_CluDecUsingCofs( word * pTruth, int nVars, int nLutLeaf )
{
If_Grp_t G = {0};
word pF2[CLU_WRD_MAX], * pF = pF2;
int Var2Pla[CLU_VAR_MAX+2], Pla2Var[CLU_VAR_MAX+2];
int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2];
int nVarsNeeded = nVars - nLutLeaf;
int v, i, k, iVar, State;
//Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
// create local copy
If_CluCopy( pF, pTruth, nVars );
for ( k = 0; k < nVars; k++ )
Var2Pla[k] = Pla2Var[k] = k;
// find decomposable vars
for ( i = 0; i < nVarsNeeded; i++ )
{
for ( v = nVars - 1; v >= 0; v-- )
{
State = If_CluDetectSpecialCaseCofs( pF, nVars, v );
if ( State == -1 )
continue;
// update the variable place
iVar = Pla2Var[v];
while ( Var2Pla[iVar] < nVars - 1 )
{
int iPlace0 = Var2Pla[iVar];
int iPlace1 = Var2Pla[iVar]+1;
Var2Pla[Pla2Var[iPlace0]]++;
Var2Pla[Pla2Var[iPlace1]]--;
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
}
// move this variable to the top
for ( k = 0; k < nVars; k++ )
V2P[k] = P2V[k] = k;
//Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
If_CluMoveVar( pF, nVars, V2P, P2V, v, nVars - 1 );
//Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
// choose cofactor to follow
iVar = nVars - 1;
if ( State == 0 || State == 1 ) // need cof1
{
if ( iVar < 6 )
pF[0] = (pF[0] & Truth6[iVar]) | ((pF[0] & Truth6[iVar]) >> (1 << iVar));
else
pF += If_CluWordNum( nVars ) / 2;
}
else // need cof0
{
if ( iVar < 6 )
pF[0] = (pF[0] & ~Truth6[iVar]) | ((pF[0] & ~Truth6[iVar]) << (1 << iVar));
}
// update the variable count
nVars--;
break;
}
if ( v == -1 )
return G;
}
// create the resulting group
G.nVars = nLutLeaf;
G.nMyu = 2;
for ( v = 0; v < G.nVars; v++ )
G.pVars[v] = Pla2Var[v];
return G;
}
// deriving decomposition
word If_CluDeriveDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r )
{
word pCofs[3][CLU_WRD_MAX/4];
int i, RetValue, nFSset = nVars - g->nVars;
RetValue = If_CluCountCofs( pF, nVars, g->nVars, 0, pCofs );
// assert( RetValue == 2 );
if ( nFSset < 6 )
pF[0] = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0];
else
{
If_CluCopy( pF, pCofs[0], nFSset );
If_CluCopy( pF + If_CluWordNum(nFSset), pCofs[1], nFSset );
}
// create the resulting group
if ( r )
{
r->nVars = nFSset + 1;
r->nMyu = 0;
for ( i = 0; i < nFSset; i++ )
r->pVars[i] = P2V[i];
r->pVars[nFSset] = nVars;
}
return pCofs[2][0];
}
void If_CluDeriveDisjoint4( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r, word * pTruth0, word * pTruth1 )
{
word pCofs[6][CLU_WRD_MAX/4];
word Cof0, Cof1;
int i, RetValue, nFSset = nVars - g->nVars;
assert( g->nVars <= 6 && nFSset <= 4 );
RetValue = If_CluCountCofs4( pF, nVars, g->nVars, pCofs );
if ( RetValue != 3 && RetValue != 4 )
printf( "If_CluDeriveDisjoint4(): Error!!!\n" );
Cof0 = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0];
Cof1 = (pCofs[3][0] << (1 << nFSset)) | pCofs[2][0];
pF[0] = (Cof1 << (1 << (nFSset+1))) | Cof0;
pF[0] = If_CluAdjust( pF[0], nFSset + 2 );
// create the resulting group
r->nVars = nFSset + 2;
r->nMyu = 0;
for ( i = 0; i < nFSset; i++ )
r->pVars[i] = P2V[i];
r->pVars[nFSset] = nVars;
r->pVars[nFSset+1] = nVars+1;
*pTruth0 = If_CluAdjust( pCofs[4][0], g->nVars );
*pTruth1 = If_CluAdjust( pCofs[5][0], g->nVars );
}
word If_CluDeriveNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r )
{
word pCofs[2][CLU_WRD_MAX];
word Truth0, Truth1, Truth;
int i, nFSset = nVars - g->nVars, nFSset1 = nFSset + 1;
If_CluCofactors( pF, nVars, nVars - 1, pCofs[0], pCofs[1] );
// Extra_PrintHex( stdout, (unsigned *)pCofs[0], nVars ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)pCofs[1], nVars ); printf( "\n" );
g->nVars--;
Truth0 = If_CluDeriveDisjoint( pCofs[0], nVars - 1, V2P, P2V, g, NULL );
Truth1 = If_CluDeriveDisjoint( pCofs[1], nVars - 1, V2P, P2V, g, NULL );
Truth = (Truth1 << (1 << g->nVars)) | Truth0;
g->nVars++;
if ( nFSset1 < 6 )
pF[0] = (pCofs[1][0] << (1 << nFSset1)) | pCofs[0][0];
else
{
If_CluCopy( pF, pCofs[0], nFSset1 );
If_CluCopy( pF + If_CluWordNum(nFSset1), pCofs[1], nFSset1 );
}
// Extra_PrintHex( stdout, (unsigned *)&Truth0, 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&Truth1, 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&pCofs[0][0], 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&pCofs[1][0], 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&Truth, 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&pF[0], 6 ); printf( "\n" );
// create the resulting group
r->nVars = nFSset + 2;
r->nMyu = 0;
for ( i = 0; i < nFSset; i++ )
r->pVars[i] = P2V[i];
r->pVars[nFSset] = nVars;
r->pVars[nFSset+1] = g->pVars[g->nVars - 1];
return Truth;
}
// check non-disjoint decomposition
int If_CluCheckNonDisjointGroup( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g )
{
int v, i, nCofsBest2;
if ( (g->nMyu == 3 || g->nMyu == 4) )
{
word pCofs[2][CLU_WRD_MAX];
// try cofactoring w.r.t. each variable
for ( v = 0; v < g->nVars; v++ )
{
If_CluCofactors( pF, nVars, V2P[(int)g->pVars[v]], pCofs[0], pCofs[1] );
nCofsBest2 = If_CluCountCofs( pCofs[0], nVars, g->nVars, 0, NULL );
if ( nCofsBest2 > 2 )
continue;
nCofsBest2 = If_CluCountCofs( pCofs[1], nVars, g->nVars, 0, NULL );
if ( nCofsBest2 > 2 )
continue;
// found good shared variable - move to the end
If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[v], nVars-1 );
for ( i = 0; i < g->nVars; i++ )
g->pVars[i] = P2V[nVars-g->nVars+i];
return 1;
}
}
return 0;
}
// finds a good var group (cof count < 6; vars are MSBs)
If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V, int nBSsize, int fDisjoint )
{
int fVerbose = 0;
int nRounds = 2;//nBSsize;
If_Grp_t G = {0}, * g = &G;//, BestG = {0};
int i, r, v, nCofs, VarBest, nCofsBest2;
assert( nVars > nBSsize && nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX );
assert( nBSsize >= 2 && nBSsize <= 6 );
// start with the default group
g->nVars = nBSsize;
g->nMyu = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
for ( i = 0; i < nBSsize; i++ )
g->pVars[i] = P2V[nVars-nBSsize+i];
// check if good enough
if ( g->nMyu == 2 )
return G;
if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) )
{
// BestG = G;
return G;
}
if ( nVars == nBSsize + iVarStart )
{
g->nVars = 0;
return G;
}
if ( fVerbose )
{
printf( "Iter %2d ", -1 );
If_CluPrintGroup( g );
}
// try to find better group
for ( r = 0; r < nRounds; r++ )
{
if ( nBSsize < nVars-1 )
{
// find the best var to add
VarBest = P2V[nVars-1-nBSsize];
nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
for ( v = nVars-2-nBSsize; v >= iVarStart; v-- )
{
// If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
if ( nCofsBest2 >= nCofs )
{
nCofsBest2 = nCofs;
VarBest = P2V[nVars-1-nBSsize];
}
}
// go back
// If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
// update best bound set
nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
assert( nCofs == nCofsBest2 );
}
// find the best var to remove
VarBest = P2V[nVars-1-nBSsize];
nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
for ( v = nVars-nBSsize; v < nVars; v++ )
{
// If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
if ( nCofsBest2 >= nCofs )
{
nCofsBest2 = nCofs;
VarBest = P2V[nVars-1-nBSsize];
}
}
// go back
// If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
// update best bound set
nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
assert( nCofs == nCofsBest2 );
if ( g->nMyu >= nCofs )
{
g->nVars = nBSsize;
g->nMyu = nCofs;
for ( i = 0; i < nBSsize; i++ )
g->pVars[i] = P2V[nVars-nBSsize+i];
}
if ( fVerbose )
{
printf( "Iter %2d ", r );
If_CluPrintGroup( g );
}
// check if good enough
if ( g->nMyu == 2 )
return G;
if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) )
{
// BestG = G;
return G;
}
}
assert( r == nRounds );
g->nVars = 0;
return G;
// return BestG;
}
// double check that the given group has a decomposition
void If_CluCheckGroup( word * pTruth, int nVars, If_Grp_t * g )
{
word pF[CLU_WRD_MAX];
int v, nCofs, V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX];
assert( g->nVars >= 2 && g->nVars <= 6 ); // vars
assert( g->nMyu >= 2 && g->nMyu <= 4 ); // cofs
// create permutation
for ( v = 0; v < nVars; v++ )
V2P[v] = P2V[v] = v;
// create truth table
If_CluCopy( pF, pTruth, nVars );
// move group up
If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, g );
// check the number of cofactors
nCofs = If_CluCountCofs( pF, nVars, g->nVars, 0, NULL );
if ( nCofs != g->nMyu )
printf( "Group check 0 has failed.\n" );
// check compatible
if ( nCofs > 2 )
{
nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, 0, NULL );
if ( nCofs > 2 )
printf( "Group check 1 has failed.\n" );
nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, (1 << (nVars-1)), NULL );
if ( nCofs > 2 )
printf( "Group check 2 has failed.\n" );
}
}
// double check that the permutation derived is correct
void If_CluCheckPerm( word * pTruth, word * pF, int nVars, int * V2P, int * P2V )
{
int i;
for ( i = 0; i < nVars; i++ )
If_CluMoveVar( pF, nVars, V2P, P2V, i, i );
if ( !If_CluEqual( pTruth, pF, nVars ) )
printf( "Permutation FAILED.\n" );
// else
// printf( "Permutation successful\n" );
}
static inline int If_CluSuppIsMinBase( int Supp )
{
return (Supp & (Supp+1)) == 0;
}
static inline int If_CluHasVar( word * t, int nVars, int iVar )
{
int nWords = If_CluWordNum( nVars );
assert( iVar < nVars );
if ( iVar < 6 )
{
int i, Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
return 1;
return 0;
}
else
{
int i, k, Step = (1 << (iVar - 6));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
if ( t[i] != t[Step+i] )
return 1;
t += 2*Step;
}
return 0;
}
}
static inline int If_CluSupport( word * t, int nVars )
{
int v, Supp = 0;
for ( v = 0; v < nVars; v++ )
if ( If_CluHasVar( t, nVars, v ) )
Supp |= (1 << v);
return Supp;
}
int If_CluSupportSize( word * t, int nVars )
{
int v, SuppSize = 0;
for ( v = 0; v < nVars; v++ )
if ( If_CluHasVar( t, nVars, v ) )
SuppSize++;
return SuppSize;
}
static inline void If_CluTruthShrink( word * pF, int nVars, int nVarsAll, unsigned Phase )
{
word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp;
int i, k, Var = 0, Counter = 0;
assert( nVarsAll <= 16 );
for ( i = 0; i < nVarsAll; i++ )
if ( Phase & (1 << i) )
{
for ( k = i-1; k >= Var; k-- )
{
If_CluSwapAdjacent( pOut, pIn, k, nVarsAll );
pTemp = pIn; pIn = pOut, pOut = pTemp;
Counter++;
}
Var++;
}
assert( Var == nVars );
// swap if it was moved an odd number of times
if ( Counter & 1 )
If_CluCopy( pOut, pIn, nVarsAll );
}
int If_CluMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars )
{
int v, iVar = 0, uSupp = 0;
assert( nVarsAll <= 16 );
for ( v = 0; v < nVarsAll; v++ )
if ( If_CluHasVar( t, nVarsAll, v ) )
{
uSupp |= (1 << v);
if ( pSupp )
pSupp[iVar] = pSupp[v];
iVar++;
}
if ( pnVars )
*pnVars = iVar;
if ( If_CluSuppIsMinBase( uSupp ) )
return 0;
If_CluTruthShrink( t, iVar, nVarsAll, uSupp );
return 1;
}
// returns the best group found
If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int iVarStart, int nLutLeaf, int nLutRoot,
If_Grp_t * pR, word * pFunc0, word * pFunc1, word * pLeftOver, int fHashing )
{
// int fEnableHashing = 0;
If_Grp_t G1 = {0}, R = {0};
unsigned * pHashed = NULL;
word Truth, pTruth[CLU_WRD_MAX], pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX];
int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2], pCanonPerm[CLU_VAR_MAX];
int i, nSupp, uCanonPhase;
int nLutSize = p ? p->pPars->nLutSize : nVars;
assert( nVars <= CLU_VAR_MAX );
assert( nVars <= nLutLeaf + nLutRoot - 1 );
if ( pR )
{
pR->nVars = 0;
*pFunc0 = 0;
*pFunc1 = 0;
}
// canonicize truth table
If_CluCopy( pTruth, pTruth0, nLutSize );
if ( 0 )
{
uCanonPhase = If_CluSemiCanonicize( pTruth, nVars, pCanonPerm );
If_CluAdjustBig( pTruth, nVars, nLutSize );
}
// If_CluSemiCanonicizeVerify( pTruth, pTruth0, nVars, pCanonPerm, uCanonPhase );
// If_CluCopy( pTruth, pTruth0, nLutSize );
/*
{
int pCanonPerm[32];
short pStore[32];
unsigned uCanonPhase;
If_CluCopy( pF, pTruth, nVars );
uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm, pStore );
G1.nVars = 1;
return G1;
}
*/
// check minnimum base
If_CluCopy( pF, pTruth, nVars );
for ( i = 0; i < nVars; i++ )
V2P[i] = P2V[i] = i;
// check support
nSupp = If_CluSupport( pF, nVars );
//Extra_PrintBinary( stdout, &nSupp, 16 ); printf( "\n" );
if ( !nSupp || !If_CluSuppIsMinBase(nSupp) )
{
// assert( 0 );
return G1;
}
// check hash table
if ( p && fHashing )
{
pHashed = If_CluHashLookup( p, pTruth, 0 );
if ( pHashed && *pHashed != CLU_UNUSED )
If_CluUns2Grp( *pHashed, &G1 );
}
if ( G1.nVars == 0 )
{
// detect easy cofs
if ( iVarStart == 0 )
G1 = If_CluDecUsingCofs( pTruth, nVars, nLutLeaf );
if ( G1.nVars == 0 )
{
// perform testing
G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
// If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
if ( G1.nVars == 0 )
{
// perform testing with a smaller set
if ( nVars < nLutLeaf + nLutRoot - 2 )
{
nLutLeaf--;
G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
nLutLeaf++;
}
// perform testing with a smaller set
if ( nLutLeaf > 4 && nVars < nLutLeaf + nLutRoot - 3 )
{
nLutLeaf--;
nLutLeaf--;
G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
nLutLeaf++;
nLutLeaf++;
}
if ( G1.nVars == 0 )
{
// perform testing with a different order
If_CluReverseOrder( pF, nVars, V2P, P2V, iVarStart );
G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
// check permutation
// If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
if ( G1.nVars == 0 )
{
// remember free set, just in case
// for ( i = 0; i < nVars - nLutLeaf; i++ )
/// G1.pVars[nLutLeaf+i] = P2V[i];
// if <XY>, this will not be used
// if <XYZ>, this will not be hashed
/*
if ( nVars == 6 )
{
Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( " " );
Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
if ( !If_CutPerformCheck07( (unsigned *)pF, 6, 6, NULL ) )
printf( "no\n" );
}
*/
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G1 );
return G1;
}
}
}
}
}
// derive
if ( pR )
{
int iNewPos;
If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, &G1 );
if ( G1.nMyu == 2 )
{
Truth = If_CluDeriveDisjoint( pF, nVars, V2P, P2V, &G1, &R );
iNewPos = R.nVars - 1;
}
else
{
Truth = If_CluDeriveNonDisjoint( pF, nVars, V2P, P2V, &G1, &R );
iNewPos = R.nVars - 2;
}
assert( R.pVars[iNewPos] == nVars );
// adjust the functions
Truth = If_CluAdjust( Truth, G1.nVars );
if ( R.nVars < 6 )
pF[0] = If_CluAdjust( pF[0], R.nVars );
// Kit_DsdPrintFromTruth( (unsigned*)&Truth, G1.nVars ); printf( " ...1\n" );
// Kit_DsdPrintFromTruth( (unsigned*)pF, R.nVars ); printf( " ...1\n" );
// update the variable order of R so that the new var was the first one
// if ( iVarStart == 0 )
{
int k, V2P2[CLU_VAR_MAX+2], P2V2[CLU_VAR_MAX+2];
assert( iNewPos >= iVarStart );
for ( k = 0; k < R.nVars; k++ )
V2P2[k] = P2V2[k] = k;
If_CluMoveVar( pF, R.nVars, V2P2, P2V2, iNewPos, iVarStart );
for ( k = iNewPos; k > iVarStart; k-- )
R.pVars[k] = R.pVars[k-1];
R.pVars[iVarStart] = nVars;
}
// Kit_DsdPrintFromTruth( (unsigned*)pF, R.nVars ); printf( " ...2\n" );
if ( pLeftOver )
{
if ( R.nVars < 6 )
*pLeftOver = If_CluAdjust( pF[0], R.nVars );
else
If_CluCopy( pLeftOver, pF, R.nVars );
If_CluAdjustBig( pLeftOver, R.nVars, nLutSize );
}
// perform checking
if ( 0 )
{
If_CluCheckGroup( pTruth, nVars, &G1 );
If_CluVerify( pTruth, nVars, &G1, &R, Truth, pF );
}
// save functions
*pR = R;
if ( pFunc0 )
*pFunc0 = pF[0];
if ( pFunc1 )
*pFunc1 = Truth;
}
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G1 );
return G1;
}
// returns the best group found
If_Grp_t If_CluCheck3( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 )
{
int fEnableHashing = 1;
static int Counter = 0;
unsigned * pHashed = NULL;
word pLeftOver[CLU_WRD_MAX], Func0, Func1, Func2;
If_Grp_t G1 = {0}, G2 = {0}, R = {0}, R2 = {0};
int i;
Counter++;
// if ( Counter == 37590 )
// {
// int ns = 0;
// }
// check hash table
if ( p && fEnableHashing )
{
pHashed = If_CluHashLookup( p, pTruth0, 1 );
if ( pHashed && *pHashed != CLU_UNUSED )
{
If_CluUns2Grp( *pHashed, &G1 );
return G1;
}
}
// check two-node decomposition
G1 = If_CluCheck( p, pTruth0, nVars, 0, nLutLeaf, nLutRoot + nLutLeaf2 - 1, &R2, &Func0, &Func1, pLeftOver, 0 );
// decomposition does not exist
if ( G1.nVars == 0 )
{
// check for decomposition with two outputs
if ( (G1.nMyu == 3 || G1.nMyu == 4) && nLutLeaf == nLutLeaf2 && nVars - nLutLeaf + 2 <= nLutRoot )
{
int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2];
word Func0, Func1, Func2;
int iVar0, iVar1;
G1.nVars = nLutLeaf;
If_CluCopy( pLeftOver, pTruth0, nVars );
for ( i = 0; i < nVars; i++ )
V2P[i] = P2V[i] = i;
If_CluMoveGroupToMsb( pLeftOver, nVars, V2P, P2V, &G1 );
If_CluDeriveDisjoint4( pLeftOver, nVars, V2P, P2V, &G1, &R, &Func1, &Func2 );
// move the two vars to the front
for ( i = 0; i < R.nVars; i++ )
V2P[i] = P2V[i] = i;
If_CluMoveVar( pLeftOver, R.nVars, V2P, P2V, R.nVars-2, 0 );
If_CluMoveVar( pLeftOver, R.nVars, V2P, P2V, R.nVars-1, 1 );
iVar0 = R.pVars[R.nVars-2];
iVar1 = R.pVars[R.nVars-1];
for ( i = R.nVars-1; i > 1; i-- )
R.pVars[i] = R.pVars[i-2];
R.pVars[0] = iVar0;
R.pVars[1] = iVar1;
Func0 = pLeftOver[0];
If_CluVerify3( pTruth0, nVars, &G1, &G1, &R, Func1, Func2, Func0 );
if ( pFunc1 && pFunc2 )
{
*pFunc0 = Func0;
*pFunc1 = Func1;
*pFunc2 = Func2;
*pG2 = G1;
*pR = R;
}
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G1 );
// Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" );
// If_CluPrintGroup( &G1 );
return G1;
}
/*
// if ( nVars == 6 )
{
// Extra_PrintHex( stdout, (unsigned *)pTruth0, nVars ); printf( " " );
Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" );
if ( p != NULL )
If_CluCheck3( NULL, pTruth0, nVars, nLutLeaf, nLutLeaf2, nLutRoot, pR, pG2, pFunc0, pFunc1, pFunc2 );
}
*/
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G1 );
return G1;
}
// decomposition exists and sufficient
if ( R2.nVars <= nLutRoot )
{
if ( pG2 ) *pG2 = G2;
if ( pR ) *pR = R2;
if ( pFunc0 ) *pFunc0 = Func0;
if ( pFunc1 ) *pFunc1 = Func1;
if ( pFunc2 ) *pFunc2 = 0;
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G1 );
return G1;
}
// try second decomposition
{
int Test = 0;
if ( Test )
{
Kit_DsdPrintFromTruth( (unsigned*)&pLeftOver, R2.nVars ); printf( "\n" );
}
}
// the new variable is at the bottom - skip it (iVarStart = 1)
#ifdef IF_USE_CASE3
G2 = If_CluCheck( p, pLeftOver, R2.nVars, 0, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 );
#else
G2 = If_CluCheck( p, pLeftOver, R2.nVars, 1, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 );
#endif
if ( G2.nVars == 0 )
{
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G2 );
return G2;
}
// remap variables
for ( i = 0; i < G2.nVars; i++ )
{
assert( G2.pVars[i] < R2.nVars );
G2.pVars[i] = R2.pVars[ (int)G2.pVars[i] ];
}
// remap variables
for ( i = 0; i < R.nVars; i++ )
{
if ( R.pVars[i] == R2.nVars )
R.pVars[i] = nVars + 1;
else
R.pVars[i] = R2.pVars[ (int)R.pVars[i] ];
}
// decomposition exist
if ( pG2 ) *pG2 = G2;
if ( pR ) *pR = R;
if ( pFunc0 ) *pFunc0 = Func0;
if ( pFunc1 ) *pFunc1 = Func1;
if ( pFunc2 ) *pFunc2 = Func2;
if ( pHashed )
*pHashed = If_CluGrp2Uns( &G1 );
// verify
// If_CluVerify3( pTruth0, nVars, &G1, &G2, &R, Func1, Func2, Func0 );
return G1;
}
// returns the best group found
int If_CluCheckExt( void * pMan, word * pTruth, int nVars, int nLutLeaf, int nLutRoot,
char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 )
{
If_Man_t * p = (If_Man_t *)pMan;
If_Grp_t G, R;
G = If_CluCheck( p, pTruth, nVars, 0, nLutLeaf, nLutRoot, &R, pFunc0, pFunc1, NULL, 0 );
memcpy( pLut0, &R, sizeof(If_Grp_t) );
memcpy( pLut1, &G, sizeof(If_Grp_t) );
// memcpy( pLut2, &G2, sizeof(If_Grp_t) );
return (G.nVars > 0);
}
// returns the best group found
int If_CluCheckExt3( void * pMan, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 )
{
If_Man_t * p = (If_Man_t *)pMan;
If_Grp_t G, G2, R;
G = If_CluCheck3( p, pTruth, nVars, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, pFunc0, pFunc1, pFunc2 );
memcpy( pLut0, &R, sizeof(If_Grp_t) );
memcpy( pLut1, &G, sizeof(If_Grp_t) );
memcpy( pLut2, &G2, sizeof(If_Grp_t) );
return (G.nVars > 0);
}
// computes delay of the decomposition
float If_CluDelayMax( If_Grp_t * g, float * pDelays )
{
float Delay = 0.0;
int i;
for ( i = 0; i < g->nVars; i++ )
Delay = Abc_MaxFloat( Delay, pDelays[(int)g->pVars[i]] );
return Delay;
}
// returns delay of the decomposition; sets area of the cut as its cost
float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float WireDelay )
{
float Delays[CLU_VAR_MAX+2];
int fUsed[CLU_VAR_MAX+2] = {0};
If_Obj_t * pLeaf;
If_Grp_t G1 = {0}, G2 = {0}, G3 = {0};
int nLeaves = If_CutLeaveNum(pCut);
int i, nLutLeaf, nLutRoot;
// mark the cut as user cut
// pCut->fUser = 1;
// quit if parameters are wrong
if ( strlen(pStr) != 2 )
{
printf( "Wrong LUT struct (%s)\n", pStr );
return ABC_INFINITY;
}
nLutLeaf = pStr[0] - '0';
if ( nLutLeaf < 3 || nLutLeaf > 6 )
{
printf( "Leaf size (%d) should belong to {3,4,5,6}.\n", nLutLeaf );
return ABC_INFINITY;
}
nLutRoot = pStr[1] - '0';
if ( nLutRoot < 3 || nLutRoot > 6 )
{
printf( "Root size (%d) should belong to {3,4,5,6}.\n", nLutRoot );
return ABC_INFINITY;
}
if ( nLeaves > nLutLeaf + nLutRoot - 1 )
{
printf( "The cut size (%d) is too large for the LUT structure %d%d.\n", If_CutLeaveNum(pCut), nLutLeaf, nLutRoot );
return ABC_INFINITY;
}
// remember the delays
If_CutForEachLeaf( p, pCut, pLeaf, i )
Delays[i] = If_ObjCutBest(pLeaf)->Delay;
// consider easy case
if ( nLeaves <= Abc_MaxInt( nLutLeaf, nLutRoot ) )
{
assert( nLeaves <= 6 );
for ( i = 0; i < nLeaves; i++ )
{
pCut->pPerm[i] = 1;
G1.pVars[i] = i;
}
G1.nVars = nLeaves;
return 1.0 + If_CluDelayMax( &G1, Delays );
}
// derive the first group
G1 = If_CluCheck( p, (word *)If_CutTruth(pCut), nLeaves, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 );
if ( G1.nVars == 0 )
return ABC_INFINITY;
// compute the delay
Delays[nLeaves] = If_CluDelayMax( &G1, Delays ) + (WireDelay == 0.0)?1.0:WireDelay;
if ( G2.nVars )
Delays[nLeaves+1] = If_CluDelayMax( &G2, Delays ) + (WireDelay == 0.0)?1.0:WireDelay;
// mark used groups
for ( i = 0; i < G1.nVars; i++ )
fUsed[(int)G1.pVars[i]] = 1;
for ( i = 0; i < G2.nVars; i++ )
fUsed[(int)G2.pVars[i]] = 1;
// mark unused groups
assert( G1.nMyu >= 2 && G1.nMyu <= 4 );
if ( G1.nMyu > 2 )
fUsed[(int)G1.pVars[G1.nVars-1]] = 0;
assert( !G2.nVars || (G2.nMyu >= 2 && G2.nMyu <= 4) );
if ( G2.nMyu > 2 )
fUsed[(int)G2.pVars[G2.nVars-1]] = 0;
// create remaining group
assert( G3.nVars == 0 );
for ( i = 0; i < nLeaves; i++ )
if ( !fUsed[i] )
G3.pVars[(int)G3.nVars++] = i;
G3.pVars[(int)G3.nVars++] = nLeaves;
if ( G2.nVars )
G3.pVars[(int)G3.nVars++] = nLeaves+1;
assert( G1.nVars + G2.nVars + G3.nVars == nLeaves +
(G1.nVars > 0) + (G2.nVars > 0) + (G1.nMyu > 2) + (G2.nMyu > 2) );
// what if both non-disjoint vars are the same???
pCut->Cost = 2 + (G2.nVars > 0);
return 1.0 + If_CluDelayMax( &G3, Delays );
}
/**Function*************************************************************
Synopsis [Performs additional check.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
If_Grp_t G1 = {0};//, G3 = {0};
int i, nLutLeaf, nLutLeaf2, nLutRoot, Length;
// if cutmin is disabled, minimize the cut
if ( !p->pPars->fCutMin && If_CluSupportSize((word *)pTruth, nVars) < nLeaves )
{
If_Cut_t * pCut = p->pCutTemp;
pCut->nLimit = nVars;
pCut->nLeaves = nLeaves;
pCut->pLeaves = (int *)(pCut + 1);
for ( i = 0; i < nLeaves; i++ )
pCut->pLeaves[i] = i;
pCut->pTruth = (unsigned *)pCut->pLeaves + pCut->nLimit + p->nPermWords;
If_CluCopy( (word *)If_CutTruth(pCut), (word *)pTruth, nVars );
if ( If_CutTruthMinimize( p, pCut ) >= 2 )
return 0;
nLeaves = pCut->nLeaves;
// If_CluCopy( (word *)pTruth, (word *)If_CutTruth(pCut), nVars );
pTruth = If_CutTruth(pCut);
}
// quit if parameters are wrong
Length = strlen(pStr);
if ( Length != 2 && Length != 3 )
{
printf( "Wrong LUT struct (%s)\n", pStr );
return 0;
}
for ( i = 0; i < Length; i++ )
if ( pStr[i] - '0' < 3 || pStr[i] - '0' > 6 )
{
printf( "The LUT size (%d) should belong to {3,4,5,6}.\n", pStr[i] - '0' );
return 0;
}
nLutLeaf = pStr[0] - '0';
nLutLeaf2 = ( Length == 3 ) ? pStr[1] - '0' : 0;
nLutRoot = pStr[Length-1] - '0';
if ( nLeaves > nLutLeaf - 1 + (nLutLeaf2 ? nLutLeaf2 - 1 : 0) + nLutRoot )
{
printf( "The cut size (%d) is too large for the LUT structure %s.\n", nLeaves, pStr );
return 0;
}
// consider easy case
if ( nLeaves <= Abc_MaxInt( nLutLeaf2, Abc_MaxInt(nLutLeaf, nLutRoot) ) )
return 1;
// derive the first group
if ( Length == 2 )
G1 = If_CluCheck( p, (word *)pTruth, nLeaves, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 );
else
G1 = If_CluCheck3( p, (word *)pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, NULL, NULL, NULL, NULL, NULL );
// if ( G1.nVars > 0 )
// If_CluPrintGroup( &G1 );
return (int)(G1.nVars > 0);
}
// testing procedure
void If_CluTest()
{
// word t = 0xff00f0f0ccccaaaa;
// word t = 0xfedcba9876543210;
// word t = 0xec64000000000000;
// word t = 0x0100200000000001;
// word t2[4] = { 0x0000800080008000, 0x8000000000008000, 0x8000000080008000, 0x0000000080008000 };
// word t = 0x07770FFF07770FFF;
// word t = 0x002000D000D00020;
// word t = 0x000F000E000F000F;
// word t = 0xF7FFF7F7F7F7F7F7;
// word t = 0x0234AFDE23400BCE;
// word t = 0x0080008880A088FF;
// word s = t;
// word t = 0xFFBBBBFFF0B0B0F0;
word t = 0x6DD9926D962D6996;
int nVars = 6;
int nLutLeaf = 4;
int nLutLeaf2 = 4;
int nLutRoot = 4;
/*
word t2[2] = { 0x7f807f807f80807f, 0x7f807f807f807f80 };
int nVars = 7;
int nLutLeaf = 3;
int nLutLeaf2 = 3;
int nLutRoot = 3;
*/
If_Grp_t G;
If_Grp_t G2, R;
word Func0, Func1, Func2;
return;
/*
int pCanonPerm[CLU_VAR_MAX];
int uCanonPhase;
Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" );
uCanonPhase = If_CluSemiCanonicize( &s, nVars, pCanonPerm );
Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" );
If_CluSemiCanonicizeVerify( &s, &t, nVars, pCanonPerm, uCanonPhase );
*/
Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" );
G = If_CluCheck3( NULL, &t, nVars, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 );
If_CluPrintGroup( &G );
If_CluPrintGroup( &G2 );
If_CluPrintGroup( &R );
// If_CluVerify3( &t, nVars, &G, &G2, &R, Func1, Func2, Func0 );
return;
// If_CutPerformCheck07( NULL, (unsigned *)&t, 6, 6, NULL );
// return;
// Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" );
// G = If_CluCheck( NULL, &t, nVars, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 0 );
// If_CluPrintGroup( &G );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END