source: vis_dev/vis-2.3/src/mark/mark.c@ 40

Last change on this file since 40 was 14, checked in by cecile, 15 years ago

vis2.3
File size: 29.8 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [mark.c]
4
5 PackageName [mark]
6
7 Synopsis [Functions for Markov analysis.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Mark_FsmComputeStateProbs()
12 <li> Mark_ComputeStateProbsWithTr()
13 </ul>
14 Internal procedures included in this module:
15 <ul>
16 <li> MarkAverageBitChange()
17 </ul> ]
18
19 Author [Balakrishna Kumthekar]
20
21 Copyright [This file was created at the University of Colorado at
22 Boulder. The University of Colorado at Boulder makes no warranty
23 about the suitability of this software for any purpose. It is
24 presented on an AS IS basis.]
25
26******************************************************************************/
27
28#include "markInt.h"
29
30static char rcsid[] UNUSED = "$Id: mark.c,v 1.29 2005/04/27 05:24:08 fabio Exp $";
31
32/*---------------------------------------------------------------------------*/
33/* Constant declarations */
34/*---------------------------------------------------------------------------*/
35
36
37/*---------------------------------------------------------------------------*/
38/* Stucture declarations */
39/*---------------------------------------------------------------------------*/
40
41
42/*---------------------------------------------------------------------------*/
43/* Type declarations */
44/*---------------------------------------------------------------------------*/
45
46
47/*---------------------------------------------------------------------------*/
48/* Variable declarations */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Macro declarations */
54/*---------------------------------------------------------------------------*/
55
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Static function prototypes */
61/*---------------------------------------------------------------------------*/
62
63static void ckInterface(CK *ck);
64static bdd_node * recTC(CK *ck, bdd_node *tr);
65static bdd_node * transitiveClosureByIterSquaring(bdd_manager *ddManager, bdd_node *TR, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, int nVars);
66static bdd_node * bddCollapseTSCC(CK *ck);
67static int sccGetPeriod(CK *ck, bdd_node *reset);
68static array_t * markGetBddArray(array_t *mvfArray);
69static bdd_node ** BddNodeArrayFromIdArray(bdd_manager *ddManager, array_t *idArray);
70static bdd_node * computeTransitionRelationWithIds(bdd_manager *ddManager, array_t *nextBdds, bdd_node **yVars, int nVars);
71
72/**AutomaticEnd***************************************************************/
73
74
75/*---------------------------------------------------------------------------*/
76/* Definition of exported functions */
77/*---------------------------------------------------------------------------*/
78
79/**Function********************************************************************
80
81 Synopsis [Perform markovian analysis for Fsm.]
82
83 Description [Performs Markovian analysis on the given FSM. The function
84 takes as an input an FSM and computes the steady state probabilites. The
85 function returns a pair of DdNodes. The first bdd_node is an ADD representing
86 the steady state probabilities. The support of the ADD is the present state
87 variables. The second one is an ADD representing the one-step transition
88 probability matrix. The support of this ADD is both the present state
89 variables and the next state variables.
90
91 The function assumes that the partition of the network representing the
92 FSM, has vertices corresponding to the next state functions. No check is
93 made regarding this. Hence, this function should be called only after
94 creating BDDs for the next state functions.
95
96 solveMethod is one of Solve_GenMethod_c, Solve_FPMethod_c, Solve_CKMethod_c
97 or Solve_Default_c. Currently only Solve_FPMethod_c is supported.
98 Solve_Default_c corresponds to Solve_FPMethod_c.
99
100 startMethod is one of Start_Default_c, Start_Reset_c or Start_EquiProb_c.
101 The default method is Start_Reset_c.
102
103 inputProb is a hash table (<name>,<probability>) of primary inputs. If
104 inputProb is NULL, the primary inputs are assumed to be equi probable.
105 Probability here means the probability of the primary input to be 1.
106
107 roundOff is used to round off the calculations to "roundOff" digits
108 after the decimal.
109
110 The description of algorithms implemented here can be found in <Ref>.]
111
112 SideEffects [Reachability analysis is done.]
113
114 SeeAlso [Mark_ComputeStateProbsWithTr]
115******************************************************************************/
116bdd_node **
117Mark_FsmComputeStateProbs(
118 Fsm_Fsm_t *fsm,
119 Mark_SolveMethod solveMethod,
120 Mark_StartMethod startMethod,
121 st_table *inputProb,
122 int roundOff)
123{
124 graph_t *partition;
125 bdd_manager *ddManager;
126
127 array_t *tranFunArray, *leaveIds;
128 array_t *nextBdds, *nextMvfs;
129
130 int i, phase;
131 int nVars, nPi;
132
133 bdd_node *tranRelation, **result;
134 bdd_node **xVars,**yVars, **piVars;
135 bdd_node *ddTemp, *reachable;
136
137 mdd_t *reachStates;
138
139 if (bdd_get_package_name() != CUDD) {
140 (void) fprintf(vis_stderr,"Synthesis package can be used only with CUDD package\n");
141 (void) fprintf(vis_stderr,"Please compile with CUDD package\n");
142 return 0;
143 }
144
145 if (solveMethod == Solve_CKMethod_c ||
146 solveMethod == Solve_GenMethod_c) {
147 fprintf(vis_stdout,"Mark: Solve_CKMethod_c and Solve_GenMethod_c");
148 fprintf(vis_stdout," not implemented yet\n");
149 return NIL(bdd_node *);
150 }
151
152 ddManager = (bdd_manager *)Fsm_FsmReadMddManager(fsm);
153
154 /*
155 * tranFunArray is a list of next state funs.
156 */
157
158 tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
159
160 leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
161 Fsm_FsmReadPresentStateVars(fsm));
162 /*
163 * Get the BDDs for transition functions.Duplicate functions are returned.
164 */
165 partition = Fsm_FsmReadPartition(fsm);
166 nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
167 NIL(mdd_t));
168 array_free(leaveIds);
169 array_free(tranFunArray);
170 nextBdds = markGetBddArray(nextMvfs);
171
172 Mvf_FunctionArrayFree(nextMvfs);
173
174 /* Get the DdNodes for all the variables.*/
175
176 piVars = BddNodeArrayFromIdArray(ddManager,
177 Fsm_FsmReadInputVars(fsm));
178 xVars = BddNodeArrayFromIdArray(ddManager,
179 Fsm_FsmReadPresentStateVars(fsm));
180 yVars = BddNodeArrayFromIdArray(ddManager,
181 Fsm_FsmReadNextStateVars(fsm));
182
183 nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
184 nPi = array_n(Fsm_FsmReadInputVars(fsm));
185
186 /* Compute the transition relation */
187 tranRelation = computeTransitionRelationWithIds(ddManager, nextBdds,
188 yVars, nVars);
189
190 arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
191 bdd_recursive_deref(ddManager,ddTemp);
192 }
193 array_free(nextBdds);
194
195 /* Compute the reachable states. */
196 reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
197 Fsm_Rch_Default_c,0,0,
198 NIL(array_t),FALSE, NIL(array_t));
199
200 ddTemp = (bdd_node *)bdd_get_node(reachStates,&phase);
201 reachable = phase ? bdd_not_bdd_node(ddTemp) : ddTemp;
202 bdd_ref(reachable);
203 mdd_free(reachStates);
204
205 /* Restrict the STG to only the reachale states */
206 bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,tranRelation,reachable));
207 bdd_recursive_deref(ddManager,tranRelation);
208 tranRelation = ddTemp;
209
210 /* Compute the state probabilities */
211 /* result[0] = state probabilities, result[1] = transition prob. matrix */
212 result = Mark_ComputeStateProbsWithTr(ddManager,tranRelation,
213 reachable,piVars,
214 xVars,yVars,NIL(bdd_node *),inputProb,
215 nVars,nPi,roundOff,
216 solveMethod,startMethod);
217
218 bdd_recursive_deref(ddManager,tranRelation);
219 bdd_recursive_deref(ddManager,reachable);
220
221 for(i = 0; i < nVars; i++) {
222 bdd_recursive_deref(ddManager,xVars[i]);
223 bdd_recursive_deref(ddManager,yVars[i]);
224 }
225 for(i = 0 ; i < nPi; i++) {
226 bdd_recursive_deref(ddManager,piVars[i]);
227 }
228 FREE(xVars);
229 FREE(yVars);
230 FREE(piVars);
231
232 return (result);
233}
234
235/**Function********************************************************************
236
237 Synopsis [Computes the state probabilities of an FSM.]
238
239 Description [Computes the state probabilities of an FSM via Markovian
240 analysis. Returns a pointer to a pair ADDs if successful; The ADD in index
241 0 represents the steady state probabiliites and the ADD in index 1 represents
242 the one step transition probability matrix. NULL is returned in case of a
243 failure.
244
245 TR is the transition relation of the finite state machine. reachable is a
246 BDD of reachable states. piVars, xVars and yVars are the array of primary
247 inputs, present state variables and next state variables. It is optional to
248 specify a set of auxillary variables zVars for internal use. It could be NULL.
249 If specified the size of zVars equals nVars. inputProb is a
250 hash table (<name>,<probability>) for primary inputs. Probability here means
251 the probability of the primary input to be 1. nVars equal the number of
252 present state variables, nPi the number of primary inputs, roundOff implies
253 the number of digits after decimal to round off the calculations.
254
255 method is one of Solve_GenMethod_c, Solve_FPMethod_c, Solve_CKMethod_c
256 or Solve_Default_c. Currently only Solve_FPMethod_c is supported.
257 Solve_Default_c corresponds to Solve_FPMethod_c.
258
259 start is one of Start_Default_c, Start_Reset_c or Start_EquiProb_c.
260 The default method is Start_Reset_c.]
261
262 SideEffects [None]
263
264 SeeAlso [Mark_ComputeStateProbs]
265
266******************************************************************************/
267bdd_node **
268Mark_ComputeStateProbsWithTr(
269 bdd_manager *ddManager,
270 bdd_node *TR,
271 bdd_node *reachable,
272 bdd_node **piVars,
273 bdd_node **xVars,
274 bdd_node **yVars,
275 bdd_node **zVars,
276 st_table *inputProb,
277 int nVars,
278 int nPi,
279 int roundOff,
280 Mark_SolveMethod method,
281 Mark_StartMethod start)
282{
283 CK *ck;
284 bdd_node **piAddVars, **xAddVars, **yAddVars, **zAddVars;
285 bdd_node *rep, *scc;
286 bdd_node **result;
287 st_generator *gen;
288 int i, index;
289 int createdPia, createdXa, createdYa, createdZa;
290 int createdZ;
291 int period;
292
293 /* To suppress Alpha warnings */
294 yAddVars = NIL(bdd_node *);
295 zAddVars = NIL(bdd_node *);
296
297 if (bdd_get_package_name() != CUDD) {
298 (void) fprintf(vis_stderr,"Synthesis package can be used only with CUDD package\n");
299 (void) fprintf(vis_stderr,"Please compile with CUDD package\n");
300 return 0;
301 }
302
303 createdPia = createdXa = createdYa = createdZa = 0;
304 createdZ = 0;
305
306 piAddVars = ALLOC(bdd_node *, nPi);
307 if (piAddVars == NULL)
308 return NULL;
309 createdPia = 1;
310
311 xAddVars = ALLOC(bdd_node *, nVars);
312 if (xAddVars == NULL)
313 goto endgame;
314 createdXa = 1;
315
316 yAddVars = ALLOC(bdd_node *, nVars);
317 if (yAddVars == NULL)
318 goto endgame;
319 createdYa = 1;
320
321 zAddVars = ALLOC(bdd_node *, nVars);
322 if (zAddVars == NULL)
323 goto endgame;
324 createdZa = 1;
325
326 if (zVars == NULL) {
327 zVars = ALLOC(bdd_node *, nVars);
328 if (zVars == NULL)
329 goto endgame;
330 createdZ = 1;
331 for (i = 0; i < nVars; i++)
332 bdd_ref(zVars[i] = bdd_bdd_new_var(ddManager));
333 }
334
335 for(i = 0;i < nPi; i++) {
336 index = bdd_node_read_index(piVars[i]);
337 bdd_ref(piAddVars[i] = bdd_add_ith_var(ddManager,index));
338 }
339
340 for(i = 0; i < nVars; i++) {
341 index = bdd_node_read_index(xVars[i]);
342 bdd_ref(xAddVars[i] = bdd_add_ith_var(ddManager,index));
343 index = bdd_node_read_index(yVars[i]);
344 bdd_ref(yAddVars[i] = bdd_add_ith_var(ddManager,index));
345 index = bdd_node_read_index(zVars[i]);
346 bdd_ref(zAddVars[i] = bdd_add_ith_var(ddManager,index));
347 }
348
349 /* Allocate the structure for internal use */
350 ck = ALLOC(CK,1);
351
352 ck->manager = ddManager;
353 ck->piVars = piVars;
354 ck->xVars = xVars;
355 ck->yVars = yVars;
356 ck->zVars = zVars;
357 ck->piAddVars = piAddVars;
358 ck->xAddVars = xAddVars;
359 ck->yAddVars = yAddVars;
360 ck->zAddVars = zAddVars;
361 ck->coeff = NULL; /* assigned in ckInterface - ADD */
362 ck->nVars = nVars;
363 ck->nPi = nPi;
364 ck->abstol = bdd_read_epsilon(ddManager);
365 ck->scale = 1.0;
366 ck->reltol = 1.0e-4;
367 ck->start = start;
368 ck->roundOff = roundOff;
369 ck->inputProb = inputProb;
370 ck->transition = TR;
371 ck->reached = reachable;
372 ck->indexSCC = NULL; /* assigned in MarkGetSCC called by recTC */
373 ck->collapsedcoeff = NULL; /* assigned in ckInterface */
374 ck->term_SCC_states = 0;
375 ck->periods = NULL; /* assigned in bddCollapseTSCC */
376 ck->term_scc = NULL; /* assigned in ckInterface - ADD */
377 ck->init_guess = NULL; /* assigned and derefed in all the methods.*/
378
379 ckInterface(ck);
380
381 /* select resolution method */
382 if (method == Solve_CKMethod_c) {
383 fprintf(stdout,"Mark<->Equations' Solver uses CK Method\n");
384 result = MarkAddCKSolve(ck);
385 }
386 else if (method == Solve_GenMethod_c) {
387 fprintf(stdout,"Mark<->Equations' Solver uses General Method\n");
388 result = MarkAddGenSolve(ck);
389 }
390 else {
391 fprintf(stdout,"Mark<->Equations's Solver uses FP Method\n");
392 result = MarkAddFPSolve(ck);
393 }
394
395 /* Clean up */
396 bdd_recursive_deref(ddManager,ck->coeff);
397 st_foreach_item(ck->indexSCC,gen,&rep,&scc) {
398 bdd_recursive_deref(ddManager,rep);
399 bdd_recursive_deref(ddManager,scc);
400 }
401 st_free_table(ck->indexSCC);
402 bdd_recursive_deref(ddManager,ck->collapsedcoeff);
403 st_foreach_item_int(ck->periods,gen,&rep, &period) {
404 bdd_recursive_deref(ddManager,rep);
405 }
406 st_free_table(ck->periods);
407
408 bdd_recursive_deref(ddManager,ck->term_scc);
409
410 for(i = 0; i < nPi; i++) {
411 bdd_recursive_deref(ddManager,piAddVars[i]);
412 }
413
414 for(i = 0; i < nVars; i++) {
415 bdd_recursive_deref(ddManager,xAddVars[i]);
416 bdd_recursive_deref(ddManager,yAddVars[i]);
417 bdd_recursive_deref(ddManager,zAddVars[i]);
418 }
419
420 if (createdZ) {
421 for(i = 0; i < nVars; i++) {
422 bdd_recursive_deref(ddManager,zVars[i]);
423 }
424 FREE(zVars);
425 }
426 FREE(xAddVars);
427 FREE(yAddVars);
428 FREE(zAddVars);
429 FREE(piAddVars);
430 FREE(ck);
431
432 return result;
433
434endgame:
435 if (createdPia)
436 FREE(piAddVars);
437 if (createdXa)
438 FREE(xAddVars);
439 if (createdYa)
440 FREE(yAddVars);
441 if (createdZa)
442 FREE(zAddVars);
443 if (createdZ)
444 FREE(zVars);
445
446 return NULL;
447}
448
449
450/*---------------------------------------------------------------------------*/
451/* Definition of internal functions */
452/*---------------------------------------------------------------------------*/
453
454/**Function********************************************************************
455
456 Synopsis [Not implemented yet.]
457
458 Description [Not implemented yet.]
459
460 SideEffects [None]
461
462 SeeAlso []
463
464******************************************************************************/
465bdd_node **
466MarkAddCKSolve(
467 CK *ck)
468{
469 (void) fprintf(vis_stdout,"Not implemented yet. \n");
470 return NIL(bdd_node *);
471}
472
473
474/**Function********************************************************************
475
476 Synopsis [Not implemented yet.]
477
478 Description [Not implemented yet.]
479
480 SideEffects [None]
481
482 SeeAlso []
483
484******************************************************************************/
485bdd_node **
486MarkAddGenSolve(
487 CK *ck)
488{
489 (void) fprintf(vis_stdout,"Not implemented yet. \n");
490 return NIL(bdd_node *);
491}
492
493
494/**Function********************************************************************
495
496 Synopsis [Calculate the average bit change in the STG.]
497
498 Description [Calculate the average bit change in the STG. probTR is an ADD
499 representing the absolute transition probability matrix of the STG.
500 xVars and yVars are the present and next state variables respectively. nVars
501 is the number of state variables.
502
503 average bit change = (\exists^+_x(probTr * HD(x,y))).
504
505 The interested reader is referred to
506
507 R. I. Bahar and E. A. Frohm and C. M. Gaona and G. D. Hachtel and E.
508 Macii and A. Pardo and F. Somenzi, "Algebraic Decision Diagrams and
509 their Applications", International Conference on Computer Aided
510 Design, 1993.
511
512 on details pertaining to ADDs. ]
513
514 SideEffects [None]
515
516 SeeAlso []
517******************************************************************************/
518double
519MarkAverageBitChange(
520 bdd_manager *manager,
521 bdd_node *probTR,
522 bdd_node **xVars,
523 bdd_node **yVars,
524 int nVars)
525{
526 bdd_node *diff, *cube, *PA, *QA;
527 bdd_node **vars;
528 double Mean;
529 int i;
530
531 vars = ALLOC(bdd_node *,2*nVars);
532 for (i = 0; i < nVars; i++) {
533 vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i]));
534 bdd_ref(vars[i]);
535 }
536 for (i = nVars; i < 2*nVars; i++) {
537 vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars]));
538 bdd_ref(vars[i]);
539 }
540
541 cube = bdd_add_compute_cube(manager,vars,NULL,2*nVars);
542 bdd_ref(cube);
543
544 /* Calculate the Hamming distance ADD. This ADD represents the hamming
545 * distance between two vectors represented by xVars and yVars.
546 */
547 bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars));
548 bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff));
549 bdd_recursive_deref(manager,diff);
550
551 /* And now add and abstract all the variables.*/
552 bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube));
553 bdd_recursive_deref(manager,PA);
554 bdd_recursive_deref(manager,cube);
555 Mean = (double)bdd_add_value(QA);
556 bdd_recursive_deref(manager,QA);
557
558 for (i = 0; i < 2*nVars; i++) {
559 bdd_recursive_deref(manager,vars[i]);
560 }
561 FREE(vars);
562 return Mean;
563}
564
565/*---------------------------------------------------------------------------*/
566/* Definition of static functions */
567/*---------------------------------------------------------------------------*/
568
569/**Function********************************************************************
570
571 Synopsis [Perform structural decomposition of the markov chain.]
572
573 Description []
574
575 SideEffects [The data structure ck is changed.]
576
577 SeeAlso []
578
579******************************************************************************/
580static void
581ckInterface(
582 CK *ck)
583{
584 bdd_manager *ddManager;
585 bdd_node *piCube;
586 bdd_node *new_;
587 bdd_node *tmp1,*tmp2;
588 bdd_node *p, *t;
589 bdd_node *reachable, *TR;
590 bdd_node *q, *r;
591 st_table *newSCC;
592 st_table *newperiods;
593 st_generator *gen;
594 int len, nVars;
595
596 ddManager = ck->manager;
597 reachable = ck->reached;
598 TR = ck->transition;
599 nVars = ck->nVars;
600
601 bdd_ref(piCube = bdd_bdd_compute_cube(ddManager,ck->piVars,NULL,ck->nPi));
602 /* abstract the PI variables for the SCC computation */
603 bdd_ref(new_ = bdd_bdd_exist_abstract(ddManager,TR,piCube));
604 bdd_recursive_deref(ddManager,piCube);
605
606 /* now find the set of nodes in terminal SCC's */
607 p = recTC(ck,new_);
608 bdd_recursive_deref(ddManager,new_);
609
610 /* Collapse the TSCC in the graph */
611 ck->collapsedcoeff = bddCollapseTSCC(ck);
612 bdd_ref(ck->collapsedcoeff);
613
614 /* retain only reachable terminal SCC's */
615 bdd_ref(t = bdd_bdd_and(ddManager,p,reachable));
616 bdd_recursive_deref(ddManager,p);
617
618 /* count the number of states in the terminal SCC's */
619 ck->term_SCC_states = bdd_count_minterm(ddManager,t,nVars);
620 (void) fprintf(vis_stdout,"# of states in TSCCs = %f\n",
621 ck->term_SCC_states);
622
623 /* Translate the data in ck->collapsedcoeff and
624 * ck->indexSCC from BDDs to ADDs.
625 */
626
627 newSCC = st_init_table(st_ptrcmp,st_ptrhash);
628 newperiods = st_init_table(st_ptrcmp,st_ptrhash);
629 st_foreach_item(ck->indexSCC,gen,&tmp1,&tmp2) {
630 bdd_ref(q = bdd_bdd_to_add(ddManager,tmp1));
631 bdd_ref(r = bdd_bdd_to_add(ddManager,tmp2));
632 st_lookup_int(ck->periods,(char *)tmp1, &len);
633 st_insert(newSCC,(char *)q,(char *)r);
634 st_insert(newperiods,(char *)q,(char *)(long)len);
635 bdd_recursive_deref(ddManager,tmp1);
636 bdd_recursive_deref(ddManager,tmp2);
637 }
638 st_free_table(ck->indexSCC);
639 st_free_table(ck->periods);
640 bdd_ref(q = bdd_bdd_to_add(ddManager,ck->collapsedcoeff));
641 bdd_recursive_deref(ddManager,ck->collapsedcoeff);
642 ck->collapsedcoeff = q;
643 ck->indexSCC = newSCC;
644 ck->periods = newperiods;
645
646 /* Print the number of TSCCs */
647 (void) fprintf(vis_stdout,"# of TSCCs = %d\n",st_count(newSCC));
648
649 /* convert the transition relation BDD into an ADD */
650 bdd_ref(q = bdd_bdd_to_add(ddManager,TR));
651 ck->coeff = q;
652
653 /* convert the term_scc set BDD into an ADD */
654 bdd_ref(q = bdd_bdd_to_add(ddManager,t));
655 ck->term_scc = q;
656 bdd_recursive_deref(ddManager,t);
657
658} /* End of ckInterface */
659
660/**Function********************************************************************
661
662 Synopsis [Compute the strongly connected components.]
663
664 Description []
665
666 SideEffects [ck->indexSCC changed.]
667
668 SeeAlso []
669
670******************************************************************************/
671static bdd_node *
672recTC(
673 CK *ck,
674 bdd_node *tr)
675{
676
677 bdd_manager *manager = ck->manager;
678 bdd_node **xVars, **yVars, **zVars;
679 bdd_node *closure;
680 bdd_node *lastScc;
681 int nVars;
682
683 xVars = ck->xVars;
684 yVars = ck->yVars;
685 zVars = ck->zVars;
686 nVars = ck->nVars;
687
688 /* Matsunaga's procedure could also be used. Will have to implement it
689 * later.
690 */
691
692 closure = transitiveClosureByIterSquaring(manager,tr,xVars,yVars,zVars,
693 nVars);
694 bdd_ref(closure);
695 lastScc = MarkGetSCC(manager,tr,closure,ck->reached,
696 xVars, yVars, nVars, &(ck->indexSCC));
697
698 bdd_recursive_deref(manager,closure);
699
700 return(lastScc);
701}
702
703
704/**Function********************************************************************
705
706 Synopsis [Computes the transitive closure by iterative squaring.]
707
708 Description []
709
710 SideEffects [None]
711
712 SeeAlso []
713
714******************************************************************************/
715static bdd_node *
716transitiveClosureByIterSquaring(
717 bdd_manager *ddManager,
718 bdd_node *TR,
719 bdd_node **xVars,
720 bdd_node **yVars,
721 bdd_node **zVars,
722 int nVars)
723{
724 bdd_node *prev, *next, *TRxz, *TRzy;
725 bdd_node *inter;
726 bdd_node *zCube;
727
728 bdd_ref(zCube = bdd_bdd_compute_cube(ddManager,zVars,NULL,nVars));
729
730 bdd_ref(prev = TR);
731 while(1) {
732 TRxz = bdd_bdd_swap_variables(ddManager,prev,yVars,zVars,nVars);
733 bdd_ref(TRxz);
734 TRzy = bdd_bdd_swap_variables(ddManager,prev,xVars,zVars,nVars);
735 bdd_ref(TRzy);
736 inter = bdd_bdd_and_abstract(ddManager,TRxz,TRzy,zCube);
737 bdd_ref(inter);
738 bdd_recursive_deref(ddManager,TRxz);
739 bdd_recursive_deref(ddManager,TRzy);
740 next = bdd_bdd_or(ddManager,TR,inter);
741 bdd_ref(next);
742 bdd_recursive_deref(ddManager,inter);
743 if(prev == next)
744 break;
745 bdd_recursive_deref(ddManager,prev);
746 prev = next;
747 }
748 bdd_recursive_deref(ddManager,zCube);
749 bdd_recursive_deref(ddManager,prev);
750 bdd_deref(next);
751 return next;
752}
753
754/**Function********************************************************************
755
756 Synopsis [Collapse the Terminal SCCs into a macro node.]
757
758 Description []
759
760 SideEffects [ck->periods is changed.]
761
762 SeeAlso []
763
764******************************************************************************/
765static bdd_node *
766bddCollapseTSCC(
767 CK *ck)
768{
769 bdd_manager *manager = ck->manager;
770 bdd_node *tmp1,*tmp2;
771 bdd_node *repr,*scc,*restscc;
772 bdd_node *newtr;
773 bdd_node *xCube,*yCube;
774 bdd_node *sccfanout,*sccfanin;
775 st_generator *gen;
776 int i;
777
778 bdd_ref(xCube = bdd_bdd_compute_cube(manager,ck->xVars,NULL,ck->nVars));
779 bdd_ref(yCube = bdd_bdd_compute_cube(manager,ck->yVars,NULL,ck->nVars));
780
781 ck->periods = st_init_table(st_ptrcmp,st_ptrhash);
782
783 bdd_ref(newtr = ck->transition);
784 i = 0;
785 st_foreach_item(ck->indexSCC,gen,&repr,&scc) {
786 /* Traverse the SCC to obtain the period */
787 st_insert(ck->periods,(char *)repr,(char *)(long)sccGetPeriod(ck,repr));
788
789 /* Add edges from scc to the representatives in the fanout */
790 bdd_ref(sccfanout = bdd_bdd_and_abstract(manager,newtr,scc,xCube));
791
792 bdd_ref(tmp1 = bdd_bdd_and(manager,scc,sccfanout));
793 bdd_recursive_deref(manager,sccfanout);
794 bdd_ref(tmp2 = bdd_bdd_or(manager,newtr,tmp1));
795 bdd_recursive_deref(manager,tmp1);
796 bdd_recursive_deref(manager,newtr);
797 newtr = tmp2;
798
799 /* Add edges from fanin to representative */
800 bdd_ref(tmp2 = bdd_bdd_swap_variables(manager,scc,ck->xVars,ck->yVars,
801 ck->nVars));
802 bdd_ref(sccfanin = bdd_bdd_and_abstract(manager,newtr,tmp2,yCube));
803 bdd_recursive_deref(manager,tmp2);
804
805 /* Add edges (fanin,representative) to the TR */
806 bdd_ref(tmp1 = bdd_bdd_swap_variables(manager,repr,ck->xVars,
807 ck->yVars,ck->nVars));
808 bdd_ref(tmp2 = bdd_bdd_and(manager,sccfanin,tmp1));
809 bdd_recursive_deref(manager,tmp1);
810 bdd_recursive_deref(manager,sccfanin);
811 bdd_ref(tmp1 = bdd_bdd_or(manager,newtr,tmp2));
812 bdd_recursive_deref(manager,tmp2);
813 bdd_recursive_deref(manager,newtr);
814 newtr = tmp1;
815
816 /*Delete the edges that go to the non-representative nodes */
817 bdd_ref(restscc = bdd_bdd_and(manager,scc,bdd_not_bdd_node(repr)));
818
819 bdd_ref(tmp1 = bdd_bdd_and(manager,newtr,bdd_not_bdd_node(restscc)));
820 bdd_ref(tmp2 = bdd_bdd_swap_variables(manager,restscc,ck->xVars,
821 ck->yVars,ck->nVars));
822 bdd_recursive_deref(manager,restscc);
823 bdd_recursive_deref(manager,newtr);
824 bdd_ref(newtr = bdd_bdd_and(manager,tmp1,bdd_not_bdd_node(tmp2)));
825 bdd_recursive_deref(manager,tmp1);
826 bdd_recursive_deref(manager,tmp2);
827
828 i++;
829 }
830
831 bdd_recursive_deref(manager,xCube);
832 bdd_recursive_deref(manager,yCube);
833
834 bdd_deref(newtr);
835 return(newtr);
836}
837
838/**Function********************************************************************
839
840 Synopsis [Compute the period of the SCC.]
841
842 Description []
843
844 SideEffects [None]
845
846 SeeAlso []
847
848******************************************************************************/
849static int
850sccGetPeriod(
851 CK *ck,
852 bdd_node *reset)
853{
854
855 bdd_manager *manager = ck->manager;
856 bdd_node *new_,*from;
857 bdd_node *tmp1;
858 bdd_node *xCube, *inputCube;
859 bdd_node *transition;
860 int pos,result = 0;
861 int depth;
862 int stop = 0;
863 st_table *tos;
864 st_generator *gen;
865
866 /* Calculate the cube for abstraction */
867
868 bdd_ref(xCube = bdd_bdd_compute_cube(manager,ck->xVars,NULL,ck->nVars));
869 bdd_ref(inputCube = bdd_bdd_compute_cube(manager,ck->piVars,NULL,ck->nPi));
870 bdd_ref(transition = bdd_bdd_exist_abstract(manager,ck->transition,
871 inputCube));
872 bdd_recursive_deref(manager,inputCube);
873
874 depth = 0;
875 bdd_ref(from = reset);
876 bdd_ref(tmp1 = reset);
877 tos = st_init_table(st_ptrcmp,st_ptrhash);
878 depth++;
879 st_insert(tos,(char *)tmp1,(char *)(long)depth);
880
881 while(!stop) {
882 bdd_ref(tmp1 = bdd_bdd_and_abstract(manager,from,transition,xCube));
883 bdd_ref(new_ = bdd_bdd_swap_variables(manager,tmp1,ck->yVars,ck->xVars,
884 ck->nVars));
885 bdd_recursive_deref(manager,tmp1);
886
887 if((stop = st_lookup_int(tos,(char *)new_, &pos)))
888 result = depth - pos;
889 else
890 st_insert(tos,(char *)new_,(char *)(long)depth);
891
892 bdd_recursive_deref(manager,from);
893 bdd_ref(from = new_);
894 depth++;
895 }
896
897 bdd_recursive_deref(manager,new_);
898 bdd_recursive_deref(manager,xCube);
899 bdd_recursive_deref(manager,from);
900
901 st_foreach_item_int(tos,gen,&new_, &pos) {
902 bdd_recursive_deref(manager,new_);
903 }
904 st_free_table(tos);
905
906 return result;
907}
908
909
910/**Function********************************************************************
911
912 Synopsis [Returns a BDD array from an Mvf array]
913
914 SideEffects [None]
915
916 SeeAlso []
917
918******************************************************************************/
919static array_t *
920markGetBddArray(array_t *mvfArray)
921{
922 int i,phase;
923 array_t *bddArray;
924 Mvf_Function_t *mvf;
925
926 bddArray = array_alloc(bdd_node *,0);
927
928 arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
929 mdd_t *mddTemp;
930 bdd_node *ddNode;
931
932 mddTemp = array_fetch(mdd_t *, mvf, 1);
933 ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
934 bdd_ref(ddNode);
935
936 ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
937 array_insert_last(bdd_node *, bddArray, ddNode);
938 }
939 return bddArray;
940}
941
942/**Function********************************************************************
943
944 Synopsis [Returns a BDD array given an integer array of variable indices.]
945
946 SideEffects [None]
947
948 SeeAlso []
949
950******************************************************************************/
951static bdd_node **
952BddNodeArrayFromIdArray(
953 bdd_manager *ddManager,
954 array_t *idArray)
955{
956 bdd_node **xvars;
957 int i,id;
958 int nvars = array_n(idArray);
959
960 xvars = ALLOC(bdd_node *, nvars);
961 if (xvars == NULL)
962 return NULL;
963
964 for(i = 0; i < nvars; i++) {
965 id = array_fetch(int,idArray,i);
966 xvars[i] = bdd_bdd_ith_var(ddManager,id);
967 bdd_ref(xvars[i]);
968 }
969 return xvars;
970}
971
972/**Function********************************************************************
973
974 Synopsis [Compute the relation between an array of function and a
975 corresponding array of variables. A BDD is returned which represents
976 AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]
977
978 SideEffects []
979
980 SeeAlso []
981
982******************************************************************************/
983static bdd_node *
984computeTransitionRelationWithIds(
985 bdd_manager *ddManager,
986 array_t *nextBdds,
987 bdd_node **yVars,
988 int nVars)
989{
990 bdd_node *ddtemp1, *ddtemp2;
991 bdd_node *oldTR, *fn;
992 int i;
993
994
995 oldTR = bdd_read_one(ddManager);
996
997 for(i = 0; i < nVars; i++) {
998 ddtemp2 = array_fetch(bdd_node *, nextBdds, i);
999
1000 fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
1001 bdd_ref(fn);
1002 ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
1003 bdd_ref(ddtemp1);
1004 bdd_recursive_deref(ddManager,fn);
1005 bdd_recursive_deref(ddManager,oldTR);
1006 oldTR = ddtemp1;
1007 }
1008
1009 return oldTR;
1010}
1011
Note: See TracBrowser for help on using the repository browser.