extraUtilDsd.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "extra.h"
#include "misc/vec/vec.h"
#include "misc/vec/vecHsh.h"
#include "misc/util/utilTruth.h"
#include "bool/rsb/rsb.h"

Go to the source code of this file.

Data Structures
struct	Sdm_Dsd_t_
struct	Sdm_Man_t_

Macros
#define	DSD_CLASS_NUM   595

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Sdm_Dsd_t_	Sdm_Dsd_t
	DECLARATIONS ///. More...

Functions
void	Sdm_ManPrintDsdStats (Sdm_Man_t *p, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
Hsh_IntMan_t *	Sdm_ManBuildHashTable (Vec_Int_t **pvConfgRes)
void	Sdm_ManPrecomputePerms (Sdm_Man_t *p)
void	Sdm_ManPrintPerm (unsigned s)
int	Sdm_ManCheckDsd6 (Sdm_Man_t *p, word t)
int	Sdm_ManComputeFunc (Sdm_Man_t *p, int iDsdLit0, int iDsdLit1, int *pCut, int uMask, int fXor)
int	Sdm_ManReadDsdVarNum (Sdm_Man_t *p, int iDsd)
int	Sdm_ManReadDsdAndNum (Sdm_Man_t *p, int iDsd)
int	Sdm_ManReadDsdClauseNum (Sdm_Man_t *p, int iDsd)
word	Sdm_ManReadDsdTruth (Sdm_Man_t *p, int iDsd)
char *	Sdm_ManReadDsdStr (Sdm_Man_t *p, int iDsd)
void	Sdm_ManReadCnfCosts (Sdm_Man_t *p, int *pCosts, int nCosts)
Sdm_Man_t *	Sdm_ManAlloc ()
void	Sdm_ManFree (Sdm_Man_t *p)
Sdm_Man_t *	Sdm_ManRead ()
void	Sdm_ManQuit ()
int	Sdm_ManCanRead ()
void	Sdm_ManTest ()
void	Sdm_ManDivCollect_rec (word t, Vec_Wrd_t **pvDivs)
void	Sdm_ManDivTest ()

Variables
static Sdm_Dsd_t	s_DsdClass6 [DSD_CLASS_NUM]
static Sdm_Man_t *	s_SdmMan = NULL

Macro Definition Documentation

#define DSD_CLASS_NUM   595

Definition at line 48 of file extraUtilDsd.c.

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Sdm_Dsd_t_ Sdm_Dsd_t

DECLARATIONS ///.

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

FileName [extraUtilDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [File management utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

extraUtilDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 38 of file extraUtilDsd.c.

Function Documentation

Sdm_Man_t* Sdm_ManAlloc

(

)

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

Synopsis [Manager manipulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1038 of file extraUtilDsd.c.

{
    Sdm_Man_t * p;
    p = ABC_CALLOC( Sdm_Man_t, 1 );
    Sdm_ManPrecomputePerms( p );
    return p;
}

Hsh_IntMan_t* Sdm_ManBuildHashTable

(

Vec_Int_t **

pvConfgRes

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 710 of file extraUtilDsd.c.

{
    FILE * pFile;
    char * pFileName = "dsdfuncs6.dat";
    int RetValue, size = Extra_FileSize( pFileName ) / 12;  // 2866420
    Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size );
    Vec_Int_t * vConfgRes = Vec_IntAlloc( size );
    Hsh_IntMan_t * pHash;

    pFile = fopen( pFileName, "rb" );
    RetValue = fread( Vec_WrdArray(vTruthRes), sizeof(word), size, pFile );
    RetValue = fread( Vec_IntArray(vConfgRes), sizeof(int), size, pFile );
    vTruthRes->nSize = size;
    vConfgRes->nSize = size;
    // create hash table
    pHash = Hsh_WrdManHashArrayStart( vTruthRes, 1 );
    // cleanup
    if ( pvConfgRes )
        *pvConfgRes = vConfgRes;
    else
        Vec_IntFree( vConfgRes );
    Vec_WrdFree( vTruthRes );
//    Hsh_IntManStop( pHash );
    return pHash;
}

int Sdm_ManCanRead

(

)

Definition at line 1080 of file extraUtilDsd.c.

{
    char * pFileName = "dsdfuncs6.dat";
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
        return 0;
    fclose( pFile );
    return 1;
}

int Sdm_ManCheckDsd6	(	Sdm_Man_t *	p,
		word	t
	)

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

Synopsis [Checks hash table for DSD class.]

Description []

SideEffects []

SeeAlso []

Definition at line 895 of file extraUtilDsd.c.

{
    int fCompl, Entry, Config;
    if ( (fCompl = (t & 1)) )
        t = ~t;
    Entry = *Hsh_IntManLookup( p->pHash, (unsigned *)&t );
    if ( Entry == -1 )
        return -1;
    Config = Vec_IntEntry( p->vConfgRes, Entry );
    if ( fCompl )
        Config ^= (1 << 16);
    return Config;
}

int Sdm_ManComputeFunc	(	Sdm_Man_t *	p,
		int	iDsdLit0,
		int	iDsdLit1,
		int *	pCut,
		int	uMask,
		int	fXor
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 920 of file extraUtilDsd.c.

{
//    int fVerbose = 0;
    int i, Config, iClass, fCompl, Res;
    int PermMask = uMask & 0x3FFFF;
    int ComplMask = uMask >> 18;
    word Truth0, Truth1p, t0, t1, t;
    p->nAllDsd++;

    assert( uMask > 1 );
    assert( iDsdLit0 < DSD_CLASS_NUM * 2 );
    assert( iDsdLit1 < DSD_CLASS_NUM * 2 );
    Truth0  = p->pDsd6[Abc_Lit2Var(iDsdLit0)].uTruth;
    Truth1p = Vec_WrdEntry( p->vPerm6, Abc_Lit2Var(iDsdLit1) * 720 + Vec_IntEntry(p->vMap2Perm, PermMask ) );
    if ( ComplMask )
        for ( i = 0; i < 6; i++ )
            if ( (ComplMask >> i) & 1 )
                Truth1p = Abc_Tt6Flip( Truth1p, i );            
    t0 = Abc_LitIsCompl(iDsdLit0) ? ~Truth0  : Truth0;
    t1 = Abc_LitIsCompl(iDsdLit1) ? ~Truth1p : Truth1p;
    t = fXor ? t0 ^ t1 : t0 & t1;
/*
if ( fVerbose )
{
Sdm_ManPrintPerm( PermMask );                      printf( "\n" );
Extra_PrintBinary( stdout, &ComplMask, 6 );        printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&Truth0, 6 );   printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&Truth1p, 6 );  printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );        printf( "\n" );
}
*/
    // find configuration
    Config = Sdm_ManCheckDsd6( p, t );
    if ( Config == -1 )
    {
        p->nNonDsd++;
        return -1;
    }

    // get the class
    iClass = Config >> 17;
    fCompl = (Config >> 16) & 1;
    Config &= 0xFFFF;

    // set the function
    Res = Abc_Var2Lit( iClass, fCompl );

    // update cut
    assert( (Config >> 6) < 720 );
    if ( pCut )
    {
        int pLeavesNew[6] = { -1, -1, -1, -1, -1, -1 };
        assert( pCut[0] <= 6 );
        for ( i = 0; i < pCut[0]; i++ )
            pLeavesNew[(int)(p->Perm6[Config >> 6][i])] = Abc_LitNotCond( pCut[i+1], (Config >> i) & 1 );
        pCut[0] = p->pDsd6[iClass].nVars;
        for ( i = 0; i < pCut[0]; i++ )
            assert( pLeavesNew[i] != -1 );
        for ( i = 0; i < pCut[0]; i++ )
            pCut[i+1] = pLeavesNew[i];
    }
    assert( iClass < DSD_CLASS_NUM );
    p->nCountDsd[iClass]++;
    return Res;
}

void Sdm_ManDivCollect_rec	(	word	t,
		Vec_Wrd_t **	pvDivs
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso [] Function*************************************************************

Synopsis [Collect DSD divisors of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 1167 of file extraUtilDsd.c.

{
    int i, Config, Counter = 0;
    // check if function is decomposable
    Config = Sdm_ManCheckDsd6( s_SdmMan, t );
    if ( Config != -1 && (Config >> 17) < 2 )
        return;
    for ( i = 0; i < 6; i++ )
    {
        if ( !Abc_Tt6HasVar( t, i ) )
            continue;
        Sdm_ManDivCollect_rec( Abc_Tt6Cofactor0(t, i), pvDivs );
        Sdm_ManDivCollect_rec( Abc_Tt6Cofactor1(t, i), pvDivs );
        Counter++;
    }
    if ( Config != -1 && Counter >= 2 && Counter <= 4 )
    {
        Vec_WrdPush( pvDivs[Counter], (t & 1) ? ~t : t );
//        Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
    }
}

void Sdm_ManDivTest

(

)

Definition at line 1188 of file extraUtilDsd.c.

{
//    word u, t0, t1, t = ABC_CONST(0xB0F0BBFFB0F0BAFE);
//    word u, t0, t1, t = ABC_CONST(0x3F1F3F13FFDFFFD3);
    word u, t0, t1, t = ABC_CONST(0x3F3FFFFF37003700);
    Rsb_Man_t * pManRsb = Rsb_ManAlloc( 6, 200, 3, 1 );
    Vec_Wrd_t * pvDivs[7] = { NULL };
    Vec_Wrd_t * vDivs = Vec_WrdAlloc( 100 );
    int i, RetValue;

    // collect divisors
    for ( i = 2; i <= 4; i++ )
        pvDivs[i] = Vec_WrdAlloc( 100 );
    Sdm_ManDivCollect_rec( t, pvDivs );
    for ( i = 2; i <= 4; i++ )
        Vec_WrdUniqify( pvDivs[i] );

    // prepare the set
    vDivs = Vec_WrdAlloc( 100 );
    for ( i = 0; i < 6; i++ )
        Vec_WrdPush( vDivs, s_Truths6[i] );
    for ( i = 2; i <= 4; i++ )
        Vec_WrdAppend( vDivs, pvDivs[i] );
    for ( i = 2; i <= 4; i++ )
        Vec_WrdFree( pvDivs[i] );

    Vec_WrdForEachEntry( vDivs, u, i )
    {
        printf( "%2d : ", i );
//        Kit_DsdPrintFromTruth( (unsigned *)&u, 6 ); 
        printf( "\n" );
    }

    RetValue = Rsb_ManPerformResub6( pManRsb, 6, t, vDivs, &t0, &t1, 1 );
    if ( RetValue )
    {
//        Kit_DsdPrintFromTruth( (unsigned *)&t0, 6 ); printf( "\n" );
//        Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ); printf( "\n" );
        printf( "Decomposition exits.\n" );
    }


    Vec_WrdFree( vDivs );
    Rsb_ManFree( pManRsb );
}

void Sdm_ManFree

(

Sdm_Man_t *

p

)

Definition at line 1045 of file extraUtilDsd.c.

{
    Vec_WrdFree( p->vPerm6 );
    Vec_IntFree( p->vMap2Perm );
    Vec_IntFree( p->vConfgRes );
    Vec_IntFree( p->pHash->vData );
    Hsh_IntManStop( p->pHash );
    ABC_FREE( p );
}

void Sdm_ManPrecomputePerms

(

Sdm_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 747 of file extraUtilDsd.c.

{
    int nVars = 6;
    // 0(1:1) 1(2:1) 2(4:2) 3(10:6) 4(33:23) 5(131:98) 6(595:464)
    int nClasses[7] = { 1, 2, 4, 10, 33, 131, 595 };
    int nPerms = Extra_Factorial( nVars );
//    int nSwaps = (1 << nVars);
    int * pComp, * pPerm;
    int i, k, x, One, OneCopy, Num;
    Vec_Int_t * vVars;
    abctime clk = Abc_Clock();
    assert( p->pDsd6 == NULL );
    p->pDsd6 = s_DsdClass6;
    // precompute schedules
    pComp = Extra_GreyCodeSchedule( nVars );
    pPerm = Extra_PermSchedule( nVars );
    // map numbers into perms
    p->vMap2Perm = Vec_IntStartFull( (1<<(3*nVars)) );
    // store permutations
    One = 0;
    for ( x = 0; x < nVars; x++ )
    {
        p->Perm6[0][x] = (char)x;
        One |= (x << (3*x));
    }
//    Vec_IntWriteEntry( p->vMap2Perm, One, 0 );
    OneCopy = One;
    for ( k = 0; k < nPerms; k++ )
    {
        if ( k > 0 )
        for ( x = 0; x < nVars; x++ )
            p->Perm6[k][x] = p->Perm6[k-1][x];
        ABC_SWAP( char, p->Perm6[k][pPerm[k]], p->Perm6[k][pPerm[k]+1] );

        Num = ( (One >> (3*(pPerm[k]  ))) ^ (One >> (3*(pPerm[k]+1))) ) & 7;
        One ^=  (Num << (3*(pPerm[k]  )));
        One ^=  (Num << (3*(pPerm[k]+1)));

        Vec_IntWriteEntry( p->vMap2Perm, One, k );
        
//        Sdm_ManPrintPerm( One );
//        for ( x = 0; x < nVars; x++ )
//            printf( "%d ", p->Perm6[k][x] );
//        printf( "\n" );
    }
    assert( OneCopy == One );
    // fill in the gaps
    vVars = Vec_IntAlloc( 6 );
    Vec_IntForEachEntry( p->vMap2Perm, Num, i )
    {
        // mark used variables
        int Count = 0;
        One = i;
        Vec_IntFill( vVars, 6, 0 );
        for ( k = 0; k < nVars; k++ )
        {
            int iVar = ((One >> (3*k)) & 7);
            if ( iVar >= nVars && iVar < 7 )
                break;
            if ( iVar != 7 )
            {
                if ( Vec_IntEntry( vVars, iVar ) == 1 )
                    break;
                Vec_IntWriteEntry( vVars, iVar, 1 );
                Count++;
            }
        }
        // skip ones with dups and complete
        if ( k < nVars || Count == nVars )
            continue;
        // find unused variables
        for ( x = k = 0; k < 6; k++ )
            if ( Vec_IntEntry(vVars, k) == 0 )
                Vec_IntWriteEntry( vVars, x++, k );
        Vec_IntShrink( vVars, x );
        // fill in used variables
        x = 0;
        for ( k = 0; k < nVars; k++ )
        {
            int iVar = ((One >> (3*k)) & 7);
            if ( iVar == 7 )
                One ^= ((Vec_IntEntry(vVars, x++) ^ 7) << (3*k));
        }
        assert( x == Vec_IntSize(vVars) );
        // save this one
        assert( Vec_IntEntry( p->vMap2Perm, One ) != -1 );
        Vec_IntWriteEntry( p->vMap2Perm, i, Vec_IntEntry(p->vMap2Perm, One) );
/*
        // mapping
        Sdm_ManPrintPerm( i );
        printf( "->  " );
        Sdm_ManPrintPerm( One );
        printf( "\n" );
*/
    }
    Vec_IntFree( vVars );

    // store permuted truth tables
    assert( p->vPerm6 == NULL );
    p->vPerm6 = Vec_WrdAlloc( nPerms * DSD_CLASS_NUM );
    for ( i = 0; i < nClasses[nVars]; i++ )
    {
        word uTruth = s_DsdClass6[i].uTruth;
        for ( k = 0; k < nPerms; k++ )
        {
            uTruth = Abc_Tt6SwapAdjacent( uTruth, pPerm[k] );
            Vec_WrdPush( p->vPerm6, uTruth );
        }
        assert( uTruth == s_DsdClass6[i].uTruth );
    }
    ABC_FREE( pPerm );
    ABC_FREE( pComp );
    // build hash table
    p->pHash = Sdm_ManBuildHashTable( &p->vConfgRes );
    Abc_PrintTime( 1, "Setting up DSD information", Abc_Clock() - clk );
}

void Sdm_ManPrintDsdStats	(	Sdm_Man_t *	p,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 676 of file extraUtilDsd.c.

{
    int i, Absent = 0;
    for ( i = 0; i < DSD_CLASS_NUM; i++ )
    {
        if ( p->nCountDsd[i] == 0 )
        {
            Absent++;
            continue;
        }
        if ( fVerbose )
        {
            printf( "%5d  :  ", i );
            printf( "%-20s   ", p->pDsd6[i].pStr );
            printf( "%8d ",     p->nCountDsd[i] );
            printf( "\n" );
        }
    }
    printf( "Unused classes = %d (%.2f %%).  ", Absent, 100.0 * Absent / DSD_CLASS_NUM );
    printf( "Non-DSD cuts = %d (%.2f %%).  ",   p->nNonDsd, 100.0 * p->nNonDsd / Abc_MaxInt(1, p->nAllDsd) );
    printf( "\n" );
}

void Sdm_ManPrintPerm

(

unsigned

s

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 876 of file extraUtilDsd.c.

{
    int i;
    for ( i = 0; i < 6; i++ )
        printf( "%d ", (s >> (3*i)) & 7 );
    printf( "  " );
}

void Sdm_ManQuit

(

)

Definition at line 1074 of file extraUtilDsd.c.

{
    if ( s_SdmMan != NULL )
        Sdm_ManFree( s_SdmMan );
    s_SdmMan = NULL;
}

Sdm_Man_t* Sdm_ManRead

(

)

Definition at line 1067 of file extraUtilDsd.c.

{
    if ( s_SdmMan == NULL )
        s_SdmMan = Sdm_ManAlloc();
    memset( s_SdmMan->nCountDsd, 0, sizeof(int) * DSD_CLASS_NUM );
    return s_SdmMan;
}

void Sdm_ManReadCnfCosts	(	Sdm_Man_t *	p,
		int *	pCosts,
		int	nCosts
	)

Definition at line 1017 of file extraUtilDsd.c.

{
    int i;
    assert( nCosts == DSD_CLASS_NUM );
    pCosts[0] = pCosts[1] = 0;
    for ( i = 2; i < DSD_CLASS_NUM; i++ )
        pCosts[i] = Sdm_ManReadDsdClauseNum( p, i );
}

int Sdm_ManReadDsdAndNum	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1001 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].nAnds;
}

int Sdm_ManReadDsdClauseNum	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1005 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].nClauses;
}

char* Sdm_ManReadDsdStr	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1013 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].pStr;
}

word Sdm_ManReadDsdTruth	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1009 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].uTruth;
}

int Sdm_ManReadDsdVarNum	(	Sdm_Man_t *	p,
		int	iDsd
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 997 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].nVars;
}

void Sdm_ManTest

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1101 of file extraUtilDsd.c.

{
    Sdm_Man_t * p;
    int iDsd0 = 4;
    int iDsd1 = 6;
    int iDsd;
    int uMask = 0x3FFFF ^ ((7 ^ 0) << 6) ^ ((7 ^ 1) << 9);
    int pCut[7] = { 4, 10, 20, 30, 40 };
//    Sdm_ManPrintPerm( uMask );
    p = Sdm_ManAlloc();
    iDsd = Sdm_ManComputeFunc( p, iDsd0, iDsd1, pCut, uMask, 0 );
    Sdm_ManFree( p );
}

Variable Documentation

Sdm_Dsd_t s_DsdClass6[DSD_CLASS_NUM]

static

Definition at line 50 of file extraUtilDsd.c.

Sdm_Man_t* s_SdmMan = NULL

static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1066 of file extraUtilDsd.c.