summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/dau/dauNpn2.c615
1 files changed, 594 insertions, 21 deletions
diff --git a/src/opt/dau/dauNpn2.c b/src/opt/dau/dauNpn2.c
index bca65ad0..cf6a4f60 100644
--- a/src/opt/dau/dauNpn2.c
+++ b/src/opt/dau/dauNpn2.c
@@ -1,26 +1,27 @@
/**CFile****************************************************************
- FileName [dau.c]
+ FileName [dauNpn2.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [DAG-aware unmapping.]
+ PackageName [Functional enumeration.]
- Synopsis []
+ Synopsis [Functional enumeration.]
- Author [Alan Mishchenko]
+ Author [Siang-Yun Lee]
- Affiliation [UC Berkeley]
+ Affiliation [National Taiwan University]
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: dau.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: dauNpn2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
+#include "aig/gia/gia.h"
ABC_NAMESPACE_IMPL_START
@@ -65,6 +66,239 @@ struct Dtt_Man_t_
/**Function*************************************************************
+ Synopsis [Parse one formula into a truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Dau_ParseFormulaEndToken( char * pForm )
+{
+ int Counter = 0;
+ char * pThis;
+ for ( pThis = pForm; *pThis; pThis++ )
+ {
+ if ( *pThis == '~' )
+ continue;
+ if ( *pThis == '(' )
+ Counter++;
+ else if ( *pThis == ')' )
+ Counter--;
+ if ( Counter == 0 )
+ return pThis + 1;
+ }
+ assert( 0 );
+ return NULL;
+}
+word Dau_ParseFormula_rec( char * pBeg, char * pEnd )
+{
+ word iFans[2], Res, Oper = -1;
+ char * pEndNew;
+ int fCompl = 0;
+ while ( pBeg[0] == '~' )
+ {
+ pBeg++;
+ fCompl ^= 1;
+ }
+ if ( pBeg + 1 == pEnd )
+ {
+ if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' )
+ return fCompl ? ~s_Truths6[pBeg[0] - 'a'] : s_Truths6[pBeg[0] - 'a'];
+ assert( 0 );
+ return -1;
+ }
+ if ( pBeg[0] == '(' )
+ {
+ pEndNew = Dau_ParseFormulaEndToken( pBeg );
+ if ( pEndNew == pEnd )
+ {
+ assert( pBeg[0] == '(' );
+ assert( pBeg[pEnd-pBeg-1] == ')' );
+ Res = Dau_ParseFormula_rec( pBeg + 1, pEnd - 1 );
+ return fCompl ? ~Res : Res;
+ }
+ }
+ // get first part
+ pEndNew = Dau_ParseFormulaEndToken( pBeg );
+ iFans[0] = Dau_ParseFormula_rec( pBeg, pEndNew );
+ iFans[0] = fCompl ? ~iFans[0] : iFans[0];
+ Oper = pEndNew[0];
+ // get second part
+ pBeg = pEndNew + 1;
+ pEndNew = Dau_ParseFormulaEndToken( pBeg );
+ iFans[1] = Dau_ParseFormula_rec( pBeg, pEndNew );
+ // derive the formula
+ if ( Oper == '&' )
+ return iFans[0] & iFans[1];
+ if ( Oper == '^' )
+ return iFans[0] ^ iFans[1];
+ assert( 0 );
+ return -1;
+}
+word Dau_ParseFormula( char * p )
+{
+ return Dau_ParseFormula_rec( p, p + strlen(p) );
+}
+void Dau_ParseFormulaTest()
+{
+ char * p = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))";
+ word r = ABC_CONST(0x037d037d037d037d);
+ word t = Dau_ParseFormula( p );
+ assert( r == t );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Parse one formula into a AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dau_ParseFormulaAig_rec( Gia_Man_t * p, char * pBeg, char * pEnd )
+{
+ int iFans[2], Res, Oper = -1;
+ char * pEndNew;
+ int fCompl = 0;
+ while ( pBeg[0] == '~' )
+ {
+ pBeg++;
+ fCompl ^= 1;
+ }
+ if ( pBeg + 1 == pEnd )
+ {
+ if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' )
+ return Abc_Var2Lit( 1 + pBeg[0] - 'a', fCompl );
+ assert( 0 );
+ return -1;
+ }
+ if ( pBeg[0] == '(' )
+ {
+ pEndNew = Dau_ParseFormulaEndToken( pBeg );
+ if ( pEndNew == pEnd )
+ {
+ assert( pBeg[0] == '(' );
+ assert( pBeg[pEnd-pBeg-1] == ')' );
+ Res = Dau_ParseFormulaAig_rec( p, pBeg + 1, pEnd - 1 );
+ return Abc_LitNotCond( Res, fCompl );
+ }
+ }
+ // get first part
+ pEndNew = Dau_ParseFormulaEndToken( pBeg );
+ iFans[0] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew );
+ iFans[0] = Abc_LitNotCond( iFans[0], fCompl );
+ Oper = pEndNew[0];
+ // get second part
+ pBeg = pEndNew + 1;
+ pEndNew = Dau_ParseFormulaEndToken( pBeg );
+ iFans[1] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew );
+ // derive the formula
+ if ( Oper == '&' )
+ return Gia_ManHashAnd( p, iFans[0], iFans[1] );
+ if ( Oper == '^' )
+ return Gia_ManHashXor( p, iFans[0], iFans[1] );
+ assert( 0 );
+ return -1;
+}
+int Dau_ParseFormulaAig( Gia_Man_t * p, char * pStr )
+{
+ return Dau_ParseFormulaAig_rec( p, pStr, pStr + strlen(pStr) );
+}
+Gia_Man_t * Dau_ParseFormulaAigTest()
+{
+ int i;
+ char * pStr = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))";
+ Gia_Man_t * p = Gia_ManStart( 1000 );
+ p->pName = Abc_UtilStrsav( "func_enum_aig" );
+ Gia_ManHashAlloc( p );
+ for ( i = 0; i < 5; i++ )
+ Gia_ManAppendCi( p );
+ Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, pStr) );
+ return p;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Verify one file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_VerifyFile( char * pFileName )
+{
+ char Buffer[1000];
+ unsigned uTruth, uTruth2;
+ int nFails = 0, nLines = 0;
+ FILE * pFile = fopen( pFileName, "rb" );
+ while ( fgets( Buffer, 1000, pFile ) )
+ {
+ if ( Buffer[strlen(Buffer)-1] == '\n' )
+ Buffer[strlen(Buffer)-1] = 0;
+ if ( Buffer[strlen(Buffer)-1] == '\r' )
+ Buffer[strlen(Buffer)-1] = 0;
+ Extra_ReadHexadecimal( &uTruth2, Buffer, 5 );
+ uTruth = (unsigned)Dau_ParseFormula( Buffer + 11 );
+ if ( uTruth != uTruth2 )
+ printf( "Verification failed in line %d: %s\n", nLines, Buffer ), nFails++;
+ nLines++;
+ }
+ printf( "Verification succeeded for %d functions and failed for %d functions.\n", nLines-nFails, nFails );
+}
+void Dau_VerifyFileTest()
+{
+ char * pFileName = "lib4var.txt";
+ Dau_VerifyFile( pFileName );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Create AIG for one file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Dau_ConstructAigFromFile( char * pFileName )
+{
+ char Buffer[1000];
+ int i, nLines = 0;
+ FILE * pFile = fopen( pFileName, "rb" );
+ Gia_Man_t * p = Gia_ManStart( 1000 );
+ p->pName = Abc_UtilStrsav( "func_enum_aig" );
+ Gia_ManHashAlloc( p );
+ for ( i = 0; i < 5; i++ )
+ Gia_ManAppendCi( p );
+ while ( fgets( Buffer, 1000, pFile ) )
+ {
+ if ( Buffer[strlen(Buffer)-1] == '\n' )
+ Buffer[strlen(Buffer)-1] = 0;
+ if ( Buffer[strlen(Buffer)-1] == '\r' )
+ Buffer[strlen(Buffer)-1] = 0;
+ Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, Buffer + 11) );
+ nLines++;
+ }
+ printf( "Finish constructing AIG for %d structures.\n", nLines );
+ return p;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -282,10 +516,23 @@ Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
SeeAlso []
***********************************************************************/
-static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun )
+static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun, int n )
{
+ unsigned Class;
tFun = tFun & p->CmpMask ? ~tFun : tFun;
- return Abc_TtGetBit( p->pPres, tFun & p->FunMask );
+ //return Abc_TtGetBit( p->pPres, tFun & p->FunMask );
+ if ( !Abc_TtGetBit( p->pPres, tFun & p->FunMask ) ) return 0;
+ if ( p->pTable == NULL ) return 1;
+
+ Class = p->pTable[tFun & p->FunMask];
+ assert( Class < (unsigned)p->nClasses );
+ if ( p->pNodes[Class] < n )
+ return 1;
+ assert( p->pNodes[Class] == n );
+ if ( p->pVisited[Class] )
+ return 1;
+
+ return 0;
}
static inline void Dtt_ManSetFun( Dtt_Man_t * p, unsigned tFun )
{
@@ -313,13 +560,13 @@ void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, uns
Vec_IntForEachEntry( vFuncs, Min, i )
Dtt_ManSetFun( p, Min );
assert( nNodes < 32 );
- p->Counts[nNodes]++;
+ p->Counts[nNodes]++;
if ( p->pTable == NULL )
return;
Truth = Truth & p->CmpMask ? ~Truth : Truth;
Truth &= p->FunMask;
- assert( p->pNodes[p->pTable[Truth]] == 0 );
+ //assert( p->pNodes[p->pTable[Truth]] == 0 );
p->pNodes[p->pTable[Truth]] = n;
}
@@ -397,7 +644,7 @@ void Dtt_PrintMulti1( Dtt_Man_t * p )
}
void Dtt_PrintMulti( Dtt_Man_t * p )
{
- int n, Counts[13][11] = {{0}};
+ int n, Counts[13][15] = {{0}};
for ( n = 0; n < 13; n++ )
{
int i, Total = 0, Count = 0;
@@ -405,7 +652,7 @@ void Dtt_PrintMulti( Dtt_Man_t * p )
if ( p->pNodes[i] == n )
{
int Log = Abc_Base2Log(p->pTimes[i]);
- assert( Log < 11 );
+ assert( Log < 15 );
if ( p->pTimes[i] < 2 )
Counts[n][0]++;
else
@@ -418,7 +665,7 @@ void Dtt_PrintMulti( Dtt_Man_t * p )
printf( "n=%2d : ", n );
printf( "All = %7d ", Count );
printf( "Ave = %6.2f ", 1.0*Total/Count );
- for ( i = 0; i < 11; i++ )
+ for ( i = 0; i < 15; i++ )
if ( Counts[n][i] )
printf( "%6d", Counts[n][i] );
else
@@ -426,10 +673,334 @@ void Dtt_PrintMulti( Dtt_Man_t * p )
printf( "\n" );
}
}
-void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose )
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+typedef struct Dtt_FunImpl_t_ Dtt_FunImpl_t;
+struct Dtt_FunImpl_t_
+{
+ int Type;
+ int NP1; // 4 bits for an input (NPPP)
+ int FI1; // the id (in vLibFun) of the first fanin function
+ int NP2;
+ int FI2; // the id (in vLibFun) of the second fanin function
+};
+
+void Dtt_FunImplFI2Str( int FI, int NP, Vec_Int_t* vLibFun, char* str )
+{
+ int i, P[5], N[5];
+ for ( i = 0; i < 5; i++ )
+ {
+ P[i] = NP & 0x7;
+ NP = NP >> 3;
+ N[i] = NP & 0x1;
+ NP = NP >> 1 ;
+ }
+ sprintf( str, "[%08x(%03d),%d%d%d%d%d,%d%d%d%d%d]", Vec_IntEntry( vLibFun, FI ), FI, P[0], P[1], P[2], P[3], P[4], N[0], N[1], N[2], N[3], N[4] );
+}
+
+void Dtt_FunImpl2Str( int Type, char* sFI1, char* sFI2, char* str )
+{
+ // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
+ // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
+ switch( Type )
+ {
+ case 0: sprintf( str, "(%s&%s)", sFI1, sFI2 ); break;
+ case 1: sprintf( str, "(~%s&%s)", sFI1, sFI2 ); break;
+ case 2: sprintf( str, "(%s&~%s)", sFI1, sFI2 ); break;
+ case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break;
+ case 4: sprintf( str, "(%s^%s)", sFI1, sFI2 ); break;
+ case 5: sprintf( str, "~(%s&%s)", sFI1, sFI2 ); break;
+ case 6: sprintf( str, "~(~%s&%s)", sFI1, sFI2 ); break;
+ case 7: sprintf( str, "~(%s&~%s)", sFI1, sFI2 ); break;
+ case 8: sprintf( str, "(~%s&~%s)", sFI1, sFI2 ); break;
+ case 9: sprintf( str, "~(%s^%s)", sFI1, sFI2 ); break;
+ /*case 0: sprintf( str, " ( %s& %s)", sFI1, sFI2 ); break;
+ case 1: sprintf( str, " (~%s& %s)", sFI1, sFI2 ); break;
+ case 2: sprintf( str, " ( %s&~%s)", sFI1, sFI2 ); break;
+ case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break;
+ case 4: sprintf( str, " ( %s^ %s)", sFI1, sFI2 ); break;
+ case 5: sprintf( str, "~( %s& %s)", sFI1, sFI2 ); break;
+ case 6: sprintf( str, "~(~%s& %s)", sFI1, sFI2 ); break;
+ case 7: sprintf( str, "~( %s&~%s)", sFI1, sFI2 ); break;
+ case 8: sprintf( str, " (~%s&~%s)", sFI1, sFI2 ); break;
+ case 9: sprintf( str, "~( %s^ %s)", sFI1, sFI2 ); break;*/
+ }
+}
+
+int Dtt_ComposeNP( int NP1, int NP2 )
+{
+ // NP[i] = NP1[NP2[i]]
+ int NP = 0, i;
+ for ( i = 0; i < 5; i++ )
+ {
+ NP |= ( ( NP1 >> ((NP2&0x7)<<2) ) & 0x7 ) << (i<<2); // P'[i] = P1[P2[i]]
+ NP |= ( ( NP1 >> ((NP2&0x7)<<2) ^ NP2 ) & 0x8 ) << (i<<2); // N'[i] = N1[P2[i]] ^ N2[i]
+ NP2 = NP2 >> 4;
+ }
+ return NP;
+}
+
+void Dtt_MakePI( int NP, char* str )
+{
+ // apply P'[i], find the i s.t. P'[i]==0, correspond to N'[i]
+ int i;
+ for ( i = 0; i < 5; i++ )
+ {
+ if ( ( NP & 0x7 ) == 0 )
+ {
+ if ( NP & 0x8 )
+ sprintf( str, "~%c", 'a'+i );
+ else
+ sprintf( str, "%c", 'a'+i );
+ return;
+ }
+ NP = NP >> 4;
+ }
+ assert(0);
+}
+
+void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile );
+void Dtt_MakeFormulaFI2( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sFI1, char* sF, int fPrint, FILE* pFile )
+{
+ int j;
+ Dtt_FunImpl_t* pImpl2;
+ char sFI2[100]; sprintf( sFI2, "" );
+
+ if ( pFun->FI2 == 0 ) // PI
+ {
+ Dtt_MakePI( Dtt_ComposeNP( pFun->NP2, NP ), sFI2 );
+ Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF );
+ if (fPrint)
+ fprintf(pFile, "%08x = %s\n", tFun, sF);
+ }
+ else
+ {
+ Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl2, j, pFun->FI2 )
+ {
+ Dtt_MakeFormula( tFun, pImpl2, vLibImpl, Dtt_ComposeNP( pFun->NP2, NP ), sFI2, 0, pFile );
+ Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF );
+ if (fPrint)
+ fprintf(pFile, "%08x = %s\n", tFun, sF);
+ }
+ }
+}
+
+void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile )
+{
+ int j;
+ Dtt_FunImpl_t* pImpl1;
+ char sFI1[100], sCopy[100]; sprintf( sFI1, "" );
+
+ if ( pFun->FI1 == 0 ) // PI
+ {
+ Dtt_MakePI( Dtt_ComposeNP( pFun->NP1, NP ), sFI1 );
+ sprintf( sCopy, "%s", sF );
+ Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile );
+ }
+ else
+ {
+ Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl1, j, pFun->FI1 )
+ {
+ Dtt_MakeFormula( tFun, pImpl1, vLibImpl, Dtt_ComposeNP( pFun->NP1, NP ), sFI1, 0, pFile );
+ sprintf( sCopy, "%s", sF );
+ Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile );
+ }
+ }
+}
+
+void Dtt_ProcessType( int* Type, int nFanin )
+{
+ // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
+ // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
+ if ( nFanin == 3 ) // for output negation
+ *Type += (*Type<5)? 5: -5;
+ else if ( *Type == 0 || *Type == 5 )
+ *Type += nFanin;
+ else if ( *Type == nFanin ) // 1,1 ; 2,2
+ *Type = 0;
+ else if ( *Type + nFanin == 3 ) // 1,2 ; 2,1
+ *Type = 8;
+ else if ( *Type == 3 )
+ *Type = (nFanin==1)? 7: 6;
+ else if ( *Type == 4 )
+ *Type = 9;
+ else if ( *Type == nFanin+5 ) // 6,1 ; 7,2
+ *Type = 5;
+ else if ( *Type + nFanin == 8 ) // 6,2 ; 7,1
+ *Type = 3;
+ else if ( *Type == 8 )
+ *Type = (nFanin==1)? 2: 1;
+ else if ( *Type == 9 )
+ *Type = 4;
+ else
+ assert( 0 );
+}
+
+int Dtt_Check( unsigned tFun, unsigned tGoal, unsigned tCur, int* pType )
+{
+ if (!tGoal) //for Fanin2 and output
+ return ( tCur == tFun || ~tCur == tFun );
+ //for Fanin1: check if tFun(Type)tCur==tGoal
+ switch (*pType)
+ {
+ // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
+ // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
+ case 0: case 5: if ( (~tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
+ else return ( (tCur & tFun) == tGoal );
+ case 1: case 6: if ( (tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
+ else return ( (~tCur & tFun) == tGoal );
+ case 2: case 7: if ( (~tCur & ~tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
+ else return ( (tCur & ~tFun) == tGoal );
+ case 3: case 8: if ( (~tCur | tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
+ else return ( (tCur | tFun) == tGoal );
+ case 4: case 9: if ( (~tCur ^ tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
+ else return ( (tCur ^ tFun) == tGoal );
+ default: assert(0);
+ }
+ return -1;
+}
+
+void Dtt_FindNP( Dtt_Man_t * p, unsigned tFun, unsigned tGoal, unsigned tNpn, int * NP, int* pType, int NPout )
+{
+ int i, k, j;
+ int P[5] = { 0, 1, 2, 3, 4 };
+ int N[5] = { 0, 0, 0, 0, 0 };
+ int temp;
+
+ word tCur = ((word)tNpn << 32) | (word)tNpn;
+ for ( i = 0; i < p->nPerms; i++ )
+ {
+ for ( k = 0; k < p->nComps; k++ )
+ {
+ if ( Dtt_Check( tFun, tGoal, (unsigned)tCur, pType ))
+ {
+ if ( !tGoal && ( tFun == (unsigned)~tCur ) ) // !tGoal: not FI1
+ {
+ if (!NPout) Dtt_ProcessType( pType, 3 );
+ else Dtt_ProcessType( pType, 2 );
+ }
+ *NP = 0;
+ if (!NPout)
+ {
+ for ( j = 0; j < 5; j++ )
+ *NP |= ( ( ( N[j] & 0x1 ) << 3 ) | ( P[j] & 0x7 ) ) << (j<<2) ;
+ }
+ else
+ {
+ for ( j = 0; j < 5; j++ )
+ {
+ *NP |= P[NPout&0x7] << (j<<2); // P'[j] = P[Pout[j]]
+ *NP |= ( N[NPout&0x7] ^ ( (NPout>>3) & 0x1 )) << (j<<2) << 3; // N'[i] = N1[P2[i]] ^ N2[i]
+ NPout = NPout >> 4;
+ }
+ }
+
+ return;
+ }
+ tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
+ N[p->pComps[k]] ^= 0x1;
+ }
+ tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] );
+ temp = P[p->pPerms[i]]; P[p->pPerms[i]] = P[p->pPerms[i]+1]; P[p->pPerms[i]+1] = temp;
+ }
+ assert(0);
+}
+
+void Dtt_DumpLibrary( Dtt_Man_t * p )
+{
+ FILE * pFile;
+ char FileName[100], str[100], sFI1[50], sFI2[50];
+ int i, j, Entry, fRepeat;
+ Dtt_FunImpl_t * pFun, * pFun2;
+ Vec_Int_t * vLibFun = Vec_IntDup( p->vTruthNpns ); // none-duplicating vector of NPN representitives
+ Vec_Vec_t * vLibImpl;
+ Vec_IntUniqify( vLibFun );
+ vLibImpl = Vec_VecStart( Vec_IntSize( vLibFun ) );
+ Vec_IntForEachEntry( p->vTruths, Entry, i )
+ {
+ int NP, Fanin2, Fanin1Npn, Fanin2Npn;
+ if (i<2) continue; // skip const 0
+ pFun = ABC_CALLOC( Dtt_FunImpl_t, 1 );
+ pFun->Type = (int)( 0x7 & Vec_IntEntry(p->vConfigs, i) );
+ //word Fanin1 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2 ) );
+ Fanin2 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2+1 ) );
+ Fanin1Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2 ) );
+ Fanin2Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2+1 ) );
+ pFun->FI1 = Vec_IntFind( vLibFun, Fanin1Npn );
+ pFun->FI2 = Vec_IntFind( vLibFun, Fanin2Npn );
+
+ fRepeat = 0;
+ Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun2, j, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ) )
+ {
+ if ( ( pFun2->FI1 == pFun->FI1 && pFun2->FI2 == pFun->FI2 ) || ( pFun2->FI2 == pFun->FI1 && pFun2->FI1 == pFun->FI2 ) )
+ {
+ fRepeat = 1;
+ break;
+ }
+ }
+ if (fRepeat)
+ {
+ ABC_FREE( pFun );
+ continue;
+ }
+
+ Dtt_FindNP( p, Vec_IntEntry( p->vTruthNpns, i ), 0, Entry, &NP, &(pFun->Type), 0 ); //out: tGoal=0, NPout=0
+ Dtt_FindNP( p, Fanin2, Entry, Fanin1Npn, &(pFun->NP1), &(pFun->Type), NP ); //FI1
+ Dtt_FindNP( p, Fanin2, 0, Fanin2Npn, &(pFun->NP2), &(pFun->Type), NP ); //FI2: tGoal=0
+
+ Vec_VecPush( vLibImpl, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ), pFun );
+ }
+
+ // print to file
+ sprintf( FileName, "lib%dvar.txt", p->nVars );
+ pFile = fopen( FileName, "wb" );
+
+ if (0)
+ Vec_IntForEachEntry( vLibFun, Entry, i )
+ {
+ if (!Entry) continue; // skip const 0
+ fprintf( pFile, "%08x: ", (unsigned)Entry );
+ Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i )
+ {
+ Dtt_FunImplFI2Str( pFun->FI1, pFun->NP1, vLibFun, sFI1 );
+ Dtt_FunImplFI2Str( pFun->FI2, pFun->NP2, vLibFun, sFI2 );
+ Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, str );
+ fprintf( pFile, "%s, ", str );
+ }
+ fprintf( pFile, "\n" );
+ }
+
+ // formula format
+ Vec_IntForEachEntry( vLibFun, Entry, i )
+ {
+ if ( i<2 ) continue; // skip const 0 and buffer
+ Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i )
+ {
+ sprintf( str, "" );
+ Dtt_MakeFormula( (unsigned)Entry, pFun, vLibImpl, (4<<16)+(3<<12)+(2<<8)+(1<<4), str, 1, pFile );
+ }
+ }
+
+ fclose( pFile );
+ printf( "Dumped file \"%s\". \n", FileName );
+ fflush( stdout );
+}
+
+void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose, int fDump )
{
abctime clk = Abc_Clock(); word nSteps = 0, nMultis = 0;
Dtt_Man_t * p = Dtt_ManAlloc( nVars, fMulti ); int n, i, j;
+
// constant zero class
Vec_IntPushTwo( p->vFanins, 0, 0 );
Vec_IntPush( p->vTruths, 0 );
@@ -466,15 +1037,15 @@ void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerb
unsigned Truth, TruthJ = Vec_IntEntry(p->vTruths, EntryJ);
Vec_IntForEachEntry( vFuns, Truth, k )
{
- if ( !Dtt_ManGetFun(p, TruthJ & Truth) )
+ if ( !Dtt_ManGetFun(p, TruthJ & Truth, n) )
Dtt_ManAddFunction( p, n, EntryI, EntryJ, 0, TruthJ & Truth );
- if ( !Dtt_ManGetFun(p, TruthJ & ~Truth) )
+ if ( !Dtt_ManGetFun(p, TruthJ & ~Truth, n) )
Dtt_ManAddFunction( p, n, EntryI, EntryJ, 1, TruthJ & ~Truth );
- if ( !Dtt_ManGetFun(p, ~TruthJ & Truth) )
+ if ( !Dtt_ManGetFun(p, ~TruthJ & Truth, n) )
Dtt_ManAddFunction( p, n, EntryI, EntryJ, 2, ~TruthJ & Truth );
- if ( !Dtt_ManGetFun(p, TruthJ | Truth) )
+ if ( !Dtt_ManGetFun(p, TruthJ | Truth, n) )
Dtt_ManAddFunction( p, n, EntryI, EntryJ, 3, TruthJ | Truth );
- if ( !Dtt_ManGetFun(p, TruthJ ^ Truth) )
+ if ( !Dtt_ManGetFun(p, TruthJ ^ Truth, n) )
Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4, TruthJ ^ Truth );
nSteps += 5;
@@ -494,8 +1065,10 @@ void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerb
}
if ( fDelay )
Dtt_PrintDistrib( p );
- if ( p->pTable )
- Dtt_PrintMulti( p );
+ //if ( p->pTable )
+ //Dtt_PrintMulti( p );
+ if ( !fDelay && fDump )
+ Dtt_DumpLibrary( p );
Dtt_ManFree( p );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-16 05:28:27 +0000