src/restr/restrDebug.c File Reference

#include "restrInt.h"

Include dependency graph for restrDebug.c:

Go to the source code of this file.

Functions
void	RestrNamePrintByMddId (Ntk_Network_t *network, array_t *array)
void	RestrPrintMvfArray (mdd_manager *ddManager, Mvf_Function_t *mvfArray, array_t *nodeArray, array_t *idArray)
void	RestrPrintAllVarNames (bdd_manager *ddManager)
void	RestrPrintBddNode (bdd_manager *manager, bdd_node *ddNode)
void	RestrVerifyFsmEquivBySimulation (bdd_manager *ddManager, bdd_node *oldTr, bdd_node *newTr, array_t *outBdds1, array_t *outBdds2, bdd_node *initBdd1, bdd_node *initBdd2, bdd_node **xVars, bdd_node **yVars, bdd_node **piVars, int nVars, int nPi)
void	RestrTestIsEquivRelation (bdd_manager *ddManager, bdd_node *rel, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, int nVars)
void	RestrPrintVarArrayNames (bdd_manager *ddManager, bdd_node **xVars, int nVars)
void	RestrPrintNameArray (array_t *nameArray)
int	RestrTestIsDeterministic (bdd_manager *ddManager, bdd_node *tr, bdd_node *initBdd, bdd_node **xVars, bdd_node **yVars, int nVars)

---

Function Documentation

void RestrNamePrintByMddId	(	Ntk_Network_t *	network,
		array_t *	array
	)

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

FileName [restrDebug.c]

PackageName [restr]

Synopsis [Utility functions to aid in debugging.]

Description [Utility functions to aid in debugging.]

SeeAlso [restrUtil.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 [Print names of network nodes given their id.]

SideEffects [Print names of network nodes given their id.]

SeeAlso []

Definition at line 79 of file restrDebug.c.

{
  char *name;
  int i,id;

  arrayForEachItem(int, array, i, id) {
    name = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(network,id));
    fprintf(vis_stdout, "%s\n",name);
  }
}

Here is the call graph for this function:

void RestrPrintAllVarNames

(

bdd_manager *

ddManager

)

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

Synopsis [Prints the variable names of all variables in the manager.]

SideEffects [Prints the variable names of all variables in the manager]

SeeAlso []

Definition at line 139 of file restrDebug.c.

{
  int size, i;
  mvar_type var;
  size = bdd_num_vars((bdd_manager *)ddManager);
  for(i=0;i<size;i++) {
    var = mdd_get_var_by_id(ddManager,i);
    fprintf(vis_stdout," %s",var.name);
  }
  fprintf(vis_stdout,"\n");
}

void RestrPrintBddNode	(	bdd_manager *	manager,
		bdd_node *	ddNode
	)

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

Synopsis [Print minterms in the onset given a bdd_node *.]

SideEffects [Print minterms in the onset given a bdd_node *.]

SeeAlso []

Definition at line 163 of file restrDebug.c.

{
    bdd_t *mdd;
    bdd_node *temp;
    bdd_ref(temp = ddNode);
    mdd = bdd_construct_bdd_t(manager,temp);
    bdd_print_minterm(mdd);
    bdd_free(mdd);
    return;
}

Here is the caller graph for this function:

void RestrPrintMvfArray	(	mdd_manager *	ddManager,
		Mvf_Function_t *	mvfArray,
		array_t *	nodeArray,
		array_t *	idArray
	)

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

Synopsis [Interface function to bdd_print_minterm given an mvf array.]

SideEffects [Interface function to bdd_print_minterm given an mvf array.]

SeeAlso []

Definition at line 103 of file restrDebug.c.

{
  int i;
  mdd_t *tempMdd;
  Mvf_Function_t *mvf;
  Ntk_Node_t    *node;

  for(i=0;i<array_n(mvfArray);i++){
    mvf = array_fetch(Mvf_Function_t *, mvfArray, i);
    tempMdd = array_fetch(mdd_t *, mvf, 1);
    if(!(nodeArray == NIL(array_t))) {
      node = array_fetch(Ntk_Node_t *, nodeArray, i);
      fprintf(vis_stdout, "%s ", Ntk_NodeReadName(node));
    }
    if(!(idArray == NIL(array_t))) {
      fprintf(vis_stdout, " %d", array_fetch(int,idArray,i));
    }
    fprintf(vis_stdout, "\n");
    bdd_print_minterm(tempMdd);
  }
}

Here is the call graph for this function:

void RestrPrintNameArray

(

array_t *

nameArray

)

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

Synopsis [Print an array of character strings.]

SideEffects [None]

SeeAlso []

Definition at line 401 of file restrDebug.c.

{
  int i;
  char *str;
  arrayForEachItem(char *,nameArray,i,str) {
    (void) fprintf(vis_stdout,"%s\n",str);
  }
}

void RestrPrintVarArrayNames	(	bdd_manager *	ddManager,
		bdd_node **	xVars,
		int	nVars
	)

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

Synopsis [Print the names of an array of BDD variables.]

SideEffects [None]

SeeAlso []

Definition at line 375 of file restrDebug.c.

{
  int index, i;
  mvar_type var;

  for(i=0;i<nVars;i++) {
    index = bdd_node_read_index(xVars[i]);
    var = mdd_get_var_by_id(ddManager,index);
    fprintf(vis_stdout," %s",var.name);
  }
  fprintf(vis_stdout,"\n");
}

int RestrTestIsDeterministic	(	bdd_manager *	ddManager,
		bdd_node *	tr,
		bdd_node *	initBdd,
		bdd_node **	xVars,
		bdd_node **	yVars,
		int	nVars
	)

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

Synopsis [Test if the given relation is deterministic.]

SideEffects [None]

SeeAlso []

Definition at line 420 of file restrDebug.c.

{
  bdd_node *cproj2,*ref;
  int flag;

  bdd_ref(ref = bdd_bdd_swap_variables(ddManager,initBdd,xVars,
                                       yVars,nVars));
  bdd_ref(cproj2 = bdd_bdd_cprojection(ddManager,tr,ref));
  if (cproj2 != tr) {
    bdd_node *newEdges;
    (void) fprintf(vis_stdout,"** restr diag: Relation is non-deterministic\n");
    /* Let's find out the newly added edges */
    bdd_ref(newEdges = bdd_bdd_and(ddManager,tr,
                                   bdd_not_bdd_node(cproj2)));
    (void) fprintf(vis_stdout,"** restr diag: New edges are:\n");
    RestrPrintBddNode(ddManager,newEdges);
    bdd_recursive_deref(ddManager,newEdges);
    flag = 0;
  } else {
    (void) fprintf(vis_stdout,"** restr diag: Relation IS deterministic\n");
    flag = 1;
  }
  bdd_recursive_deref(ddManager,cproj2);
  bdd_recursive_deref(ddManager,ref);
  
  return flag;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void RestrTestIsEquivRelation	(	bdd_manager *	ddManager,
		bdd_node *	rel,
		bdd_node **	xVars,
		bdd_node **	yVars,
		bdd_node **	uVars,
		bdd_node **	vVars,
		int	nVars
	)

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

Synopsis [Test if the given relation is an equivalence relation.]

SideEffects [None]

SeeAlso []

Definition at line 297 of file restrDebug.c.

{
  
  bdd_node *one,*reflex;
  bdd_node *Rxy,*Rvy,*Ruy,*Rux;
  bdd_node *left,*result,*uCube;
  bdd_node **compose;
  int numVars,i;

  numVars = bdd_num_vars(ddManager);
  one = bdd_read_one(ddManager);
  
  /* rel is interms of xVars and uVars */
  /* Test if rel is reflexive: R(x,x) == 1 */
  compose = ALLOC(bdd_node *,numVars);
  for (i = 0; i < numVars; i++) {
    compose[i] = bdd_bdd_ith_var(ddManager,i);
  }
  for (i = 0; i < nVars; i++) {
    int index;
    index = bdd_node_read_index(uVars[i]);
    compose[index] = xVars[i];
  }
  bdd_ref(reflex = bdd_bdd_vector_compose(ddManager,rel,compose));
  if (reflex != one) {
    (void) fprintf(vis_stdout,"Relation is not reflexive.\n");
  } else {
    (void) fprintf(vis_stdout,"Relation IS reflexive.\n");
  }
  bdd_recursive_deref(ddManager,reflex);
  FREE(compose);

  /* Test if rel is symmetric: R(x,u) == R(u,x) */
  bdd_ref(Rxy = bdd_bdd_swap_variables(ddManager,rel,uVars,yVars,nVars));
  bdd_ref(Rvy = bdd_bdd_swap_variables(ddManager,Rxy,xVars,vVars,nVars));
  bdd_ref(Ruy = bdd_bdd_swap_variables(ddManager,Rvy,vVars,uVars,nVars));
  bdd_ref(Rux = bdd_bdd_swap_variables(ddManager,Ruy,yVars,xVars,nVars));
  bdd_recursive_deref(ddManager,Rvy);
  if (Rux != rel) {
    (void) fprintf(vis_stdout,"Relation is not symmetric.\n");
  } else {
    (void) fprintf(vis_stdout,"Relation IS symmetric.\n");
  }
  bdd_recursive_deref(ddManager,Rux);
  
  /* Test if rel is transitive: (\exists_u R(x,u) * R(u,y)) ==> R(x,y) */
  bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
  bdd_ref(left = bdd_bdd_and_abstract(ddManager,rel,Ruy,uCube));
  bdd_recursive_deref(ddManager,Ruy);
  bdd_recursive_deref(ddManager,uCube);
  bdd_ref(result = bdd_bdd_ite(ddManager,left,Rxy,one));
  bdd_recursive_deref(ddManager,Rxy);
  bdd_recursive_deref(ddManager,left);
  if (result != one) {
    (void) fprintf(vis_stdout,"Relation is not transitive.\n");
  } else {
    (void) fprintf(vis_stdout,"Relation IS transitive.\n");
  }
  bdd_recursive_deref(ddManager,result);
}

void RestrVerifyFsmEquivBySimulation	(	bdd_manager *	ddManager,
		bdd_node *	oldTr,
		bdd_node *	newTr,
		array_t *	outBdds1,
		array_t *	outBdds2,
		bdd_node *	initBdd1,
		bdd_node *	initBdd2,
		bdd_node **	xVars,
		bdd_node **	yVars,
		bdd_node **	piVars,
		int	nVars,
		int	nPi
	)

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

Synopsis [Perform token simulations to check functional equivalence of two STGs.]

SideEffects [None]

SeeAlso []

Definition at line 187 of file restrDebug.c.

{
  int **sim, N = 11;
  int i,j,numOut1,numOut2;
  bdd_node *lambda1,*lambda2;
  bdd_node **lVars;
  bdd_node *present1,*present2,*next1,*next2;
  bdd_node *out1,*out2;
  bdd_node *input,*inputPre1,*inputPre2;

  sim = ALLOC(int *,N);
  for (i = 0; i < N; i++) {
    sim[i] = ALLOC(int,nPi);
    for (j = 0; j < nPi; j++) {
      sim[i][j] = 0;
    }
  }
  
  numOut1 = array_n(outBdds1);
  numOut2 = array_n(outBdds2);
  assert(numOut1 == numOut2);

  /* New variables to compute output relation */
  lVars = ALLOC(bdd_node *,numOut1);
  for (i = 0; i < numOut1; i++) {
    bdd_ref(lVars[i] = bdd_bdd_new_var(ddManager));
  }

  bdd_ref(lambda1 = bdd_read_one(ddManager));
  bdd_ref(lambda2 = bdd_read_one(ddManager));
  for (i = 0; i < numOut1; i++) {
    bdd_node *temp,*outRel;
    bdd_ref(outRel = bdd_bdd_xnor(ddManager,lVars[i],
                                  array_fetch(bdd_node *,outBdds1,i)));
    bdd_ref(temp = bdd_bdd_and(ddManager,lambda1,outRel));
    bdd_recursive_deref(ddManager,outRel);
    bdd_recursive_deref(ddManager,lambda1);
    lambda1 = temp;

    bdd_ref(outRel = bdd_bdd_xnor(ddManager,lVars[i],
                                  array_fetch(bdd_node *,outBdds2,i)));
    bdd_ref(temp = bdd_bdd_and(ddManager,lambda2,outRel));
    bdd_recursive_deref(ddManager,outRel);
    bdd_recursive_deref(ddManager,lambda2);
    lambda2 = temp;
  }

  bdd_ref(present1 = initBdd1);
  bdd_ref(present2 = initBdd2);
  /* Simulate the patterns */
  for (i = 0; i < N; i++) {
    bdd_node *temp1;

    bdd_ref(input = bdd_bdd_compute_cube(ddManager,piVars,sim[i],nPi));

    /* Compute next state and outputs for machine 1 */
    bdd_ref(inputPre1 = bdd_bdd_and(ddManager,input,present1));
    bdd_ref(temp1 = bdd_bdd_cofactor(ddManager,oldTr,inputPre1));
    bdd_ref(next1 = bdd_bdd_swap_variables(ddManager,temp1,yVars,xVars,nVars));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,present1);
    present1 = next1;
    bdd_ref(out1 = bdd_bdd_cofactor(ddManager,lambda1,inputPre1));
    bdd_recursive_deref(ddManager,inputPre1);

    /* Compute next state and outputs for machine 2 */
    bdd_ref(inputPre2 = bdd_bdd_and(ddManager,input,present2));
    bdd_ref(temp1 = bdd_bdd_cofactor(ddManager,newTr,inputPre2));
    bdd_ref(next2 = bdd_bdd_swap_variables(ddManager,temp1,yVars,xVars,nVars));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,present2);
    present2 = next2;
    bdd_ref(out2 = bdd_bdd_cofactor(ddManager,lambda2,inputPre2));
    bdd_recursive_deref(ddManager,inputPre2);
    
    bdd_recursive_deref(ddManager,input);

    if (out1 != out2) {
      (void) fprintf(vis_stdout,"Unequal outputs at i = %d\n",i);
    }
    bdd_recursive_deref(ddManager,out1);
    bdd_recursive_deref(ddManager,out2);
  }

  bdd_recursive_deref(ddManager,present1);
  bdd_recursive_deref(ddManager,present2);
}