src/restr/restrDebug.c

Go to the documentation of this file.

#include "restrInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

void
RestrNamePrintByMddId(
  Ntk_Network_t *network,
  array_t       *array)

{
  char *name;
  int i,id;

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

void
RestrPrintMvfArray(
  mdd_manager    *ddManager,
  Mvf_Function_t *mvfArray,
  array_t        *nodeArray,
  array_t        *idArray)
{
  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);
  }
}

void
RestrPrintAllVarNames(
  bdd_manager   *ddManager)
{
  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)
{
    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;
}

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)
{
  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);
}

void
RestrTestIsEquivRelation(
  bdd_manager *ddManager,
  bdd_node *rel,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **uVars,
  bdd_node **vVars,
  int nVars)
{
  
  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
RestrPrintVarArrayNames(
  bdd_manager *ddManager,
  bdd_node **xVars,
  int nVars)
{
  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");
}

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

int
RestrTestIsDeterministic(
  bdd_manager *ddManager,
  bdd_node *tr,
  bdd_node *initBdd,
  bdd_node **xVars,
  bdd_node **yVars,
  int nVars)
{
  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;
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/