sfm.h File Reference

#include "misc/vec/vecWec.h"

Go to the source code of this file.

Data Structures
struct	Sfm_Par_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Sfm_Ntk_t_	Sfm_Ntk_t
	INCLUDES ///. More...
typedef struct Sfm_Par_t_	Sfm_Par_t

Functions
void	Sfm_ParSetDefault (Sfm_Par_t *pPars)
	MACRO DEFINITIONS ///. More...
int	Sfm_NtkPerform (Sfm_Ntk_t *p, Sfm_Par_t *pPars)
Sfm_Ntk_t *	Sfm_NtkConstruct (Vec_Wec_t *vFanins, int nPis, int nPos, Vec_Str_t *vFixed, Vec_Str_t *vEmpty, Vec_Wrd_t *vTruths)
void	Sfm_NtkFree (Sfm_Ntk_t *p)
Vec_Int_t *	Sfm_NodeReadFanins (Sfm_Ntk_t *p, int i)
word *	Sfm_NodeReadTruth (Sfm_Ntk_t *p, int i)
int	Sfm_NodeReadFixed (Sfm_Ntk_t *p, int i)
int	Sfm_NodeReadUsed (Sfm_Ntk_t *p, int i)
Vec_Int_t *	Sfm_NtkDfs (Sfm_Ntk_t *p, Vec_Wec_t *vGroups, Vec_Int_t *vGroupMap, Vec_Int_t *vBoxesLeft)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Sfm_Ntk_t_ Sfm_Ntk_t

INCLUDES ///.

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

FileName [sfm.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

sfm.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 41 of file sfm.h.

typedef struct Sfm_Par_t_ Sfm_Par_t

Definition at line 42 of file sfm.h.

Function Documentation

Vec_Int_t* Sfm_NodeReadFanins	(	Sfm_Ntk_t *	p,
		int	i
	)

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

Synopsis [Public APIs of this network.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file sfmNtk.c.

{
    return Vec_WecEntry( &p->vFanins, i );
}

int Sfm_NodeReadFixed	(	Sfm_Ntk_t *	p,
		int	i
	)

Definition at line 366 of file sfmNtk.c.

{
    return (int)Vec_StrEntry( p->vFixed, i );
}

word* Sfm_NodeReadTruth	(	Sfm_Ntk_t *	p,
		int	i
	)

Definition at line 362 of file sfmNtk.c.

{
    return Vec_WrdEntryP( p->vTruths, i );
}

int Sfm_NodeReadUsed	(	Sfm_Ntk_t *	p,
		int	i
	)

Definition at line 370 of file sfmNtk.c.

{
    return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
}

Sfm_Ntk_t* Sfm_NtkConstruct	(	Vec_Wec_t *	vFanins,
		int	nPis,
		int	nPos,
		Vec_Str_t *	vFixed,
		Vec_Str_t *	vEmpty,
		Vec_Wrd_t *	vTruths
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file sfmNtk.c.

{
    Sfm_Ntk_t * p;
    Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
    p = ABC_CALLOC( Sfm_Ntk_t, 1 );
    p->nObjs    = Vec_WecSize( vFanins );
    p->nPis     = nPis;
    p->nPos     = nPos;
    p->nNodes   = p->nObjs - p->nPis - p->nPos;
    // user data
    p->vFixed   = vFixed;
    p->vEmpty   = vEmpty;
    p->vTruths  = vTruths;
    p->vFanins  = *vFanins;
    ABC_FREE( vFanins );
    // attributes
    Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
    Sfm_CreateLevel( &p->vFanins, &p->vLevels, vEmpty );
    Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR, vEmpty );
    Vec_IntFill( &p->vCounts,   p->nObjs,  0 );
    Vec_IntFill( &p->vTravIds,  p->nObjs,  0 );
    Vec_IntFill( &p->vTravIds2, p->nObjs,  0 );
    Vec_IntFill( &p->vId2Var,   2*p->nObjs, -1 );
    Vec_IntFill( &p->vVar2Id,   2*p->nObjs, -1 );
    p->vCover   = Vec_IntAlloc( 1 << 16 );
    p->vCnfs    = Sfm_CreateCnf( p );
    return p;
}

Vec_Int_t* Sfm_NtkDfs	(	Sfm_Ntk_t *	p,
		Vec_Wec_t *	vGroups,
		Vec_Int_t *	vGroupMap,
		Vec_Int_t *	vBoxesLeft
	)

Definition at line 166 of file sfmWin.c.

{
    Vec_Int_t * vNodes;
    int i;
    Vec_IntClear( vBoxesLeft );
    vNodes = Vec_IntAlloc( p->nObjs );
    Sfm_NtkIncrementTravId( p );
    Sfm_NtkForEachPo( p, i )
        Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
    return vNodes;
}

void Sfm_NtkFree

(

Sfm_Ntk_t *

p

)

Definition at line 213 of file sfmNtk.c.

{
    // user data
    Vec_StrFree( p->vFixed );
    Vec_StrFreeP( &p->vEmpty );
    Vec_WrdFree( p->vTruths );
    Vec_WecErase( &p->vFanins );
    // attributes
    Vec_WecErase( &p->vFanouts );
    ABC_FREE( p->vLevels.pArray );
    ABC_FREE( p->vLevelsR.pArray );
    ABC_FREE( p->vCounts.pArray );
    ABC_FREE( p->vTravIds.pArray );
    ABC_FREE( p->vTravIds2.pArray );
    ABC_FREE( p->vId2Var.pArray );
    ABC_FREE( p->vVar2Id.pArray );
    Vec_WecFree( p->vCnfs );
    Vec_IntFree( p->vCover );
    // other data
    Vec_IntFreeP( &p->vNodes );
    Vec_IntFreeP( &p->vDivs  );
    Vec_IntFreeP( &p->vRoots );
    Vec_IntFreeP( &p->vTfo   );
    Vec_WrdFreeP( &p->vDivCexes );
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vDivVars );
    Vec_IntFreeP( &p->vDivIds );
    Vec_IntFreeP( &p->vLits  );
    Vec_IntFreeP( &p->vValues );
    Vec_WecFreeP( &p->vClauses );
    Vec_IntFreeP( &p->vFaninMap );
    if ( p->pSat  ) sat_solver_delete( p->pSat );
    ABC_FREE( p );
}

int Sfm_NtkPerform	(	Sfm_Ntk_t *	p,
		Sfm_Par_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file sfmCore.c.

{
    int i, k, Counter = 0;
    p->timeTotal = Abc_Clock();
    if ( pPars->fVerbose )
    {
        int nFixed = p->vFixed ? Vec_StrSum(p->vFixed) : 0;
        int nEmpty = p->vEmpty ? Vec_StrSum(p->vEmpty) : 0;
        printf( "Performing MFS with %d PIs, %d POs, %d nodes (%d flexible, %d fixed, %d empty).\n", 
            p->nPis, p->nPos, p->nNodes, p->nNodes-nFixed, nFixed, nEmpty );
    }
    p->pPars = pPars;
    Sfm_NtkPrepare( p );
//    Sfm_ComputeInterpolantCheck( p );
//    return 0;
    p->nTotalNodesBeg = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
    p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
    Sfm_NtkForEachNode( p, i )
    {
        if ( Sfm_ObjIsFixed( p, i ) )
            continue;
        if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
            continue;
        if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
            continue;
        for ( k = 0; Sfm_NodeResub(p, i); k++ )
        {
//            Counter++;
//            break;
        }
        Counter += (k > 0);
        if ( pPars->nNodesMax && Counter >= pPars->nNodesMax )
            break;
    }
    p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
    p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
    p->timeTotal = Abc_Clock() - p->timeTotal;
    if ( pPars->fVerbose )
        Sfm_NtkPrintStats( p );
    return Counter;
}

void Sfm_ParSetDefault

(

Sfm_Par_t *

pPars

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

FileName [sfmCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Setup parameter structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sfmCore.c.

{
    memset( pPars, 0, sizeof(Sfm_Par_t) );
    pPars->nTfoLevMax   =    2;  // the maximum fanout levels
    pPars->nFanoutMax   =   30;  // the maximum number of fanouts
    pPars->nDepthMax    =   20;  // the maximum depth to try  
    pPars->nWinSizeMax  =  300;  // the maximum window size
    pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
    pPars->nBTLimit     = 5000;  // the maximum number of conflicts in one SAT run
    pPars->fRrOnly      =    0;  // perform redundancy removal
    pPars->fArea        =    0;  // performs optimization for area
    pPars->fMoreEffort  =    0;  // performs high-affort minimization
    pPars->fVerbose     =    0;  // enable basic stats
    pPars->fVeryVerbose =    0;  // enable detailed stats
}