diff options
| -rw-r--r-- | src/base/abci/abc.c | 1 | ||||
| -rw-r--r-- | src/base/abci/abcNpn.c | 28 | ||||
| -rw-r--r-- | src/opt/dau/dau.h | 1 | ||||
| -rw-r--r-- | src/opt/dau/dauCanon.c | 143 | 
4 files changed, 170 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index afd2bcfe..7db89a44 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6159,6 +6159,7 @@ usage:      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               7: new hierarchical matching\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" ); diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c index 87a00651..e667a074 100644 --- a/src/base/abci/abcNpn.c +++ b/src/base/abci/abcNpn.c @@ -181,7 +181,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )      char pCanonPerm[16];      unsigned uCanonPhase=0;      abctime clk = Abc_Clock(); -    int i; +    int i, nClasses = -1;      char * pAlgoName = NULL;      if ( NpnType == 0 ) @@ -198,6 +198,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )          pAlgoName = "new hybrid fast    ";      else if ( NpnType == 6 )          pAlgoName = "new phase flipping "; +    else if ( NpnType == 7 ) +        pAlgoName = "new hier. matching ";      assert( p->nVars <= 16 );      if ( pAlgoName ) @@ -289,9 +291,29 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )                  Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );          }      } +    else if ( NpnType == 7 ) +    { +        extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm ); +        extern Abc_TtMan_t * Abc_TtManStart( int nVars ); +        extern void Abc_TtManStop( Abc_TtMan_t * p ); +        extern int Abc_TtManNumClasses( Abc_TtMan_t * p ); + +        Abc_TtMan_t * pMan = Abc_TtManStart( p->nVars ); +        for ( i = 0; i < p->nFuncs; i++ ) +        { +            if ( fVerbose ) +                printf( "%7d : ", i ); +            uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm ); +            if ( fVerbose ) +//                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" ); +                printf( "\n" ); +        } +        nClasses = Abc_TtManNumClasses( pMan ); +        Abc_TtManStop( pMan ); +    }      else assert( 0 );      clk = Abc_Clock() - clk; -    printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) ); +    printf( "Classes =%9d  ", nClasses == -1 ? Abc_TruthNpnCountUnique(p) : nClasses );      Abc_PrintTime( 1, "Time", clk );  } @@ -352,7 +374,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 <= 6 ) +    if ( NpnType >= 0 && NpnType <= 7 )          Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );      else          printf( "Unknown canonical form value (%d).\n", NpnType ); diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index ddffa905..1fa22494 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -59,6 +59,7 @@ typedef enum {  } Dau_DsdType_t;  typedef struct Dss_Man_t_ Dss_Man_t; +typedef struct Abc_TtMan_t_ Abc_TtMan_t;  ////////////////////////////////////////////////////////////////////////  ///                      MACRO DEFINITIONS                           /// diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c index 26edca9b..4fd8361c 100644 --- a/src/opt/dau/dauCanon.c +++ b/src/opt/dau/dauCanon.c @@ -20,6 +20,7 @@  #include "dauInt.h"  #include "misc/util/utilTruth.h" +#include "misc/vec/vecMem.h"  ABC_NAMESPACE_IMPL_START @@ -1041,6 +1042,148 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )  } +/**Function************************************************************* + +  Synopsis    [Hierarchical semi-canonical form computation.] + +  Description [] +                +  SideEffects [] + +  SeeAlso     [] + +***********************************************************************/ +#define TT_NUM_TABLES 4 + +struct Abc_TtMan_t_ +{ +    Vec_Mem_t *   vTtMem[TT_NUM_TABLES];   // truth table memory and hash tables +}; + +Abc_TtMan_t * Abc_TtManStart( int nVars ) +{ +    Abc_TtMan_t * p = ABC_CALLOC( Abc_TtMan_t, 1 ); +    int i, nWords = Abc_TtWordNum( nVars ); +    for ( i = 0; i < TT_NUM_TABLES; i++ ) +    { +        p->vTtMem[i] = Vec_MemAlloc( nWords, 12 ); +        Vec_MemHashAlloc( p->vTtMem[i], 10000 ); +    } +    return p; +} +void Abc_TtManStop( Abc_TtMan_t * p ) +{ +    int i; +    for ( i = 0; i < TT_NUM_TABLES; i++ ) +    { +        Vec_MemHashFree( p->vTtMem[i] ); +        Vec_MemFreeP( &p->vTtMem[i] ); +    } +    ABC_FREE( p ); +} +int Abc_TtManNumClasses( Abc_TtMan_t * p ) +{ +    return Vec_MemEntryNum( p->vTtMem[TT_NUM_TABLES-1] ); +} + +unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm ) +{ +    int fNaive = 1; +    int pStore[17]; +    static word pTruth[1024]; +    unsigned uCanonPhase = 0; +    int nOnes, nWords = Abc_TtWordNum( nVars ); +    int i, k, truthId; +    int * pSpot; +    assert( nVars <= 16 ); + +    Abc_TtCopy( pTruth, pTruthInit, nWords, 0 ); + +    for ( i = 0; i < nVars; i++ ) +        pCanonPerm[i] = i; + +    // normalize polarity     +    nOnes = Abc_TtCountOnesInTruth( pTruth, nVars ); +    if ( nOnes > nWords * 32 ) +    { +        Abc_TtNot( pTruth, nWords ); +        nOnes = nWords*64 - nOnes; +        uCanonPhase |= (1 << nVars); +    } +    // check cache +    pSpot = Vec_MemHashLookup( p->vTtMem[0], pTruth ); +    if ( *pSpot != -1 ) +        return 0; +    truthId = Vec_MemHashInsert( p->vTtMem[0], pTruth ); + +    // normalize phase +    Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); +    pStore[nVars] = nOnes; +    for ( i = 0; i < nVars; i++ ) +    { +        if ( pStore[i] >= nOnes - pStore[i] ) +            continue; +        Abc_TtFlip( pTruth, nWords, i ); +        uCanonPhase |= (1 << i); +        pStore[i] = nOnes - pStore[i];  +    } +    // check cache +    pSpot = Vec_MemHashLookup( p->vTtMem[1], pTruth ); +    if ( *pSpot != -1 ) +        return 0; +    truthId = Vec_MemHashInsert( p->vTtMem[1], pTruth ); + +    // normalize permutation +    { +        int k, BestK; +        for ( i = 0; i < nVars - 1; i++ ) +        { +            BestK = i + 1; +            for ( k = i + 2; k < nVars; k++ ) +                if ( pStore[BestK] > pStore[k] ) +                    BestK = k; +            if ( pStore[i] <= pStore[BestK] ) +                continue; +            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] ); +            ABC_SWAP( int, pStore[i], pStore[BestK] ); +            if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) +            { +                uCanonPhase ^= (1 << i); +                uCanonPhase ^= (1 << BestK); +            } +            Abc_TtSwapVars( pTruth, nVars, i, BestK ); +        } +    } +    // check cache +    pSpot = Vec_MemHashLookup( p->vTtMem[2], pTruth ); +    if ( *pSpot != -1 ) +        return 0; +    truthId = Vec_MemHashInsert( p->vTtMem[2], pTruth ); + +    // iterate TT permutations for tied variables +    for ( k = 0; k < 5; k++ ) +    { +        int fChanges = 0; +        for ( i = nVars - 2; i >= 0; i-- ) +            if ( pStore[i] == pStore[i+1] ) +                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive ); +        if ( !fChanges ) +            break; +        fChanges = 0; +        for ( i = 1; i < nVars - 1; i++ ) +            if ( pStore[i] == pStore[i+1] ) +                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive ); +        if ( !fChanges ) +            break; +    } +    // check cache +    pSpot = Vec_MemHashLookup( p->vTtMem[3], pTruth ); +    if ( *pSpot != -1 ) +        return 0; +    truthId = Vec_MemHashInsert( p->vTtMem[3], pTruth ); +    return 0; +} +  ////////////////////////////////////////////////////////////////////////  ///                       END OF FILE                                ///  ////////////////////////////////////////////////////////////////////////  | 
