1 /**
2 @file
3
4 @ingroup nanotrav
5
6 @brief A very simple reachability analysis program.
7
8 @author Fabio Somenzi
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "cuddInt.h"
47 #include "ntr.h"
48
49 /*---------------------------------------------------------------------------*/
50 /* Constant declarations */
51 /*---------------------------------------------------------------------------*/
52
53 #define NTR_MAX_DEP_SIZE 20
54
55 /*---------------------------------------------------------------------------*/
56 /* Stucture declarations */
57 /*---------------------------------------------------------------------------*/
58
59 /*---------------------------------------------------------------------------*/
60 /* Type declarations */
61 /*---------------------------------------------------------------------------*/
62
63 /*---------------------------------------------------------------------------*/
64 /* Variable declarations */
65 /*---------------------------------------------------------------------------*/
66
67 static char const *onames[] = {"T", "R"}; /**< names of functions to be dumped */
68 static double *signatures; /**< signatures for all variables */
69 static BnetNetwork *staticNet; /**< pointer to network used by qsort
70 ** comparison function */
71 static DdNode **staticPart; /**< pointer to parts used by qsort
72 ** comparison function */
73
74 /*---------------------------------------------------------------------------*/
75 /* Macro declarations */
76 /*---------------------------------------------------------------------------*/
77
78 /** \cond */
79
80 /*---------------------------------------------------------------------------*/
81 /* Static function prototypes */
82 /*---------------------------------------------------------------------------*/
83
84 static DdNode * makecube (DdManager *dd, DdNode **x, int n);
85 static void ntrInitializeCount (BnetNetwork *net, NtrOptions *option);
86 static void ntrCountDFS (BnetNetwork *net, BnetNode *node);
87 static DdNode * ntrImage (DdManager *dd, NtrPartTR *TR, DdNode *from, NtrOptions *option);
88 static DdNode * ntrPreimage (DdManager *dd, NtrPartTR *T, DdNode *from);
89 static DdNode * ntrChooseFrom (DdManager *dd, DdNode *neW, DdNode *reached, NtrOptions *option);
90 static DdNode * ntrUpdateReached (DdManager *dd, DdNode *oldreached, DdNode *to);
91 static int ntrLatchDependencies (DdManager *dd, DdNode *reached, BnetNetwork *net, NtrOptions *option);
92 static NtrPartTR * ntrEliminateDependencies (DdManager *dd, NtrPartTR *TR, DdNode **states, NtrOptions *option);
93 static int ntrUpdateQuantificationSchedule (DdManager *dd, NtrPartTR *T);
94 static int ntrSignatureCompare (int * ptrX, int * ptrY);
95 static int ntrSignatureCompare2 (int * ptrX, int * ptrY);
96 static int ntrPartCompare (int * ptrX, int * ptrY);
97 static char ** ntrAllocMatrix (int nrows, int ncols);
98 static void ntrFreeMatrix (char **matrix);
99 static void ntrPermuteParts (DdNode **a, DdNode **b, int *comesFrom, int *goesTo, int size);
100 static void ntrIncreaseRef(void * e, void * arg);
101 static void ntrDecreaseRef(void * e, void * arg);
102
103 /** \endcond */
104
105
106 /*---------------------------------------------------------------------------*/
107 /* Definition of exported functions */
108 /*---------------------------------------------------------------------------*/
109
110
111 /**
112 @brief Builds DDs for a network outputs and next state functions.
113
114 @details The method is really brain-dead, but it is very simple.
115 Some inputs to the network may be shared with another network whose
116 DDs have already been built. In this case we want to share the DDs
117 as well.
118
119 @return 1 in case of success; 0 otherwise.
120
121 @sideeffect the dd fields of the network nodes are modified. Uses the
122 count fields of the nodes.
123
124 */
125 int
Ntr_buildDDs(BnetNetwork * net,DdManager * dd,NtrOptions * option,BnetNetwork * net2)126 Ntr_buildDDs(
127 BnetNetwork * net /**< network for which DDs are to be built */,
128 DdManager * dd /**< %DD manager */,
129 NtrOptions * option /**< option structure */,
130 BnetNetwork * net2 /**< companion network with which inputs may be shared */)
131 {
132 int pr = option->verb;
133 int result;
134 int i;
135 BnetNode *node, *node2;
136
137 /* If some inputs or present state variables are shared with
138 ** another network, we initialize their BDDs from that network.
139 */
140 if (net2 != NULL) {
141 for (i = 0; i < net->npis; i++) {
142 if (!st_lookup(net->hash,net->inputs[i],(void **)&node)) {
143 return(0);
144 }
145 if (!st_lookup(net2->hash,net->inputs[i],(void **)&node2)) {
146 /* This input is not shared. */
147 result = Bnet_BuildNodeBDD(dd,node,net->hash,
148 option->locGlob,option->nodrop);
149 if (result == 0) return(0);
150 } else {
151 if (node2->dd == NULL) return(0);
152 node->dd = node2->dd;
153 Cudd_Ref(node->dd);
154 node->var = node2->var;
155 node->active = node2->active;
156 }
157 }
158 for (i = 0; i < net->nlatches; i++) {
159 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
160 return(0);
161 }
162 if (!st_lookup(net2->hash,net->latches[i][1],(void **)&node2)) {
163 /* This present state variable is not shared. */
164 result = Bnet_BuildNodeBDD(dd,node,net->hash,
165 option->locGlob,option->nodrop);
166 if (result == 0) return(0);
167 } else {
168 if (node2->dd == NULL) return(0);
169 node->dd = node2->dd;
170 Cudd_Ref(node->dd);
171 node->var = node2->var;
172 node->active = node2->active;
173 }
174 }
175 } else {
176 /* First assign variables to inputs if the order is provided.
177 ** (Either in the .blif file or in an order file.)
178 */
179 if (option->ordering == PI_PS_FROM_FILE) {
180 /* Follow order given in input file. First primary inputs
181 ** and then present state variables.
182 */
183 for (i = 0; i < net->npis; i++) {
184 if (!st_lookup(net->hash,net->inputs[i],(void **)&node)) {
185 return(0);
186 }
187 result = Bnet_BuildNodeBDD(dd,node,net->hash,
188 option->locGlob,option->nodrop);
189 if (result == 0) return(0);
190 }
191 for (i = 0; i < net->nlatches; i++) {
192 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
193 return(0);
194 }
195 result = Bnet_BuildNodeBDD(dd,node,net->hash,
196 option->locGlob,option->nodrop);
197 if (result == 0) return(0);
198 }
199 } else if (option->ordering == PI_PS_GIVEN) {
200 result = Bnet_ReadOrder(dd,option->orderPiPs,net,option->locGlob,
201 option->nodrop);
202 if (result == 0) return(0);
203 } else {
204 result = Bnet_DfsVariableOrder(dd,net);
205 if (result == 0) return(0);
206 }
207 }
208 /* At this point the BDDs of all primary inputs and present state
209 ** variables have been built. */
210
211 /* Currently noBuild doesn't do much. */
212 if (option->noBuild == TRUE)
213 return(1);
214
215 if (option->locGlob == BNET_LOCAL_DD) {
216 node = net->nodes;
217 while (node != NULL) {
218 result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_LOCAL_DD,TRUE);
219 if (result == 0) {
220 return(0);
221 }
222 if (pr > 2) {
223 (void) fprintf(stdout,"%s",node->name);
224 Cudd_PrintDebug(dd,node->dd,Cudd_ReadSize(dd),pr);
225 }
226 node = node->next;
227 }
228 } else { /* option->locGlob == BNET_GLOBAL_DD */
229 /* Create BDDs with DFS from the primary outputs and the next
230 ** state functions. If the inputs had not been ordered yet,
231 ** this would result in a DFS order for the variables.
232 */
233
234 ntrInitializeCount(net,option);
235
236 if (option->node != NULL &&
237 option->closestCube == FALSE && option->dontcares == FALSE) {
238 if (!st_lookup(net->hash,option->node,(void **)&node)) {
239 return(0);
240 }
241 result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
242 option->nodrop);
243 if (result == 0) return(0);
244 } else {
245 if (option->stateOnly == FALSE) {
246 for (i = 0; i < net->npos; i++) {
247 if (!st_lookup(net->hash,net->outputs[i],(void **)&node)) {
248 continue;
249 }
250 result = Bnet_BuildNodeBDD(dd,node,net->hash,
251 BNET_GLOBAL_DD,option->nodrop);
252 if (result == 0) return(0);
253 if (option->progress) {
254 (void) fprintf(stdout,"%s\n",node->name);
255 }
256 #if 0
257 Cudd_PrintDebug(dd,node->dd,net->ninputs,option->verb);
258 #endif
259 }
260 }
261 for (i = 0; i < net->nlatches; i++) {
262 if (!st_lookup(net->hash,net->latches[i][0],(void **)&node)) {
263 continue;
264 }
265 result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
266 option->nodrop);
267 if (result == 0) return(0);
268 if (option->progress) {
269 (void) fprintf(stdout,"%s\n",node->name);
270 }
271 #if 0
272 Cudd_PrintDebug(dd,node->dd,net->ninputs,option->verb);
273 #endif
274 }
275 }
276 /* Make sure all inputs have a DD and dereference the DDs of
277 ** the nodes that are not reachable from the outputs.
278 */
279 for (i = 0; i < net->npis; i++) {
280 if (!st_lookup(net->hash,net->inputs[i],(void **)&node)) {
281 return(0);
282 }
283 result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
284 option->nodrop);
285 if (result == 0) return(0);
286 if (node->count == -1) Cudd_RecursiveDeref(dd,node->dd);
287 }
288 for (i = 0; i < net->nlatches; i++) {
289 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
290 return(0);
291 }
292 result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
293 option->nodrop);
294 if (result == 0) return(0);
295 if (node->count == -1) Cudd_RecursiveDeref(dd,node->dd);
296 }
297
298 /* Dispose of the BDDs of the internal nodes if they have not
299 ** been dropped already.
300 */
301 if (option->nodrop == TRUE) {
302 for (node = net->nodes; node != NULL; node = node->next) {
303 if (node->dd != NULL && node->count != -1 &&
304 (node->type == BNET_INTERNAL_NODE ||
305 node->type == BNET_INPUT_NODE ||
306 node->type == BNET_PRESENT_STATE_NODE)) {
307 Cudd_RecursiveDeref(dd,node->dd);
308 if (node->type == BNET_INTERNAL_NODE) node->dd = NULL;
309 }
310 }
311 }
312 }
313
314 return(1);
315
316 } /* end of Ntr_buildDDs */
317
318
319 /**
320 @brief Builds the transition relation for a network.
321
322 @return a pointer to the transition relation structure if
323 successful; NULL otherwise.
324
325 @sideeffect None
326
327 */
328 NtrPartTR *
Ntr_buildTR(DdManager * dd,BnetNetwork * net,NtrOptions * option,int image)329 Ntr_buildTR(
330 DdManager * dd /**< manager */,
331 BnetNetwork * net /**< network */,
332 NtrOptions * option /**< options */,
333 int image /**< image type: monolithic ... */)
334 {
335 NtrPartTR *TR;
336 DdNode *T, *delta, *support, *scan, *tmp, *preiabs, *prepabs;
337 DdNode **part, **absicubes, **abspcubes, **nscube, *mnscube;
338 DdNode **x, **y;
339 DdNode **pi;
340 int i;
341 int xlevel;
342 BnetNode *node;
343 int *schedule;
344 int depth = 0;
345
346 /* Initialize transition relation structure. */
347 TR = ALLOC(NtrPartTR,1);
348 if (TR == NULL) goto endgame;
349 TR->nlatches = net->nlatches;
350 if (image == NTR_IMAGE_MONO) {
351 TR->nparts = 1;
352 } else if (image == NTR_IMAGE_PART || image == NTR_IMAGE_CLIP ||
353 image == NTR_IMAGE_DEPEND) {
354 TR->nparts = net->nlatches;
355 } else {
356 (void) fprintf(stderr,"Unrecognized image method (%d). Using part.\n",
357 image);
358 TR->nparts = net->nlatches;
359 }
360 TR->factors = Ntr_InitHeap(TR->nlatches);
361 if (TR->factors == NULL) goto endgame;
362 /* Allocate arrays for present state and next state variables. */
363 TR->x = x = ALLOC(DdNode *,TR->nlatches);
364 if (x == NULL) goto endgame;
365 TR->y = y = ALLOC(DdNode *,TR->nlatches);
366 if (y == NULL) goto endgame;
367 /* Allocate array for primary input variables. */
368 pi = ALLOC(DdNode *,net->npis);
369 if (pi == NULL) goto endgame;
370 /* Allocate array for partitioned transition relation. */
371 part = ALLOC(DdNode *,net->nlatches);
372 if (part == NULL) goto endgame;
373 /* Allocate array of next state cubes. */
374 nscube = ALLOC(DdNode *,net->nlatches);
375 if (nscube == NULL) goto endgame;
376 /* Allocate array for quantification schedule and initialize it. */
377 schedule = ALLOC(int,Cudd_ReadSize(dd));
378 if (schedule == NULL) goto endgame;
379 for (i = 0; i < Cudd_ReadSize(dd); i++) {
380 schedule[i] = -1;
381 }
382
383 /* Create partitioned transition relation from network. */
384 TR->xw = Cudd_ReadOne(dd);
385 Cudd_Ref(TR->xw);
386 for (i = 0; i < net->nlatches; i++) {
387 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
388 goto endgame;
389 }
390 x[i] = node->dd;
391 Cudd_Ref(x[i]);
392 /* Add present state variable to cube TR->xw. */
393 tmp = Cudd_bddAnd(dd,TR->xw,x[i]);
394 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
395 Cudd_RecursiveDeref(dd,TR->xw);
396 TR->xw = tmp;
397 /* Create new y variable immediately above the x variable. */
398 xlevel = Cudd_ReadPerm(dd,x[i]->index);
399 y[i] = Cudd_bddNewVarAtLevel(dd,xlevel);
400 Cudd_Ref(y[i]);
401 /* Initialize cube of next state variables for this part. */
402 nscube[i] = y[i];
403 Cudd_Ref(nscube[i]);
404 /* Group present and next state variable if so requested. */
405 if (option->groupnsps != NTR_GROUP_NONE) {
406 int method = option->groupnsps == NTR_GROUP_DEFAULT ?
407 MTR_DEFAULT : MTR_FIXED;
408 if (Cudd_MakeTreeNode(dd,y[i]->index,2,method) == NULL)
409 goto endgame;
410 }
411 /* Get next state function and create transition relation part. */
412 if (!st_lookup(net->hash,net->latches[i][0],(void **)&node)) {
413 goto endgame;
414 }
415 delta = node->dd;
416 if (image != NTR_IMAGE_DEPEND) {
417 part[i] = Cudd_bddXnor(dd,delta,y[i]);
418 if (part[i] == NULL) goto endgame;
419 } else {
420 part[i] = delta;
421 }
422 Cudd_Ref(part[i]);
423 /* Collect scheduling info for this delta. At the end of this loop
424 ** schedule[i] == j means that the variable of index i does not
425 ** appear in any part with index greater than j, unless j == -1,
426 ** in which case the variable appears in no part.
427 */
428 support = Cudd_Support(dd,delta);
429 Cudd_Ref(support);
430 scan = support;
431 while (!Cudd_IsConstant(scan)) {
432 schedule[scan->index] = i;
433 scan = Cudd_T(scan);
434 }
435 Cudd_RecursiveDeref(dd,support);
436 }
437
438 /* Collect primary inputs. */
439 for (i = 0; i < net->npis; i++) {
440 if (!st_lookup(net->hash,net->inputs[i],(void **)&node)) {
441 goto endgame;
442 }
443 pi[i] = node->dd;
444 tmp = Cudd_bddAnd(dd,TR->xw,pi[i]);
445 if (tmp == NULL) goto endgame; Cudd_Ref(tmp);
446 Cudd_RecursiveDeref(dd,TR->xw);
447 TR->xw = tmp;
448 }
449
450 /* Build abstraction cubes. First primary input variables that go
451 ** in the abstraction cubes for both monolithic and partitioned
452 ** transition relations. */
453 absicubes = ALLOC(DdNode *, net->nlatches);
454 if (absicubes == NULL) goto endgame;
455 abspcubes = ALLOC(DdNode *, net->nlatches);
456 if (abspcubes == NULL) goto endgame;
457
458 for (i = 0; i < net->nlatches; i++) {
459 absicubes[i] = Cudd_ReadOne(dd);
460 Cudd_Ref(absicubes[i]);
461 }
462 preiabs = Cudd_ReadOne(dd);
463 Cudd_Ref(preiabs);
464
465 for (i = 0; i < net->npis; i++) {
466 int j = pi[i]->index;
467 int k = schedule[j];
468 if (k >= 0) {
469 tmp = Cudd_bddAnd(dd,absicubes[k],pi[i]);
470 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
471 Cudd_RecursiveDeref(dd,absicubes[k]);
472 absicubes[k] = tmp;
473 } else {
474 tmp = Cudd_bddAnd(dd,preiabs,pi[i]);
475 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
476 Cudd_RecursiveDeref(dd,preiabs);
477 preiabs = tmp;
478 }
479 }
480 FREE(pi);
481
482 /* Build preimage abstraction cubes from image abstraction cubes. */
483 for (i = 0; i < net->nlatches; i++) {
484 abspcubes[i] = Cudd_bddAnd(dd,absicubes[i],nscube[i]);
485 if (abspcubes[i] == NULL) return(NULL);
486 Cudd_Ref(abspcubes[i]);
487 }
488 Cudd_Ref(prepabs = preiabs);
489
490 /* For partitioned transition relations we add present state variables
491 ** to the image abstraction cubes. */
492 if (image != NTR_IMAGE_MONO) {
493 for (i = 0; i < net->nlatches; i++) {
494 int j = x[i]->index;
495 int k = schedule[j];
496 if (k >= 0) {
497 tmp = Cudd_bddAnd(dd,absicubes[k],x[i]);
498 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
499 Cudd_RecursiveDeref(dd,absicubes[k]);
500 absicubes[k] = tmp;
501 } else {
502 tmp = Cudd_bddAnd(dd,preiabs,x[i]);
503 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
504 Cudd_RecursiveDeref(dd,preiabs);
505 preiabs = tmp;
506 }
507 }
508 }
509 FREE(schedule);
510
511 if (image != NTR_IMAGE_MONO) {
512 TR->part = part;
513 TR->icube = absicubes;
514 TR->pcube = abspcubes;
515 TR->nscube = nscube;
516 TR->preiabs = preiabs;
517 TR->prepabs = prepabs;
518 return(TR);
519 }
520
521 /* Here we are building a monolithic TR. */
522
523 /* Reinitialize the cube of variables to be quantified before
524 ** image computation. */
525 Cudd_RecursiveDeref(dd,preiabs);
526 preiabs = Cudd_ReadOne(dd);
527 Cudd_Ref(preiabs);
528
529 if (option->imageClip != 1.0) {
530 depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
531 }
532
533 /* Collapse transition relation. */
534 T = Cudd_ReadOne(dd);
535 Cudd_Ref(T);
536 mnscube = Cudd_ReadOne(dd);
537 Cudd_Ref(mnscube);
538 for (i = 0; i < net->nlatches; i++) {
539 /* Eliminate the primary inputs that do not appear in other parts. */
540 if (depth != 0) {
541 tmp = Cudd_bddClippingAndAbstract(dd,T,part[i],absicubes[i],
542 depth,option->approx);
543 } else {
544 tmp = Cudd_bddAndAbstract(dd,T,part[i],absicubes[i]);
545 }
546 Cudd_Ref(tmp);
547 Cudd_RecursiveDeref(dd,T);
548 Cudd_RecursiveDeref(dd,part[i]);
549 Cudd_RecursiveDeref(dd,absicubes[i]);
550 Cudd_RecursiveDeref(dd,abspcubes[i]);
551 if (option->threshold >= 0) {
552 if (option->approx) {
553 T = Cudd_RemapOverApprox(dd,tmp,2*net->nlatches,
554 option->threshold,option->quality);
555 } else {
556 T = Cudd_RemapUnderApprox(dd,tmp,2*net->nlatches,
557 option->threshold,option->quality);
558 }
559 } else {
560 T = tmp;
561 }
562 if (T == NULL) return(NULL);
563 Cudd_Ref(T);
564 Cudd_RecursiveDeref(dd,tmp);
565 /* Add the next state variables of this part to the cube of all
566 ** next state variables. */
567 tmp = Cudd_bddAnd(dd,mnscube,nscube[i]);
568 if (tmp == NULL) return(NULL);
569 Cudd_Ref(tmp);
570 Cudd_RecursiveDeref(dd,mnscube);
571 mnscube = tmp;
572 Cudd_RecursiveDeref(dd,nscube[i]);
573 (void) printf("@"); fflush(stdout);
574 }
575 (void) printf("\n");
576 #if 0
577 (void) printf("T"); Cudd_PrintDebug(dd,T,2*net->nlatches,2);
578 #endif
579
580 /* Clean up. */
581 FREE(absicubes);
582 FREE(abspcubes);
583 FREE(part);
584 FREE(nscube);
585
586 TR->part = part = ALLOC(DdNode *,1);
587 if (part == NULL) goto endgame;
588 part[0] = T;
589
590 /* Build cube of x (present state) variables for abstraction. */
591 TR->icube = absicubes = ALLOC(DdNode *,1);
592 if (absicubes == NULL) goto endgame;
593 absicubes[0] = makecube(dd,x,TR->nlatches);
594 if (absicubes[0] == NULL) return(0);
595 Cudd_Ref(absicubes[0]);
596 /* Build cube of y (next state) variables for abstraction. */
597 TR->pcube = abspcubes = ALLOC(DdNode *,1);
598 if (abspcubes == NULL) goto endgame;
599 abspcubes[0] = makecube(dd,y,TR->nlatches);
600 if (abspcubes[0] == NULL) return(0);
601 Cudd_Ref(abspcubes[0]);
602 TR->preiabs = preiabs;
603 TR->prepabs = prepabs;
604
605 TR->nscube = ALLOC(DdNode *,1);
606 if (TR->nscube == NULL) return(NULL);
607 TR->nscube[0] = mnscube;
608
609 return(TR);
610
611 endgame:
612
613 return(NULL);
614
615 } /* end of Ntr_buildTR */
616
617
618 /**
619 @brief Frees the transition relation for a network.
620
621 @sideeffect None
622
623 */
624 void
Ntr_freeTR(DdManager * dd,NtrPartTR * TR)625 Ntr_freeTR(
626 DdManager * dd,
627 NtrPartTR * TR)
628 {
629 int i;
630 for (i = 0; i < TR->nlatches; i++) {
631 Cudd_RecursiveDeref(dd,TR->x[i]);
632 Cudd_RecursiveDeref(dd,TR->y[i]);
633 }
634 FREE(TR->x);
635 FREE(TR->y);
636 for (i = 0; i < TR->nparts; i++) {
637 Cudd_RecursiveDeref(dd,TR->part[i]);
638 Cudd_RecursiveDeref(dd,TR->icube[i]);
639 Cudd_RecursiveDeref(dd,TR->pcube[i]);
640 Cudd_RecursiveDeref(dd,TR->nscube[i]);
641 }
642 FREE(TR->part);
643 FREE(TR->icube);
644 FREE(TR->pcube);
645 FREE(TR->nscube);
646 Cudd_RecursiveDeref(dd,TR->preiabs);
647 Cudd_RecursiveDeref(dd,TR->prepabs);
648 Cudd_RecursiveDeref(dd,TR->xw);
649 Ntr_HeapForeach(TR->factors, ntrDecreaseRef, dd);
650 Ntr_FreeHeap(TR->factors);
651 FREE(TR);
652
653 return;
654
655 } /* end of Ntr_freeTR */
656
657
658 /**
659 @brief Makes a copy of a transition relation.
660
661 @return a pointer to the copy if successful; NULL otherwise.
662
663 @sideeffect None
664
665 @see Ntr_buildTR Ntr_freeTR
666
667 */
668 NtrPartTR *
Ntr_cloneTR(NtrPartTR * TR)669 Ntr_cloneTR(
670 NtrPartTR *TR)
671 {
672 NtrPartTR *T;
673 int nparts, nlatches, i;
674
675 T = ALLOC(NtrPartTR,1);
676 if (T == NULL) return(NULL);
677 nparts = T->nparts = TR->nparts;
678 nlatches = T->nlatches = TR->nlatches;
679 T->part = ALLOC(DdNode *,nparts);
680 if (T->part == NULL) {
681 FREE(T);
682 return(NULL);
683 }
684 T->icube = ALLOC(DdNode *,nparts);
685 if (T->icube == NULL) {
686 FREE(T->part);
687 FREE(T);
688 return(NULL);
689 }
690 T->pcube = ALLOC(DdNode *,nparts);
691 if (T->pcube == NULL) {
692 FREE(T->icube);
693 FREE(T->part);
694 FREE(T);
695 return(NULL);
696 }
697 T->x = ALLOC(DdNode *,nlatches);
698 if (T->x == NULL) {
699 FREE(T->pcube);
700 FREE(T->icube);
701 FREE(T->part);
702 FREE(T);
703 return(NULL);
704 }
705 T->y = ALLOC(DdNode *,nlatches);
706 if (T->y == NULL) {
707 FREE(T->x);
708 FREE(T->pcube);
709 FREE(T->icube);
710 FREE(T->part);
711 FREE(T);
712 return(NULL);
713 }
714 T->nscube = ALLOC(DdNode *,nparts);
715 if (T->nscube == NULL) {
716 FREE(T->y);
717 FREE(T->x);
718 FREE(T->pcube);
719 FREE(T->icube);
720 FREE(T->part);
721 FREE(T);
722 return(NULL);
723 }
724 T->factors = Ntr_HeapClone(TR->factors);
725 if (T->factors == NULL) {
726 FREE(T->nscube);
727 FREE(T->y);
728 FREE(T->x);
729 FREE(T->pcube);
730 FREE(T->icube);
731 FREE(T->part);
732 FREE(T);
733 return(NULL);
734 }
735 Ntr_HeapForeach(T->factors, ntrIncreaseRef, NULL);
736 for (i = 0; i < nparts; i++) {
737 T->part[i] = TR->part[i];
738 Cudd_Ref(T->part[i]);
739 T->icube[i] = TR->icube[i];
740 Cudd_Ref(T->icube[i]);
741 T->pcube[i] = TR->pcube[i];
742 Cudd_Ref(T->pcube[i]);
743 T->nscube[i] = TR->nscube[i];
744 Cudd_Ref(T->nscube[i]);
745 }
746 T->preiabs = TR->preiabs;
747 Cudd_Ref(T->preiabs);
748 T->prepabs = TR->prepabs;
749 Cudd_Ref(T->prepabs);
750 T->xw = TR->xw;
751 Cudd_Ref(T->xw);
752 for (i = 0; i < nlatches; i++) {
753 T->x[i] = TR->x[i];
754 Cudd_Ref(T->x[i]);
755 T->y[i] = TR->y[i];
756 Cudd_Ref(T->y[i]);
757 }
758
759 return(T);
760
761 } /* end of Ntr_cloneTR */
762
763
764 /**
765 @brief Poor man's traversal procedure.
766
767 @details Based on the monolithic transition relation.
768
769 @return 1 in case of success; 0 otherwise.
770
771 @sideeffect None
772
773 @see Ntr_ClosureTrav
774
775 */
776 int
Ntr_Trav(DdManager * dd,BnetNetwork * net,NtrOptions * option)777 Ntr_Trav(
778 DdManager * dd /**< %DD manager */,
779 BnetNetwork * net /**< network */,
780 NtrOptions * option /**< options */)
781 {
782 NtrPartTR *TR; /* Transition relation */
783 DdNode *init; /* initial state(s) */
784 DdNode *from;
785 DdNode *to;
786 DdNode *reached;
787 DdNode *neW;
788 DdNode *one, *zero;
789 int depth;
790 int retval;
791 int pr = option->verb;
792 unsigned int initReord = Cudd_ReadReorderings(dd);
793
794 if (option->traverse == FALSE || net->nlatches == 0) return(1);
795 (void) printf("Building transition relation. Time = %s\n",
796 util_print_time(util_cpu_time() - option->initialTime));
797 one = Cudd_ReadOne(dd);
798 zero = Cudd_Not(one);
799
800 /* Build transition relation and initial states. */
801 TR = Ntr_buildTR(dd,net,option,option->image);
802 if (TR == NULL) return(0);
803 retval = Cudd_SetVarMap(dd,TR->x,TR->y,TR->nlatches);
804 if (retval == 0) return(0);
805 (void) printf("Transition relation: %d parts %d latches %d nodes\n",
806 TR->nparts, TR->nlatches,
807 Cudd_SharingSize(TR->part, TR->nparts));
808 (void) printf("Traversing. Time = %s\n",
809 util_print_time(util_cpu_time() - option->initialTime));
810 init = Ntr_initState(dd,net,option);
811 if (init == NULL) return(0);
812
813 /* Initialize From. */
814 Cudd_Ref(from = init);
815 (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
816
817 /* Initialize Reached. */
818 Cudd_Ref(reached = from);
819
820 /* Start traversal. */
821 for (depth = 0; ; depth++) {
822 /* Image computation. */
823 to = ntrImage(dd,TR,from,option);
824 if (to == NULL) {
825 Cudd_RecursiveDeref(dd,reached);
826 Cudd_RecursiveDeref(dd,from);
827 return(0);
828 }
829 Cudd_RecursiveDeref(dd,from);
830
831 /* Find new states. */
832 neW = Cudd_bddAnd(dd,to,Cudd_Not(reached));
833 if (neW == NULL) {
834 Cudd_RecursiveDeref(dd,reached);
835 Cudd_RecursiveDeref(dd,to);
836 return(0);
837 }
838 Cudd_Ref(neW);
839 Cudd_RecursiveDeref(dd,to);
840
841 /* Check for convergence. */
842 if (neW == zero) break;
843
844 /* Dump current reached states if requested. */
845 if (option->store == depth) {
846 int ok = Dddmp_cuddBddStore(dd, NULL, reached, NULL,
847 NULL, DDDMP_MODE_TEXT, DDDMP_VARIDS,
848 option->storefile, NULL);
849 if (ok == 0) return(0);
850 (void) printf("Storing reached in %s after %i iterations.\n",
851 option->storefile, depth);
852 break;
853 }
854
855 /* Update reached. */
856 reached = ntrUpdateReached(dd,reached,neW);
857 if (reached == NULL) {
858 Cudd_RecursiveDeref(dd,neW);
859 return(0);
860 }
861
862 /* Prepare for new iteration. */
863 from = ntrChooseFrom(dd,neW,reached,option);
864 if (from == NULL) {
865 Cudd_RecursiveDeref(dd,reached);
866 Cudd_RecursiveDeref(dd,neW);
867 return(0);
868 }
869 Cudd_RecursiveDeref(dd,neW);
870 (void) printf("From[%d]",depth+1);
871 Cudd_PrintDebug(dd,from,TR->nlatches,pr);
872 (void) printf("Reached[%d]",depth+1);
873 Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
874 if (pr > 0) {
875 if (!Cudd_ApaPrintMinterm(stdout, dd, reached, TR->nlatches))
876 return(0);
877 if (!Cudd_ApaPrintMintermExp(stdout, dd, reached, TR->nlatches, 6))
878 return(0);
879 } else {
880 (void) printf("\n");
881 }
882 }
883
884 /* Print out result. */
885 (void) printf("depth = %d\n", depth);
886 (void) printf("R"); Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
887
888 /* Dump to file if requested. */
889 if (option->bdddump) {
890 DdNode *dfunc[2]; /* addresses of the functions to be dumped */
891 char *onames[2]; /* names of the functions to be dumped */
892 dfunc[0] = TR->part[0]; onames[0] = (char *) "T";
893 dfunc[1] = reached; onames[1] = (char *) "R";
894 retval = Bnet_bddArrayDump(dd, net, option->dumpfile, dfunc,
895 onames, 2, option->dumpFmt);
896 if (retval == 0) return(0);
897 }
898
899 if (option->depend) {
900 retval = ntrLatchDependencies(dd, reached, net, option);
901 if (retval == -1) return(0);
902 (void) printf("%d latches are redundant\n", retval);
903 }
904 /* Clean up. */
905 Cudd_RecursiveDeref(dd,reached);
906 Cudd_RecursiveDeref(dd,neW);
907 Cudd_RecursiveDeref(dd,init);
908 Ntr_freeTR(dd,TR);
909
910 if (Cudd_ReadReorderings(dd) > initReord) {
911 (void) printf("Order at the end of reachability analysis\n");
912 retval = Bnet_PrintOrder(net,dd);
913 if (retval == 0) return(0);
914 }
915 return(1);
916
917 } /* end of Ntr_Trav */
918
919
920 /**
921 @brief Computes the SCCs of the STG.
922
923 @details Computes the strongly connected components of the state
924 transition graph. Only the first 10 SCCs are computed.
925
926 @return 1 in case of success; 0 otherwise.
927
928 @sideeffect None
929
930 @see Ntr_Trav
931
932 */
933 int
Ntr_SCC(DdManager * dd,BnetNetwork * net,NtrOptions * option)934 Ntr_SCC(
935 DdManager * dd /**< %DD manager */,
936 BnetNetwork * net /**< network */,
937 NtrOptions * option /**< options */)
938 {
939 NtrPartTR *TR; /* Transition relation */
940 DdNode *init; /* initial state(s) */
941 DdNode *from;
942 DdNode *to;
943 DdNode *reached, *reaching;
944 DdNode *neW;
945 DdNode *one, *zero;
946 DdNode *states, *scc;
947 DdNode *tmp = NULL;
948 DdNode *SCCs[10];
949 int depth;
950 int nscc = 0;
951 int retval;
952 int pr = option->verb;
953 int i;
954
955 if (option->scc == FALSE || net->nlatches == 0) return(1);
956 (void) printf("Building transition relation. Time = %s\n",
957 util_print_time(util_cpu_time() - option->initialTime));
958 one = Cudd_ReadOne(dd);
959 zero = Cudd_Not(one);
960
961 /* Build transition relation and initial states. */
962 TR = Ntr_buildTR(dd,net,option,option->image);
963 if (TR == NULL) return(0);
964 retval = Cudd_SetVarMap(dd,TR->x,TR->y,TR->nlatches);
965 if (retval == 0) return(0);
966 (void) printf("Transition relation: %d parts %d latches %d nodes\n",
967 TR->nparts, TR->nlatches,
968 Cudd_SharingSize(TR->part, TR->nparts));
969 (void) printf("Computing SCCs. Time = %s\n",
970 util_print_time(util_cpu_time() - option->initialTime));
971
972 /* Consider all SCCs, including those not reachable. */
973 states = one;
974 Cudd_Ref(states);
975
976 while (states != zero) {
977 if (nscc == 0) {
978 tmp = Ntr_initState(dd,net,option);
979 if (tmp == NULL) return(0);
980 init = Cudd_bddPickOneMinterm(dd,tmp,TR->x,TR->nlatches);
981 } else {
982 init = Cudd_bddPickOneMinterm(dd,states,TR->x,TR->nlatches);
983 }
984 if (init == NULL) return(0);
985 Cudd_Ref(init);
986 if (nscc == 0) {
987 Cudd_RecursiveDeref(dd,tmp);
988 }
989 /* Initialize From. */
990 Cudd_Ref(from = init);
991 (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
992
993 /* Initialize Reached. */
994 Cudd_Ref(reached = from);
995
996 /* Start forward traversal. */
997 for (depth = 0; ; depth++) {
998 /* Image computation. */
999 to = ntrImage(dd,TR,from,option);
1000 if (to == NULL) {
1001 return(0);
1002 }
1003 Cudd_RecursiveDeref(dd,from);
1004
1005 /* Find new states. */
1006 tmp = Cudd_bddAnd(dd,to,states);
1007 if (tmp == NULL) return(0); Cudd_Ref(tmp);
1008 Cudd_RecursiveDeref(dd,to);
1009 neW = Cudd_bddAnd(dd,tmp,Cudd_Not(reached));
1010 if (neW == NULL) return(0); Cudd_Ref(neW);
1011 Cudd_RecursiveDeref(dd,tmp);
1012
1013 /* Check for convergence. */
1014 if (neW == zero) break;
1015
1016 /* Update reached. */
1017 reached = ntrUpdateReached(dd,reached,neW);
1018 if (reached == NULL) {
1019 return(0);
1020 }
1021
1022 /* Prepare for new iteration. */
1023 from = ntrChooseFrom(dd,neW,reached,option);
1024 if (from == NULL) {
1025 return(0);
1026 }
1027 Cudd_RecursiveDeref(dd,neW);
1028 (void) printf("From[%d]",depth+1);
1029 Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1030 (void) printf("Reached[%d]",depth+1);
1031 Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
1032 if (pr <= 0) {
1033 (void) printf("\n");
1034 }
1035 }
1036 Cudd_RecursiveDeref(dd,neW);
1037
1038 /* Express reached in terms of y variables. This allows us to
1039 ** efficiently test for termination during the backward traversal. */
1040 tmp = Cudd_bddVarMap(dd,reached);
1041 if (tmp == NULL) return(0);
1042 Cudd_Ref(tmp);
1043 Cudd_RecursiveDeref(dd,reached);
1044 reached = tmp;
1045
1046 /* Initialize from and reaching. */
1047 from = Cudd_bddVarMap(dd,init);
1048 Cudd_Ref(from);
1049 (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1050 Cudd_Ref(reaching = from);
1051
1052 /* Start backward traversal. */
1053 for (depth = 0; ; depth++) {
1054 /* Preimage computation. */
1055 to = ntrPreimage(dd,TR,from);
1056 if (to == NULL) {
1057 return(0);
1058 }
1059 Cudd_RecursiveDeref(dd,from);
1060
1061 /* Find new states. */
1062 tmp = Cudd_bddAnd(dd,to,reached);
1063 if (tmp == NULL) return(0); Cudd_Ref(tmp);
1064 Cudd_RecursiveDeref(dd,to);
1065 neW = Cudd_bddAnd(dd,tmp,Cudd_Not(reaching));
1066 if (neW == NULL) return(0); Cudd_Ref(neW);
1067 Cudd_RecursiveDeref(dd,tmp);
1068
1069 /* Check for convergence. */
1070 if (neW == zero) break;
1071
1072 /* Update reaching. */
1073 reaching = ntrUpdateReached(dd,reaching,neW);
1074 if (reaching == NULL) {
1075 return(0);
1076 }
1077
1078 /* Prepare for new iteration. */
1079 from = ntrChooseFrom(dd,neW,reaching,option);
1080 if (from == NULL) {
1081 return(0);
1082 }
1083 Cudd_RecursiveDeref(dd,neW);
1084 (void) printf("From[%d]",depth+1);
1085 Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1086 (void) printf("Reaching[%d]",depth+1);
1087 Cudd_PrintDebug(dd,reaching,TR->nlatches,pr);
1088 if (pr <= 0) {
1089 (void) printf("\n");
1090 }
1091 }
1092
1093 scc = Cudd_bddAnd(dd,reached,reaching);
1094 if (scc == NULL) {
1095 return(0);
1096 }
1097 Cudd_Ref(scc);
1098 SCCs[nscc] = Cudd_bddVarMap(dd,scc);
1099 if (SCCs[nscc] == NULL) return(0);
1100 Cudd_Ref(SCCs[nscc]);
1101 Cudd_RecursiveDeref(dd,scc);
1102 /* Print out result. */
1103 (void) printf("SCC[%d]",nscc);
1104 Cudd_PrintDebug(dd,SCCs[nscc],TR->nlatches,pr);
1105 tmp = Cudd_bddAnd(dd,states,Cudd_Not(SCCs[nscc]));
1106 if (tmp == NULL) {
1107 return(0);
1108 }
1109 Cudd_Ref(tmp);
1110 Cudd_RecursiveDeref(dd,states);
1111 states = tmp;
1112 Cudd_RecursiveDeref(dd,reached);
1113 Cudd_RecursiveDeref(dd,reaching);
1114 Cudd_RecursiveDeref(dd,neW);
1115 Cudd_RecursiveDeref(dd,init);
1116 nscc++;
1117 if (nscc > 9) break;
1118 }
1119
1120 if (states != zero) {
1121 (void) fprintf(stdout,"More than 10 SCCs. Only the first 10 are computed.\n");
1122 }
1123
1124 /* Dump to file if requested. */
1125 if (option->bdddump) {
1126 char *sccnames[10]; /* names of the SCCs */
1127 sccnames[0] = (char *) "SCC0";
1128 sccnames[1] = (char *) "SCC1";
1129 sccnames[2] = (char *) "SCC2";
1130 sccnames[3] = (char *) "SCC3";
1131 sccnames[4] = (char *) "SCC4";
1132 sccnames[5] = (char *) "SCC5";
1133 sccnames[6] = (char *) "SCC6";
1134 sccnames[7] = (char *) "SCC7";
1135 sccnames[8] = (char *) "SCC8";
1136 sccnames[9] = (char *) "SCC9";
1137 retval = Bnet_bddArrayDump(dd, net, option->dumpfile, SCCs,
1138 sccnames, nscc, option->dumpFmt);
1139 if (retval == 0) return(0);
1140 }
1141
1142 /* Verify that the SCCs form a partition of the universe. */
1143 scc = zero;
1144 Cudd_Ref(scc);
1145 for (i = 0; i < nscc; i++) {
1146 assert(Cudd_bddLeq(dd,SCCs[i],Cudd_Not(scc)));
1147 tmp = Cudd_bddOr(dd,SCCs[i],scc);
1148 if (tmp == NULL) return(0);
1149 Cudd_Ref(tmp);
1150 Cudd_RecursiveDeref(dd,scc);
1151 scc = tmp;
1152 Cudd_RecursiveDeref(dd,SCCs[i]);
1153 }
1154 assert(scc == Cudd_Not(states));
1155
1156 /* Clean up. */
1157 Cudd_RecursiveDeref(dd,scc);
1158 Cudd_RecursiveDeref(dd,states);
1159 Ntr_freeTR(dd,TR);
1160
1161 return(1);
1162
1163 } /* end of Ntr_SCC */
1164
1165
1166 /**
1167 @brief Transitive closure traversal procedure.
1168
1169 @details Traversal procedure based on the transitive closure of the
1170 transition relation.
1171
1172 @return 1 in case of success; 0 otherwise.
1173
1174 @sideeffect None
1175
1176 @see Ntr_Trav
1177
1178 */
1179 int
Ntr_ClosureTrav(DdManager * dd,BnetNetwork * net,NtrOptions * option)1180 Ntr_ClosureTrav(
1181 DdManager * dd /**< %DD manager */,
1182 BnetNetwork * net /**< network */,
1183 NtrOptions * option /**< options */)
1184 {
1185 DdNode *init;
1186 DdNode *T;
1187 NtrPartTR *TR;
1188 int retval;
1189 int pr = option->verb; /* verbosity level */
1190 DdNode *dfunc[2]; /* addresses of the functions to be dumped */
1191 char *onames[2]; /* names of the functions to be dumped */
1192 DdNode *reached, *reachedy, *reachedx;
1193
1194 /* Traverse if requested and if the circuit is sequential. */
1195 if (option->closure == FALSE || net->nlatches == 0) return(1);
1196
1197 TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
1198 if (TR == NULL) return(0);
1199 (void) printf("TR"); Cudd_PrintDebug(dd,TR->part[0],2*TR->nlatches,pr);
1200 T = Ntr_TransitiveClosure(dd,TR,option);
1201 if (T == NULL) return(0);
1202 Cudd_Ref(T);
1203 (void) printf("TC"); Cudd_PrintDebug(dd,T,2*TR->nlatches,pr);
1204
1205 init = Ntr_initState(dd,net,option);
1206 if (init == NULL) return(0);
1207 (void) printf("S0"); Cudd_PrintDebug(dd,init,TR->nlatches,pr);
1208
1209 /* Image computation. */
1210 if (option->closureClip != 1.0) {
1211 int depth = (int) ((double) Cudd_ReadSize(dd) * option->closureClip);
1212 reachedy = Cudd_bddClippingAndAbstract(dd,T,init,TR->icube[0],
1213 depth,option->approx);
1214 } else {
1215 reachedy = Cudd_bddAndAbstract(dd,T,init,TR->icube[0]);
1216 }
1217 if (reachedy == NULL) return(0);
1218 Cudd_Ref(reachedy);
1219
1220 /* Express in terms of present state variables. */
1221 reachedx = Cudd_bddSwapVariables(dd,reachedy,TR->x,TR->y,TR->nlatches);
1222 if (reachedx == NULL) return(0);
1223 Cudd_Ref(reachedx);
1224 Cudd_RecursiveDeref(dd,reachedy);
1225
1226 /* Add initial state. */
1227 reached = Cudd_bddOr(dd,reachedx,init);
1228 if (reached == NULL) return(0);
1229 Cudd_Ref(reached);
1230 Cudd_RecursiveDeref(dd,reachedx);
1231
1232 /* Print out result. */
1233 (void) printf("R"); Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
1234
1235 /* Dump to file if requested. */
1236 if (option->bdddump) {
1237 dfunc[0] = T; onames[0] = (char *) "TC";
1238 dfunc[1] = reached; onames[1] = (char *) "R";
1239 retval = Bnet_bddArrayDump(dd, net, option->dumpfile, dfunc,
1240 onames, 2, option->dumpFmt);
1241 if (retval == 0) return(0);
1242 }
1243
1244 /* Clean up. */
1245 Cudd_RecursiveDeref(dd,reached);
1246 Cudd_RecursiveDeref(dd,init);
1247 Cudd_RecursiveDeref(dd,T);
1248 Ntr_freeTR(dd,TR);
1249
1250 return(1);
1251
1252 } /* end of Ntr_ClosureTrav */
1253
1254
1255 /**
1256 @brief Builds the transitive closure of a transition relation.
1257
1258 @details Uses a simple squaring algorithm.
1259
1260 @return a %BDD if successful; NULL otherwise.
1261
1262 @sideeffect None
1263
1264 */
1265 DdNode *
Ntr_TransitiveClosure(DdManager * dd,NtrPartTR * TR,NtrOptions * option)1266 Ntr_TransitiveClosure(
1267 DdManager * dd,
1268 NtrPartTR * TR,
1269 NtrOptions * option)
1270 {
1271 DdNode *T,*oldT,*Txz,*Tzy,*Tred,*square,*zcube;
1272 DdNode **z;
1273 int i;
1274 int depth = 0;
1275 int ylevel;
1276 int done;
1277
1278 if (option->image != NTR_IMAGE_MONO) return(NULL);
1279
1280 /* Create array of auxiliary variables. */
1281 z = ALLOC(DdNode *,TR->nlatches);
1282 if (z == NULL)
1283 return(NULL);
1284 for (i = 0; i < TR->nlatches; i++) {
1285 ylevel = Cudd_ReadIndex(dd,TR->y[i]->index);
1286 z[i] = Cudd_bddNewVarAtLevel(dd,ylevel);
1287 if (z[i] == NULL)
1288 return(NULL);
1289 }
1290 /* Build cube of auxiliary variables. */
1291 zcube = makecube(dd,z,TR->nlatches);
1292 if (zcube == NULL) return(NULL);
1293 Cudd_Ref(zcube);
1294
1295 if (option->closureClip != 1.0) {
1296 depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
1297 }
1298
1299 T = TR->part[0];
1300 Cudd_Ref(T);
1301 for (i = 0; ; i++) {
1302 if (option->threshold >= 0) {
1303 if (option->approx) {
1304 Tred = Cudd_RemapOverApprox(dd,T,TR->nlatches*2,
1305 option->threshold,
1306 option->quality);
1307 } else {
1308 Tred = Cudd_RemapUnderApprox(dd,T,TR->nlatches*2,
1309 option->threshold,
1310 option->quality);
1311 }
1312 } else {
1313 Tred = T;
1314 }
1315 if (Tred == NULL) return(NULL);
1316 Cudd_Ref(Tred);
1317 /* Express T in terms of z and y variables. */
1318 Tzy = Cudd_bddSwapVariables(dd,Tred,TR->x,z,TR->nlatches);
1319 if (Tzy == NULL) return(NULL);
1320 Cudd_Ref(Tzy);
1321 /* Express T in terms of x and z variables. */
1322 Txz = Cudd_bddSwapVariables(dd,Tred,TR->y,z,TR->nlatches);
1323 if (Txz == NULL) return(NULL);
1324 Cudd_Ref(Txz);
1325 Cudd_RecursiveDeref(dd,Tred);
1326 /* Square */
1327 if (depth == 0) {
1328 square = Cudd_bddAndAbstract(dd,Txz,Tzy,zcube);
1329 } else {
1330 square = Cudd_bddClippingAndAbstract(dd,Txz,Tzy,zcube,depth,
1331 option->approx);
1332 }
1333 if (square == NULL) return(NULL);
1334 Cudd_Ref(square);
1335 Cudd_RecursiveDeref(dd,Tzy);
1336 Cudd_RecursiveDeref(dd,Txz);
1337 oldT = T;
1338 T = Cudd_bddOr(dd,square,TR->part[0]);
1339 if (T == NULL) return(NULL);
1340 Cudd_Ref(T);
1341 Cudd_RecursiveDeref(dd,square);
1342 done = T == oldT;
1343 Cudd_RecursiveDeref(dd,oldT);
1344 if (done) break;
1345 (void) fprintf(stdout,"@"); fflush(stdout);
1346 }
1347 (void) fprintf(stdout, "\n");
1348
1349 Cudd_RecursiveDeref(dd,zcube);
1350 Cudd_Deref(T);
1351 FREE(z);
1352 return(T);
1353
1354 } /* end of Ntr_TransitiveClosure */
1355
1356
1357 /**
1358 @brief Builds the %BDD of the initial state(s).
1359
1360 @return a %BDD if successful; NULL otherwise.
1361
1362 @sideeffect None
1363
1364 */
1365 DdNode *
Ntr_initState(DdManager * dd,BnetNetwork * net,NtrOptions * option)1366 Ntr_initState(
1367 DdManager * dd,
1368 BnetNetwork * net,
1369 NtrOptions * option)
1370 {
1371 DdNode *res, *x, *w, *one;
1372 BnetNode *node;
1373 int i;
1374
1375 if (option->load) {
1376 res = Dddmp_cuddBddLoad(dd, DDDMP_VAR_MATCHIDS, NULL, NULL, NULL,
1377 DDDMP_MODE_DEFAULT, option->loadfile, NULL);
1378 } else {
1379 one = Cudd_ReadOne(dd);
1380 Cudd_Ref(res = one);
1381
1382 if (net->nlatches == 0) return(res);
1383
1384 for (i = 0; i < net->nlatches; i++) {
1385 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
1386 goto endgame;
1387 }
1388 x = node->dd;
1389 switch (net->latches[i][2][0]) {
1390 case '0':
1391 w = Cudd_bddAnd(dd,res,Cudd_Not(x));
1392 break;
1393 case '1':
1394 w = Cudd_bddAnd(dd,res,x);
1395 break;
1396 default: /* don't care */
1397 w = res;
1398 break;
1399 }
1400
1401 if (w == NULL) {
1402 Cudd_RecursiveDeref(dd,res);
1403 return(NULL);
1404 }
1405 Cudd_Ref(w);
1406 Cudd_RecursiveDeref(dd,res);
1407 res = w;
1408 }
1409 }
1410 return(res);
1411
1412 endgame:
1413
1414 return(NULL);
1415
1416 } /* end of Ntr_initState */
1417
1418
1419 /**
1420 @brief Reads a state cube from a file or creates a random one.
1421
1422 @return a pointer to the %BDD of the sink nodes if successful; NULL
1423 otherwise.
1424
1425 @sideeffect None
1426
1427 */
1428 DdNode *
Ntr_getStateCube(DdManager * dd,BnetNetwork * net,char * filename,int pr)1429 Ntr_getStateCube(
1430 DdManager * dd,
1431 BnetNetwork * net,
1432 char * filename,
1433 int pr)
1434 {
1435 FILE *fp;
1436 DdNode *cube;
1437 DdNode *w;
1438 char *state;
1439 int i;
1440 int err;
1441 BnetNode *node;
1442 DdNode *x;
1443 char c[2];
1444
1445 cube = Cudd_ReadOne(dd);
1446 if (net->nlatches == 0) {
1447 Cudd_Ref(cube);
1448 return(cube);
1449 }
1450
1451 state = ALLOC(char,net->nlatches+1);
1452 if (state == NULL)
1453 return(NULL);
1454 state[net->nlatches] = 0;
1455
1456 if (filename == NULL) {
1457 /* Pick one random minterm. */
1458 for (i = 0; i < net->nlatches; i++) {
1459 state[i] = (char) ((Cudd_Random(dd) & 0x2000) ? '1' : '0');
1460 }
1461 } else {
1462 if ((fp = fopen(filename,"r")) == NULL) {
1463 (void) fprintf(stderr,"Unable to open %s\n",filename);
1464 return(NULL);
1465 }
1466
1467 /* Read string from file. Allow arbitrary amount of white space. */
1468 for (i = 0; !feof(fp); i++) {
1469 err = fscanf(fp, "%1s", c);
1470 state[i] = c[0];
1471 if (err == EOF || i == net->nlatches - 1) {
1472 break;
1473 } else if (err != 1 || strchr("012xX-", c[0]) == NULL ) {
1474 FREE(state);
1475 return(NULL);
1476 }
1477 }
1478 err = fclose(fp);
1479 if (err == EOF) {
1480 FREE(state);
1481 return(NULL);
1482 }
1483 }
1484
1485 /* Echo the chosen state(s). */
1486 if (pr > 0) {(void) fprintf(stdout,"%s\n", state);}
1487
1488 Cudd_Ref(cube);
1489 for (i = 0; i < net->nlatches; i++) {
1490 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
1491 Cudd_RecursiveDeref(dd,cube);
1492 FREE(state);
1493 return(NULL);
1494 }
1495 x = node->dd;
1496 switch (state[i]) {
1497 case '0':
1498 w = Cudd_bddAnd(dd,cube,Cudd_Not(x));
1499 break;
1500 case '1':
1501 w = Cudd_bddAnd(dd,cube,x);
1502 break;
1503 default: /* don't care */
1504 w = cube;
1505 break;
1506 }
1507
1508 if (w == NULL) {
1509 Cudd_RecursiveDeref(dd,cube);
1510 FREE(state);
1511 return(NULL);
1512 }
1513 Cudd_Ref(w);
1514 Cudd_RecursiveDeref(dd,cube);
1515 cube = w;
1516 }
1517
1518 FREE(state);
1519 return(cube);
1520
1521 } /* end of Ntr_getStateCube */
1522
1523
1524 /**
1525 @brief Poor man's outer envelope computation.
1526
1527 @details Based on the monolithic transition relation.
1528
1529 @return 1 in case of success; 0 otherwise.
1530
1531 @sideeffect None
1532
1533 */
1534 int
Ntr_Envelope(DdManager * dd,NtrPartTR * TR,FILE * dfp,NtrOptions * option)1535 Ntr_Envelope(
1536 DdManager * dd /**< %DD manager */,
1537 NtrPartTR * TR /**< transition relation */,
1538 FILE * dfp /**< pointer to file for %DD dump */,
1539 NtrOptions * option /**< program options */)
1540 {
1541 DdNode **x; /* array of x variables */
1542 DdNode **y; /* array of y variables */
1543 int ns; /* number of x and y variables */
1544 DdNode *dfunc[2]; /* addresses of the functions to be dumped */
1545 DdNode *envelope, *oldEnvelope;
1546 DdNode *one;
1547 int depth;
1548 int retval;
1549 int pr = option->verb;
1550 int dumpFmt = option->dumpFmt;
1551
1552 x = TR->x;
1553 y = TR->y;
1554 ns = TR->nlatches;
1555
1556 one = Cudd_ReadOne(dd);
1557 retval = Cudd_SetVarMap(dd,x,y,ns);
1558 if (retval == 0) return(0);
1559
1560 /* Initialize From. */
1561 envelope = one;
1562 if (envelope == NULL) return(0);
1563 Cudd_Ref(envelope);
1564 (void) printf("S0"); Cudd_PrintDebug(dd,envelope,ns,pr);
1565
1566 /* Start traversal. */
1567 for (depth = 0; ; depth++) {
1568 oldEnvelope = envelope;
1569 /* Image computation. */
1570 envelope = ntrImage(dd,TR,oldEnvelope,option);
1571 if (envelope == NULL) {
1572 Cudd_RecursiveDeref(dd,oldEnvelope);
1573 return(0);
1574 }
1575
1576 /* Check for convergence. */
1577 if (envelope == oldEnvelope) break;
1578
1579 /* Prepare for new iteration. */
1580 Cudd_RecursiveDeref(dd,oldEnvelope);
1581 (void) fprintf(stdout,"Envelope[%d]%s",depth+1,(pr>0)? "" : "\n");
1582 if (pr > 0 ) {
1583 Cudd_PrintSummary(dd, envelope, ns, 1 /* exponential format */);
1584 }
1585 }
1586 /* Clean up. */
1587 Cudd_RecursiveDeref(dd,oldEnvelope);
1588
1589 /* Print out result. */
1590 (void) printf("depth = %d\n", depth);
1591 (void) printf("Envelope"); Cudd_PrintDebug(dd,envelope,ns,pr);
1592
1593 /* Write dump file if requested. */
1594 if (dfp != NULL) {
1595 dfunc[0] = TR->part[0];
1596 dfunc[1] = envelope;
1597 if (dumpFmt == 1) {
1598 retval = Cudd_DumpBlif(dd,2,dfunc,NULL,(char const * const *)onames,NULL,dfp,0);
1599 } else if (dumpFmt == 2) {
1600 retval = Cudd_DumpDaVinci(dd,2,dfunc,NULL,
1601 (char const * const *)onames,dfp);
1602 } else if (dumpFmt == 3) {
1603 retval = Cudd_DumpDDcal(dd,2,dfunc,NULL,
1604 (char const * const *)onames,dfp);
1605 } else if (dumpFmt == 4) {
1606 retval = Cudd_DumpFactoredForm(dd,2,dfunc,NULL,
1607 (char const * const *)onames,dfp);
1608 } else if (dumpFmt == 5) {
1609 retval = Cudd_DumpBlif(dd,2,dfunc,NULL,
1610 (char const * const *)onames,NULL,dfp,1);
1611 } else {
1612 retval = Cudd_DumpDot(dd,2,dfunc,NULL,
1613 (char const * const *)onames,dfp);
1614 }
1615 if (retval != 1) {
1616 (void) fprintf(stderr,"abnormal termination\n");
1617 return(0);
1618 }
1619 fclose(dfp);
1620 }
1621
1622 /* Clean up. */
1623 Cudd_RecursiveDeref(dd,envelope);
1624
1625 return(1);
1626
1627 } /* end of Ntr_Envelope */
1628
1629
1630 /**
1631 @brief Maximum 0-1 flow between source and sink states.
1632
1633 @return 1 in case of success; 0 otherwise.
1634
1635 @sideeffect Creates two new sets of variables.
1636
1637 */
1638 int
Ntr_maxflow(DdManager * dd,BnetNetwork * net,NtrOptions * option)1639 Ntr_maxflow(
1640 DdManager * dd,
1641 BnetNetwork * net,
1642 NtrOptions * option)
1643 {
1644 DdNode **x = NULL;
1645 DdNode **y = NULL;
1646 DdNode **z = NULL;
1647 DdNode *E = NULL;
1648 DdNode *F = NULL;
1649 DdNode *cut = NULL;
1650 DdNode *sx = NULL;
1651 DdNode *ty = NULL;
1652 DdNode *tx = NULL;
1653 int n;
1654 int pr;
1655 int ylevel;
1656 int i;
1657 double flow;
1658 int result = 0;
1659 NtrPartTR *TR;
1660
1661 n = net->nlatches;
1662 pr = option->verb;
1663 TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
1664 if (TR == NULL)
1665 goto endgame;
1666 E = TR->part[0];
1667 x = TR->x;
1668 y = TR->y;
1669 /* Create array of auxiliary variables. */
1670 z = ALLOC(DdNode *,n);
1671 if (z == NULL)
1672 goto endgame;
1673 for (i = 0; i < n; i++) {
1674 ylevel = Cudd_ReadIndex(dd,y[i]->index);
1675 z[i] = Cudd_bddNewVarAtLevel(dd,ylevel);
1676 if (z[i] == NULL)
1677 goto endgame;
1678 Cudd_Ref(z[i]);
1679 }
1680 /* Create BDDs for source and sink. */
1681 sx = Ntr_initState(dd,net,option);
1682 if (sx == NULL)
1683 goto endgame;
1684 if (pr > 0) (void) fprintf(stdout, "Sink(s): ");
1685 tx = Ntr_getStateCube(dd,net,option->sinkfile,pr);
1686 if (tx == NULL)
1687 goto endgame;
1688 ty = Cudd_bddSwapVariables(dd,tx,x,y,n);
1689 if (ty == NULL)
1690 goto endgame;
1691 Cudd_Ref(ty);
1692 Cudd_RecursiveDeref(dd,tx);
1693 tx = NULL;
1694
1695 flow = Ntr_maximum01Flow(dd, sx, ty, E, &F, &cut, x, y, z, n, pr);
1696 if (flow >= 0.0)
1697 result = 1;
1698 if (pr >= 0) {
1699 (void) fprintf(stdout,"Maximum flow = %g\n", flow);
1700 (void) fprintf(stdout,"E"); Cudd_PrintDebug(dd,E,2*n,pr);
1701 (void) fprintf(stdout,"F"); Cudd_PrintDebug(dd,F,2*n,pr);
1702 (void) fprintf(stdout,"cut"); Cudd_PrintDebug(dd,cut,2*n,pr);
1703 }
1704 endgame:
1705 /* Clean up. */
1706 if (TR != NULL) Ntr_freeTR(dd,TR);
1707 for (i = 0; i < n; i++) {
1708 if (z != NULL && z[i] != NULL) Cudd_RecursiveDeref(dd,z[i]);
1709 }
1710 if (z != NULL) FREE(z);
1711 if (F != NULL) Cudd_RecursiveDeref(dd,F);
1712 if (cut != NULL) Cudd_RecursiveDeref(dd,cut);
1713 if (sx != NULL) Cudd_RecursiveDeref(dd,sx);
1714 if (ty != NULL) Cudd_RecursiveDeref(dd,ty);
1715 return(result);
1716
1717 } /* end of Ntr_Maxflow */
1718
1719 /*---------------------------------------------------------------------------*/
1720 /* Definition of internal functions */
1721 /*---------------------------------------------------------------------------*/
1722
1723 /*---------------------------------------------------------------------------*/
1724 /* Definition of static functions */
1725 /*---------------------------------------------------------------------------*/
1726
1727
1728 /**
1729 @brief Builds a positive cube of all the variables in x.
1730
1731 @return a %BDD for the cube if successful; NULL otherwise.
1732
1733 @sideeffect None
1734
1735 */
1736 static DdNode *
makecube(DdManager * dd,DdNode ** x,int n)1737 makecube(
1738 DdManager * dd,
1739 DdNode ** x,
1740 int n)
1741 {
1742 DdNode *res, *w, *one;
1743 int i;
1744
1745 one = Cudd_ReadOne(dd);
1746 Cudd_Ref(res = one);
1747
1748 for (i = n-1; i >= 0; i--) {
1749 w = Cudd_bddAnd(dd,res,x[i]);
1750 if (w == NULL) {
1751 Cudd_RecursiveDeref(dd,res);
1752 return(NULL);
1753 }
1754 Cudd_Ref(w);
1755 Cudd_RecursiveDeref(dd,res);
1756 res = w;
1757 }
1758 Cudd_Deref(res);
1759 return(res);
1760
1761 } /* end of makecube */
1762
1763
1764 /**
1765 @brief Initializes the count fields used to drop DDs.
1766
1767 @details Before actually building the BDDs, we perform a DFS from
1768 the outputs to initialize the count fields of the nodes. The
1769 initial value of the count field will normally coincide with the
1770 fanout of the node. However, if there are nodes with no path to any
1771 primary output or next state variable, then the initial value of
1772 count for some nodes will be less than the fanout. For primary
1773 outputs and next state functions we add 1, so that we will never try
1774 to free their DDs. The count fields of the nodes that are not
1775 reachable from the outputs are set to -1.
1776
1777 @sideeffect Changes the count fields of the network nodes. Uses the
1778 visited fields.
1779
1780 */
1781 static void
ntrInitializeCount(BnetNetwork * net,NtrOptions * option)1782 ntrInitializeCount(
1783 BnetNetwork * net,
1784 NtrOptions * option)
1785 {
1786 BnetNode *node;
1787 int i;
1788
1789 if (option->node != NULL &&
1790 option->closestCube == FALSE && option->dontcares == FALSE) {
1791 if (!st_lookup(net->hash,option->node,(void **)&node)) {
1792 (void) fprintf(stdout, "Warning: node %s not found!\n",
1793 option->node);
1794 } else {
1795 ntrCountDFS(net,node);
1796 node->count++;
1797 }
1798 } else {
1799 if (option->stateOnly == FALSE) {
1800 for (i = 0; i < net->npos; i++) {
1801 if (!st_lookup(net->hash,net->outputs[i],(void **)&node)) {
1802 (void) fprintf(stdout,
1803 "Warning: output %s is not driven!\n",
1804 net->outputs[i]);
1805 continue;
1806 }
1807 ntrCountDFS(net,node);
1808 node->count++;
1809 }
1810 }
1811 for (i = 0; i < net->nlatches; i++) {
1812 if (!st_lookup(net->hash,net->latches[i][0],(void **)&node)) {
1813 (void) fprintf(stdout,
1814 "Warning: latch input %s is not driven!\n",
1815 net->outputs[i]);
1816 continue;
1817 }
1818 ntrCountDFS(net,node);
1819 node->count++;
1820 }
1821 }
1822
1823 /* Clear visited flags. */
1824 node = net->nodes;
1825 while (node != NULL) {
1826 if (node->visited == 0) {
1827 node->count = -1;
1828 } else {
1829 node->visited = 0;
1830 }
1831 node = node->next;
1832 }
1833
1834 } /* end of ntrInitializeCount */
1835
1836
1837 /**
1838 @brief Does a DFS from a node setting the count field.
1839
1840 @sideeffect Changes the count and visited fields of the nodes it
1841 visits.
1842
1843 @see ntrLevelDFS
1844
1845 */
1846 static void
ntrCountDFS(BnetNetwork * net,BnetNode * node)1847 ntrCountDFS(
1848 BnetNetwork * net,
1849 BnetNode * node)
1850 {
1851 int i;
1852 BnetNode *auxnd;
1853
1854 node->count++;
1855
1856 if (node->visited == 1) {
1857 return;
1858 }
1859
1860 node->visited = 1;
1861
1862 for (i = 0; i < node->ninp; i++) {
1863 if (!st_lookup(net->hash, node->inputs[i], (void **)&auxnd)) {
1864 exit(2);
1865 }
1866 ntrCountDFS(net,auxnd);
1867 }
1868
1869 } /* end of ntrCountDFS */
1870
1871
1872 /**
1873 @brief Computes the image of a set given a transition relation.
1874
1875 @details The image is returned in terms of the present state
1876 variables; its reference count is already increased.
1877
1878 @return a pointer to the result if successful; NULL otherwise.
1879
1880 @sideeffect None
1881
1882 @see Ntr_Trav
1883
1884 */
1885 static DdNode *
ntrImage(DdManager * dd,NtrPartTR * TR,DdNode * from,NtrOptions * option)1886 ntrImage(
1887 DdManager * dd,
1888 NtrPartTR * TR,
1889 DdNode * from,
1890 NtrOptions * option)
1891 {
1892 int i;
1893 DdNode *image;
1894 DdNode *to;
1895 NtrPartTR *T;
1896 int depth = 0;
1897
1898 if (option->image == NTR_IMAGE_CLIP) {
1899 depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
1900 }
1901
1902 /* Existentially quantify the present state variables that are not
1903 ** in the support of any next state function. */
1904 image = Cudd_bddExistAbstract(dd,from,TR->preiabs);
1905 if (image == NULL) return(NULL);
1906 Cudd_Ref(image);
1907 if (option->image == NTR_IMAGE_DEPEND) {
1908 /* Simplify the transition relation based on dependencies
1909 ** and build the conjuncts from the deltas. */
1910 T = ntrEliminateDependencies(dd,TR,&image,option);
1911 } else {
1912 T = TR;
1913 }
1914 if (T == NULL) return(NULL);
1915 for (i = 0; i < T->nparts; i++) {
1916 #if 0
1917 (void) printf(" Intermediate product[%d]: %d nodes\n",
1918 i,Cudd_DagSize(image));
1919 #endif
1920 if (option->image == NTR_IMAGE_CLIP) {
1921 to = Cudd_bddClippingAndAbstract(dd,T->part[i],image,T->icube[i],
1922 depth,option->approx);
1923 } else {
1924 to = Cudd_bddAndAbstract(dd,T->part[i],image,T->icube[i]);
1925 }
1926 if (to == NULL) return(NULL);
1927 Cudd_Ref(to);
1928 if (option->image == NTR_IMAGE_DEPEND) {
1929 /* Extract dependencies from intermediate product. */
1930 DdNode *abs, *positive, *absabs, *phi, *exnor, *tmp;
1931 abs = Cudd_bddExistAbstract(dd,to,T->xw);
1932 if (abs == NULL) return(NULL); Cudd_Ref(abs);
1933 if (Cudd_bddVarIsDependent(dd,abs,T->nscube[i]) &&
1934 Cudd_EstimateCofactor(dd,abs,T->nscube[i]->index,1) <=
1935 T->nlatches) {
1936 int retval, sizex;
1937 positive = Cudd_Cofactor(dd,abs,T->nscube[i]);
1938 if (positive == NULL) return(NULL); Cudd_Ref(positive);
1939 absabs = Cudd_bddExistAbstract(dd,abs,T->nscube[i]);
1940 if (absabs == NULL) return(NULL); Cudd_Ref(absabs);
1941 Cudd_RecursiveDeref(dd,abs);
1942 phi = Cudd_bddLICompaction(dd,positive,absabs);
1943 if (phi == NULL) return(NULL); Cudd_Ref(phi);
1944 Cudd_RecursiveDeref(dd,positive);
1945 Cudd_RecursiveDeref(dd,absabs);
1946 exnor = Cudd_bddXnor(dd,T->nscube[i],phi);
1947 if (exnor == NULL) return(NULL); Cudd_Ref(exnor);
1948 Cudd_RecursiveDeref(dd,phi);
1949 sizex = Cudd_DagSize(exnor);
1950 (void) printf("new factor of %d nodes\n", sizex);
1951 retval = Ntr_HeapInsert(T->factors,exnor,sizex);
1952 if (retval == 0) return(NULL);
1953 tmp = Cudd_bddExistAbstract(dd,to,T->nscube[i]);
1954 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
1955 Cudd_RecursiveDeref(dd,to);
1956 to = tmp;
1957 } else {
1958 Cudd_RecursiveDeref(dd,abs);
1959 }
1960 }
1961 Cudd_RecursiveDeref(dd,image);
1962 image = to;
1963 }
1964 if (option->image == NTR_IMAGE_DEPEND) {
1965 int size1, size2;
1966 DdNode *factor1, *factor2, *tmp;
1967 int retval;
1968 size1 = Cudd_DagSize(image);
1969 retval = Ntr_HeapInsert(T->factors,image,size1);
1970 if (retval == 0) return(NULL);
1971 (void) printf("Merging %d factors. Independent image: %d nodes\n",
1972 Ntr_HeapCount(T->factors), size1);
1973 while (Ntr_HeapCount(T->factors) > 1) {
1974 retval = Ntr_HeapExtractMin(T->factors,&factor1,&size1);
1975 if (retval == 0) return(NULL);
1976 retval = Ntr_HeapExtractMin(T->factors,&factor2,&size2);
1977 if (retval == 0) return(NULL);
1978 tmp = Cudd_bddAnd(dd,factor1,factor2);
1979 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
1980 size1 = Cudd_DagSize(tmp);
1981 (void) printf("new factor %d nodes\n", size1);
1982 Cudd_RecursiveDeref(dd,factor1);
1983 Cudd_RecursiveDeref(dd,factor2);
1984 retval = Ntr_HeapInsert(T->factors,tmp,size1);
1985 if (retval == 0) return(NULL);
1986 }
1987 retval = Ntr_HeapExtractMin(T->factors,&image,&size1);
1988 if (retval == 0) return(NULL);
1989 Ntr_freeTR(dd,T);
1990 }
1991
1992 /* Express image in terms of x variables. */
1993 to = Cudd_bddVarMap(dd,image);
1994 if (to == NULL) {
1995 Cudd_RecursiveDeref(dd,image);
1996 return(NULL);
1997 }
1998 Cudd_Ref(to);
1999 Cudd_RecursiveDeref(dd,image);
2000 return(to);
2001
2002 } /* end of ntrImage */
2003
2004
2005 /**
2006 @brief Computes the preimage of a set given a transition relation.
2007
2008 @details The preimage is returned in terms of the next state
2009 variables; its reference count is already increased.
2010
2011 @return a pointer to the result if successful; NULL otherwise.
2012
2013 @sideeffect None
2014
2015 @see ntrImage Ntr_SCC
2016
2017 */
2018 static DdNode *
ntrPreimage(DdManager * dd,NtrPartTR * T,DdNode * from)2019 ntrPreimage(
2020 DdManager * dd,
2021 NtrPartTR * T,
2022 DdNode * from)
2023 {
2024 int i;
2025 DdNode *preimage;
2026 DdNode *to;
2027
2028 /* Existentially quantify the present state variables that are not
2029 ** in the support of any next state function. */
2030 preimage = Cudd_bddExistAbstract(dd,from,T->prepabs);
2031 if (preimage == NULL) return(NULL);
2032 Cudd_Ref(preimage);
2033 for (i = 0; i < T->nparts; i++) {
2034 #if 0
2035 (void) printf(" Intermediate product[%d]: %d nodes\n",
2036 i,Cudd_DagSize(preimage));
2037 #endif
2038 to = Cudd_bddAndAbstract(dd,T->part[i],preimage,T->pcube[i]);
2039 if (to == NULL) return(NULL);
2040 Cudd_Ref(to);
2041 Cudd_RecursiveDeref(dd,preimage);
2042 preimage = to;
2043 }
2044
2045 /* Express preimage in terms of x variables. */
2046 to = Cudd_bddVarMap(dd,preimage);
2047 if (to == NULL) {
2048 Cudd_RecursiveDeref(dd,preimage);
2049 return(NULL);
2050 }
2051 Cudd_Ref(to);
2052 Cudd_RecursiveDeref(dd,preimage);
2053 return(to);
2054
2055 } /* end of ntrPreimage */
2056
2057
2058 /**
2059 @brief Chooses the initial states for a BFS step.
2060
2061 @details The reference count of the result is already incremented.
2062
2063 @return a pointer to the chose set if successful; NULL otherwise.
2064
2065 @sideeffect none
2066
2067 @see Ntr_Trav
2068
2069 */
2070 static DdNode *
ntrChooseFrom(DdManager * dd,DdNode * neW,DdNode * reached,NtrOptions * option)2071 ntrChooseFrom(
2072 DdManager * dd,
2073 DdNode * neW,
2074 DdNode * reached,
2075 NtrOptions * option)
2076 {
2077 DdNode *min, *c;
2078 int threshold;
2079
2080 switch (option->from) {
2081 case NTR_FROM_NEW:
2082 Cudd_Ref(neW);
2083 return(neW);
2084 case NTR_FROM_REACHED:
2085 Cudd_Ref(reached);
2086 return(reached);
2087 case NTR_FROM_RESTRICT:
2088 c = Cudd_bddOr(dd, neW, Cudd_Not(reached));
2089 if (c == NULL) return(NULL);
2090 Cudd_Ref(c);
2091 min = Cudd_bddRestrict(dd,neW,c);
2092 if (min == NULL) {
2093 Cudd_RecursiveDeref(dd, c);
2094 return(NULL);
2095 }
2096 Cudd_Ref(min);
2097 Cudd_RecursiveDeref(dd, c);
2098 return(min);
2099 case NTR_FROM_COMPACT:
2100 c = Cudd_bddOr(dd, neW, Cudd_Not(reached));
2101 if (c == NULL) return(NULL);
2102 Cudd_Ref(c);
2103 min = Cudd_bddLICompaction(dd,neW,c);
2104 if (min == NULL) {
2105 Cudd_RecursiveDeref(dd, c);
2106 return(NULL);
2107 }
2108 Cudd_Ref(min);
2109 Cudd_RecursiveDeref(dd, c);
2110 return(min);
2111 case NTR_FROM_SQUEEZE:
2112 min = Cudd_bddSqueeze(dd,neW,reached);
2113 if (min == NULL) return(NULL);
2114 Cudd_Ref(min);
2115 return(min);
2116 case NTR_FROM_UNDERAPPROX:
2117 threshold = (option->threshold < 0) ? 0 : option->threshold;
2118 min = Cudd_RemapUnderApprox(dd,neW,Cudd_SupportSize(dd,neW),
2119 threshold,option->quality);
2120 if (min == NULL) return(NULL);
2121 Cudd_Ref(min);
2122 return(min);
2123 case NTR_FROM_OVERAPPROX:
2124 threshold = (option->threshold < 0) ? 0 : option->threshold;
2125 min = Cudd_RemapOverApprox(dd,neW,Cudd_SupportSize(dd,neW),
2126 threshold,option->quality);
2127 if (min == NULL) return(NULL);
2128 Cudd_Ref(min);
2129 return(min);
2130 default:
2131 return(NULL);
2132 }
2133
2134 } /* end of ntrChooseFrom */
2135
2136
2137 /**
2138 @brief Updates the reached states after a traversal step.
2139
2140 @details The reference count of the result is already incremented.
2141
2142 @return a pointer to the new reached set if successful; NULL
2143 otherwise.
2144
2145 @sideeffect The old reached set is dereferenced.
2146
2147 @see Ntr_Trav
2148
2149 */
2150 static DdNode *
ntrUpdateReached(DdManager * dd,DdNode * oldreached,DdNode * to)2151 ntrUpdateReached(
2152 DdManager * dd /**< manager */,
2153 DdNode * oldreached /**< old reached state set */,
2154 DdNode * to /**< result of last image computation */)
2155 {
2156 DdNode *reached;
2157
2158 reached = Cudd_bddOr(dd,oldreached,to);
2159 if (reached == NULL) {
2160 Cudd_RecursiveDeref(dd,oldreached);
2161 return(NULL);
2162 }
2163 Cudd_Ref(reached);
2164 Cudd_RecursiveDeref(dd,oldreached);
2165 return(reached);
2166
2167 } /* end of ntrUpdateReached */
2168
2169
2170 /**
2171 @brief Analyzes the reached states after traversal to find
2172 dependent latches.
2173
2174 @details The algorithm is greedy and determines a local optimum, not
2175 a global one.
2176
2177 @return the number of latches that can be eliminated because they
2178 are stuck at a constant value or are dependent on others if
2179 successful; -1 otherwise.
2180
2181 @see Ntr_Trav
2182
2183 */
2184 static int
ntrLatchDependencies(DdManager * dd,DdNode * reached,BnetNetwork * net,NtrOptions * option)2185 ntrLatchDependencies(
2186 DdManager *dd,
2187 DdNode *reached,
2188 BnetNetwork *net,
2189 NtrOptions *option)
2190 {
2191 int i;
2192 int howMany; /* number of latches that can be eliminated */
2193 DdNode *var, *newreached, *abs, *positive, *phi;
2194 char *name;
2195 BnetNode *node;
2196 int initVars, finalVars;
2197 double initStates, finalStates;
2198 DdNode **roots;
2199 char **onames;
2200 int howManySmall = 0;
2201 int *candidates;
2202 double minStates;
2203 int totalVars;
2204
2205 (void) printf("Analyzing latch dependencies\n");
2206 roots = ALLOC(DdNode *, net->nlatches);
2207 if (roots == NULL) return(-1);
2208 onames = ALLOC(char *, net->nlatches);
2209 if (onames == NULL) return(-1);
2210
2211 candidates = ALLOC(int,net->nlatches);
2212 if (candidates == NULL) return(-1);
2213 for (i = 0; i < net->nlatches; i++) {
2214 candidates[i] = i;
2215 }
2216 /* The signatures of the variables in a function are the number
2217 ** of minterms of the positive cofactors with respect to the
2218 ** variables themselves. */
2219 newreached = reached;
2220 Cudd_Ref(newreached);
2221 signatures = Cudd_CofMinterm(dd,newreached);
2222 if (signatures == NULL) return(-1);
2223 /* We now extract a positive quantity which is higher for those
2224 ** variables that are closer to being essential. */
2225 totalVars = Cudd_ReadSize(dd);
2226 minStates = signatures[totalVars];
2227 #if 0
2228 (void) printf("Raw signatures (minStates = %g)\n", minStates);
2229 for (i = 0; i < net->nlatches; i++) {
2230 int j = candidates[i];
2231 if (!st_lookup(net->hash,net->latches[j][1],(void **)&node)) {
2232 return(-1);
2233 }
2234 (void) printf("%s -> %g\n", node->name, signatures[node->dd->index]);
2235 }
2236 #endif
2237 for (i = 0; i < totalVars; i++) {
2238 double z = signatures[i] / minStates - 1.0;
2239 signatures[i] = (z >= 0.0) ? z : -z; /* make positive */
2240 }
2241 staticNet = net;
2242 util_qsort(candidates,net->nlatches,sizeof(int),
2243 (DD_QSFP)ntrSignatureCompare2);
2244 #if 0
2245 (void) printf("Cooked signatures\n");
2246 for (i = 0; i < net->nlatches; i++) {
2247 int j = candidates[i];
2248 if (!st_lookup(net->hash,net->latches[j][1],(void **)&node)) {
2249 return(-1);
2250 }
2251 (void) printf("%s -> %g\n", node->name, signatures[node->dd->index]);
2252 }
2253 #endif
2254 FREE(signatures);
2255
2256 /* Extract simple dependencies. */
2257 for (i = 0; i < net->nlatches; i++) {
2258 int j = candidates[i];
2259 if (!st_lookup(net->hash,net->latches[j][1],(void **)&node)) {
2260 return(-1);
2261 }
2262 var = node->dd;
2263 name = node->name;
2264 if (Cudd_bddVarIsDependent(dd,newreached,var)) {
2265 positive = Cudd_Cofactor(dd,newreached,var);
2266 if (positive == NULL) return(-1); Cudd_Ref(positive);
2267 abs = Cudd_bddExistAbstract(dd,newreached,var);
2268 if (abs == NULL) return(-1); Cudd_Ref(abs);
2269 phi = Cudd_bddLICompaction(dd,positive,abs);
2270 if (phi == NULL) return(-1); Cudd_Ref(phi);
2271 Cudd_RecursiveDeref(dd,positive);
2272 if (Cudd_DagSize(phi) < NTR_MAX_DEP_SIZE) {
2273 if (Cudd_bddLeq(dd,newreached,var)) {
2274 (void) printf("%s is stuck at 1\n",name);
2275 } else if (Cudd_bddLeq(dd,newreached,Cudd_Not(var))) {
2276 (void) printf("%s is stuck at 0\n",name);
2277 } else {
2278 (void) printf("%s depends on the other variables\n",name);
2279 }
2280 roots[howManySmall] = phi;
2281 onames[howManySmall] = util_strsav(name);
2282 Cudd_RecursiveDeref(dd,newreached);
2283 newreached = abs;
2284 howManySmall++;
2285 candidates[i] = -1; /* do not reconsider */
2286 } else {
2287 Cudd_RecursiveDeref(dd,abs);
2288 Cudd_RecursiveDeref(dd,phi);
2289 }
2290 } else {
2291 candidates[i] = -1; /* do not reconsider */
2292 }
2293 }
2294 /* Now remove remaining dependent variables. */
2295 howMany = howManySmall;
2296 for (i = 0; i < net->nlatches; i++) {
2297 int j = candidates[i];
2298 if (j == -1) continue;
2299 if (!st_lookup(net->hash,net->latches[j][1],(void **)&node)) {
2300 return(-1);
2301 }
2302 var = node->dd;
2303 name = node->name;
2304 if (Cudd_bddVarIsDependent(dd,newreached,var)) {
2305 if (Cudd_bddLeq(dd,newreached,var)) {
2306 (void) printf("%s is stuck at 1\n",name);
2307 } else if (Cudd_bddLeq(dd,newreached,Cudd_Not(var))) {
2308 (void) printf("%s is stuck at 0\n",name);
2309 } else {
2310 (void) printf("%s depends on the other variables\n",name);
2311 }
2312 abs = Cudd_bddExistAbstract(dd,newreached,var);
2313 if (abs == NULL) return(-1); Cudd_Ref(abs);
2314 Cudd_RecursiveDeref(dd,newreached);
2315 newreached = abs;
2316 howMany++;
2317 }
2318 }
2319 FREE(candidates);
2320 if (howManySmall > 0 && option->verb > 1) {
2321 if (!Bnet_bddArrayDump(dd,net,(char *)"-",roots,onames,howManySmall,1))
2322 return(-1);
2323 }
2324 for (i = 0; i < howManySmall; i++) {
2325 Cudd_RecursiveDeref(dd,roots[i]);
2326 FREE(onames[i]);
2327 }
2328 FREE(roots);
2329 FREE(onames);
2330
2331 initVars = net->nlatches;
2332 initStates = Cudd_CountMinterm(dd,reached,initVars);
2333 finalVars = initVars - howMany;
2334 finalStates = Cudd_CountMinterm(dd,newreached,finalVars);
2335 if (initStates != finalStates) {
2336 (void) printf("Error: the number of states changed from %g to %g\n",
2337 initStates, finalStates);
2338 return(-1);
2339 }
2340 (void) printf("new reached");
2341 Cudd_PrintDebug(dd,newreached,finalVars,option->verb);
2342 Cudd_RecursiveDeref(dd,newreached);
2343 return(howMany);
2344
2345 } /* end of ntrLatchDependencies */
2346
2347
2348 /**
2349 @brief Eliminates dependent variables from a transition relation.
2350
2351 @return a simplified copy of the given transition relation if
2352 successful; NULL otherwise.
2353
2354 @sideeffect The modified set of states is returned as a side effect.
2355
2356 @see ntrImage
2357
2358 */
2359 static NtrPartTR *
ntrEliminateDependencies(DdManager * dd,NtrPartTR * TR,DdNode ** states,NtrOptions * option)2360 ntrEliminateDependencies(
2361 DdManager *dd,
2362 NtrPartTR *TR,
2363 DdNode **states,
2364 NtrOptions *option)
2365 {
2366 NtrPartTR *T; /* new TR without dependent vars */
2367 int pr = option->verb;
2368 int i, j;
2369 int howMany = 0; /* number of latches that can be eliminated */
2370 DdNode *var, *newstates, *abs, *positive, *phi;
2371 DdNode *support, *scan, *tmp;
2372 int finalSize; /* size of the TR after substitutions */
2373 int nvars; /* vars in the support of the state set */
2374 int *candidates; /* vars to be considered for elimination */
2375 int totalVars;
2376 double minStates;
2377
2378 /* Initialize the new transition relation by copying the old one. */
2379 T = Ntr_cloneTR(TR);
2380 if (T == NULL) return(NULL);
2381
2382 /* Find and rank the candidate variables. */
2383 newstates = *states;
2384 Cudd_Ref(newstates);
2385 support = Cudd_Support(dd,newstates);
2386 if (support == NULL) {
2387 Cudd_RecursiveDeref(dd,newstates);
2388 Ntr_freeTR(dd,T);
2389 return(NULL);
2390 }
2391 Cudd_Ref(support);
2392 nvars = Cudd_DagSize(support) - 1;
2393 candidates = ALLOC(int,nvars);
2394 if (candidates == NULL) {
2395 Cudd_RecursiveDeref(dd,support);
2396 Cudd_RecursiveDeref(dd,newstates);
2397 Ntr_freeTR(dd,T);
2398 return(NULL);
2399 }
2400 scan = support;
2401 for (i = 0; i < nvars; i++) {
2402 candidates[i] = scan->index;
2403 scan = Cudd_T(scan);
2404 }
2405 Cudd_RecursiveDeref(dd,support);
2406 /* The signatures of the variables in a function are the number
2407 ** of minterms of the positive cofactors with respect to the
2408 ** variables themselves. */
2409 signatures = Cudd_CofMinterm(dd,newstates);
2410 if (signatures == NULL) {
2411 FREE(candidates);
2412 Cudd_RecursiveDeref(dd,newstates);
2413 Ntr_freeTR(dd,T);
2414 return(NULL);
2415 }
2416 /* We now extract a positive quantity which is higher for those
2417 ** variables that are closer to being essential. */
2418 totalVars = Cudd_ReadSize(dd);
2419 minStates = signatures[totalVars];
2420 for (i = 0; i < totalVars; i++) {
2421 double z = signatures[i] / minStates - 1.0;
2422 signatures[i] = (z < 0.0) ? -z : z; /* make positive */
2423 }
2424 /* Sort candidates in decreasing order of signature. */
2425 util_qsort(candidates,nvars,sizeof(int), (DD_QSFP)ntrSignatureCompare);
2426 FREE(signatures);
2427
2428 /* Now process the candidates in the given order. */
2429 for (i = 0; i < nvars; i++) {
2430 var = Cudd_bddIthVar(dd,candidates[i]);
2431 if (Cudd_bddVarIsDependent(dd,newstates,var)) {
2432 abs = Cudd_bddExistAbstract(dd,newstates,var);
2433 if (abs == NULL) return(NULL); Cudd_Ref(abs);
2434 positive = Cudd_Cofactor(dd,newstates,var);
2435 if (positive == NULL) return(NULL); Cudd_Ref(positive);
2436 phi = Cudd_bddLICompaction(dd,positive,abs);
2437 if (phi == NULL) return(NULL); Cudd_Ref(phi);
2438 Cudd_RecursiveDeref(dd,positive);
2439 #if 0
2440 if (pr > 0) {
2441 (void) printf("Phi");
2442 Cudd_PrintDebug(dd,phi,T->nlatches,pr);
2443 }
2444 #endif
2445 if (Cudd_DagSize(phi) < NTR_MAX_DEP_SIZE) {
2446 howMany++;
2447 for (j = 0; j < T->nparts; j++) {
2448 tmp = Cudd_bddCompose(dd,T->part[j],phi,candidates[i]);
2449 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
2450 Cudd_RecursiveDeref(dd,T->part[j]);
2451 T->part[j] = tmp;
2452 }
2453 Cudd_RecursiveDeref(dd,newstates);
2454 newstates = abs;
2455 } else {
2456 Cudd_RecursiveDeref(dd,abs);
2457 }
2458 Cudd_RecursiveDeref(dd,phi);
2459 }
2460 }
2461 FREE(candidates);
2462
2463 if (pr > 0) {
2464 finalSize = Cudd_SharingSize(T->part,T->nparts);
2465 (void) printf("Eliminated %d vars. Transition function %d nodes.\n",
2466 howMany,finalSize);
2467 }
2468
2469 if (!ntrUpdateQuantificationSchedule(dd,T)) return(NULL);
2470
2471 /* Quantify out of states variables that no longer appear in any part. */
2472 Cudd_RecursiveDeref(dd,*states);
2473 *states = Cudd_bddExistAbstract(dd,newstates,T->preiabs);
2474 if (*states == NULL) {
2475 Cudd_RecursiveDeref(dd,newstates);
2476 return(NULL);
2477 }
2478 Cudd_Ref(*states);
2479 Cudd_RecursiveDeref(dd,newstates);
2480 return(T);
2481
2482 } /* end of ntrEliminateDependencies */
2483
2484
2485 /**
2486 @brief Updates the quantification schedule of a transition relation.
2487
2488 @return 1 if successful; 0 otherwise.
2489
2490 @sideeffect None
2491
2492 @see ntrEliminateDependencies
2493
2494 */
2495 static int
ntrUpdateQuantificationSchedule(DdManager * dd,NtrPartTR * T)2496 ntrUpdateQuantificationSchedule(
2497 DdManager *dd,
2498 NtrPartTR *T)
2499 {
2500 int i, j, k;
2501 int *schedule;
2502 DdNode *one, *support, *scan, *var, *tmp;
2503 char **matrix;
2504 int *position, *row;
2505 char *flags;
2506 int nparts, nvars;
2507 int extracted;
2508 #if 0
2509 int schedcost;
2510 #endif
2511
2512 nparts = T->nparts;
2513 nvars = Cudd_ReadSize(dd);
2514 one = Cudd_ReadOne(dd);
2515
2516 /* Reinitialize the abstraction cubes. */
2517 Cudd_RecursiveDeref(dd,T->preiabs);
2518 T->preiabs = one;
2519 Cudd_Ref(one);
2520 for (i = 0; i < nparts; i++) {
2521 Cudd_RecursiveDeref(dd,T->icube[i]);
2522 T->icube[i] = one;
2523 Cudd_Ref(one);
2524 }
2525
2526 /* Initialize row permutations to the identity. */
2527 position = ALLOC(int,nparts);
2528 if (position == NULL) return(0);
2529 for (i = 0; i < nparts; i++) {
2530 position[i] = i;
2531 }
2532 /* Sort parts so that parts that differ only
2533 ** in the index of the next state variable are contiguous. */
2534 staticPart = T->part;
2535 util_qsort(position,nparts,sizeof(int), (DD_QSFP)ntrPartCompare);
2536 /* Extract repeated parts. */
2537 extracted = 0;
2538 for (i = 0; i < nparts - 1; i += j) {
2539 int pi, pij;
2540 DdNode *eq;
2541 j = 1;
2542 pi = position[i];
2543 eq = one;
2544 Cudd_Ref(eq);
2545 pij = position[i+j];
2546 while (Cudd_Regular(staticPart[pij]) == Cudd_Regular(staticPart[pi])) {
2547 int comple = staticPart[pij] != staticPart[pi];
2548 DdNode *xnor = Cudd_bddXnor(dd,T->nscube[pi],
2549 Cudd_NotCond(T->nscube[pij],comple));
2550 if (xnor == NULL) return(0); Cudd_Ref(xnor);
2551 tmp = Cudd_bddAnd(dd,xnor,eq);
2552 if (tmp == NULL) return(0); Cudd_Ref(tmp);
2553 Cudd_RecursiveDeref(dd,xnor);
2554 Cudd_RecursiveDeref(dd,eq);
2555 eq = tmp;
2556 Cudd_RecursiveDeref(dd,T->part[pij]);
2557 Cudd_RecursiveDeref(dd,T->icube[pij]);
2558 Cudd_RecursiveDeref(dd,T->pcube[pij]);
2559 Cudd_RecursiveDeref(dd,T->nscube[pij]);
2560 T->part[pij] = NULL;
2561 j++;
2562 if (i+j == nparts) break;
2563 pij = position[i+j];
2564 }
2565 if (eq != one) {
2566 int retval = Ntr_HeapInsert(T->factors,eq,Cudd_DagSize(eq));
2567 if (retval == 0) return(0);
2568 extracted += j - 1;
2569 } else {
2570 Cudd_RecursiveDeref(dd,eq);
2571 }
2572 }
2573 /* Compact the part array by removing extracted parts. */
2574 for (i = 0, j = 0; i < nparts; i++) {
2575 if (T->part[i] != NULL) {
2576 T->part[j] = T->part[i];
2577 T->icube[j] = T->icube[i];
2578 T->pcube[j] = T->pcube[i];
2579 T->nscube[j] = T->nscube[i];
2580 j++;
2581 }
2582 }
2583 nparts = T->nparts -= extracted;
2584 (void) printf("Extracted %d repeated parts in %d factors.\n",
2585 extracted, Ntr_HeapCount(T->factors));
2586
2587 /* Build the support matrix. Each row corresponds to a part of the
2588 ** transition relation; each column corresponds to a variable in
2589 ** the manager. A 1 in position (i,j) means that Part i depends
2590 ** on Variable j. */
2591 matrix = ntrAllocMatrix(nparts,nvars);
2592 if (matrix == NULL) return(0);
2593
2594 /* Allocate array for quantification schedule and initialize it. */
2595 schedule = ALLOC(int,nvars);
2596 if (schedule == NULL) return(0);
2597 for (i = 0; i < nvars; i++) {
2598 schedule[i] = -1;
2599 }
2600 /* Collect scheduling info for this part. At the end of this loop
2601 ** schedule[i] == j means that the variable of index i does not
2602 ** appear in any part with index greater than j, unless j == -1,
2603 ** in which case the variable appears in no part.
2604 */
2605 for (i = 0; i < nparts; i++) {
2606 support = Cudd_Support(dd,T->part[i]);
2607 if (support == NULL) return(0); Cudd_Ref(support);
2608 scan = support;
2609 while (!Cudd_IsConstant(scan)) {
2610 int index = scan->index;
2611 schedule[index] = i;
2612 matrix[i][index] = 1;
2613 scan = Cudd_T(scan);
2614 }
2615 Cudd_RecursiveDeref(dd,support);
2616 }
2617 #if 0
2618 (void) printf("Initial schedule:");
2619 schedcost = 0;
2620 for (i = 0; i < nvars; i++) {
2621 (void) printf(" %d", schedule[i]);
2622 if (schedule[i] != -1) schedcost += schedule[i];
2623 }
2624 (void) printf("\nCost = %d\n", schedcost);
2625 #endif
2626
2627 /* Initialize direct and inverse row permutations to the identity
2628 ** permutation. */
2629 row = ALLOC(int,nparts);
2630 if (row == NULL) return(0);
2631 for (i = 0; i < nparts; i++) {
2632 position[i] = row[i] = i;
2633 }
2634
2635 /* Sift the matrix. */
2636 flags = ALLOC(char,nvars);
2637 if (flags == NULL) return(0);
2638 for (i = 0; i < nparts; i++) {
2639 int cost = 0; /* cost of moving the row */
2640 int bestcost = 0;
2641 int posn = position[i];
2642 int bestposn = posn;
2643 /* Sift up. */
2644 /* Initialize the flags to one is for the variables that are
2645 ** currently scheduled to be quantified after this part gets
2646 ** multiplied. When we cross a row of a part that depends on
2647 ** a variable whose flag is 1, we know that the row being sifted
2648 ** is no longer responsible for that variable. */
2649 for (k = 0; k < nvars; k++) {
2650 flags[k] = (char) (schedule[k] == i);
2651 }
2652 for (j = posn - 1; j >= 0; j--) {
2653 for (k = 0; k < nvars; k++) {
2654 if (schedule[k] == row[j]) {
2655 cost++;
2656 } else {
2657 flags[k] &= (matrix[row[j]][k] == 0);
2658 cost -= flags[k];
2659 }
2660 }
2661 if (cost < bestcost) {
2662 bestposn = j;
2663 bestcost = cost;
2664 }
2665 }
2666 /* Sift down. */
2667 /* Reinitialize the flags. (We are implicitly undoing the sift
2668 ** down step.) */
2669 for (k = 0; k < nvars; k++) {
2670 flags[k] = (char) (schedule[k] == i);
2671 }
2672 for (j = posn + 1; j < nparts; j++) {
2673 for (k = 0; k < nvars; k++) {
2674 if (schedule[k] == row[j]) {
2675 flags[k] |= (matrix[i][k] == 1);
2676 cost -= flags[k] == 0;
2677 } else {
2678 cost += flags[k];
2679 }
2680 }
2681 if (cost < bestcost) {
2682 bestposn = j;
2683 bestcost = cost;
2684 }
2685 }
2686 /* Move to best position. */
2687 if (bestposn < posn) {
2688 for (j = posn; j >= bestposn; j--) {
2689 k = row[j];
2690 if (j > 0) row[j] = row[j-1];
2691 position[k]++;
2692 }
2693 } else {
2694 for (j = posn; j <= bestposn; j++) {
2695 k = row[j];
2696 if (j < nparts - 1) row[j] = row[j+1];
2697 position[k]--;
2698 }
2699 }
2700 position[i] = bestposn;
2701 row[bestposn] = i;
2702 /* Fix the schedule. */
2703 for (k = 0; k < nvars; k++) {
2704 if (matrix[i][k] == 1) {
2705 if (position[schedule[k]] < bestposn) {
2706 schedule[k] = i;
2707 } else {
2708 for (j = nparts - 1; j >= position[i]; j--) {
2709 if (matrix[row[j]][k] == 1) break;
2710 }
2711 schedule[k] = row[j];
2712 }
2713 }
2714 }
2715 }
2716 ntrFreeMatrix(matrix);
2717 FREE(flags);
2718
2719 /* Update schedule to account for the permutation. */
2720 for (i = 0; i < nvars; i++) {
2721 if (schedule[i] >= 0) {
2722 schedule[i] = position[schedule[i]];
2723 }
2724 }
2725 /* Sort parts. */
2726 ntrPermuteParts(T->part,T->nscube,row,position,nparts);
2727 FREE(position);
2728 FREE(row);
2729 #if 0
2730 (void) printf("New schedule:");
2731 schedcost = 0;
2732 for (i = 0; i < nvars; i++) {
2733 (void) printf(" %d", schedule[i]);
2734 if (schedule[i] != -1) schedcost += schedule[i];
2735 }
2736 (void) printf("\nCost = %d\n", schedcost);
2737 #endif
2738
2739 /* Mark the next state varibles so that they do not go in the
2740 ** abstraction cubes. */
2741 for (i = 0; i < T->nlatches; i++) {
2742 schedule[T->y[i]->index] = -2;
2743 }
2744
2745 /* Rebuild the cubes from the schedule. */
2746 for (i = 0; i < nvars; i++) {
2747 k = schedule[i];
2748 var = Cudd_bddIthVar(dd,i);
2749 if (k >= 0) {
2750 tmp = Cudd_bddAnd(dd,T->icube[k],var);
2751 if (tmp == NULL) return(0); Cudd_Ref(tmp);
2752 Cudd_RecursiveDeref(dd,T->icube[k]);
2753 T->icube[k] = tmp;
2754 } else if (k != -2) {
2755 tmp = Cudd_bddAnd(dd,T->preiabs,var);
2756 if (tmp == NULL) return(0); Cudd_Ref(tmp);
2757 Cudd_RecursiveDeref(dd,T->preiabs);
2758 T->preiabs = tmp;
2759 }
2760 }
2761 FREE(schedule);
2762
2763 /* Build the conjuncts. */
2764 for (i = 0; i < nparts; i++) {
2765 tmp = Cudd_bddXnor(dd,T->nscube[i],T->part[i]);
2766 if (tmp == NULL) return(0); Cudd_Ref(tmp);
2767 Cudd_RecursiveDeref(dd,T->part[i]);
2768 T->part[i] = tmp;
2769 }
2770
2771 return(1);
2772
2773 } /* end of ntrUpdateQuantificationSchedule */
2774
2775
2776 /**
2777 @brief Comparison function used by qsort.
2778
2779 @details Used to order the variables according to their signatures.
2780
2781 @sideeffect None
2782
2783 */
2784 static int
ntrSignatureCompare(int * ptrX,int * ptrY)2785 ntrSignatureCompare(
2786 int * ptrX,
2787 int * ptrY)
2788 {
2789 if (signatures[*ptrY] > signatures[*ptrX]) return(1);
2790 if (signatures[*ptrY] < signatures[*ptrX]) return(-1);
2791 return(0);
2792
2793 } /* end of ntrSignatureCompare */
2794
2795
2796 /**
2797 @brief Comparison function used by qsort.
2798
2799 @details Used to order the variables according to their signatures.
2800
2801 @sideeffect None
2802
2803 */
2804 static int
ntrSignatureCompare2(int * ptrX,int * ptrY)2805 ntrSignatureCompare2(
2806 int * ptrX,
2807 int * ptrY)
2808 {
2809 BnetNode *node;
2810 int x,y;
2811 if (!st_lookup(staticNet->hash,staticNet->latches[*ptrX][1],(void**)&node)) {
2812 return(0);
2813 }
2814 x = node->dd->index;
2815 if (!st_lookup(staticNet->hash,staticNet->latches[*ptrY][1],(void**)&node)) {
2816 return(0);
2817 }
2818 y = node->dd->index;
2819 if (signatures[x] < signatures[y]) return(1);
2820 if (signatures[x] > signatures[y]) return(-1);
2821 return(0);
2822
2823 } /* end of ntrSignatureCompare2 */
2824
2825
2826 /**
2827 @brief Comparison function used by qsort.
2828
2829 @details Used to order the parts according to their %BDD addresses.
2830
2831 @sideeffect None
2832
2833 */
2834 static int
ntrPartCompare(int * ptrX,int * ptrY)2835 ntrPartCompare(
2836 int * ptrX,
2837 int * ptrY)
2838 {
2839 if (staticPart[*ptrY] > staticPart[*ptrX]) return(1);
2840 if (staticPart[*ptrY] < staticPart[*ptrX]) return(-1);
2841 return(0);
2842
2843 } /* end of ntrPartCompare */
2844
2845
2846 /**
2847 @brief Allocates a matrix of char's.
2848
2849 @return a pointer to the matrix if successful; NULL otherwise.
2850
2851 @sideeffect None
2852
2853 */
2854 static char **
ntrAllocMatrix(int nrows,int ncols)2855 ntrAllocMatrix(
2856 int nrows,
2857 int ncols)
2858 {
2859 int i;
2860 char **matrix;
2861
2862 matrix = ALLOC(char *,nrows);
2863 if (matrix == NULL) return(NULL);
2864 matrix[0] = ALLOC(char,nrows * ncols);
2865 if (matrix[0] == NULL) {
2866 FREE(matrix);
2867 return(NULL);
2868 }
2869 for (i = 1; i < nrows; i++) {
2870 matrix[i] = matrix[i-1] + ncols;
2871 }
2872 for (i = 0; i < nrows * ncols; i++) {
2873 matrix[0][i] = 0;
2874 }
2875 return(matrix);
2876
2877 } /* end of ntrAllocMatrix */
2878
2879
2880 /**
2881 @brief Frees a matrix of char's.
2882
2883 @sideeffect None
2884
2885 */
2886 static void
ntrFreeMatrix(char ** matrix)2887 ntrFreeMatrix(
2888 char **matrix)
2889 {
2890 FREE(matrix[0]);
2891 FREE(matrix);
2892 return;
2893
2894 } /* end of ntrFreeMatrix */
2895
2896
2897 /**
2898 @brief Sorts parts according to given permutation.
2899
2900 @sideeffect The permutation arrays are turned into the identity
2901 permutations.
2902
2903 */
2904 static void
ntrPermuteParts(DdNode ** a,DdNode ** b,int * comesFrom,int * goesTo,int size)2905 ntrPermuteParts(
2906 DdNode **a,
2907 DdNode **b,
2908 int *comesFrom,
2909 int *goesTo,
2910 int size)
2911 {
2912 int i, j;
2913 DdNode *tmp;
2914
2915 for (i = 0; i < size; i++) {
2916 if (comesFrom[i] == i) continue;
2917 j = comesFrom[i];
2918 tmp = a[i]; a[i] = a[j]; a[j] = tmp;
2919 tmp = b[i]; b[i] = b[j]; b[j] = tmp;
2920 comesFrom[goesTo[i]] = j;
2921 comesFrom[i] = i;
2922 goesTo[j] = goesTo[i];
2923 goesTo[i] = i;
2924 }
2925 return;
2926
2927 } /* end of ntrPermuteParts */
2928
2929
2930 /**
2931 @brief Calls Cudd_Ref on its first argument.
2932 */
2933 static void
ntrIncreaseRef(void * e,void * arg)2934 ntrIncreaseRef(
2935 void * e,
2936 void * arg)
2937 {
2938 DdNode * node = (DdNode *) e;
2939 (void) arg; /* avoid warning */
2940 Cudd_Ref(node);
2941
2942 } /* end of ntrIncreaseRef */
2943
2944
2945 /**
2946 @brief Calls Cudd_RecursiveDeref on its first argument.
2947 */
2948 static void
ntrDecreaseRef(void * e,void * arg)2949 ntrDecreaseRef(
2950 void * e,
2951 void * arg)
2952 {
2953 DdNode * node = (DdNode *) e;
2954 DdManager * dd = (DdManager *) arg;
2955 Cudd_RecursiveDeref(dd, node);
2956
2957 } /* end of ntrIncreaseRef */
2958