#include "restrInt.h"

Include dependency graph for restrUtil.c:

Functions
array_t *	RestrGetOutputArray (Ntk_Network_t *network)
bdd_node *	RestrCreateProductOutput (bdd_manager ddManager, array_t funArray, bdd_node xVars, bdd_node yVars, int nVars)
array_t *	RestrComputeTRWithIds (bdd_manager ddManager, array_t nextBdds, bdd_node xVars, bdd_node yVars, bdd_node uVars, bdd_node vVars, int nVars)
bdd_node *	RestrGetEquivRelation (bdd_manager mgr, bdd_node Lambda, bdd_node tranRelation, bdd_node xVars, bdd_node yVars, bdd_node uVars, bdd_node vVars, bdd_node *piVars, int nVars, int nPi, boolean restrVerbose)
bdd_node *	RestrComputeEquivRelationUsingCofactors (bdd_manager mgr, bdd_node Lambda, bdd_node TR, bdd_node xVars, bdd_node yVars, bdd_node uVars, bdd_node vVars, bdd_node *piVars, int nVars, int nPi, boolean restrVerbose)
bdd_node *	RestrComputeTrWithGhostEdges (bdd_manager mgr, bdd_node yVars, bdd_node vVars, bdd_node tr, bdd_node *equivRelation, int nVars)
bdd_node *	RestrAddMaximum (bdd_manager ddManager, bdd_node f, bdd_node *g)
bdd_node *	RestrAddEqual (bdd_manager ddManager, bdd_node f, bdd_node *g)
bdd_node **	RestrBddNodeArrayFromIdArray (bdd_manager ddManager, array_t idArray)
double	RestrAverageBitChange (bdd_manager manager, bdd_node probTR, bdd_node xVars, bdd_node yVars, int nVars)
array_t *	RestrCreateNewStateVars (Ntk_Network_t network, bdd_manager ddManager, bdd_node xVars, bdd_node yVars)
void	RestrSetInitialOrder (Ntk_Network_t network, bdd_manager ddManager)

Function Documentation

bdd_node* RestrAddEqual	(	bdd_manager *	ddManager,
		bdd_node **	f,
		bdd_node **	g
	)

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

Synopsis [Returns a 0-1 ADD containing minterms such that the discriminant for those minterms in f is equal to that in g.]

Description [Returns a 0-1 ADD containing minterms such that the discriminant for those minterms in f is equal to that in g.]

SideEffects [None]

SeeAlso [cuddAddApply.c]

Definition at line 559 of file restrUtil.c.

{
  bdd_node *zero, *one;

  zero = bdd_read_zero(ddManager);
  one = bdd_read_one(ddManager);

  if(*f == *g) {
    return one;
  }

  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
      return zero;
  }
  return NULL;
}

Here is the caller graph for this function:

bdd_node* RestrAddMaximum	(	bdd_manager *	ddManager,
		bdd_node **	f,
		bdd_node **	g
	)

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

Synopsis [Returns a 0-1 ADD containing minterms such that the discriminant for those minterms in f is greater than that in g.]

Description [Returns a 0-1 ADD containing minterms such that the discriminant for those minterms in f is greater than that in g.]

SideEffects [None]

SeeAlso [cuddAddApply.c]

Definition at line 518 of file restrUtil.c.

{
  bdd_node *plusInf;
  bdd_node *zero, *one;

  zero = bdd_read_zero(ddManager);
  one = bdd_read_one(ddManager);
  plusInf = bdd_read_plus_infinity(ddManager);

  if(*g == plusInf) {
    return zero;
  }

  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
    if(bdd_add_value(*f) > bdd_add_value(*g)) {
      return one;
    } else {
      return zero;
    }
  }
  return NULL;
}

Here is the caller graph for this function:

double RestrAverageBitChange	(	bdd_manager *	manager,
		bdd_node *	probTR,
		bdd_node **	xVars,
		bdd_node **	yVars,
		int	nVars
	)

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

Synopsis [Calculate the average bit change in the STG.]

Description [Calculate the average bit change in the STG. probTR is an ADD representing the absolute transition probability matrix of the STG. xVars and yVars are the present and next state variables respectively. nVars is the number of state variables.

average bit change = (^+_x(probTr * HD(x,y))). ]

SideEffects [None]

SeeAlso []

Definition at line 629 of file restrUtil.c.

{
  bdd_node *diff, *cube, *PA, *QA;
  bdd_node **vars;
  double Mean;
  int i;

  vars = ALLOC(bdd_node *,2*nVars);
  for (i = 0; i < nVars; i++) {
    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i]));
    bdd_ref(vars[i]);
  }
  for (i = nVars; i < 2*nVars; i++) {
    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars]));
    bdd_ref(vars[i]);
  }

  cube = bdd_add_compute_cube(manager,vars,NIL(int),2*nVars);
  bdd_ref(cube);

  /* Calculate the Hamming distance ADD. This ADD represents the hamming
   * distance between two vectors represented by xVars and yVars.
   */
  bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars));
  bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff));
  bdd_recursive_deref(manager,diff);
  
  /* And now add and abstract all the variables.*/
  bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube));
  bdd_recursive_deref(manager,PA);
  bdd_recursive_deref(manager,cube);
  Mean = (double)bdd_add_value(QA);
  bdd_recursive_deref(manager,QA); 

  for (i = 0; i < 2*nVars; i++) {
    bdd_recursive_deref(manager,vars[i]);
  }
  FREE(vars);
  return Mean;
}

Here is the caller graph for this function:

bdd_node** RestrBddNodeArrayFromIdArray	(	bdd_manager *	ddManager,
		array_t *	idArray
	)

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

Synopsis [Given an array of BDD ids, return the array of corresponding BDDs.]

Description [Given an array of BDD ids, return the array of corresponding BDDs.]

SideEffects [None]

SeeAlso []

Definition at line 593 of file restrUtil.c.

{
  bdd_node **xvars;
  int i,id;
  int nvars = array_n(idArray);

  xvars = ALLOC(bdd_node *, nvars);
  if (xvars == NULL)
    return NULL;

  for(i = 0; i < nvars; i++) {
    id = array_fetch(int,idArray,i);
    xvars[i] = bdd_bdd_ith_var(ddManager,id);
    bdd_ref(xvars[i]);
  }
  return xvars;
}

Here is the caller graph for this function:

bdd_node* RestrComputeEquivRelationUsingCofactors	(	bdd_manager *	mgr,
		bdd_node *	Lambda,
		bdd_node *	TR,
		bdd_node **	xVars,
		bdd_node **	yVars,
		bdd_node **	uVars,
		bdd_node **	vVars,
		bdd_node **	piVars,
		int	nVars,
		int	nPi,
		boolean	restrVerbose
	)

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

Synopsis [This function returns the state equivalence relation for an FSM.]

Description [This function returns the state equivalence relation for an FSM. Lambda is the primary output relation and TR is the state transition relation of the product machine. Lambda has xVars, uVars and piVars in its support. TR has piVars, xVars,yVars,uVars and vVars in its support. nPi is the number of piVars and nVars is the number of xVars. xVars, yVars, uVars and vVars are all of the same size, i.e., nVars. The returned BDD is a function of xVars and uVars.

For more information on the algorithm, please refer to "Extending Equivalence Class Computation to Large FSMs", ICCD 96.]

SideEffects []

SeeAlso [RestrGetEquivRelation]

Definition at line 347 of file restrUtil.c.

{
  bdd_node *espKxu, *espKyv, *espKPlusOne, *espKMinusOne;
  bdd_node *espKCofKMinusOne;
  bdd_node *inputCube, *nextCube;
  bdd_node *tranRelation;
  bdd_node *newTran;
  bdd_node **allPreVars, **allNexVars;
  int i,depth;

  bdd_ref(tranRelation = TR);

  allPreVars = ALLOC(bdd_node *, 2*nVars);
  allNexVars = ALLOC(bdd_node *, 2*nVars);
  for(i = 0; i < nVars;i++) {
    allPreVars[i] = xVars[i];
    allNexVars[i] = yVars[i];
  } 
  for(i = 0; i < nVars;i++) {
    allPreVars[i+nVars] = uVars[i];
    allNexVars[i+nVars] = vVars[i];
  } 

  /* nextCube is a cube of yVars and vVars */
  nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
  bdd_ref(nextCube);

  /* inputCube is a cube of piVars */
  inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
  bdd_ref(inputCube);

  /* espKxu = \forall_{piVars} Lambda */
  espKxu = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
  bdd_ref(espKxu);

  espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
                                  allNexVars,2*nVars);
  bdd_ref(espKyv);
  bdd_ref(espKMinusOne = bdd_read_one(mgr));
  bdd_ref(espKPlusOne = bdd_read_one(mgr));

  /* The following loop is essentially the following:
   * E_{k+1} = E_k \wedge (\forall_x(func)) where
   * func = \exists_{yv} ((TR \downarrow E_k) \wedge (E_k \downarrow E_{k-1}))
   */
  depth = 0;
  while (1) {
    bdd_node *image, *temp1;
        
    bdd_recursive_deref(mgr, espKPlusOne);
    bdd_ref(espKCofKMinusOne = bdd_bdd_constrain(mgr, espKyv, 
                                                 espKMinusOne));
    bdd_recursive_deref(mgr, espKMinusOne);
    bdd_ref(espKMinusOne = espKyv);

    bdd_ref(newTran = bdd_bdd_constrain(mgr, tranRelation, espKxu));

    image = bdd_bdd_and_abstract(mgr,newTran, espKCofKMinusOne, nextCube);
    bdd_ref(image);
    bdd_recursive_deref(mgr, newTran);
    bdd_recursive_deref(mgr, espKCofKMinusOne);

    temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
    bdd_ref(temp1);
    bdd_recursive_deref(mgr,image);
    espKPlusOne = bdd_bdd_and(mgr,temp1,espKxu);
    bdd_ref(espKPlusOne);
    bdd_recursive_deref(mgr,temp1);

    if (espKPlusOne == espKxu) {
      bdd_recursive_deref(mgr,espKMinusOne);
      bdd_recursive_deref(mgr,espKxu);
      bdd_recursive_deref(mgr,espKyv);
      bdd_recursive_deref(mgr,tranRelation);
      bdd_recursive_deref(mgr,inputCube);
      bdd_recursive_deref(mgr,nextCube);
      FREE(allPreVars);
      FREE(allNexVars);
      if (restrVerbose) {
        (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
                       depth);
      }
      return espKPlusOne;
    }

    bdd_recursive_deref(mgr, espKxu);
    bdd_ref(espKxu = espKPlusOne);
    bdd_recursive_deref(mgr, espKyv);
    espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
                                    allNexVars,2*nVars);
    bdd_ref(espKyv);
        
    depth++;
  }

}

Here is the caller graph for this function:

bdd_node* RestrComputeTrWithGhostEdges	(	bdd_manager *	mgr,
		bdd_node **	yVars,
		bdd_node **	vVars,
		bdd_node *	tr,
		bdd_node *	equivRelation,
		int	nVars
	)

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

Synopsis [Returns the BDD for the augmented tr.]

Description [Returns the BDD for the augmented tr. The procedure of augmentation is as follows: If there exists a pair (x,y) in tr and a pair (y,v) in equivRelation, then the augmented tr has an additional pair (x,v) added to it. The newly added edges are called 'ghost edges'. Moreover, tr is a function of xVars and yVars, while equivRelation is a function of yVars and vVars. nVars is the size of yVars and vVars each. The returned BDD has the same support variables as tr.

The boolean formulation is:

T^a(x,y) = E(y,z) T(x,z)]

SideEffects [None]

SeeAlso []

Definition at line 479 of file restrUtil.c.

{
  bdd_node *abstractCube;
  bdd_node *temp;
  bdd_node *ghostTR;

  abstractCube = bdd_bdd_compute_cube(mgr,yVars,NIL(int),nVars);
  bdd_ref(abstractCube);

  temp = bdd_bdd_and_abstract(mgr,tr,equivRelation,abstractCube);
  bdd_ref(temp);
  bdd_recursive_deref(mgr,abstractCube);

  ghostTR = bdd_bdd_swap_variables(mgr,temp,vVars,yVars,nVars);
  bdd_ref(ghostTR);
  bdd_recursive_deref(mgr,temp);

  return ghostTR;
}

Here is the caller graph for this function:

array_t* RestrComputeTRWithIds	(	bdd_manager *	ddManager,
		array_t *	nextBdds,
		bdd_node **	xVars,
		bdd_node **	yVars,
		bdd_node **	uVars,
		bdd_node **	vVars,
		int	nVars
	)

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

Synopsis [The function computes the following relations: {i=0}^{i=n-1} (y_i f_i(x)) and {i=0}^{i=n-1} (y_i f_i(x)) (v_i f_i(u)) and returns them in an array.]

Description [The function computes the following relations: {i=0}^{i=n-1} (y_i f_i(x)) and {i=0}^{i=n-1} (y_i f_i(x)) (v_i f_i(u)) and returns them in an array.

nextBdds is an array of nVar BDDs and has xVars in its support. xVars, yVars, uVars and vVars are arrays of BDD variables.]

SideEffects [None]

SeeAlso [RestrCreateProductOutput]

Definition at line 163 of file restrUtil.c.

{
  bdd_node      *ddtemp1, *ddtemp2;
  bdd_node      *oldTR, *fn;
  array_t       *composite;
  int            i;


  /* First compute oldTR(x,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) */
  bdd_ref(oldTR = bdd_read_one(ddManager));

  for(i = 0; i < nVars; i++) {
    ddtemp2  = array_fetch(bdd_node *, nextBdds, i);

    fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
    bdd_ref(fn);
    ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
    bdd_ref(ddtemp1);
    bdd_recursive_deref(ddManager,fn);
    bdd_recursive_deref(ddManager,oldTR);
    oldTR = ddtemp1;
  }
  
  /* fn(u,v) = oldTR(x-->u,y-->v) */
  ddtemp2 = bdd_bdd_swap_variables(ddManager,oldTR,xVars,uVars,nVars);
  bdd_ref(ddtemp2);
  fn = bdd_bdd_swap_variables(ddManager,ddtemp2,yVars,vVars,nVars);
  bdd_ref(fn);
  bdd_recursive_deref(ddManager,ddtemp2);
  ddtemp1 = bdd_bdd_and(ddManager,fn,oldTR);
  bdd_ref(ddtemp1);
  bdd_recursive_deref(ddManager,fn);

  /* Return both the relations */
  composite = array_alloc(bdd_node *,0);
  array_insert_last(bdd_node *,composite,oldTR);
  array_insert_last(bdd_node *,composite,ddtemp1);

  return composite;
}

Here is the caller graph for this function:

array_t* RestrCreateNewStateVars	(	Ntk_Network_t *	network,
		bdd_manager *	ddManager,
		bdd_node **	xVars,
		bdd_node **	yVars
	)

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

Synopsis [Create an extra set of auxillary BDD variables--corresponding to present and next state variables of the network--required during restructuring.]

SideEffects [None]

SeeAlso []

Definition at line 687 of file restrUtil.c.

{
  Ntk_Node_t *node1;
  char *name, *name1;
  array_t *varValues;
  array_t *nameArray;
  int i,id,index;
  int nVars = Ntk_NetworkReadNumLatches(network);

  array_t *uVarIds, *vVarIds;
  array_t *result;

  varValues = array_alloc(int, 0);
  nameArray = array_alloc(char *,0);    
  uVarIds = array_alloc(int, 0);
  vVarIds = array_alloc(int, 0);
  result = array_alloc(array_t *, 0);

  id = bdd_num_vars(ddManager);

  for (i = 0; i < nVars; i++) {
    index = bdd_node_read_index(yVars[i]);
    node1 = Ntk_NetworkFindNodeByMddId(network,index);
    name = Ntk_NodeReadName(node1);
    name1 = util_strcat3(name,"$NTK2","");
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name1);
    array_insert_last(int, vVarIds, id);
    id++;

    index = bdd_node_read_index(xVars[i]);
    node1 = Ntk_NetworkFindNodeByMddId(network,index);
    name = Ntk_NodeReadName(node1);
    name1 = util_strcat3(name,"$NTK2","");
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name1);
    array_insert_last(int, uVarIds, id);
    id++;

  }
  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));

  arrayForEachItem(char *,nameArray,i,name) {
    FREE(name);
  }
  array_free(nameArray);
  array_free(varValues);

  array_insert_last(array_t *, result, uVarIds);
  array_insert_last(array_t *, result, vVarIds);

  return result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bdd_node* RestrCreateProductOutput	(	bdd_manager *	ddManager,
		array_t *	funArray,
		bdd_node **	xVars,
		bdd_node **	yVars,
		int	nVars
	)

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

Synopsis [Computes the product {i=0}^{i=n-1} funArray_{i}(x) funArray_{i}(y)]

Description [Computes the product {i=0}^{i=n-1} funArray_{i}(x) funArray_{i}(y).

funArray is an array of BDDs and each has xVars in its support. nVars is the number of xVars and yVars.]

SideEffects [None]

SeeAlso [RestrComputeTRWithIds]

Definition at line 110 of file restrUtil.c.

{
  bdd_node      *ddtemp, *ddtemp1;
  bdd_node      *fn, *result;
  int           i, num = array_n(funArray);

  bdd_ref(result = bdd_read_one(ddManager));

  for(i = 0; i < num; i++) {

    ddtemp = array_fetch(bdd_node *, funArray, i);;

    ddtemp1 = bdd_bdd_swap_variables(ddManager,ddtemp,xVars,yVars,nVars);
    bdd_ref(ddtemp1);
    fn = bdd_bdd_xnor(ddManager,ddtemp1,ddtemp);
    bdd_ref(fn);
    bdd_recursive_deref(ddManager,ddtemp1);
    ddtemp1 = bdd_bdd_and(ddManager,result,fn);
    bdd_ref(ddtemp1);
    bdd_recursive_deref(ddManager,fn);
    bdd_recursive_deref(ddManager,result);
    result = ddtemp1;
  }

  return result;
}

Here is the caller graph for this function:

bdd_node* RestrGetEquivRelation	(	bdd_manager *	mgr,
		bdd_node *	Lambda,
		bdd_node *	tranRelation,
		bdd_node **	xVars,
		bdd_node **	yVars,
		bdd_node **	uVars,
		bdd_node **	vVars,
		bdd_node **	piVars,
		int	nVars,
		int	nPi,
		boolean	restrVerbose
	)

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

Synopsis [This function returns the state equivalence relation for an FSM.]

Description [This function returns the state equivalence relation for an FSM. Lambda is the primary output relation and TR is the state transition relation of the product machine. Lambda has xVars, uVars and piVars in its support. TR has piVars, xVars,yVars,uVars and vVars in its support. nPi is the number of piVars and nVars is the number of xVars. xVars, yVars, uVars and vVars are all of the same size, i.e., nVars. The returned BDD is a function of xVars and uVars.

For more information on the algorithm, please refer to "Dont care minimization of multi-level sequential logic networks", ICCAD 90.]

SideEffects [None]

SeeAlso [RestrComputeEquivRelationUsingCofactors]

Definition at line 233 of file restrUtil.c.

{
    bdd_node *initialEsp, *espK;
    bdd_node *espKPlusOne;
    bdd_node *inputCube, *nextCube;
    bdd_node **allPreVars, **allNexVars;
    bdd_node *temp;
    int i,depth;

    allPreVars = ALLOC(bdd_node *, 2*nVars);
    allNexVars = ALLOC(bdd_node *, 2*nVars);
    for(i = 0; i < nVars;i++) {
        allPreVars[i] = xVars[i];
        allNexVars[i] = yVars[i];
    } 
    for(i = 0; i < nVars;i++) {
        allPreVars[i+nVars] = uVars[i];
        allNexVars[i+nVars] = vVars[i];
    } 

    nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
    bdd_ref(nextCube);

    inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
    bdd_ref(inputCube);

    initialEsp = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
    bdd_ref(initialEsp);

    espK = bdd_bdd_swap_variables(mgr,initialEsp,allPreVars,
                                 allNexVars,2*nVars);
    bdd_ref(espK);
    
    depth = 0;
    do {
        bdd_node *image, *temp1;
        image = bdd_bdd_and_abstract(mgr,tranRelation, espK, nextCube);
        bdd_ref(image);

        temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
        bdd_ref(temp1);
        bdd_recursive_deref(mgr,image);

        espKPlusOne = bdd_bdd_and(mgr,temp1,initialEsp);
        bdd_ref(espKPlusOne);
        bdd_recursive_deref(mgr,temp1);
        temp1 = bdd_bdd_swap_variables(mgr,espKPlusOne,allPreVars,
                                     allNexVars,2*nVars);
        bdd_ref(temp1);
        bdd_recursive_deref(mgr,espKPlusOne);
        espKPlusOne = temp1;
        
        if (espKPlusOne == espK) {
          break;
        }
        bdd_recursive_deref(mgr,espK);
        espK = espKPlusOne;
        depth++;
    } while (1);

    if (restrVerbose)
      (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
                     depth);

    bdd_recursive_deref(mgr,espKPlusOne);
    bdd_recursive_deref(mgr,initialEsp);
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,nextCube);

    bdd_ref(temp = bdd_bdd_swap_variables(mgr,espK,allNexVars,
                                          allPreVars,2*nVars));
    bdd_recursive_deref(mgr,espK);
    espK = temp;

    FREE(allPreVars);
    FREE(allNexVars);

    return espK;
}

Here is the caller graph for this function:

array_t* RestrGetOutputArray ( Ntk_Network_t * network )

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

FileName [restrUtil.c]

PackageName [restr]

Synopsis [Support functions used in the package.]

Description [Support functions used in the package.]

SeeAlso [restrDebug.c]

Author [Balakrishna Kumthekar <kumtheka@colorado.edu>]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Returns the primary output node array for the given network.]

Description [Returns the primary output node array for the given network.]

SideEffects [None]

SeeAlso [RestrGetNextStateArray]

Definition at line 79 of file restrUtil.c.

{
    lsGen                gen;
    Ntk_Node_t  *node;
    array_t     *outputArray;

    outputArray = array_alloc(char *, 0);
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
        array_insert_last(char *, outputArray, Ntk_NodeReadName(node));
    }

    return outputArray;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void RestrSetInitialOrder	(	Ntk_Network_t *	network,
		bdd_manager *	ddManager
	)

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

Synopsis [In the absence of initial order of the variables, this function assings MDD Ids to the input, present state and next state variables.]

Description [In the absence of initial order of the variables, this function assigns MDD Ids to the input, present state and next state variables.

This procedure is NOT currently used and is here for future purposes.]

SideEffects [The BDD manager is changed accordingly.]

SeeAlso []

Definition at line 764 of file restrUtil.c.

{
  Ntk_Node_t *node, *node1;
  lsGen gen;
  char *name;
  array_t       *varValues;
  array_t       *nameArray;
  int           id;

  varValues = array_alloc(int,0);
  nameArray = array_alloc(char *,0);

  id = 0;
  Ntk_NetworkForEachLatch(network,gen,node) {
    node1 = Ntk_NodeReadShadow(node);
    name = util_strsav(Ntk_NodeReadName(node1));
    Ntk_NodeSetMddId(node1,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;

    name = util_strsav(Ntk_NodeReadName(node));
    Ntk_NodeSetMddId(node,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;
  }

  Ntk_NetworkForEachPrimaryInput(network,gen,node) {
    name = util_strsav(Ntk_NodeReadName(node));
    Ntk_NodeSetMddId(node,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;
  }

  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));

  id = 0;
  arrayForEachItem(char *, nameArray, id, name) {
    FREE(name);
  }
  array_free(nameArray);
  array_free(varValues);

}

Here is the call graph for this function:

src/restr/restrUtil.c File Reference

Functions

Function Documentation