mirror of https://github.com/YosysHQ/abc.git
Improvements to the truth table computation in 'if' package.
This commit is contained in:
Alan Mishchenko
parent
90529df059
commit
c3298ec225
|
|
@ -115,7 +115,7 @@ static inline int Abc_TtSuppIsMinBase( int Supp )
|
|||
}
|
||||
static inline int Abc_Tt6HasVar( word t, int iVar )
|
||||
{
|
||||
return (t & ~s_Truths6[iVar]) != ((t & s_Truths6[iVar]) >> (1<<iVar));
|
||||
return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]);
|
||||
}
|
||||
static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
|
||||
{
|
||||
|
|
@ -125,14 +125,15 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
|
|||
{
|
||||
int i, Shift = (1 << iVar);
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (t[i] & ~s_Truths6[iVar]) != ((t[i] & s_Truths6[iVar]) >> Shift) )
|
||||
if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, k, Step = (1 << (iVar - 6));
|
||||
for ( k = 0; k < nWords; k += 2*Step, t += 2*Step )
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != t[Step+i] )
|
||||
return 1;
|
||||
|
|
@ -188,6 +189,103 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
|
|||
|
||||
***********************************************************************/
|
||||
static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
|
||||
{
|
||||
static word PPMasks[5][6][3] = {
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0
|
||||
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1
|
||||
{ 0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050 }, // 0 2
|
||||
{ 0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 }, // 0 3
|
||||
{ 0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 }, // 0 4
|
||||
{ 0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 } // 0 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 1
|
||||
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, // 1 2
|
||||
{ 0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 }, // 1 3
|
||||
{ 0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 }, // 1 4
|
||||
{ 0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 } // 1 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 1
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 2
|
||||
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, // 2 3
|
||||
{ 0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 }, // 2 4
|
||||
{ 0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 } // 2 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 1
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 2
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 3
|
||||
{ 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, // 3 4
|
||||
{ 0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 } // 3 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 1
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 2
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 3
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 4
|
||||
{ 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } // 4 5
|
||||
}
|
||||
};
|
||||
if ( iVar == jVar )
|
||||
return;
|
||||
if ( jVar < iVar )
|
||||
ABC_SWAP( int, iVar, jVar );
|
||||
assert( iVar < jVar && jVar < nVars );
|
||||
if ( nVars <= 6 )
|
||||
{
|
||||
word * pMasks = PPMasks[iVar][jVar];
|
||||
int shift = (1 << jVar) - (1 << iVar);
|
||||
pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift);
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( jVar <= 5 )
|
||||
{
|
||||
word * pMasks = PPMasks[iVar][jVar];
|
||||
int nWords = Abc_TtWordNum(nVars);
|
||||
int w, shift = (1 << jVar) - (1 << iVar);
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
|
||||
}
|
||||
else if ( iVar <= 5 && jVar > 5 )
|
||||
{
|
||||
word low2High, high2Low;
|
||||
word * pLimit = pTruth + Abc_TtWordNum(nVars);
|
||||
int j, jStep = Abc_TtWordNum(jVar);
|
||||
int shift = 1 << iVar;
|
||||
for ( ; pTruth < pLimit; pTruth += 2*jStep )
|
||||
for ( j = 0; j < jStep; j++ )
|
||||
{
|
||||
low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
|
||||
high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
|
||||
pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
|
||||
pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
word temp, * pLimit = pTruth + Abc_TtWordNum(nVars);
|
||||
int i, iStep = Abc_TtWordNum(iVar);
|
||||
int j, jStep = Abc_TtWordNum(jVar);
|
||||
for ( ; pTruth < pLimit; pTruth += 2*jStep )
|
||||
for ( i = 0; i < jStep; i += 2*iStep )
|
||||
for ( j = 0; j < iStep; j++ )
|
||||
{
|
||||
temp = pTruth[iStep + i + j];
|
||||
pTruth[iStep + i + j] = pTruth[jStep + i + j];
|
||||
pTruth[jStep + i + j] = temp;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar )
|
||||
{
|
||||
static word PPMasks[6][6] = {
|
||||
{ 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
|
||||
|
|
@ -269,6 +367,7 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
|
|||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stretch truthtable to have more input variables.]
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@
|
|||
***********************************************************************/
|
||||
|
||||
#include "dauInt.h"
|
||||
#include "misc/util/utilTruth.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -463,6 +464,344 @@ void Dau_DsdTestOne( word t, int i )
|
|||
Dau_DsdTestOne( *p->pFuncs[i], i );
|
||||
*/
|
||||
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; }
|
||||
static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
|
||||
|
||||
static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( t[i] & ~s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (t[i] & ~s_Truths6[iVar]) != ~s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != ~(word)0 )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( t[i] & s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i+Step] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i+Step] != ~(word)0 )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i, Shift = (1 << iVar);
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != ~t[i+Step] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Abc_TtCof0HasVar( word * t, int nWords, int iVarI, int iVarJ )
|
||||
{
|
||||
assert( iVarI > iVarJ );
|
||||
if ( iVarI < 6 )
|
||||
{
|
||||
int i, Shift = (1 << iVarJ);
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (((t[i] & ~s_Truths6[iVarI]) << Shift) & s_Truths6[iVarJ]) != ((t[i] & ~s_Truths6[iVarI]) & s_Truths6[iVarJ]) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else if ( iVarI == 6 )
|
||||
{
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVarJ - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != t[i+Step] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdMinimize( word * p, int * pVars, int nVars )
|
||||
{
|
||||
int i, k;
|
||||
assert( nVars > 6 );
|
||||
for ( i = k = nVars - 1; i >= 0; i-- )
|
||||
{
|
||||
if ( Abc_TtHasVar( p, nVars, i ) )
|
||||
continue;
|
||||
if ( i < k )
|
||||
{
|
||||
pVars[i] = pVars[k];
|
||||
Abc_TtSwapVars( p, nVars, i, k );
|
||||
}
|
||||
k--;
|
||||
nVars--;
|
||||
}
|
||||
return nVars;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
|
||||
{
|
||||
int v, nWords = Abc_TtWordNum( nVars );
|
||||
nVars = Dau_DsdMinimize( p, pVars, nVars );
|
||||
if ( nVars <= 6 )
|
||||
return Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
|
||||
if ( p[0] & 1 )
|
||||
{
|
||||
// check for !(ax)
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof0IsConst0( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// check for ax
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof0IsConst1( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
if ( (p[nWords-1] >> 63) & 1 )
|
||||
{
|
||||
// check for !(!ax)
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof0IsConst1( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// check for !ax
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof1IsConst0( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
// check for a^x
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCofsOpposite( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '[';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ']';
|
||||
return Pos;
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
char * Dau_DsdRun( word * p, int nVars )
|
||||
{
|
||||
static char pBuffer[DAU_MAX_STR+20];
|
||||
static char pStore[16][16];
|
||||
int nWords = Abc_TtWordNum( nVars );
|
||||
int i, Pos = 0, Func = 0, pVars[16];
|
||||
assert( nVars <= 16 );
|
||||
for ( i = 0; i < nVars; i++ )
|
||||
pVars[i] = i;
|
||||
if ( Abc_TtTruthIsConst0( p, nWords ) )
|
||||
pBuffer[Pos++] = '0';
|
||||
else if ( Abc_TtTruthIsConst1( p, nWords ) )
|
||||
pBuffer[Pos++] = '1';
|
||||
else if ( nVars <= 6 )
|
||||
Pos = Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
|
||||
else
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = 0;
|
||||
Dau_DsdCleanBraces( pBuffer );
|
||||
return pBuffer;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
Loading…
Reference in New Issue