aigCanon.c File Reference

#include "aig.h"
#include "bool/kit/kit.h"
#include "bool/bdc/bdc.h"
#include "aig/ioa/ioa.h"

Include dependency graph for aigCanon.c:

Go to the source code of this file.

Classes
struct	Aig_VSig_t_
struct	Aig_Tru_t_
struct	Aig_RMan_t_

Macros
#define	RMAN_MAXVARS   12
	DECLARATIONS ///.
#define	RMAX_MAXWORD   (RMAN_MAXVARS <= 5 ? 1 : (1 << (RMAN_MAXVARS - 5)))

Typedefs
typedef struct Aig_VSig_t_	Aig_VSig_t
typedef struct Aig_Tru_t_	Aig_Tru_t
typedef struct Aig_RMan_t_	Aig_RMan_t

Functions
Aig_RMan_t *	Aig_RManStart ()
	FUNCTION DEFINITIONS ///.
Aig_Tru_t **	Aig_RManTableLookup (Aig_RMan_t *p, unsigned *pTruth, int nVars)
void	Aig_RManTableResize (Aig_RMan_t *p)
int	Aig_RManTableFindOrAdd (Aig_RMan_t *p, unsigned *pTruth, int nVars)
void	Aig_RManStop (Aig_RMan_t *p)
void	Aig_RManQuit ()
void	Aig_RManPrintVarProfile (unsigned *pTruth, int nVars, unsigned *pTruthAux)
void	Aig_RManSortNums (int *pArray, int nVars)
void	Aig_RManPrintSigs (Aig_VSig_t *pSigs, int nVars)
void	Aig_RManComputeVSigs (unsigned *pTruth, int nVars, Aig_VSig_t *pSigs, unsigned *pAux)
int	Aig_RManVarsAreUnique (Aig_VSig_t *pMints, int nVars)
void	Aig_RManPrintUniqueVars (Aig_VSig_t *pMints, int nVars)
unsigned	Aig_RManSemiCanonicize (unsigned *pOut, unsigned *pIn, int nVars, char *pCanonPerm, Aig_VSig_t *pSigs, int fReturnIn)
void	Aig_RManSaveOne (Aig_RMan_t *p, unsigned *pTruth, int nVars)
void	Aig_RManRecord (unsigned *pTruth, int nVarsInit)

Macro Definition Documentation

RMAN_MAXVARS

#define RMAN_MAXVARS   12

DECLARATIONS ///.

CFile****************************************************************

FileName [aigCanon.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Processing the library of semi-canonical AIGs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id

aigCanon.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

Definition at line 33 of file aigCanon.c.

RMAX_MAXWORD

#define RMAX_MAXWORD   (RMAN_MAXVARS <= 5 ? 1 : (1 << (RMAN_MAXVARS - 5)))

Definition at line 34 of file aigCanon.c.

Typedef Documentation

Aig_RMan_t

typedef struct Aig_RMan_t_ Aig_RMan_t

Definition at line 53 of file aigCanon.c.

Aig_Tru_t

typedef struct Aig_Tru_t_ Aig_Tru_t

Definition at line 43 of file aigCanon.c.

Aig_VSig_t

typedef struct Aig_VSig_t_ Aig_VSig_t

Definition at line 36 of file aigCanon.c.

Function Documentation

Aig_RManComputeVSigs()

void Aig_RManComputeVSigs	(	unsigned *	pTruth,
		int	nVars,
		Aig_VSig_t *	pSigs,
		unsigned *	pAux )

Function*************************************************************

Synopsis [Computes signatures for all variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file aigCanon.c.

{
    int v;
    for ( v = 0; v < nVars; v++ )
    {
        Kit_TruthCofactor0New( pAux, pTruth, nVars, v );
        pSigs[2*v+0].nOnes = Kit_TruthCountOnes( pAux, nVars );
        Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+0].nCofOnes );
        Aig_RManSortNums( pSigs[2*v+0].nCofOnes, nVars );
 
        Kit_TruthCofactor1New( pAux, pTruth, nVars, v );
        pSigs[2*v+1].nOnes = Kit_TruthCountOnes( pAux, nVars );
        Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+1].nCofOnes );
        Aig_RManSortNums( pSigs[2*v+1].nCofOnes, nVars );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManPrintSigs()

void Aig_RManPrintSigs	(	Aig_VSig_t *	pSigs,
		int	nVars )

Function*************************************************************

Synopsis [Prints signatures for all variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 353 of file aigCanon.c.

{
    int v, i, k;
    for ( v = 0; v < nVars; v++ )
    {
        printf( "%2d : ", v );
        for ( k = 0; k < 2; k++ )
        {
            printf( "%5d  ", pSigs[2*v+k].nOnes );
            printf( "(" );
            for ( i = 0; i < nVars; i++ )
                printf( "%4d ", pSigs[2*v+k].nCofOnes[i] );
            printf( ")  " );
        }
        printf( "\n" );
    }
}

Aig_RManPrintUniqueVars()

void Aig_RManPrintUniqueVars	(	Aig_VSig_t *	pMints,
		int	nVars )

Function*************************************************************

Synopsis [Returns 1 if all variables are unique.]

Description []

SideEffects []

SeeAlso []

Definition at line 447 of file aigCanon.c.

{
    int i;
    for ( i = 0; i < nVars; i++ )
        if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*i+1], nVars ) == 0 )
            printf( "=" );
        else 
            printf( "x" );
    printf( "\n" );
 
    printf( "0" );
    for ( i = 1; i < nVars; i++ )
        if ( Aig_RManCompareSigs( &pMints[2*(i-1)], &pMints[2*i], nVars ) == 0 )
            printf( "-" );
        else if ( i < 10 )
            printf( "%c", '0' + i );
        else 
            printf( "%c", 'A' + i-10 );
    printf( "\n" );
}

Aig_RManPrintVarProfile()

void Aig_RManPrintVarProfile	(	unsigned *	pTruth,
		int	nVars,
		unsigned *	pTruthAux )

Function*************************************************************

Synopsis [Returns 1 if all variables are unique.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file aigCanon.c.

{
    int pStore2[32];
    int i;
    Kit_TruthCountOnesInCofsSlow( pTruth, nVars, pStore2, pTruthAux );
    for ( i = 0; i < nVars; i++ )
        printf( "%2d/%2d ", pStore2[2*i], pStore2[2*i+1] );
    printf( "\n" );
}

Here is the call graph for this function:

Aig_RManQuit()

void Aig_RManQuit

(

)

Function*************************************************************

Synopsis [Stops recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file aigCanon.c.

{
//    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
    char Buffer[20];
    if ( s_pRMan == NULL )
        return;
    // dump the library file
    sprintf( Buffer, "aiglib%02d.aig", s_pRMan->nVars );
    Ioa_WriteAiger( s_pRMan->pAig, Buffer, 0, 1 );
    // quit the manager
    Aig_RManStop( s_pRMan );
    s_pRMan = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManRecord()

void Aig_RManRecord	(	unsigned *	pTruth,
		int	nVarsInit )

Function*************************************************************

Synopsis [Records one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 598 of file aigCanon.c.

{
    int fVerify = 1;
    Kit_DsdNtk_t * pNtk;
    Kit_DsdObj_t * pObj;
    unsigned uPhaseC;
    int i, nVars, nWords;
    int fUniqueVars;
 
    if ( nVarsInit > RMAN_MAXVARS )
    {
        printf( "The number of variables in too large.\n" );
        return;
    }
 
    if ( s_pRMan == NULL )
        s_pRMan = Aig_RManStart();
    s_pRMan->nTotal++;
    // canonicize the function
    pNtk = Kit_DsdDecompose( pTruth, nVarsInit );
    pObj = Kit_DsdNonDsdPrimeMax( pNtk );
    if ( pObj == NULL || pObj->nFans == 3 )
    {
        s_pRMan->nTtDsd++;
        Kit_DsdNtkFree( pNtk );
        return;
    }
    nVars = pObj->nFans;
    s_pRMan->nVarFuncs[nVars]++;
    if ( nVars < nVarsInit )
        s_pRMan->nTtDsdPart++;
    else
        s_pRMan->nTtDsdNot++;
    // compute the number of words
    nWords = Abc_TruthWordNum( nVars );
    // copy the function
    memcpy( s_pRMan->pTruthInit, Kit_DsdObjTruth(pObj), (size_t)(4*nWords) );
    Kit_DsdNtkFree( pNtk );
    // canonicize the output
    if ( s_pRMan->pTruthInit[0] & 1 )
        Kit_TruthNot( s_pRMan->pTruthInit, s_pRMan->pTruthInit, nVars );
    memcpy( s_pRMan->pTruth, s_pRMan->pTruthInit, 4*nWords );
 
    // canonize the function
    for ( i = 0; i < nVars; i++ )
        s_pRMan->pPerm[i] = i;
    uPhaseC = Aig_RManSemiCanonicize( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPerm, s_pRMan->pMints, 1 );
    // check unique variables
    fUniqueVars = Aig_RManVarsAreUnique( s_pRMan->pMints, nVars );
    s_pRMan->nUniqueVars += fUniqueVars;
 
/*
    printf( "%4d : ", s_pRMan->nTotal );
    printf( "%2d %2d  ", nVarsInit, nVars );
    Extra_PrintBinary( stdout, &uPhaseC, nVars );
    printf( "  " );
    for ( i = 0; i < nVars; i++ )
        printf( "%2d/%2d ", s_pRMan->pMints[2*i], s_pRMan->pMints[2*i+1] );
    printf( "\n" );
    Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars );
Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
*/
/*
    printf( "\n" );
    printf( "%4d : ", s_pRMan->nTotal );
    printf( "%2d %2d  ", nVarsInit, nVars );
    printf( "   " );
    printf( "\n" );
    Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars );
//    Aig_RManPrintSigs( s_pRMan->pMints, nVars );
*/
 
//Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
 
    if ( Aig_RManTableFindOrAdd( s_pRMan, s_pRMan->pTruth, nVars ) )
        Aig_RManSaveOne( s_pRMan, s_pRMan->pTruth, nVars );
 
    if ( fVerify )
    {
        // derive reverse permutation
        for ( i = 0; i < nVars; i++ )
            s_pRMan->pPermR[i] = s_pRMan->pPerm[i];
        // implement permutation
        Kit_TruthPermute( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPermR, 1 );
        // implement polarity
        for ( i = 0; i < nVars; i++ )
            if ( uPhaseC & (1 << i) )
                Kit_TruthChangePhase( s_pRMan->pTruth, nVars, i );
 
        // perform verification
        if ( fUniqueVars && !Kit_TruthIsEqual( s_pRMan->pTruth, s_pRMan->pTruthInit, nVars ) )
            printf( "Verification failed.\n" );
    }
//Aig_RManPrintVarProfile( s_pRMan->pTruth, nVars, s_pRMan->pTruthTemp );
//Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManSaveOne()

void Aig_RManSaveOne	(	Aig_RMan_t *	p,
		unsigned *	pTruth,
		int	nVars )

Function*************************************************************

Synopsis [Records one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 558 of file aigCanon.c.

{
    int i, nNodes, RetValue;
    Bdc_Fun_t * pFunc;
    Aig_Obj_t * pTerm;
    // perform decomposition
    RetValue = Bdc_ManDecompose( p->pBidec, pTruth, NULL, nVars, NULL, 1000 );
    if ( RetValue < 0 )
    {
        printf( "Decomposition failed.\n" );
        return;
    }
    // convert back into HOP
    Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, 0 ), Aig_ManConst1(p->pAig) );
    for ( i = 0; i < nVars; i++ )
        Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, i+1 ), Aig_IthVar(p->pAig, i) );
    nNodes = Bdc_ManNodeNum(p->pBidec);
    for ( i = nVars + 1; i < nNodes; i++ )
    {
        pFunc = Bdc_ManFunc( p->pBidec, i );
        Bdc_FuncSetCopy( pFunc, Aig_And( p->pAig, 
            Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), 
            Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
    }
    pTerm = Bdc_FunCopyHop( Bdc_ManRoot(p->pBidec) );
    pTerm = Aig_ObjCreateCo( p->pAig, pTerm );
//    assert( pTerm->fPhase == 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManSemiCanonicize()

unsigned Aig_RManSemiCanonicize	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		char *	pCanonPerm,
		Aig_VSig_t *	pSigs,
		int	fReturnIn )

Function*************************************************************

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 479 of file aigCanon.c.

{
    Aig_VSig_t TempSig;
    int i, Temp, fChange, Counter;
    unsigned * pTemp, uCanonPhase = 0;
    // collect signatures 
    Aig_RManComputeVSigs( pIn, nVars, pSigs, pOut );
    // canonicize phase
    for ( i = 0; i < nVars; i++ )
    {
//        if ( pStore[2*i+0] <= pStore[2*i+1] )
        if ( Aig_RManCompareSigs( &pSigs[2*i+0], &pSigs[2*i+1], nVars ) <= 0 )
            continue;
        uCanonPhase |= (1 << i);
        TempSig = pSigs[2*i+0];
        pSigs[2*i+0] = pSigs[2*i+1];
        pSigs[2*i+1] = TempSig;
        Kit_TruthChangePhase( pIn, nVars, i );
    }
    // permute
    Counter = 0;
    do {
        fChange = 0;
        for ( i = 0; i < nVars-1; i++ )
        {
//            if ( pStore[2*i] <= pStore[2*(i+1)] )
            if ( Aig_RManCompareSigs( &pSigs[2*i], &pSigs[2*(i+1)], nVars ) <= 0 )
                continue;
            Counter++;
            fChange = 1;
 
            Temp = pCanonPerm[i];
            pCanonPerm[i] = pCanonPerm[i+1];
            pCanonPerm[i+1] = Temp;
 
            TempSig = pSigs[2*i];
            pSigs[2*i] = pSigs[2*(i+1)];
            pSigs[2*(i+1)] = TempSig;
 
            TempSig = pSigs[2*i+1];
            pSigs[2*i+1] = pSigs[2*(i+1)+1];
            pSigs[2*(i+1)+1] = TempSig;
 
            Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
        }
    } while ( fChange );
 
    // swap if it was moved an even number of times
    if ( fReturnIn ^ !(Counter & 1) )
        Kit_TruthCopy( pOut, pIn, nVars );
    return uCanonPhase;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManSortNums()

void Aig_RManSortNums	(	int *	pArray,
		int	nVars )

Function*************************************************************

Synopsis [Sorts numbers in the increasing order.]

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file aigCanon.c.

{
    int i, j, best_i, tmp;
    for ( i = 0; i < nVars-1; i++ )
    {
        best_i = i;
        for ( j = i+1; j < nVars; j++ )
            if ( pArray[j] > pArray[best_i] )
                best_i = j;
        tmp = pArray[i]; pArray[i] = pArray[best_i]; pArray[best_i] = tmp;
    }
}

Here is the caller graph for this function:

Aig_RManStart()

Aig_RMan_t * Aig_RManStart

(

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Allocates recording manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file aigCanon.c.

{
    static Bdc_Par_t Pars = {0}, * pPars = &Pars;
    Aig_RMan_t * p;
    p = ABC_ALLOC( Aig_RMan_t, 1 );
    memset( p, 0, sizeof(Aig_RMan_t) );
    p->nVars = RMAN_MAXVARS;
    p->pAig  = Aig_ManStart( 1000000 );
    Aig_IthVar( p->pAig, p->nVars-1 );
    // create hash table
    p->nBins = Abc_PrimeCudd(5000);
    p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
    p->pMemTrus = Aig_MmFlexStart();
    // bi-decomposition manager
    pPars->nVarsMax = p->nVars;
    pPars->fVerbose = 0;
    p->pBidec = Bdc_ManAlloc( pPars );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManStop()

void Aig_RManStop

(

Aig_RMan_t *

p

)

Function*************************************************************

Synopsis [Deallocates recording manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file aigCanon.c.

{
    int i;
    printf( "Total funcs    = %10d\n", p->nTotal );
    printf( "Full DSD funcs = %10d\n", p->nTtDsd );
    printf( "Part DSD funcs = %10d\n", p->nTtDsdPart );
    printf( "Non- DSD funcs = %10d\n", p->nTtDsdNot );
    printf( "Uniq-var funcs = %10d\n", p->nUniqueVars );
    printf( "Unique   funcs = %10d\n", p->nEntries );
    printf( "Distribution of functions:\n" );
    for ( i = 5; i <= p->nVars; i++ )
        printf( "%2d = %8d\n", i, p->nVarFuncs[i] );
    Aig_MmFlexStop( p->pMemTrus, 0 );
    Aig_ManStop( p->pAig );
    Bdc_ManFree( p->pBidec );
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManTableFindOrAdd()

int Aig_RManTableFindOrAdd	(	Aig_RMan_t *	p,
		unsigned *	pTruth,
		int	nVars )

Function*************************************************************

Synopsis [Find or add new entry.]

Description [Returns 1 if this is a new entry.]

SideEffects []

SeeAlso []

Definition at line 218 of file aigCanon.c.

{
    Aig_Tru_t ** ppSpot, * pEntry;
    int nBytes;
    ppSpot = Aig_RManTableLookup( p, pTruth, nVars );
    if ( *ppSpot )
    {
        (*ppSpot)->nVisits++;
        return 0;
    }
    nBytes = sizeof(Aig_Tru_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars);
    if ( p->nEntries == 3*p->nBins )
        Aig_RManTableResize( p );
    pEntry = (Aig_Tru_t *)Aig_MmFlexEntryFetch( p->pMemTrus, nBytes );
    pEntry->Id = p->nEntries++;
    pEntry->nVars = nVars;
    pEntry->nVisits = 1;
    pEntry->pNext = NULL;
    memcpy( pEntry->pTruth, pTruth, sizeof(unsigned) * Kit_TruthWordNum(nVars) );
    *ppSpot = pEntry;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManTableLookup()

Aig_Tru_t ** Aig_RManTableLookup	(	Aig_RMan_t *	p,
		unsigned *	pTruth,
		int	nVars )

Function*************************************************************

Synopsis [Returns the given record.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file aigCanon.c.

{
    static int s_Primes[16] = { 
        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
    Aig_Tru_t ** ppSpot, * pEntry;
    ppSpot = p->pBins + Aig_RManTableHash( pTruth, nVars, p->nBins, s_Primes );
    for ( pEntry = *ppSpot; pEntry; ppSpot = &pEntry->pNext, pEntry = pEntry->pNext )
        if ( Kit_TruthIsEqual( pEntry->pTruth, pTruth, nVars ) )
            return ppSpot;
    return ppSpot;
}

Here is the caller graph for this function:

Aig_RManTableResize()

void Aig_RManTableResize

(

Aig_RMan_t *

p

)

Function*************************************************************

Synopsis [Find or add new entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file aigCanon.c.

{
    Aig_Tru_t * pEntry, * pNext;
    Aig_Tru_t ** pBinsOld, ** ppPlace;
    int nBinsOld, Counter, i;
    abctime clk;
    assert( p->pBins != NULL );
clk = Abc_Clock();
    // save the old Bins
    pBinsOld = p->pBins;
    nBinsOld = p->nBins;
    // get the new Bins
    p->nBins = Abc_PrimeCudd( 3 * nBinsOld ); 
    p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
    // rehash the entries from the old table
    Counter = 0;
    for ( i = 0; i < nBinsOld; i++ )
    for ( pEntry = pBinsOld[i], pNext = pEntry? pEntry->pNext : NULL; 
          pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
    {
        // get the place where this entry goes in the Bins 
        ppPlace = Aig_RManTableLookup( p, pEntry->pTruth, pEntry->nVars );
        assert( *ppPlace == NULL ); // should not be there
        // add the entry to the list
        *ppPlace = pEntry;
        pEntry->pNext = NULL;
        Counter++;
    }
    assert( Counter == p->nEntries );
//    ABC_PRT( "Time", Abc_Clock() - clk );
    ABC_FREE( pBinsOld );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_RManVarsAreUnique()

int Aig_RManVarsAreUnique	(	Aig_VSig_t *	pMints,
		int	nVars )

Function*************************************************************

Synopsis [Returns 1 if all variables are unique.]

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file aigCanon.c.

{
    int i;
    for ( i = 0; i < nVars - 1; i++ )
        if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*(i+1)], nVars ) == 0 )
            return 0;
    return 1;
}

Here is the caller graph for this function: