mirror of https://github.com/YosysHQ/abc.git
Updating command 'majgen'.
This commit is contained in:
parent
18bc189aba
commit
7d641b7cbe
|
|
@ -27,6 +27,7 @@
|
||||||
#include "misc/vec/vecMem.h"
|
#include "misc/vec/vecMem.h"
|
||||||
#include "misc/extra/extra.h"
|
#include "misc/extra/extra.h"
|
||||||
#include "misc/util/utilTruth.h"
|
#include "misc/util/utilTruth.h"
|
||||||
|
#include "opt/dau/dau.h"
|
||||||
|
|
||||||
ABC_NAMESPACE_IMPL_START
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
|
@ -215,47 +216,36 @@ void Gem_FuncExpand( Gem_Man_t * p, int f, int i )
|
||||||
Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
|
Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
|
||||||
word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
|
word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
|
||||||
word * pResult = p->pTtElems[p->nVars];
|
word * pResult = p->pTtElems[p->nVars];
|
||||||
word * pBest = p->pTtElems[p->nVars+1];
|
|
||||||
word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
|
word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
|
||||||
int v, iFunc, BestPlace, GroupsMod;
|
int v, iFunc;
|
||||||
|
char pCanonPermC[16];
|
||||||
assert( i < (int)pObj->nVars );
|
assert( i < (int)pObj->nVars );
|
||||||
assert( (int)pObj->nVars + 2 <= p->nVars );
|
assert( (int)pObj->nVars + 2 <= p->nVars );
|
||||||
Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
|
Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
|
||||||
// move i variable to the end
|
// move i variable to the end
|
||||||
for ( v = i; v < (int)pObj->nVars-1; v++ )
|
for ( v = i; v < (int)pObj->nVars-1; v++ )
|
||||||
Abc_TtSwapAdjacent( pResult, p->nWords, v );
|
Abc_TtSwapAdjacent( pResult, p->nWords, v );
|
||||||
GroupsMod = Gem_GroupVarRemove( pObj->Groups, i );
|
|
||||||
//Extra_PrintBinary2( stdout, (unsigned*)&GroupsMod, p->nVars ); printf("\n");
|
|
||||||
// create new symmetric group
|
// create new symmetric group
|
||||||
assert( v == (int)pObj->nVars-1 );
|
assert( v == (int)pObj->nVars-1 );
|
||||||
Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v );
|
Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v );
|
||||||
Abc_TtCofactor1p( pCofs[1], pResult, p->nWords, v );
|
Abc_TtCofactor1p( pCofs[1], pResult, p->nWords, v );
|
||||||
Abc_TtMaj( pResult, p->pTtElems[v], p->pTtElems[v+1], p->pTtElems[v+2], p->nWords );
|
Abc_TtMaj( pResult, p->pTtElems[v], p->pTtElems[v+1], p->pTtElems[v+2], p->nWords );
|
||||||
Abc_TtMux( pResult, pResult, pCofs[1], pCofs[0], p->nWords );
|
Abc_TtMux( pResult, pResult, pCofs[1], pCofs[0], p->nWords );
|
||||||
//Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n");
|
|
||||||
// canonicize
|
// canonicize
|
||||||
BestPlace = Gem_FuncFindPlace( pResult, p->nWords, GroupsMod, pBest, 0 );
|
//Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n");
|
||||||
//Extra_PrintHex( stdout, (unsigned*)pBest, pObj->nVars + 2 ); printf("\n");
|
Abc_TtCanonicizePerm( pResult, pObj->nVars + 2, pCanonPermC );
|
||||||
iFunc = Vec_MemHashInsert( p->vTtMem, pBest );
|
Abc_TtStretch6( pResult, Abc_MaxInt(6, pObj->nVars+2), p->nVars );
|
||||||
|
//Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n\n");
|
||||||
|
iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
|
||||||
if ( iFunc < p->nObjs )
|
if ( iFunc < p->nObjs )
|
||||||
return;
|
return;
|
||||||
assert( iFunc == p->nObjs );
|
assert( iFunc == p->nObjs );
|
||||||
pNew->nVars = pObj->nVars + 2;
|
pNew->nVars = pObj->nVars + 2;
|
||||||
pNew->nNodes = pObj->nNodes + 1;
|
pNew->nNodes = pObj->nNodes + 1;
|
||||||
pNew->Groups = Gem_GroupVarsInsert3( GroupsMod, BestPlace );
|
pNew->Groups = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
|
||||||
pNew->Predec = f;
|
pNew->Predec = f;
|
||||||
pNew->History = i;
|
pNew->History = i;
|
||||||
Gem_PrintNode( p, iFunc, "Expand ", 0 );
|
Gem_PrintNode( p, iFunc, "Expand ", 0 );
|
||||||
GroupsMod = Gem_GroupsDerive( pBest, pNew->nVars, pCofs[0], pCofs[1] );
|
|
||||||
//Extra_PrintBinary2( stdout, (unsigned*)&GroupsMod, p->nVars ); printf("\n");
|
|
||||||
// assert( GroupsMod == (int)pNew->Groups );
|
|
||||||
assert( GroupsMod == (GroupsMod & (int)pNew->Groups) );
|
|
||||||
|
|
||||||
if ( GroupsMod != (int)pNew->Groups )
|
|
||||||
{
|
|
||||||
pNew->Groups = GroupsMod;
|
|
||||||
Gem_PrintNode( p, iFunc, "Expand ", 1 );
|
|
||||||
}
|
|
||||||
|
|
||||||
assert( p->nObjs < p->nObjsAlloc );
|
assert( p->nObjs < p->nObjsAlloc );
|
||||||
if ( ++p->nObjs == p->nObjsAlloc )
|
if ( ++p->nObjs == p->nObjsAlloc )
|
||||||
|
|
@ -298,20 +288,18 @@ int Gem_FuncReduce( Gem_Man_t * p, int f, int i, int j )
|
||||||
Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
|
Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
|
||||||
word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
|
word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
|
||||||
word * pResult = p->pTtElems[p->nVars];
|
word * pResult = p->pTtElems[p->nVars];
|
||||||
word * pBest = p->pTtElems[p->nVars+1];
|
|
||||||
word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
|
word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
|
||||||
int u, v, w, BestPlace, iFunc, GroupsMod;
|
int v, iFunc;
|
||||||
|
char pCanonPermC[16];
|
||||||
assert( i < j && j < 16 );
|
assert( i < j && j < 16 );
|
||||||
Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
|
Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
|
||||||
// move j variable to the end
|
// move j variable to the end
|
||||||
for ( v = j; v < (int)pObj->nVars-1; v++ )
|
for ( v = j; v < (int)pObj->nVars-1; v++ )
|
||||||
Abc_TtSwapAdjacent( pResult, p->nWords, v );
|
Abc_TtSwapAdjacent( pResult, p->nWords, v );
|
||||||
GroupsMod = Gem_GroupVarRemove( pObj->Groups, j );
|
|
||||||
assert( v == (int)pObj->nVars-1 );
|
assert( v == (int)pObj->nVars-1 );
|
||||||
// move i variable to the end
|
// move i variable to the end
|
||||||
for ( v = i; v < (int)pObj->nVars-2; v++ )
|
for ( v = i; v < (int)pObj->nVars-2; v++ )
|
||||||
Abc_TtSwapAdjacent( pResult, p->nWords, v );
|
Abc_TtSwapAdjacent( pResult, p->nWords, v );
|
||||||
GroupsMod = Gem_GroupVarRemove( GroupsMod, i );
|
|
||||||
assert( v == (int)pObj->nVars-2 );
|
assert( v == (int)pObj->nVars-2 );
|
||||||
// create new variable
|
// create new variable
|
||||||
Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v+1 );
|
Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v+1 );
|
||||||
|
|
@ -319,63 +307,22 @@ int Gem_FuncReduce( Gem_Man_t * p, int f, int i, int j )
|
||||||
Abc_TtCofactor0( pCofs[0], p->nWords, v );
|
Abc_TtCofactor0( pCofs[0], p->nWords, v );
|
||||||
Abc_TtCofactor1( pCofs[1], p->nWords, v );
|
Abc_TtCofactor1( pCofs[1], p->nWords, v );
|
||||||
Abc_TtMux( pResult, p->pTtElems[v], pCofs[1], pCofs[0], p->nWords );
|
Abc_TtMux( pResult, p->pTtElems[v], pCofs[1], pCofs[0], p->nWords );
|
||||||
// check if new variable belongs to any group
|
// canonicize
|
||||||
for ( u = 0; u < v; u++ )
|
//Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars - 1 ); printf("\n");
|
||||||
{
|
Abc_TtCanonicizePerm( pResult, pObj->nVars - 1, pCanonPermC );
|
||||||
if ( ((GroupsMod >> u) & 1) == 0 )
|
Abc_TtStretch6( pResult, Abc_MaxInt(6, pObj->nVars-1), p->nVars );
|
||||||
continue;
|
//Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars - 1 ); printf("\n\n");
|
||||||
if ( !Abc_TtVarsAreSymmetric(pResult, p->nVars, u, v, pCofs[0], pCofs[1]) )
|
iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
|
||||||
continue;
|
|
||||||
// u and v are symm
|
|
||||||
for ( w = v-1; w >= u; w-- )
|
|
||||||
Abc_TtSwapAdjacent( pResult, p->nWords, w );
|
|
||||||
// check if it exists
|
|
||||||
iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
|
|
||||||
if ( iFunc < p->nObjs )
|
|
||||||
return 0;
|
|
||||||
assert( iFunc == p->nObjs );
|
|
||||||
pNew->nVars = pObj->nVars - 1;
|
|
||||||
pNew->nNodes = pObj->nNodes;
|
|
||||||
pNew->Groups = Gem_GroupVarsInsert1( GroupsMod, u-1, 0 );
|
|
||||||
pNew->Predec = f;
|
|
||||||
pNew->History = (j << 4) | i;
|
|
||||||
Gem_PrintNode( p, iFunc, "Symmetry", 0 );
|
|
||||||
GroupsMod = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
|
|
||||||
//assert( GroupsMod == (int)pNew->Groups );
|
|
||||||
assert( GroupsMod == (GroupsMod & (int)pNew->Groups) );
|
|
||||||
|
|
||||||
if ( GroupsMod != (int)pNew->Groups )
|
|
||||||
{
|
|
||||||
pNew->Groups = GroupsMod;
|
|
||||||
Gem_PrintNode( p, iFunc, "Symmetry", 1 );
|
|
||||||
}
|
|
||||||
|
|
||||||
assert( p->nObjs < p->nObjsAlloc );
|
|
||||||
if ( ++p->nObjs == p->nObjsAlloc )
|
|
||||||
Gem_ManRealloc( p );
|
|
||||||
return Gem_FuncCheckMajority( p, iFunc );
|
|
||||||
}
|
|
||||||
// v is not symmetric to any variable
|
|
||||||
BestPlace = Gem_FuncFindPlace( pResult, p->nWords, GroupsMod, pBest, 1 );
|
|
||||||
// check if it exists
|
|
||||||
iFunc = Vec_MemHashInsert( p->vTtMem, pBest );
|
|
||||||
if ( iFunc < p->nObjs )
|
if ( iFunc < p->nObjs )
|
||||||
return 0;
|
return 0;
|
||||||
assert( iFunc == p->nObjs );
|
assert( iFunc == p->nObjs );
|
||||||
pNew->nVars = pObj->nVars - 1;
|
pNew->nVars = pObj->nVars - 1;
|
||||||
pNew->nNodes = pObj->nNodes;
|
pNew->nNodes = pObj->nNodes;
|
||||||
pNew->Groups = Gem_GroupVarsInsert1( GroupsMod, BestPlace, 1 );
|
pNew->Groups = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
|
||||||
pNew->Predec = f;
|
pNew->Predec = f;
|
||||||
pNew->History = (j << 4) | i;
|
pNew->History = (j << 4) | i;
|
||||||
Gem_PrintNode( p, iFunc, "Crossbar", 0 );
|
Gem_PrintNode( p, iFunc, "Crossbar", 0 );
|
||||||
GroupsMod = Gem_GroupsDerive( pBest, pNew->nVars, pCofs[0], pCofs[1] );
|
Gem_FuncCheckMajority( p, iFunc );
|
||||||
//assert( GroupsMod == (int)pNew->Groups );
|
|
||||||
assert( GroupsMod == (GroupsMod & (int)pNew->Groups) );
|
|
||||||
if ( GroupsMod != (int)pNew->Groups )
|
|
||||||
{
|
|
||||||
pNew->Groups = GroupsMod;
|
|
||||||
Gem_PrintNode( p, iFunc, "Symmetry", 1 );
|
|
||||||
}
|
|
||||||
|
|
||||||
assert( p->nObjs < p->nObjsAlloc );
|
assert( p->nObjs < p->nObjsAlloc );
|
||||||
if ( ++p->nObjs == p->nObjsAlloc )
|
if ( ++p->nObjs == p->nObjsAlloc )
|
||||||
|
|
@ -421,6 +368,8 @@ int Gem_Enumerate( int nVars, int fVerbose )
|
||||||
if ( Gem_FuncReduce( p, f, i, j ) )
|
if ( Gem_FuncReduce( p, f, i, j ) )
|
||||||
return Gem_ManFree( p );
|
return Gem_ManFree( p );
|
||||||
}
|
}
|
||||||
|
printf( "Finished %d (functions = %10d) ", v, p->nObjs );
|
||||||
|
Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
|
||||||
Vec_MemDumpTruthTables( p->vTtMem, "enum", nVars );
|
Vec_MemDumpTruthTables( p->vTtMem, "enum", nVars );
|
||||||
Gem_ManFree( p );
|
Gem_ManFree( p );
|
||||||
return 0;
|
return 0;
|
||||||
|
|
|
||||||
|
|
@ -77,6 +77,7 @@ static inline int Dau_DsdReadVar( char * p ) { if ( *p == '!' ) p++; return *p
|
||||||
|
|
||||||
/*=== dauCanon.c ==========================================================*/
|
/*=== dauCanon.c ==========================================================*/
|
||||||
extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
|
extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
|
||||||
|
extern unsigned Abc_TtCanonicizePerm( word * pTruth, int nVars, char * pCanonPerm );
|
||||||
extern unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars );
|
extern unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars );
|
||||||
/*=== dauDsd.c ==========================================================*/
|
/*=== dauDsd.c ==========================================================*/
|
||||||
extern int * Dau_DsdComputeMatches( char * p );
|
extern int * Dau_DsdComputeMatches( char * p );
|
||||||
|
|
|
||||||
|
|
@ -489,7 +489,7 @@ int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore )
|
||||||
SeeAlso []
|
SeeAlso []
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut )
|
static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut, int fOnlySwap )
|
||||||
{
|
{
|
||||||
int fOldSwap = 0;
|
int fOldSwap = 0;
|
||||||
int pStoreIn[17];
|
int pStoreIn[17];
|
||||||
|
|
@ -501,7 +501,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
|
||||||
pCanonPerm[i] = i;
|
pCanonPerm[i] = i;
|
||||||
// normalize polarity
|
// normalize polarity
|
||||||
nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
|
nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
|
||||||
if ( nOnes > nWords * 32 )
|
if ( nOnes > nWords * 32 && !fOnlySwap )
|
||||||
{
|
{
|
||||||
Abc_TtNot( pTruth, nWords );
|
Abc_TtNot( pTruth, nWords );
|
||||||
nOnes = nWords*64 - nOnes;
|
nOnes = nWords*64 - nOnes;
|
||||||
|
|
@ -512,7 +512,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
|
||||||
pStore[nVars] = nOnes;
|
pStore[nVars] = nOnes;
|
||||||
for ( i = 0; i < nVars; i++ )
|
for ( i = 0; i < nVars; i++ )
|
||||||
{
|
{
|
||||||
if ( pStore[i] >= nOnes - pStore[i] )
|
if ( pStore[i] >= nOnes - pStore[i] || fOnlySwap )
|
||||||
continue;
|
continue;
|
||||||
Abc_TtFlip( pTruth, nWords, i );
|
Abc_TtFlip( pTruth, nWords, i );
|
||||||
uCanonPhase |= (1 << i);
|
uCanonPhase |= (1 << i);
|
||||||
|
|
@ -923,7 +923,7 @@ unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
|
||||||
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
|
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
|
uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn, 0 );
|
||||||
for ( k = 0; k < 5; k++ )
|
for ( k = 0; k < 5; k++ )
|
||||||
{
|
{
|
||||||
int fChanges = 0;
|
int fChanges = 0;
|
||||||
|
|
@ -958,6 +958,53 @@ unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
|
||||||
return uCanonPhase;
|
return uCanonPhase;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
unsigned Abc_TtCanonicizePerm( word * pTruth, int nVars, char * pCanonPerm )
|
||||||
|
{
|
||||||
|
int pStoreIn[17];
|
||||||
|
unsigned uCanonPhase;
|
||||||
|
int i, k, nWords = Abc_TtWordNum( nVars );
|
||||||
|
int fNaive = 1;
|
||||||
|
|
||||||
|
#ifdef CANON_VERIFY
|
||||||
|
char pCanonPermCopy[16];
|
||||||
|
static word pCopy1[1024];
|
||||||
|
static word pCopy2[1024];
|
||||||
|
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
|
||||||
|
#endif
|
||||||
|
|
||||||
|
assert( nVars <= 16 );
|
||||||
|
for ( i = 0; i < nVars; i++ )
|
||||||
|
pCanonPerm[i] = i;
|
||||||
|
|
||||||
|
uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn, 1 );
|
||||||
|
for ( k = 0; k < 5; k++ )
|
||||||
|
{
|
||||||
|
int fChanges = 0;
|
||||||
|
for ( i = nVars - 2; i >= 0; i-- )
|
||||||
|
if ( pStoreIn[i] == pStoreIn[i+1] )
|
||||||
|
fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, 1, pCanonPerm, &uCanonPhase, fNaive );
|
||||||
|
if ( !fChanges )
|
||||||
|
break;
|
||||||
|
fChanges = 0;
|
||||||
|
for ( i = 1; i < nVars - 1; i++ )
|
||||||
|
if ( pStoreIn[i] == pStoreIn[i+1] )
|
||||||
|
fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, 1, pCanonPerm, &uCanonPhase, fNaive );
|
||||||
|
if ( !fChanges )
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
#ifdef CANON_VERIFY
|
||||||
|
Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
|
||||||
|
memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
|
||||||
|
Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
|
||||||
|
if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
|
||||||
|
printf( "Canonical form verification failed!\n" );
|
||||||
|
#endif
|
||||||
|
|
||||||
|
assert( uCanonPhase == 0 );
|
||||||
|
return uCanonPhase;
|
||||||
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Semi-canonical form computation.]
|
Synopsis [Semi-canonical form computation.]
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue