VIS
|
#include "restrInt.h"
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) |
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); } }
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;
}
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); } }
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; }
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); }