bdcInt.h File Reference

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

Go to the source code of this file.

Data Structures
struct	Bdc_Fun_t_
struct	Bdc_Isf_t_
struct	Bdc_Man_t_

Macros
#define	BDC_SCALE   1000
	INCLUDES ///. More...

Typedefs
typedef struct Bdc_Isf_t_	Bdc_Isf_t

Enumerations
enum	Bdc_Type_t {   BDC_TYPE_NONE = 0, BDC_TYPE_CONST1, BDC_TYPE_PI, BDC_TYPE_AND,   BDC_TYPE_OR, BDC_TYPE_XOR, BDC_TYPE_MUX, BDC_TYPE_OTHER }
	BASIC TYPES ///. More...

Functions
static Bdc_Fun_t *	Bdc_FunNew (Bdc_Man_t *p)
static Bdc_Fun_t *	Bdc_FunWithId (Bdc_Man_t *p, int Id)
static int	Bdc_FunId (Bdc_Man_t *p, Bdc_Fun_t *pFun)
static void	Bdc_IsfStart (Bdc_Man_t *p, Bdc_Isf_t *pF)
static void	Bdc_IsfClean (Bdc_Isf_t *p)
static void	Bdc_IsfCopy (Bdc_Isf_t *p, Bdc_Isf_t *q)
static void	Bdc_IsfNot (Bdc_Isf_t *p)
Bdc_Fun_t *	Bdc_ManDecompose_rec (Bdc_Man_t *p, Bdc_Isf_t *pIsf)
	MACRO DEFINITIONS ///. More...
void	Bdc_SuppMinimize (Bdc_Man_t *p, Bdc_Isf_t *pIsf)
int	Bdc_ManNodeVerify (Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Fun_t *pFunc)
Bdc_Fun_t *	Bdc_TableLookup (Bdc_Man_t *p, Bdc_Isf_t *pIsf)
void	Bdc_TableAdd (Bdc_Man_t *p, Bdc_Fun_t *pFunc)
void	Bdc_TableClear (Bdc_Man_t *p)
int	Bdc_TableCheckContainment (Bdc_Man_t *p, Bdc_Isf_t *pIsf, unsigned *puTruth)
	DECLARATIONS ///. More...

Macro Definition Documentation

#define BDC_SCALE   1000

INCLUDES ///.

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

FileName [bdcInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Truth-table-based bi-decomposition engine.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:

resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp

]PARAMETERS ///

Definition at line 41 of file bdcInt.h.

Typedef Documentation

typedef struct Bdc_Isf_t_ Bdc_Isf_t

Definition at line 72 of file bdcInt.h.

Enumeration Type Documentation

enum Bdc_Type_t

BASIC TYPES ///.

Enumerator
BDC_TYPE_NONE
BDC_TYPE_CONST1
BDC_TYPE_PI
BDC_TYPE_AND
BDC_TYPE_OR
BDC_TYPE_XOR
BDC_TYPE_MUX
BDC_TYPE_OTHER

Definition at line 48 of file bdcInt.h.

             { 
    BDC_TYPE_NONE = 0,  // 0:  unknown
    BDC_TYPE_CONST1,    // 1:  constant 1
    BDC_TYPE_PI,        // 2:  primary input
    BDC_TYPE_AND,       // 3:  AND-gate
    BDC_TYPE_OR,        // 4:  OR-gate (temporary)
    BDC_TYPE_XOR,       // 5:  XOR-gate
    BDC_TYPE_MUX,       // 6:  MUX-gate
    BDC_TYPE_OTHER      // 7:  unused
} Bdc_Type_t;

Function Documentation

static int Bdc_FunId ( Bdc_Man_t *  p, Bdc_Fun_t *  pFun  )

inlinestatic

Definition at line 130 of file bdcInt.h.

{ return pFun - p->pNodes; }

static Bdc_Fun_t* Bdc_FunNew ( Bdc_Man_t *  p )

inlinestatic

Definition at line 128 of file bdcInt.h.

{ Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; }

static Bdc_Fun_t* Bdc_FunWithId ( Bdc_Man_t *  p, int  Id  )

inlinestatic

Definition at line 129 of file bdcInt.h.

{ assert( Id < p->nNodes ); return p->pNodes + Id; }

static void Bdc_IsfClean ( Bdc_Isf_t *  p )

inlinestatic

Definition at line 132 of file bdcInt.h.

{ p->uSupp = 0; p->uUniq = 0;                                      }

static void Bdc_IsfCopy ( Bdc_Isf_t *  p, Bdc_Isf_t *  q  )

inlinestatic

Definition at line 133 of file bdcInt.h.

{ Bdc_Isf_t T = *p; *p = *q; *q = T;                               }

static void Bdc_IsfNot ( Bdc_Isf_t *  p )

inlinestatic

Definition at line 134 of file bdcInt.h.

{ unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT;    }

static void Bdc_IsfStart ( Bdc_Man_t *  p, Bdc_Isf_t *  pF  )

inlinestatic

Definition at line 131 of file bdcInt.h.

{ pF->uSupp = 0; pF->uUniq = 0; pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); assert( pF->puOff && pF->puOn ); }

Bdc_Fun_t* Bdc_ManDecompose_rec	(	Bdc_Man_t *	p,
		Bdc_Isf_t *	pIsf
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Performs one step of bi-decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 675 of file bdcDec.c.

{
//    int static Counter = 0;
//    int LocalCounter = Counter++;
    Bdc_Type_t Type;
    Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
    Bdc_Isf_t IsfL, * pIsfL = &IsfL;
    Bdc_Isf_t IsfB, * pIsfR = &IsfB;
    int iVar;
    abctime clk = 0; // Suppress "might be used uninitialized"
/*
printf( "Init function (%d):\n", LocalCounter );
Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
*/
    // check computed results
    assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
    if ( p->pPars->fVerbose )
        clk = Abc_Clock();
    pFunc = Bdc_TableLookup( p, pIsf );
    if ( p->pPars->fVerbose )
        p->timeCache += Abc_Clock() - clk;
    if ( pFunc )
        return pFunc;
    // decide on the decomposition type
    if ( p->pPars->fVerbose )
        clk = Abc_Clock();
    Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
    if ( p->pPars->fVerbose )
        p->timeCheck += Abc_Clock() - clk;
    if ( Type == BDC_TYPE_MUX )
    {
        if ( p->pPars->fVerbose )
            clk = Abc_Clock();
        iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
        if ( p->pPars->fVerbose )
            p->timeMuxes += Abc_Clock() - clk;
        p->numMuxes++;
        pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
        pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
        if ( pFunc0 == NULL || pFunc1 == NULL )
            return NULL;
        pFunc  = Bdc_FunWithId( p, iVar + 1 );
        pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND );
        pFunc1 = Bdc_ManCreateGate( p, pFunc,  pFunc1, BDC_TYPE_AND );
        if ( pFunc0 == NULL || pFunc1 == NULL )
            return NULL;
        pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR );
    }
    else
    {
        pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
        if ( pFunc0 == NULL )
            return NULL;
        // decompose the right branch
        if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) )
        {
            p->nNodesNew--;
            return pFunc0;
        }
        Bdc_SuppMinimize( p, pIsfR );
        pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
        if ( pFunc1 == NULL )
            return NULL;
        // create new gate
        pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
    }
    return pFunc;
}

int Bdc_ManNodeVerify	(	Bdc_Man_t *	p,
		Bdc_Isf_t *	pIsf,
		Bdc_Fun_t *	pFunc
	)

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

Synopsis [Creates gates.]

Description []

SideEffects []

SeeAlso []

Definition at line 600 of file bdcDec.c.

{
    unsigned * puTruth = p->puTemp1;
    if ( Bdc_IsComplement(pFunc) )
        Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars );
    else
        Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars );
    return Bdc_TableCheckContainment( p, pIsf, puTruth );
}

void Bdc_SuppMinimize	(	Bdc_Man_t *	p,
		Bdc_Isf_t *	pIsf
	)

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

Synopsis [Minimizes the support of the ISF.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file bdcDec.c.

{
    int v;
    abctime clk = 0; // Suppress "might be used uninitialized"
    if ( p->pPars->fVerbose )
        clk = Abc_Clock();
    // go through the support variables
    pIsf->uSupp = 0;
    for ( v = 0; v < p->nVars; v++ )
    {
        if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) && 
             !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
              continue;
        if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
        {
            Kit_TruthExist( pIsf->puOn, p->nVars, v );
            Kit_TruthExist( pIsf->puOff, p->nVars, v );
            continue;
        }
        pIsf->uSupp |= (1 << v);
    }
    if ( p->pPars->fVerbose )
        p->timeSupps += Abc_Clock() - clk;
}

void Bdc_TableAdd	(	Bdc_Man_t *	p,
		Bdc_Fun_t *	pFunc
	)

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

Synopsis [Adds the new entry to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file bdcTable.c.

{
    if ( p->pTable[pFunc->uSupp] == NULL )
        Vec_IntPush( p->vSpots, pFunc->uSupp );
    pFunc->pNext = p->pTable[pFunc->uSupp];
    p->pTable[pFunc->uSupp] = pFunc;
}

int Bdc_TableCheckContainment	(	Bdc_Man_t *	p,
		Bdc_Isf_t *	pIsf,
		unsigned *	puTruth
	)

DECLARATIONS ///.

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

FileName [bdcTable.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Truth-table-based bi-decomposition engine.]

Synopsis [Hash table for intermediate nodes.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 30, 2007.]

Revision [

Id:

bdcTable.c,v 1.00 2007/01/30 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Checks containment of the function in the ISF.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file bdcTable.c.

{
    return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
         Kit_TruthIsDisjoint( puTruth, pIsf->puOff, p->nVars );
}

void Bdc_TableClear

(

Bdc_Man_t *

p

)

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

Synopsis [Adds the new entry to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file bdcTable.c.

{
    int Spot, i;
    Vec_IntForEachEntry( p->vSpots, Spot, i )
        p->pTable[Spot] = NULL;
    Vec_IntClear( p->vSpots );
}

Bdc_Fun_t* Bdc_TableLookup	(	Bdc_Man_t *	p,
		Bdc_Isf_t *	pIsf
	)

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

Synopsis [Adds the new entry to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file bdcTable.c.

{
    int fDisableCache = 0;
    Bdc_Fun_t * pFunc;
    if ( fDisableCache && Kit_WordCountOnes(pIsf->uSupp) > 1 )
        return NULL;
    if ( pIsf->uSupp == 0 )
    {
        assert( p->pTable[pIsf->uSupp] == p->pNodes );
        if ( Kit_TruthIsConst1( pIsf->puOn, p->nVars ) )
            return p->pNodes;
        assert( Kit_TruthIsConst1( pIsf->puOff, p->nVars ) );
        return Bdc_Not(p->pNodes);
    }
    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
             return pFunc;
    Bdc_IsfNot( pIsf );
    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
        {
            Bdc_IsfNot( pIsf );
            return Bdc_Not(pFunc);
        }
    Bdc_IsfNot( pIsf );
    return NULL;
}