source: vis_dev/vis-2.3/src/restr/restrDebug.c

Last change on this file was 14, checked in by cecile, 13 years ago

vis2.3
File size: 13.5 KB
Line 
1/**CFile***********************************************************************
2
3 FileName    [restrDebug.c]
4
5 PackageName [restr]
6
7 Synopsis    [Utility functions to aid in debugging.]
8
9 Description [Utility functions to aid in debugging.]
10
11 SeeAlso     [restrUtil.c]
12
13 Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]
14
15 Copyright   [This file was created at the University of Colorado at
16 Boulder.  The University of Colorado at Boulder makes no warranty
17 about the suitability of this software for any purpose.  It is
18 presented on an AS IS basis.]
19
20******************************************************************************/
21
22#include "restrInt.h"
23
24
25/*---------------------------------------------------------------------------*/
26/* Constant declarations                                                     */
27/*---------------------------------------------------------------------------*/
28
29
30/*---------------------------------------------------------------------------*/
31/* Type declarations                                                         */
32/*---------------------------------------------------------------------------*/
33
34
35/*---------------------------------------------------------------------------*/
36/* Structure declarations                                                    */
37/*---------------------------------------------------------------------------*/
38
39
40/*---------------------------------------------------------------------------*/
41/* Variable declarations                                                     */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Macro declarations                                                        */
47/*---------------------------------------------------------------------------*/
48
49
50/**AutomaticStart*************************************************************/
51
52/*---------------------------------------------------------------------------*/
53/* Static function prototypes                                                */
54/*---------------------------------------------------------------------------*/
55
56
57/**AutomaticEnd***************************************************************/
58
59
60/*---------------------------------------------------------------------------*/
61/* Definition of exported functions                                          */
62/*---------------------------------------------------------------------------*/
63
64
65/*---------------------------------------------------------------------------*/
66/* Definition of internal functions                                          */
67/*---------------------------------------------------------------------------*/
68
69/**Function********************************************************************
70
71  Synopsis [Print names of network nodes given their id.]
72
73  SideEffects [Print names of network nodes given their id.]
74
75  SeeAlso     []
76
77******************************************************************************/
78void
79RestrNamePrintByMddId(
80  Ntk_Network_t *network,
81  array_t       *array)
82
83{
84  char *name;
85  int i,id;
86
87  arrayForEachItem(int, array, i, id) {
88    name = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(network,id));
89    fprintf(vis_stdout, "%s\n",name);
90  }
91}
92
93/**Function********************************************************************
94
95  Synopsis [Interface function to bdd_print_minterm given an mvf array.]
96
97  SideEffects [Interface function to bdd_print_minterm given an mvf array.]
98
99  SeeAlso     []
100
101******************************************************************************/
102void
103RestrPrintMvfArray(
104  mdd_manager    *ddManager,
105  Mvf_Function_t *mvfArray,
106  array_t        *nodeArray,
107  array_t        *idArray)
108{
109  int i;
110  mdd_t *tempMdd;
111  Mvf_Function_t *mvf;
112  Ntk_Node_t    *node;
113
114  for(i=0;i<array_n(mvfArray);i++){
115    mvf = array_fetch(Mvf_Function_t *, mvfArray, i);
116    tempMdd = array_fetch(mdd_t *, mvf, 1);
117    if(!(nodeArray == NIL(array_t))) {
118      node = array_fetch(Ntk_Node_t *, nodeArray, i);
119      fprintf(vis_stdout, "%s ", Ntk_NodeReadName(node));
120    }
121    if(!(idArray == NIL(array_t))) {
122      fprintf(vis_stdout, " %d", array_fetch(int,idArray,i));
123    }
124    fprintf(vis_stdout, "\n");
125    bdd_print_minterm(tempMdd);
126  }
127}
128
129/**Function********************************************************************
130
131  Synopsis [Prints the variable names of all variables in the manager.]
132
133  SideEffects [Prints the variable names of all variables in the manager]
134
135  SeeAlso     []
136
137******************************************************************************/
138void
139RestrPrintAllVarNames(
140  bdd_manager   *ddManager)
141{
142  int size, i;
143  mvar_type var;
144  size = bdd_num_vars((bdd_manager *)ddManager);
145  for(i=0;i<size;i++) {
146    var = mdd_get_var_by_id(ddManager,i);
147    fprintf(vis_stdout," %s",var.name);
148  }
149  fprintf(vis_stdout,"\n");
150}
151
152
153/**Function********************************************************************
154
155  Synopsis [Print minterms in the onset given a bdd_node *.]
156
157  SideEffects [Print minterms in the onset given a bdd_node *.]
158
159  SeeAlso     []
160
161******************************************************************************/
162void
163RestrPrintBddNode(
164  bdd_manager *manager,
165  bdd_node *ddNode)
166{
167    bdd_t *mdd;
168    bdd_node *temp;
169    bdd_ref(temp = ddNode);
170    mdd = bdd_construct_bdd_t(manager,temp);
171    bdd_print_minterm(mdd);
172    bdd_free(mdd);
173    return;
174}
175
176/**Function********************************************************************
177
178  Synopsis [Perform token simulations to check functional equivalence of two
179  STGs.]
180
181  SideEffects [None]
182
183  SeeAlso     []
184
185******************************************************************************/
186void
187RestrVerifyFsmEquivBySimulation(
188  bdd_manager *ddManager,
189  bdd_node *oldTr,
190  bdd_node *newTr,
191  array_t *outBdds1,
192  array_t *outBdds2,
193  bdd_node *initBdd1,
194  bdd_node *initBdd2,
195  bdd_node **xVars,
196  bdd_node **yVars,
197  bdd_node **piVars,
198  int nVars,
199  int nPi)
200{
201  int **sim, N = 11;
202  int i,j,numOut1,numOut2;
203  bdd_node *lambda1,*lambda2;
204  bdd_node **lVars;
205  bdd_node *present1,*present2,*next1,*next2;
206  bdd_node *out1,*out2;
207  bdd_node *input,*inputPre1,*inputPre2;
208
209  sim = ALLOC(int *,N);
210  for (i = 0; i < N; i++) {
211    sim[i] = ALLOC(int,nPi);
212    for (j = 0; j < nPi; j++) {
213      sim[i][j] = 0;
214    }
215  }
216 
217  numOut1 = array_n(outBdds1);
218  numOut2 = array_n(outBdds2);
219  assert(numOut1 == numOut2);
220
221  /* New variables to compute output relation */
222  lVars = ALLOC(bdd_node *,numOut1);
223  for (i = 0; i < numOut1; i++) {
224    bdd_ref(lVars[i] = bdd_bdd_new_var(ddManager));
225  }
226
227  bdd_ref(lambda1 = bdd_read_one(ddManager));
228  bdd_ref(lambda2 = bdd_read_one(ddManager));
229  for (i = 0; i < numOut1; i++) {
230    bdd_node *temp,*outRel;
231    bdd_ref(outRel = bdd_bdd_xnor(ddManager,lVars[i],
232                                  array_fetch(bdd_node *,outBdds1,i)));
233    bdd_ref(temp = bdd_bdd_and(ddManager,lambda1,outRel));
234    bdd_recursive_deref(ddManager,outRel);
235    bdd_recursive_deref(ddManager,lambda1);
236    lambda1 = temp;
237
238    bdd_ref(outRel = bdd_bdd_xnor(ddManager,lVars[i],
239                                  array_fetch(bdd_node *,outBdds2,i)));
240    bdd_ref(temp = bdd_bdd_and(ddManager,lambda2,outRel));
241    bdd_recursive_deref(ddManager,outRel);
242    bdd_recursive_deref(ddManager,lambda2);
243    lambda2 = temp;
244  }
245
246  bdd_ref(present1 = initBdd1);
247  bdd_ref(present2 = initBdd2);
248  /* Simulate the patterns */
249  for (i = 0; i < N; i++) {
250    bdd_node *temp1;
251
252    bdd_ref(input = bdd_bdd_compute_cube(ddManager,piVars,sim[i],nPi));
253
254    /* Compute next state and outputs for machine 1 */
255    bdd_ref(inputPre1 = bdd_bdd_and(ddManager,input,present1));
256    bdd_ref(temp1 = bdd_bdd_cofactor(ddManager,oldTr,inputPre1));
257    bdd_ref(next1 = bdd_bdd_swap_variables(ddManager,temp1,yVars,xVars,nVars));
258    bdd_recursive_deref(ddManager,temp1);
259    bdd_recursive_deref(ddManager,present1);
260    present1 = next1;
261    bdd_ref(out1 = bdd_bdd_cofactor(ddManager,lambda1,inputPre1));
262    bdd_recursive_deref(ddManager,inputPre1);
263
264    /* Compute next state and outputs for machine 2 */
265    bdd_ref(inputPre2 = bdd_bdd_and(ddManager,input,present2));
266    bdd_ref(temp1 = bdd_bdd_cofactor(ddManager,newTr,inputPre2));
267    bdd_ref(next2 = bdd_bdd_swap_variables(ddManager,temp1,yVars,xVars,nVars));
268    bdd_recursive_deref(ddManager,temp1);
269    bdd_recursive_deref(ddManager,present2);
270    present2 = next2;
271    bdd_ref(out2 = bdd_bdd_cofactor(ddManager,lambda2,inputPre2));
272    bdd_recursive_deref(ddManager,inputPre2);
273   
274    bdd_recursive_deref(ddManager,input);
275
276    if (out1 != out2) {
277      (void) fprintf(vis_stdout,"Unequal outputs at i = %d\n",i);
278    }
279    bdd_recursive_deref(ddManager,out1);
280    bdd_recursive_deref(ddManager,out2);
281  }
282
283  bdd_recursive_deref(ddManager,present1);
284  bdd_recursive_deref(ddManager,present2);
285}
286
287/**Function********************************************************************
288
289  Synopsis [Test if the given relation is an equivalence relation.]
290
291  SideEffects [None]
292
293  SeeAlso     []
294
295******************************************************************************/
296void
297RestrTestIsEquivRelation(
298  bdd_manager *ddManager,
299  bdd_node *rel,
300  bdd_node **xVars,
301  bdd_node **yVars,
302  bdd_node **uVars,
303  bdd_node **vVars,
304  int nVars)
305{
306 
307  bdd_node *one,*reflex;
308  bdd_node *Rxy,*Rvy,*Ruy,*Rux;
309  bdd_node *left,*result,*uCube;
310  bdd_node **compose;
311  int numVars,i;
312
313  numVars = bdd_num_vars(ddManager);
314  one = bdd_read_one(ddManager);
315 
316  /* rel is interms of xVars and uVars */
317  /* Test if rel is reflexive: R(x,x) == 1 */
318  compose = ALLOC(bdd_node *,numVars);
319  for (i = 0; i < numVars; i++) {
320    compose[i] = bdd_bdd_ith_var(ddManager,i);
321  }
322  for (i = 0; i < nVars; i++) {
323    int index;
324    index = bdd_node_read_index(uVars[i]);
325    compose[index] = xVars[i];
326  }
327  bdd_ref(reflex = bdd_bdd_vector_compose(ddManager,rel,compose));
328  if (reflex != one) {
329    (void) fprintf(vis_stdout,"Relation is not reflexive.\n");
330  } else {
331    (void) fprintf(vis_stdout,"Relation IS reflexive.\n");
332  }
333  bdd_recursive_deref(ddManager,reflex);
334  FREE(compose);
335
336  /* Test if rel is symmetric: R(x,u) == R(u,x) */
337  bdd_ref(Rxy = bdd_bdd_swap_variables(ddManager,rel,uVars,yVars,nVars));
338  bdd_ref(Rvy = bdd_bdd_swap_variables(ddManager,Rxy,xVars,vVars,nVars));
339  bdd_ref(Ruy = bdd_bdd_swap_variables(ddManager,Rvy,vVars,uVars,nVars));
340  bdd_ref(Rux = bdd_bdd_swap_variables(ddManager,Ruy,yVars,xVars,nVars));
341  bdd_recursive_deref(ddManager,Rvy);
342  if (Rux != rel) {
343    (void) fprintf(vis_stdout,"Relation is not symmetric.\n");
344  } else {
345    (void) fprintf(vis_stdout,"Relation IS symmetric.\n");
346  }
347  bdd_recursive_deref(ddManager,Rux);
348 
349  /* Test if rel is transitive: (\exists_u R(x,u) * R(u,y)) ==> R(x,y) */
350  bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
351  bdd_ref(left = bdd_bdd_and_abstract(ddManager,rel,Ruy,uCube));
352  bdd_recursive_deref(ddManager,Ruy);
353  bdd_recursive_deref(ddManager,uCube);
354  bdd_ref(result = bdd_bdd_ite(ddManager,left,Rxy,one));
355  bdd_recursive_deref(ddManager,Rxy);
356  bdd_recursive_deref(ddManager,left);
357  if (result != one) {
358    (void) fprintf(vis_stdout,"Relation is not transitive.\n");
359  } else {
360    (void) fprintf(vis_stdout,"Relation IS transitive.\n");
361  }
362  bdd_recursive_deref(ddManager,result);
363}
364
365/**Function********************************************************************
366
367  Synopsis [Print the names of an array of BDD variables.]
368
369  SideEffects [None]
370
371  SeeAlso     []
372
373******************************************************************************/
374void
375RestrPrintVarArrayNames(
376  bdd_manager *ddManager,
377  bdd_node **xVars,
378  int nVars)
379{
380  int index, i;
381  mvar_type var;
382
383  for(i=0;i<nVars;i++) {
384    index = bdd_node_read_index(xVars[i]);
385    var = mdd_get_var_by_id(ddManager,index);
386    fprintf(vis_stdout," %s",var.name);
387  }
388  fprintf(vis_stdout,"\n");
389}
390
391/**Function********************************************************************
392
393  Synopsis [Print an array of character strings.]
394
395  SideEffects [None]
396
397  SeeAlso     []
398
399******************************************************************************/
400void
401RestrPrintNameArray(array_t *nameArray)
402{
403  int i;
404  char *str;
405  arrayForEachItem(char *,nameArray,i,str) {
406    (void) fprintf(vis_stdout,"%s\n",str);
407  }
408}
409
410/**Function********************************************************************
411
412  Synopsis [Test if the given relation is deterministic.]
413
414  SideEffects [None]
415
416  SeeAlso     []
417
418******************************************************************************/
419int
420RestrTestIsDeterministic(
421  bdd_manager *ddManager,
422  bdd_node *tr,
423  bdd_node *initBdd,
424  bdd_node **xVars,
425  bdd_node **yVars,
426  int nVars)
427{
428  bdd_node *cproj2,*ref;
429  int flag;
430
431  bdd_ref(ref = bdd_bdd_swap_variables(ddManager,initBdd,xVars,
432                                       yVars,nVars));
433  bdd_ref(cproj2 = bdd_bdd_cprojection(ddManager,tr,ref));
434  if (cproj2 != tr) {
435    bdd_node *newEdges;
436    (void) fprintf(vis_stdout,"** restr diag: Relation is non-deterministic\n");
437    /* Let's find out the newly added edges */
438    bdd_ref(newEdges = bdd_bdd_and(ddManager,tr,
439                                   bdd_not_bdd_node(cproj2)));
440    (void) fprintf(vis_stdout,"** restr diag: New edges are:\n");
441    RestrPrintBddNode(ddManager,newEdges);
442    bdd_recursive_deref(ddManager,newEdges);
443    flag = 0;
444  } else {
445    (void) fprintf(vis_stdout,"** restr diag: Relation IS deterministic\n");
446    flag = 1;
447  }
448  bdd_recursive_deref(ddManager,cproj2);
449  bdd_recursive_deref(ddManager,ref);
450 
451  return flag;
452}
453
454/*---------------------------------------------------------------------------*/
455/* Definition of static functions                                            */
456/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.