Commit ad8a3f51 by Alan Mishchenko

New AIG optimization package.

parent 6de48109
......@@ -18,7 +18,7 @@ MODULES := \
src/misc/mem src/misc/bar src/misc/bbl \
src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau \
src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
......
......@@ -1962,6 +1962,26 @@ SOURCE=.\src\opt\nwk\nwkTiming.c
SOURCE=.\src\opt\nwk\nwkUtil.c
# End Source File
# End Group
# Begin Group "dau"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\dau\dau.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\dau\dauCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\dau\dauDsd.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\dau\dauInt.h
# End Source File
# End Group
# End Group
# Begin Group "map"
......
......@@ -823,6 +823,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
extern void Dar_LibStart();
Dar_LibStart();
}
{
extern void Dau_DsdTest();
Dau_DsdTest();
}
}
/**Function*************************************************************
......
......@@ -202,6 +202,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
for ( i = 0; i < p->nFuncs; i++ )
{
extern void Dau_DsdTestOne( word t, int i );
assert( p->nVars == 6 );
Dau_DsdTestOne( *p->pFuncs[i], i );
if ( fVerbose )
printf( "%7d : ", i );
if ( fVerbose )
......
/**CFile****************************************************************
FileName [dau.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dau.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dauInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
/**CFile****************************************************************
FileName [dauCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis [Disjoint-support decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dauCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dauInt.h"
#include "aig/aig/aig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// parameter structure
typedef struct Xyz_ParTry_t_ Xyz_ParTry_t;
struct Xyz_ParTry_t_
{
int Par;
};
// operation manager
typedef struct Xyz_ManTry_t_ Xyz_ManTry_t;
struct Xyz_ManTry_t_
{
Xyz_ParTry_t * pPar; // parameters
Aig_Man_t * pAig; // user's AIG
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Xyz_ManTry_t * Xyz_ManTryAlloc( Aig_Man_t * pAig, Xyz_ParTry_t * pPar )
{
Xyz_ManTry_t * p;
p = ABC_CALLOC( Xyz_ManTry_t, 1 );
p->pAig = pAig;
p->pPar = pPar;
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Xyz_ManTryFree( Xyz_ManTry_t * p )
{
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Xyz_ManPerform( Aig_Man_t * pAig, Xyz_ParTry_t * pPar )
{
Xyz_ManTry_t * p;
int RetValue;
p = Xyz_ManTryAlloc( pAig, pPar );
RetValue = 1;
Xyz_ManTryFree( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
/**CFile****************************************************************
FileName [dauDsd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis [Disjoint-support decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dauDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dauInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static word s_Truth6[6] =
{
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
// ! = not; (a + b) = a and b; [a + b] = a xor b; <abc> = ITE( a, b, c )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes truth table for the DSD formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Dau_DsdFindMatch( char * p )
{
int Counter = 0;
assert( *p == '(' || *p == '[' || *p == '<' );
while ( *p )
{
if ( *p == '(' || *p == '[' || *p == '<' )
Counter++;
else if ( *p == ')' || *p == ']' || *p == '>' )
Counter--;
if ( Counter == 0 )
return p;
p++;
}
return NULL;
}
word Dau_DsdToTruth_rec( char ** p )
{
int fCompl = 0;
if ( **p == '!' )
(*p)++, fCompl = 1;
if ( **p >= 'a' && **p <= 'f' )
return fCompl ? ~s_Truth6[**p - 'a'] : s_Truth6[**p - 'a'];
if ( **p == '(' || **p == '[' || **p == '<' )
{
word Res = 0;
char * q = Dau_DsdFindMatch( *p );
assert( q != NULL );
assert( (**p == '(') == (*q == ')') );
assert( (**p == '[') == (*q == ']') );
assert( (**p == '<') == (*q == '>') );
if ( **p == '(' ) // and/or
{
Res = ~0;
for ( (*p)++; *p < q; (*p)++ )
Res &= Dau_DsdToTruth_rec( p );
}
else if ( **p == '[' ) // xor
{
Res = 0;
for ( (*p)++; *p < q; (*p)++ )
Res ^= Dau_DsdToTruth_rec( p );
}
else if ( **p == '<' ) // mux
{
word Temp[3], * pTemp = Temp;
for ( (*p)++; *p < q; (*p)++ )
*pTemp++ = Dau_DsdToTruth_rec( p );
assert( pTemp == Temp + 3 );
Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]);
}
else assert( 0 );
assert( *p == q );
return fCompl ? ~Res : Res;
}
assert( 0 );
return 0;
}
word Dau_DsdToTruth( char * p )
{
word Res;
if ( *p == '0' )
Res = 0;
else if ( *p == '1' )
Res = ~0;
else
Res = Dau_DsdToTruth_rec( &p );
assert( *++p == 0 );
return Res;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdTest2()
{
// char * p = Abc_UtilStrsav( "!(ab!(de[cf]))" );
char * p = Abc_UtilStrsav( "!(a![d<ecf>]b)" );
word t = Dau_DsdToTruth( p );
}
/**Function*************************************************************
Synopsis [Performs DSD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline word Dau_DsdCof0( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
return (t &~s_Truth6[iVar]) | ((t &~s_Truth6[iVar]) << (1<<iVar));
}
static inline word Dau_DsdCof1( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
return (t & s_Truth6[iVar]) | ((t & s_Truth6[iVar]) >> (1<<iVar));
}
static inline word Dau_DsdVarPres( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
return (t & s_Truth6[iVar]) != ((t << (1<<iVar)) & s_Truth6[iVar]);
}
static inline int Dau_DsdPerformReplace2( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
{
char * pTemp, * pStop = pTemp = pBuffer + Pos;
int i, Len = strlen(pNext);
do
{
for ( pTemp = pBuffer + Pos - 1; pTemp >= pBuffer + PosStart; pTemp[Len-1] = *pTemp, pTemp-- )
if ( pTemp < pStop && *pTemp == (char)Symb )
{
for ( i = 0; i < Len; i++ )
pTemp[i] = pNext[i];
Pos += Len - 1;
pStop = pTemp;
// check if there is symbol left
for ( ; pTemp >= pBuffer + PosStart; pTemp-- )
if ( *pTemp == (char)Symb )
break;
break;
}
} while ( pTemp >= pBuffer + PosStart );
return Pos;
}
static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
{
static char pTemp[1000];
char * pCur = pTemp;
int i, k, RetValue;
for ( i = PosStart; i < Pos; i++ )
if ( pBuffer[i] != Symb )
*pCur++ = pBuffer[i];
else
for ( k = 0; pNext[k]; k++ )
*pCur++ = pNext[k];
RetValue = PosStart + (pCur - pTemp);
for ( i = PosStart; i < RetValue; i++ )
pBuffer[i] = pTemp[i-PosStart];
return RetValue;
}
int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars )
{
char pNest[10];
word Cof0[6], Cof1[6], Cof[4];
int pVarsNew[6], nVarsNew, PosStart;
int v, u, vBest, CountBest;
// copy remaining variables
nVarsNew = 0;
for ( v = 0; v < nVars; v++ )
if ( Dau_DsdVarPres( t, pVars[v] ) )
pVarsNew[ nVarsNew++ ] = pVars[v];
assert( nVarsNew > 0 );
if ( nVarsNew == 1 )
{
if ( t == s_Truth6[ pVarsNew[0] ] )
{
pBuffer[Pos++] = 'a' + pVarsNew[0];
return Pos;
}
if ( t == ~s_Truth6[ pVarsNew[0] ] )
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[0];
return Pos;
}
assert( 0 );
return Pos;
}
for ( v = 0; v < nVarsNew; v++ )
{
Cof0[v] = Dau_DsdCof0( t, pVarsNew[v] );
Cof1[v] = Dau_DsdCof1( t, pVarsNew[v] );
assert( Cof0[v] != Cof1[v] );
if ( Cof0[v] == 0 )
{
pBuffer[Pos++] = '(';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( Cof1[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof0[v] == ~0 )
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = '(';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( ~Cof1[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof1[v] == 0 )
{
pBuffer[Pos++] = '(';
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof1[v] == ~0 )
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = '(';
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( ~Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof0[v] == ~Cof1[v] )
{
pBuffer[Pos++] = '[';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ']';
return Pos;
}
}
for ( v = 0; v < nVarsNew; v++ )
for ( u = v+1; u < nVarsNew; u++ )
{
Cof[0] = Dau_DsdCof0( Cof0[v], pVarsNew[u] );
Cof[1] = Dau_DsdCof1( Cof0[v], pVarsNew[u] );
Cof[2] = Dau_DsdCof0( Cof1[v], pVarsNew[u] );
Cof[3] = Dau_DsdCof1( Cof1[v], pVarsNew[u] );
if ( Cof[0] == Cof[1] && Cof[0] == Cof[2] ) // vu
{
PosStart = Pos;
sprintf( pNest, "(%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[3]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[0] == Cof[1] && Cof[0] == Cof[3] ) // v!u
{
PosStart = Pos;
sprintf( pNest, "(%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[2]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[0] == Cof[2] && Cof[0] == Cof[3] ) // !vu
{
PosStart = Pos;
sprintf( pNest, "(!%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[1]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[1] == Cof[2] && Cof[1] == Cof[3] ) // !v!u
{
PosStart = Pos;
sprintf( pNest, "(!%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[0]) | (~s_Truth6[pVarsNew[u]] & Cof[1]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[0] == Cof[3] && Cof[1] == Cof[2] ) // v+u
{
PosStart = Pos;
sprintf( pNest, "[%c%c]", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[1]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
}
// look for MUX
vBest = -1;
CountBest = 10;
for ( v = 0; v < nVarsNew; v++ )
{
int CountCur = 0;
for ( u = 0; u < nVarsNew; u++ )
if ( u != v && Dau_DsdVarPres(Cof0[v], pVarsNew[u]) && Dau_DsdVarPres(Cof1[v], pVarsNew[u]) )
CountCur++;
if ( CountBest > CountCur )
{
CountBest = CountCur;
vBest = v;
}
if ( CountCur == 0 )
break;
}
// perform MUX decomposition
pBuffer[Pos++] = '<';
pBuffer[Pos++] = 'a' + pVarsNew[vBest];
Pos = Dau_DsdPerform_rec( Cof1[vBest], pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( Cof0[vBest], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = '>';
return Pos;
}
char * Dau_DsdPerform( word t )
{
static char pBuffer[1000];
int pVarsNew[6] = {0, 1, 2, 3, 4, 5};
int Pos = 0;
if ( t == 0 )
pBuffer[Pos++] = '0';
else if ( t == ~0 )
pBuffer[Pos++] = '1';
else
Pos = Dau_DsdPerform_rec( t, pBuffer, Pos, pVarsNew, 6 );
pBuffer[Pos++] = 0;
return pBuffer;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdTest()
{
// word t = s_Truth6[0] & s_Truth6[1] & s_Truth6[2];
// word t = ~s_Truth6[0] | (s_Truth6[1] ^ ~s_Truth6[2]);
// word t = (s_Truth6[1] & s_Truth6[2]) | (s_Truth6[0] & s_Truth6[3]);
// word t = (~s_Truth6[1] & ~s_Truth6[2]) | (s_Truth6[0] ^ s_Truth6[3]);
// word t = ((~s_Truth6[1] & ~s_Truth6[2]) | (s_Truth6[0] ^ s_Truth6[3])) ^ s_Truth6[5];
// word t = ((s_Truth6[1] & ~s_Truth6[2]) ^ (s_Truth6[0] & s_Truth6[3])) & s_Truth6[5];
// word t = (~(~s_Truth6[0] & ~s_Truth6[4]) & s_Truth6[2]) | (~s_Truth6[1] & ~s_Truth6[0] & ~s_Truth6[4]);
// word t = 0x0000000000005F3F;
// word t = 0xF3F5030503050305;
// word t = (s_Truth6[0] & s_Truth6[1] & (s_Truth6[2] ^ s_Truth6[4])) | (~s_Truth6[0] & ~s_Truth6[1] & ~(s_Truth6[2] ^ s_Truth6[4]));
// word t = 0x05050500f5f5f5f3;
word t = 0xFFAF00ACFFAF00AC;
char * p = Dau_DsdPerform( t );
word t2 = Dau_DsdToTruth( p );
if ( t != t2 )
printf( "Verification failed.\n" );
}
void Dau_DsdTestOne( word t, int i )
{
char * p;
word t2, t1;
// t = t & 0xFFFFFFFF;
// t |= (t << 32);
p = Dau_DsdPerform( t );
return;
t2 = Dau_DsdToTruth( p );
if ( t != t2 )
{
printf( "%8d : ", i );
printf( "%30s ", p );
// printf( "Verification failed. " );
Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
/*
printf( " " );
t1 = Dau_DsdCof1(t, 3);
Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 );
printf( " " );
t1 = Dau_DsdCof0(t, 3);
Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 );
*/
printf( " " );
Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 );
printf( "\n" );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
/**CFile****************************************************************
FileName [dauInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis [Interal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dauInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__DAU_INT__h
#define ABC__DAU_INT__h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "misc/vec/vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== zzz.c ==========================================================*/
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
SRC += src/opt/dau/dau.c \
src/opt/dau/daCore.c \
src/opt/dau/daDsd.c
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