Commit b9c22ba9 by Alan Mishchenko

Improved DSD.

parent 96d3348d
...@@ -172,6 +172,17 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords ) ...@@ -172,6 +172,17 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline word Abc_Tt6Cofactor0( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
}
static inline word Abc_Tt6Cofactor1( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
}
static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar ) static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
{ {
if ( nWords == 1 ) if ( nWords == 1 )
...@@ -289,18 +300,10 @@ static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths ...@@ -289,18 +300,10 @@ static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths
static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar]; } static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar]; }
static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0; } static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0; }
static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar]; } static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar]; }
static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); } static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return (~t & s_Truths6Neg[iVar]) == ((t >> (1 << iVar)) & s_Truths6Neg[iVar]); }
static inline int Abc_Tt6Cof0EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == ((t2 >> (1 << iVar)) & s_Truths6Neg[iVar]); }
static inline word Abc_Tt6Cofactor0( word t, int iVar ) static inline int Abc_Tt6Cof0EqualCof0( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == (t2 & s_Truths6Neg[iVar]); }
{ static inline int Abc_Tt6Cof1EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6[iVar]) == (t2 & s_Truths6[iVar]); }
assert( iVar >= 0 && iVar < 6 );
return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
}
static inline word Abc_Tt6Cofactor1( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
}
/**Function************************************************************* /**Function*************************************************************
...@@ -433,13 +436,12 @@ static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) ...@@ -433,13 +436,12 @@ static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Abc_TtPrintDigit( int Digit ) static inline char Abc_TtPrintDigit( int Digit )
{ {
assert( Digit >= 0 && Digit < 16 ); assert( Digit >= 0 && Digit < 16 );
if ( Digit < 10 ) if ( Digit < 10 )
printf( "%d", Digit ); return '0' + Digit;;
else return 'A' + Digit-10;
printf( "%c", 'A' + Digit-10 );
} }
static inline void Abc_TtPrintHex( word * pTruth, int nVars ) static inline void Abc_TtPrintHex( word * pTruth, int nVars )
{ {
...@@ -448,7 +450,7 @@ static inline void Abc_TtPrintHex( word * pTruth, int nVars ) ...@@ -448,7 +450,7 @@ static inline void Abc_TtPrintHex( word * pTruth, int nVars )
assert( nVars >= 2 ); assert( nVars >= 2 );
for ( pThis = pTruth; pThis < pLimit; pThis++ ) for ( pThis = pTruth; pThis < pLimit; pThis++ )
for ( k = 0; k < 16; k++ ) for ( k = 0; k < 16; k++ )
Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 ); printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
printf( "\n" ); printf( "\n" );
} }
static inline void Abc_TtPrintHexRev( word * pTruth, int nVars ) static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
...@@ -458,7 +460,7 @@ static inline void Abc_TtPrintHexRev( word * pTruth, int nVars ) ...@@ -458,7 +460,7 @@ static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
assert( nVars >= 2 ); assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- ) for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = 15; k >= 0; k-- ) for ( k = 15; k >= 0; k-- )
Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 ); printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
printf( "\n" ); printf( "\n" );
} }
static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars ) static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
...@@ -468,9 +470,20 @@ static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars ) ...@@ -468,9 +470,20 @@ static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
assert( nVars >= 2 ); assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- ) for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = 0; k < 16; k++ ) for ( k = 0; k < 16; k++ )
Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 ); printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
printf( "\n" ); printf( "\n" );
} }
static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
{
word * pThis;
char * pStrInit = pStr;
int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = StartK - 1; k >= 0; k-- )
*pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
return pStr - pStrInit;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -531,11 +544,13 @@ static inline int Abc_Tt6HasVar( word t, int iVar ) ...@@ -531,11 +544,13 @@ static inline int Abc_Tt6HasVar( word t, int iVar )
} }
static inline int Abc_TtHasVar( word * t, int nVars, int iVar ) static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
{ {
int nWords = Abc_TtWordNum( nVars );
assert( iVar < nVars ); assert( iVar < nVars );
if ( nVars <= 6 )
return Abc_Tt6HasVar( t[0], iVar );
if ( iVar < 6 ) if ( iVar < 6 )
{ {
int i, Shift = (1 << iVar); int i, Shift = (1 << iVar);
int nWords = Abc_TtWordNum( nVars );
for ( i = 0; i < nWords; i++ ) for ( i = 0; i < nWords; i++ )
if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) ) if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
return 1; return 1;
...@@ -544,7 +559,7 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar ) ...@@ -544,7 +559,7 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
else else
{ {
int i, Step = (1 << (iVar - 6)); int i, Step = (1 << (iVar - 6));
word * tLimit = t + nWords; word * tLimit = t + Abc_TtWordNum( nVars );
for ( ; t < tLimit; t += 2*Step ) for ( ; t < tLimit; t += 2*Step )
for ( i = 0; i < Step; i++ ) for ( i = 0; i < Step; i++ )
if ( t[i] != t[Step+i] ) if ( t[i] != t[Step+i] )
......
...@@ -711,6 +711,8 @@ struct Dau_Dsd_t_ ...@@ -711,6 +711,8 @@ struct Dau_Dsd_t_
char pVarDefs[32][8]; // variable definitions char pVarDefs[32][8]; // variable definitions
char pOutput[DAU_MAX_STR]; // output stream char pOutput[DAU_MAX_STR]; // output stream
int nPos; // writing position int nPos; // writing position
int nConsts; // the number of constant decompositions
int uConstMask; // constant decomposition mask
}; };
/**Function************************************************************* /**Function*************************************************************
...@@ -742,19 +744,31 @@ void Dua_DsdWriteInv( Dau_Dsd_t * p, int Cond ) ...@@ -742,19 +744,31 @@ void Dua_DsdWriteInv( Dau_Dsd_t * p, int Cond )
if ( Cond ) if ( Cond )
p->pOutput[ p->nPos++ ] = '!'; p->pOutput[ p->nPos++ ] = '!';
} }
void Dua_DsdWriteVar( Dau_Dsd_t * p, int iVar ) void Dua_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv )
{ {
char * pStr; char * pStr;
if ( fInv )
p->pOutput[ p->nPos++ ] = '!';
for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ ) for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed ) if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
Dua_DsdWriteVar( p, *pStr - 'a' ); Dua_DsdWriteVar( p, *pStr - 'a', 0 );
else else
p->pOutput[ p->nPos++ ] = *pStr; p->pOutput[ p->nPos++ ] = *pStr;
} }
void Dua_DsdWriteStop( Dau_Dsd_t * p ) void Dua_DsdWriteStop( Dau_Dsd_t * p )
{ {
int i;
for ( i = 0; i < p->nConsts; i++ )
p->pOutput[ p->nPos++ ] = ((p->uConstMask >> i) & 1) ? ']' : ')';
p->pOutput[ p->nPos++ ] = 0; p->pOutput[ p->nPos++ ] = 0;
} }
int Dua_DsdAddVarDef( Dau_Dsd_t * p, char * pStr )
{
assert( strlen(pStr) < 8 );
assert( p->nVarsUsed < 32 );
sprintf( p->pVarDefs[p->nVarsUsed++], "%s", pStr );
return p->nVarsUsed - 1;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -767,18 +781,24 @@ void Dua_DsdWriteStop( Dau_Dsd_t * p ) ...@@ -767,18 +781,24 @@ void Dua_DsdWriteStop( Dau_Dsd_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Dua_DsdMinBase( word t, int nVars, int * pVarsNew ) int Dua_DsdMinBase( word * pTruth, int nVars, int * pVarsNew )
{ {
int v, nVarsNew = 0; int v;
for ( v = 0; v < nVars; v++ ) for ( v = 0; v < nVars; v++ )
if ( Abc_Tt6HasVar( t, v ) ) pVarsNew[v] = v;
pVarsNew[nVarsNew++] = v; for ( v = nVars - 1; v >= 0; v-- )
return nVarsNew; {
if ( Abc_TtHasVar( pTruth, nVars, v ) )
continue;
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
pVarsNew[v] = pVarsNew[--nVars];
}
return nVars;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Returns 1 if constant cofactor is found.]
Description [] Description []
...@@ -787,29 +807,206 @@ int Dua_DsdMinBase( word t, int nVars, int * pVarsNew ) ...@@ -787,29 +807,206 @@ int Dua_DsdMinBase( word t, int nVars, int * pVarsNew )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word t, int * pVars, int nVars ) int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{ {
int nConstOld = p->nConsts;
// consider negative cofactors
if ( pTruth[0] & 1 )
{
if ( Abc_Tt6Cof0IsConst1( pTruth[0], v ) ) // !(ax)
{
Dua_DsdWrite( p, "!(" );
pTruth[0] = ~Abc_Tt6Cofactor1( pTruth[0], v );
p->nConsts++;
}
}
else
{
if ( Abc_Tt6Cof0IsConst0( pTruth[0], v ) ) // ax
{
Dua_DsdWrite( p, "(" );
pTruth[0] = Abc_Tt6Cofactor1( pTruth[0], v );
p->nConsts++;
}
}
// consider positive cofactors
if ( pTruth[0] >> 63 )
{
if ( Abc_Tt6Cof1IsConst1( pTruth[0], v ) ) // !(!ax)
{
Dua_DsdWrite( p, "!(!" );
pTruth[0] = ~Abc_Tt6Cofactor0( pTruth[0], v );
p->nConsts++;
}
}
else
{
if ( Abc_Tt6Cof1IsConst0( pTruth[0], v ) ) // !ax
{
Dua_DsdWrite( p, "(!" );
pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
p->nConsts++;
}
}
// consider equal cofactors
if ( Abc_Tt6CofsOpposite( pTruth[0], v ) ) // [ax]
{
Dua_DsdWrite( p, "[" );
pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
p->uConstMask |= (1 << p->nConsts++);
}
if ( nConstOld == p->nConsts )
return 0;
Dua_DsdWriteVar( p, pVars[v], 0 );
pVars[v] = pVars[nVars-1];
Abc_TtSwapVars( pTruth, 6, v, nVars-1 );
return 1;
}
int Dau_Dsd6DecomposeConstCof( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
int v;
assert( nVars > 1 );
for ( v = nVars - 1; v >= 0 && nVars > 1; v++ )
if ( Dau_Dsd6DecomposeConstCofOne( p, pTruth, pVars, nVars, v ) )
nVars--;
if ( nVars == 1 )
Dua_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
return nVars;
} }
char * Dau_DsdDecompose( word t, int nVarsInit ) void Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word t, int * pVars, int nVars )
{
char pBuffer[10];
int v, u;
nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, nVars );
if ( nVars == 0 )
return;
// consider two-variable cofactors
for ( v = nVars - 1; v > 0; v-- )
{
word tCof0 = Abc_Tt6Cofactor0( t, v );
word tCof1 = Abc_Tt6Cofactor1( t, v );
unsigned uSupp0 = 0, uSupp1 = 0;
for ( u = v - 1; u >= 0; u-- )
{
if ( Abc_Tt6HasVar(tCof0, u) )
{
uSupp0 |= (1 << u);
if ( Abc_Tt6HasVar(tCof1, u) )
{
uSupp1 |= (1 << u);
// both F(v=0) and F(v=1) depend on u
if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) )
{
// perform XOR (u, v)
t = (s_Truths6[u] & tCof1) | (~s_Truths6[u] & tCof0);
sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
break;
}
}
else
{
// F(v=0) does not depend on u; F(v=1) depends on u
if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) )
{
// perform AND (u, v)
break;
}
if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) )
{
// perform AND (u, v)
break;
}
}
}
else if ( Abc_Tt6HasVar(tCof1, u) )
{
uSupp1 |= (1 << u);
// F(v=0) depends on u; F(v=1) does not depend on u
if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) )
{
// perform AND (u, v)
break;
}
if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) )
{
// perform AND (u, v)
break;
}
}
else assert( 0 ); // should depend on u
}
// check if decomposition happened
if ( u >= 0 )
{
// finalize decomposition
pVars[u] = Dua_DsdAddVarDef( p, pBuffer );
pVars[v] = pVars[nVars-1];
Abc_TtSwapVars( &t, 6, v, nVars-1 );
nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, --nVars );
if ( nVars == 0 )
return;
continue;
}
// check MUX decomposition w.r.t. u
if ( Abc_TtSuppOnlyOne( uSupp0 & ~uSupp1 ) && Abc_TtSuppOnlyOne( ~uSupp0 & uSupp1 ) )
{
// check MUX
int iVar0 = Abc_TtSuppFindFirst( uSupp0 );
int iVar1 = Abc_TtSuppFindFirst( uSupp1 );
int fEqual0, fEqual1;
if ( iVar0 > iVar1 )
ABC_SWAP( int, iVar0, iVar1 );
// check existence conditions
assert( iVar0 < iVar1 );
fEqual0 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 3 );
fEqual1 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 2 );
if ( fEqual0 || fEqual1 )
{
// perform MUX( v, F(v=1), F(v=0) )
break;
}
}
// check MUX decomposition w.r.t. u
if ( (uSupp0 & uSupp1) == 0 )
{
// perform MUX( v, F(v=1), F(v=0) )
}
}
// this non-DSD-decomposable function
assert( nVars > 2 );
// write truth table
p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, &t, nVars );
Dua_DsdWrite( p, "{" );
for ( v = 0; v < nVars; v++ )
Dua_DsdWriteVar( p, pVars[v], 0 );
Dua_DsdWrite( p, "}" );
}
void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
}
char * Dau_DsdDecompose( word * pTruth, int nVarsInit )
{ {
Dau_Dsd_t P, * p = &P; Dau_Dsd_t P, * p = &P;
int nVars, pVars[6]; int nVars, pVars[16];
Dua_DsdInit( p, nVarsInit ); Dua_DsdInit( p, nVarsInit );
if ( t == 0 ) if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
Dua_DsdWrite( p, "0" ); Dua_DsdWrite( p, "0" );
else if ( ~t == 0 ) else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
Dua_DsdWrite( p, "1" ); Dua_DsdWrite( p, "1" );
else else
{ {
nVars = Dua_DsdMinBase( t, nVarsInit, pVars ); nVars = Dua_DsdMinBase( pTruth, nVarsInit, pVars );
assert( nVars > 0 && nVars < 6 ); assert( nVars > 0 && nVars < 6 );
if ( nVars == 1 ) if ( nVars == 1 )
{ Dua_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) );
Dua_DsdWriteInv( p, (int)(t & 1) ); else if ( nVars <= 6 )
Dua_DsdWriteVar( p, pVars[0] ); Dau_Dsd6DecomposeInternal( p, pTruth[0], pVars, nVars );
}
else else
Dau_DsdDecomposeInternal( p, t, pVars, nVars ); Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars );
} }
Dua_DsdWriteStop( p ); Dua_DsdWriteStop( p );
return p->pOutput; return p->pOutput;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment