luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improvements to the canonical form computation.

This commit is contained in:
Alan Mishchenko 2013-10-10 12:35:27 -07:00
parent 4c62b00288
commit 33695bed11
6 changed files with 133 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/aig/gia/giaJf.c
View File

@ -357,6 +357,16 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
p->clkStart = Abc_Clock();
return p;
}
void Jf_ManDumpTruthTables( Jf_Man_t * p )
{
char * pFileName = "truths.txt";
FILE * pFile = fopen( pFileName, "wb" );
Vec_MemDump( pFile, p->vTtMem );
fclose( pFile );
printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n",
Vec_MemEntryNum(p->vTtMem), p->pPars->nLutSize, pFileName,
17.0 * Vec_MemEntryNum(p->vTtMem) / (1 << 20) );
}
void Jf_ManFree( Jf_Man_t * p )
{
if ( p->pPars->fVerbose && p->pDsd )
@ -365,16 +375,6 @@ void Jf_ManFree( Jf_Man_t * p )
printf( "Unique truth tables = %d. Memory = %.2f MB\n", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) );
if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && p->pPars->fFuncDsd )
Jf_ManProfileClasses( p );
if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
{
char * pFileName = "truths.txt";
FILE * pFile = fopen( pFileName, "wb" );
Vec_MemDump( pFile, p->vTtMem );
fclose( pFile );
printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n",
Vec_MemEntryNum(p->vTtMem), p->pPars->nLutSize, pFileName,
17.0 * Vec_MemEntryNum(p->vTtMem) / (1 << 20) );
}
if ( p->pPars->fCoarsen )
Gia_ManCleanMark0( p->pGia );
ABC_FREE( p->pGia->pRefs );
@ -1689,6 +1689,8 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " );
Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " );
}
if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
Jf_ManDumpTruthTables( p );
if ( p->pPars->fPureAig )
pNew = Jf_ManDeriveGia(p);
else if ( p->pPars->fCutMin )

1
src/base/abci/abc.c
View File

@ -5388,6 +5388,7 @@ usage:
Abc_Print( -2, "\t 3: Jake's hybrid semi-canonical form (fast)\n" );
Abc_Print( -2, "\t 4: Jake's hybrid semi-canonical form (high-effort)\n" );
Abc_Print( -2, "\t 5: new fast hybrid semi-canonical form\n" );
Abc_Print( -2, "\t 6: new phase canonical form\n" );
Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
Abc_Print( -2, "\t-d : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" );
Abc_Print( -2, "\t-b : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );

22
src/base/abci/abcNpn.c
View File

@ -151,9 +151,12 @@ int Abc_TruthNpnCountUniqueSort( Abc_TtStore_t * p )
SeeAlso []
***********************************************************************/
void Abc_TruthNpnPrint( char * pCanonPerm, unsigned uCanonPhase, int nVars )
void Abc_TruthNpnPrint( char * pCanonPermInit, unsigned uCanonPhase, int nVars )
{
int i;
char pCanonPerm[16]; int i;
assert( nVars <= 16 );
for ( i = 0; i < nVars; i++ )
pCanonPerm[i] = pCanonPermInit ? pCanonPermInit[i] : 'a' + i;
printf( " %c = ( ", Abc_InfoHasBit(&uCanonPhase, nVars) ? 'Z':'z' );
for ( i = 0; i < nVars; i++ )
printf( "%c%s", pCanonPerm[i] + ('A'-'a') * Abc_InfoHasBit(&uCanonPhase, pCanonPerm[i]-'a'), i == nVars-1 ? "":"," );
@ -193,6 +196,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
pAlgoName = "Jake's hybrid good ";
else if ( NpnType == 5 )
pAlgoName = "new hybrid fast ";
else if ( NpnType == 6 )
pAlgoName = "new phase flipping ";
assert( p->nVars <= 16 );
if ( pAlgoName )
@ -273,6 +278,17 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
}
}
else if ( NpnType == 6 )
{
for ( i = 0; i < p->nFuncs; i++ )
{
if ( fVerbose )
printf( "%7d : ", i );
uCanonPhase = Abc_TtCanonicizePhase( p->pFuncs[i], p->nVars );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
}
}
else assert( 0 );
clk = Abc_Clock() - clk;
printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
@ -336,7 +352,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
{
if ( fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
if ( NpnType >= 0 && NpnType <= 5 )
if ( NpnType >= 0 && NpnType <= 6 )
Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
else
printf( "Unknown canonical form value (%d).\n", NpnType );

1
src/misc/util/utilTruth.h
View File

@ -1200,6 +1200,7 @@ static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pC
for ( i = 0; i < nVars; i++ )
if ( (uCanonPhase >> i) & 1 )
Abc_TtFlip( pTruth, nWords, i );
if ( pCanonPerm )
for ( i = 0; i < nVars; i++ )
{
for ( k = i; k < nVars; k++ )

1
src/opt/dau/dau.h
View File

@ -76,6 +76,7 @@ static inline int Dau_DsdReadVar( char * p ) { if ( *p == '!' ) p++; return *p
/*=== dauCanon.c ==========================================================*/
extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
extern unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars );
/*=== dauDsd.c ==========================================================*/
extern int * Dau_DsdComputeMatches( char * p );
extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes );

99
src/opt/dau/dauCanon.c
View File

@ -941,6 +941,105 @@ unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
return uCanonPhase;
}
/**Function*************************************************************
Synopsis [Semi-canonical form computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_TtCanonicizePhaseVar6( word * pTruth, int nVars, int v )
{
int w, nWords = Abc_TtWordNum( nVars );
int s, nStep = 1 << (v-6);
assert( v >= 6 );
for ( w = nWords - 1, s = nWords - nStep; w > 0; w-- )
{
if ( pTruth[w-nStep] == pTruth[w] )
{
if ( w == s ) { w = s - nStep; s = w - nStep; }
continue;
}
if ( pTruth[w-nStep] > pTruth[w] )
return -1;
for ( ; w > 0; w-- )
{
ABC_SWAP( word, pTruth[w-nStep], pTruth[w] );
if ( w == s ) { w = s - nStep; s = w - nStep; }
}
assert( w == -1 );
return 1;
}
return 0;
}
static inline int Abc_TtCanonicizePhaseVar5( word * pTruth, int nVars, int v )
{
int w, nWords = Abc_TtWordNum( nVars );
int Shift = 1 << v;
word Mask = s_Truths6[v];
assert( v < 6 );
for ( w = nWords - 1; w >= 0; w-- )
{
if ( ((pTruth[w] << Shift) & Mask) == (pTruth[w] & Mask) )
continue;
if ( ((pTruth[w] << Shift) & Mask) > (pTruth[w] & Mask) )
return -1;
// Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf("\n" );
for ( ; w >= 0; w-- )
pTruth[w] = ((pTruth[w] << Shift) & Mask) | ((pTruth[w] & Mask) >> Shift);
// Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf( " changed %d", v ), printf("\n" );
return 1;
}
return 0;
}
unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
{
unsigned uCanonPhase = 0;
int v, nWords = Abc_TtWordNum( nVars );
// static int Counter = 0;
// Counter++;
#ifdef CANON_VERIFY
static word pCopy1[1024];
static word pCopy2[1024];
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
#endif
if ( (pTruth[nWords-1] >> 63) & 1 )
{
Abc_TtNot( pTruth, nWords );
uCanonPhase ^= (1 << nVars);
}
// while ( 1 )
// {
// unsigned uCanonPhase2 = uCanonPhase;
for ( v = nVars - 1; v >= 6; v-- )
if ( Abc_TtCanonicizePhaseVar6( pTruth, nVars, v ) == 1 )
uCanonPhase ^= 1 << v;
for ( ; v >= 0; v-- )
if ( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) == 1 )
uCanonPhase ^= 1 << v;
// if ( uCanonPhase2 == uCanonPhase )
// break;
// }
// for ( v = 5; v >= 0; v-- )
// assert( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) != 1 );
#ifdef CANON_VERIFY
Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
Abc_TtImplementNpnConfig( pCopy2, nVars, NULL, uCanonPhase );
if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
printf( "Canonical form verification failed!\n" );
#endif
return uCanonPhase;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///