1 /**
2 @file
3
4 @ingroup nanotrav
5
6 @brief Functions to read in a boolean network.
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 "bnet.h"
48
49 /*---------------------------------------------------------------------------*/
50 /* Constant declarations */
51 /*---------------------------------------------------------------------------*/
52
53 #define MAXLENGTH 131072
54
55 /*---------------------------------------------------------------------------*/
56 /* Stucture declarations */
57 /*---------------------------------------------------------------------------*/
58
59 /*---------------------------------------------------------------------------*/
60 /* Type declarations */
61 /*---------------------------------------------------------------------------*/
62
63 /*---------------------------------------------------------------------------*/
64 /* Variable declarations */
65 /*---------------------------------------------------------------------------*/
66
67 static char BuffLine[MAXLENGTH];
68 static char *CurPos;
69 static int newNameNumber = 0;
70
71 /*---------------------------------------------------------------------------*/
72 /* Macro declarations */
73 /*---------------------------------------------------------------------------*/
74
75 /** \cond */
76
77 /*---------------------------------------------------------------------------*/
78 /* Static function prototypes */
79 /*---------------------------------------------------------------------------*/
80
81 static char * readString (FILE *fp);
82 static char ** readList (FILE *fp, int *n);
83 static void printList (char **list, int n);
84 static char ** bnetGenerateNewNames (st_table *hash, int n);
85 static int bnetDumpReencodingLogic (DdManager *dd, char *mname, int noutputs, DdNode **outputs, char **inames, char **altnames, char **onames, FILE *fp);
86 #if 0
87 static int bnetBlifXnorTable (FILE *fp, int n);
88 #endif
89 static int bnetBlifWriteReencode (DdManager *dd, char *mname, char **inames, char **altnames, int *support, FILE *fp);
90 static int * bnetFindVectorSupport (DdManager *dd, DdNode **list, int n);
91 static int buildExorBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop);
92 static int buildMuxBDD (DdManager * dd, BnetNode * nd, st_table * hash, int params, int nodrop);
93 static int bnetSetLevel (BnetNetwork *net);
94 static int bnetLevelDFS (BnetNetwork *net, BnetNode *node);
95 static BnetNode ** bnetOrderRoots (BnetNetwork *net, int *nroots);
96 static int bnetLevelCompare (BnetNode **x, BnetNode **y);
97 static int bnetDfsOrder (DdManager *dd, BnetNetwork *net, BnetNode *node);
98
99 /** \endcond */
100
101
102 /*---------------------------------------------------------------------------*/
103 /* Definition of exported functions */
104 /*---------------------------------------------------------------------------*/
105
106
107 /**
108 @brief Reads boolean network from blif file.
109
110 @details A very restricted subset of blif is supported. Specifically:
111 <ul>
112 <li> The only directives recognized are:
113 <ul>
114 <li> .model
115 <li> .inputs
116 <li> .outputs
117 <li> .latch
118 <li> .names
119 <li> .exdc
120 <li> .wire_load_slope
121 <li> .end
122 </ul>
123 <li> Latches must have an initial values and no other parameters
124 specified.
125 <li> Lines must not exceed MAXLENGTH-1 characters, and individual names must
126 not exceed 1023 characters.
127 </ul>
128 Caveat emptor: There may be other limitations as well. One should
129 check the syntax of the blif file with some other tool before relying
130 on this parser.
131
132 @return a pointer to the network if successful; NULL otherwise.
133
134 @sideeffect None
135
136 @see Bnet_PrintNetwork Bnet_FreeNetwork
137
138 */
139 BnetNetwork *
Bnet_ReadNetwork(FILE * fp,int pr)140 Bnet_ReadNetwork(
141 FILE * fp /**< pointer to the blif file */,
142 int pr /**< verbosity level */)
143 {
144 char *savestring;
145 char **list;
146 int i, j, n;
147 BnetNetwork *net;
148 BnetNode *newnode;
149 BnetNode *lastnode = NULL;
150 BnetTabline *newline;
151 BnetTabline *lastline;
152 char ***latches = NULL;
153 int maxlatches = 0;
154 int exdc = 0;
155 BnetNode *node;
156 int count;
157
158 /* Allocate network object and initialize symbol table. */
159 net = ALLOC(BnetNetwork,1);
160 if (net == NULL) goto failure;
161 memset((char *) net, 0, sizeof(BnetNetwork));
162 net->hash = st_init_table((st_compare_t) strcmp, st_strhash);
163 if (net->hash == NULL) goto failure;
164
165 savestring = readString(fp);
166 if (savestring == NULL) goto failure;
167 net->nlatches = 0;
168 while (strcmp(savestring, ".model") == 0 ||
169 strcmp(savestring, ".inputs") == 0 ||
170 strcmp(savestring, ".outputs") == 0 ||
171 strcmp(savestring, ".latch") == 0 ||
172 strcmp(savestring, ".wire_load_slope") == 0 ||
173 strcmp(savestring, ".exdc") == 0 ||
174 strcmp(savestring, ".names") == 0 || strcmp(savestring,".end") == 0) {
175 if (strcmp(savestring, ".model") == 0) {
176 /* Read .model directive. */
177 FREE(savestring);
178 /* Read network name. */
179 savestring = readString(fp);
180 if (savestring == NULL) goto failure;
181 if (savestring[0] == '.') {
182 net->name = ALLOC(char, 1);
183 if (net->name == NULL) goto failure;
184 net->name[0] = '\0';
185 } else {
186 net->name = savestring;
187 }
188 } else if (strcmp(savestring, ".inputs") == 0) {
189 /* Read .inputs directive. */
190 FREE(savestring);
191 /* Read input names. */
192 list = readList(fp,&n);
193 if (list == NULL) goto failure;
194 if (pr > 2) printList(list,n);
195 /* Expect at least one input. */
196 if (n < 1) {
197 (void) fprintf(stdout,"Empty input list.\n");
198 goto failure;
199 }
200 if (exdc) {
201 for (i = 0; i < n; i++)
202 FREE(list[i]);
203 FREE(list);
204 savestring = readString(fp);
205 if (savestring == NULL) goto failure;
206 continue;
207 }
208 if (net->ninputs) {
209 net->inputs = REALLOC(char *, net->inputs,
210 (net->ninputs + n) * sizeof(char *));
211 for (i = 0; i < n; i++)
212 net->inputs[net->ninputs + i] = list[i];
213 }
214 else
215 net->inputs = list;
216 /* Create a node for each primary input. */
217 for (i = 0; i < n; i++) {
218 newnode = ALLOC(BnetNode,1);
219 memset((char *) newnode, 0, sizeof(BnetNode));
220 if (newnode == NULL) goto failure;
221 newnode->name = list[i];
222 newnode->inputs = NULL;
223 newnode->type = BNET_INPUT_NODE;
224 newnode->active = FALSE;
225 newnode->nfo = 0;
226 newnode->ninp = 0;
227 newnode->f = NULL;
228 newnode->polarity = 0;
229 newnode->dd = NULL;
230 newnode->next = NULL;
231 if (lastnode == NULL) {
232 net->nodes = newnode;
233 } else {
234 lastnode->next = newnode;
235 }
236 lastnode = newnode;
237 }
238 net->npis += n;
239 net->ninputs += n;
240 } else if (strcmp(savestring, ".outputs") == 0) {
241 /* Read .outputs directive. We do not create nodes for the primary
242 ** outputs, because the nodes will be created when the same names
243 ** appear as outputs of some gates.
244 */
245 FREE(savestring);
246 /* Read output names. */
247 list = readList(fp,&n);
248 if (list == NULL) goto failure;
249 if (pr > 2) printList(list,n);
250 if (n < 1) {
251 (void) fprintf(stdout,"Empty .outputs list.\n");
252 goto failure;
253 }
254 if (exdc) {
255 for (i = 0; i < n; i++)
256 FREE(list[i]);
257 FREE(list);
258 savestring = readString(fp);
259 if (savestring == NULL) goto failure;
260 continue;
261 }
262 if (net->noutputs) {
263 net->outputs = REALLOC(char *, net->outputs,
264 (net->noutputs + n) * sizeof(char *));
265 for (i = 0; i < n; i++)
266 net->outputs[net->noutputs + i] = list[i];
267 } else {
268 net->outputs = list;
269 }
270 net->npos += n;
271 net->noutputs += n;
272 } else if (strcmp(savestring,".wire_load_slope") == 0) {
273 FREE(savestring);
274 savestring = readString(fp);
275 net->slope = savestring;
276 } else if (strcmp(savestring,".latch") == 0) {
277 FREE(savestring);
278 newnode = ALLOC(BnetNode,1);
279 if (newnode == NULL) goto failure;
280 memset((char *) newnode, 0, sizeof(BnetNode));
281 newnode->type = BNET_PRESENT_STATE_NODE;
282 list = readList(fp,&n);
283 if (list == NULL) goto failure;
284 if (pr > 2) printList(list,n);
285 /* Expect three names. */
286 if (n != 3) {
287 (void) fprintf(stdout,
288 ".latch not followed by three tokens.\n");
289 goto failure;
290 }
291 newnode->name = list[1];
292 newnode->inputs = NULL;
293 newnode->ninp = 0;
294 newnode->f = NULL;
295 newnode->active = FALSE;
296 newnode->nfo = 0;
297 newnode->polarity = 0;
298 newnode->dd = NULL;
299 newnode->next = NULL;
300 if (lastnode == NULL) {
301 net->nodes = newnode;
302 } else {
303 lastnode->next = newnode;
304 }
305 lastnode = newnode;
306 /* Add next state variable to list. */
307 if (maxlatches == 0) {
308 maxlatches = 20;
309 latches = ALLOC(char **,maxlatches);
310 } else if (maxlatches <= net->nlatches) {
311 maxlatches += 20;
312 latches = REALLOC(char **,latches,maxlatches);
313 }
314 latches[net->nlatches] = list;
315 net->nlatches++;
316 savestring = readString(fp);
317 if (savestring == NULL) goto failure;
318 } else if (strcmp(savestring,".names") == 0) {
319 FREE(savestring);
320 newnode = ALLOC(BnetNode,1);
321 memset((char *) newnode, 0, sizeof(BnetNode));
322 if (newnode == NULL) goto failure;
323 list = readList(fp,&n);
324 if (list == NULL) goto failure;
325 if (pr > 2) printList(list,n);
326 /* Expect at least one name (the node output). */
327 if (n < 1) {
328 (void) fprintf(stdout,"Missing output name.\n");
329 goto failure;
330 }
331 newnode->name = list[n-1];
332 newnode->inputs = list;
333 newnode->ninp = n-1;
334 newnode->active = FALSE;
335 newnode->nfo = 0;
336 newnode->polarity = 0;
337 if (newnode->ninp > 0) {
338 newnode->type = BNET_INTERNAL_NODE;
339 for (i = 0; i < net->noutputs; i++) {
340 if (strcmp(net->outputs[i], newnode->name) == 0) {
341 newnode->type = BNET_OUTPUT_NODE;
342 break;
343 }
344 }
345 } else {
346 newnode->type = BNET_CONSTANT_NODE;
347 }
348 newnode->dd = NULL;
349 newnode->next = NULL;
350 if (lastnode == NULL) {
351 net->nodes = newnode;
352 } else {
353 lastnode->next = newnode;
354 }
355 lastnode = newnode;
356 /* Read node function. */
357 newnode->f = NULL;
358 if (exdc) {
359 newnode->exdc_flag = 1;
360 node = net->nodes;
361 while (node) {
362 if (node->type == BNET_OUTPUT_NODE &&
363 strcmp(node->name, newnode->name) == 0) {
364 node->exdc = newnode;
365 break;
366 }
367 node = node->next;
368 }
369 }
370 savestring = readString(fp);
371 if (savestring == NULL) goto failure;
372 lastline = NULL;
373 while (savestring[0] != '.') {
374 /* Reading a table line. */
375 newline = ALLOC(BnetTabline,1);
376 if (newline == NULL) goto failure;
377 newline->next = NULL;
378 if (lastline == NULL) {
379 newnode->f = newline;
380 } else {
381 lastline->next = newline;
382 }
383 lastline = newline;
384 if (newnode->type == BNET_INTERNAL_NODE ||
385 newnode->type == BNET_OUTPUT_NODE) {
386 newline->values = savestring;
387 /* Read output 1 or 0. */
388 savestring = readString(fp);
389 if (savestring == NULL) goto failure;
390 } else {
391 newline->values = NULL;
392 }
393 if (savestring[0] == '0') newnode->polarity = 1;
394 FREE(savestring);
395 savestring = readString(fp);
396 if (savestring == NULL) goto failure;
397 }
398 } else if (strcmp(savestring,".exdc") == 0) {
399 FREE(savestring);
400 exdc = 1;
401 } else if (strcmp(savestring,".end") == 0) {
402 FREE(savestring);
403 break;
404 }
405 if ((!savestring) || savestring[0] != '.')
406 savestring = readString(fp);
407 if (savestring == NULL) goto failure;
408 }
409
410 /* Put nodes in symbol table. */
411 newnode = net->nodes;
412 while (newnode != NULL) {
413 int retval = st_insert(net->hash,newnode->name,(char *) newnode);
414 if (retval == ST_OUT_OF_MEM) {
415 goto failure;
416 } else if (retval == 1) {
417 printf("Error: Multiple drivers for node %s\n", newnode->name);
418 goto failure;
419 } else {
420 if (pr > 2) printf("Inserted %s\n",newnode->name);
421 }
422 newnode = newnode->next;
423 }
424
425 if (latches) {
426 net->latches = latches;
427
428 count = 0;
429 net->outputs = REALLOC(char *, net->outputs,
430 (net->noutputs + net->nlatches) * sizeof(char *));
431 for (i = 0; i < net->nlatches; i++) {
432 for (j = 0; j < net->noutputs; j++) {
433 if (strcmp(latches[i][0], net->outputs[j]) == 0)
434 break;
435 }
436 if (j < net->noutputs)
437 continue;
438 savestring = ALLOC(char, strlen(latches[i][0]) + 1);
439 strcpy(savestring, latches[i][0]);
440 net->outputs[net->noutputs + count] = savestring;
441 count++;
442 if (st_lookup(net->hash, savestring, (void **) &node)) {
443 if (node->type == BNET_INTERNAL_NODE) {
444 node->type = BNET_OUTPUT_NODE;
445 }
446 }
447 }
448 net->noutputs += count;
449
450 net->inputs = REALLOC(char *, net->inputs,
451 (net->ninputs + net->nlatches) * sizeof(char *));
452 for (i = 0; i < net->nlatches; i++) {
453 savestring = ALLOC(char, strlen(latches[i][1]) + 1);
454 strcpy(savestring, latches[i][1]);
455 net->inputs[net->ninputs + i] = savestring;
456 }
457 net->ninputs += net->nlatches;
458 }
459
460 /* Compute fanout counts. For each node in the linked list, fetch
461 ** all its fanins using the symbol table, and increment the fanout of
462 ** each fanin.
463 */
464 newnode = net->nodes;
465 while (newnode != NULL) {
466 BnetNode *auxnd;
467 for (i = 0; i < newnode->ninp; i++) {
468 if (!st_lookup(net->hash,newnode->inputs[i],(void **)&auxnd)) {
469 (void) fprintf(stdout,"%s not driven\n", newnode->inputs[i]);
470 goto failure;
471 }
472 auxnd->nfo++;
473 }
474 newnode = newnode->next;
475 }
476
477 if (!bnetSetLevel(net)) goto failure;
478
479 return(net);
480
481 failure:
482 /* Here we should clean up the mess. */
483 (void) fprintf(stdout,"Error in reading network from file.\n");
484 return(NULL);
485
486 } /* end of Bnet_ReadNetwork */
487
488
489 /**
490 @brief Prints to stdout a boolean network created by Bnet_ReadNetwork.
491
492 @details Uses the blif format; this way, one can verify the
493 equivalence of the input and the output with, say, sis.
494
495 @sideeffect None
496
497 @see Bnet_ReadNetwork
498
499 */
500 void
Bnet_PrintNetwork(BnetNetwork * net)501 Bnet_PrintNetwork(
502 BnetNetwork * net /**< boolean network */)
503 {
504 BnetNode *nd;
505 BnetTabline *tl;
506 int i;
507
508 if (net == NULL) return;
509
510 (void) fprintf(stdout,".model %s\n", net->name);
511 (void) fprintf(stdout,".inputs");
512 printList(net->inputs,net->npis);
513 (void) fprintf(stdout,".outputs");
514 printList(net->outputs,net->npos);
515 for (i = 0; i < net->nlatches; i++) {
516 (void) fprintf(stdout,".latch");
517 printList(net->latches[i],3);
518 }
519 nd = net->nodes;
520 while (nd != NULL) {
521 if (nd->type != BNET_INPUT_NODE && nd->type != BNET_PRESENT_STATE_NODE) {
522 (void) fprintf(stdout,".names");
523 for (i = 0; i < nd->ninp; i++) {
524 (void) fprintf(stdout," %s",nd->inputs[i]);
525 }
526 (void) fprintf(stdout," %s\n",nd->name);
527 tl = nd->f;
528 while (tl != NULL) {
529 if (tl->values != NULL) {
530 (void) fprintf(stdout,"%s %d\n",tl->values,
531 1 - nd->polarity);
532 } else {
533 (void) fprintf(stdout,"%d\n", 1 - nd->polarity);
534 }
535 tl = tl->next;
536 }
537 }
538 nd = nd->next;
539 }
540 (void) fprintf(stdout,".end\n");
541
542 } /* end of Bnet_PrintNetwork */
543
544
545 /**
546 @brief Frees a boolean network created by Bnet_ReadNetwork.
547
548 @sideeffect None
549
550 @see Bnet_ReadNetwork
551
552 */
553 void
Bnet_FreeNetwork(BnetNetwork * net)554 Bnet_FreeNetwork(
555 BnetNetwork * net)
556 {
557 BnetNode *node, *nextnode;
558 BnetTabline *line, *nextline;
559 int i;
560
561 FREE(net->name);
562 /* The input name strings are already pointed by the input nodes.
563 ** Here we only need to free the latch names and the array that
564 ** points to them.
565 */
566 for (i = 0; i < net->nlatches; i++) {
567 FREE(net->inputs[net->npis + i]);
568 }
569 FREE(net->inputs);
570 /* Free the output name strings and then the array pointing to them. */
571 for (i = 0; i < net->noutputs; i++) {
572 FREE(net->outputs[i]);
573 }
574 FREE(net->outputs);
575
576 for (i = 0; i < net->nlatches; i++) {
577 FREE(net->latches[i][0]);
578 FREE(net->latches[i][1]);
579 FREE(net->latches[i][2]);
580 FREE(net->latches[i]);
581 }
582 if (net->nlatches) FREE(net->latches);
583 node = net->nodes;
584 while (node != NULL) {
585 nextnode = node->next;
586 if (node->type != BNET_PRESENT_STATE_NODE)
587 FREE(node->name);
588 for (i = 0; i < node->ninp; i++) {
589 FREE(node->inputs[i]);
590 }
591 if (node->inputs != NULL) {
592 FREE(node->inputs);
593 }
594 /* Free the function table. */
595 line = node->f;
596 while (line != NULL) {
597 nextline = line->next;
598 FREE(line->values);
599 FREE(line);
600 line = nextline;
601 }
602 FREE(node);
603 node = nextnode;
604 }
605 st_free_table(net->hash);
606 if (net->slope != NULL) FREE(net->slope);
607 FREE(net);
608
609 } /* end of Bnet_FreeNetwork */
610
611
612 /**
613 @brief Builds the %BDD for the function of a node.
614
615 @details Builds the %BDD for the function of a node and stores a
616 pointer to it in the dd field of the node itself. The reference count
617 of the %BDD is incremented. If params is BNET_LOCAL_DD, then the %BDD is
618 built in terms of the local inputs to the node; otherwise, if params
619 is BNET_GLOBAL_DD, the %BDD is built in terms of the network primary
620 inputs. To build the global %BDD of a node, the BDDs for its local
621 inputs must exist. If that is not the case, Bnet_BuildNodeBDD
622 recursively builds them. Likewise, to create the local %BDD for a node,
623 the local inputs must have variables assigned to them. If that is not
624 the case, Bnet_BuildNodeBDD recursively assigns variables to nodes.
625
626 @return 1 in case of success; 0 otherwise.
627
628 @sideeffect Sets the dd field of the node.
629
630 */
631 int
Bnet_BuildNodeBDD(DdManager * dd,BnetNode * nd,st_table * hash,int params,int nodrop)632 Bnet_BuildNodeBDD(
633 DdManager * dd /**< %DD manager */,
634 BnetNode * nd /**< node of the boolean network */,
635 st_table * hash /**< symbol table of the boolean network */,
636 int params /**< type of %DD to be built */,
637 int nodrop /**< retain the intermediate node DDs until the end */)
638 {
639 DdNode *func;
640 BnetNode *auxnd;
641 DdNode *tmp;
642 DdNode *prod, *var;
643 BnetTabline *line;
644 int i;
645
646 if (nd->dd != NULL) return(1);
647
648 if (nd->type == BNET_CONSTANT_NODE) {
649 if (nd->f == NULL) { /* constant 0 */
650 func = Cudd_ReadLogicZero(dd);
651 } else { /* either constant depending on the polarity */
652 func = Cudd_ReadOne(dd);
653 }
654 Cudd_Ref(func);
655 } else if (nd->type == BNET_INPUT_NODE ||
656 nd->type == BNET_PRESENT_STATE_NODE) {
657 if (nd->active == TRUE) { /* a variable is already associated: use it */
658 func = Cudd_ReadVars(dd,nd->var);
659 if (func == NULL) goto failure;
660 } else { /* no variable associated: get a new one */
661 func = Cudd_bddNewVar(dd);
662 if (func == NULL) goto failure;
663 nd->var = func->index;
664 nd->active = TRUE;
665 }
666 Cudd_Ref(func);
667 } else if (buildExorBDD(dd,nd,hash,params,nodrop)) {
668 func = nd->dd;
669 } else if (buildMuxBDD(dd,nd,hash,params,nodrop)) {
670 func = nd->dd;
671 } else { /* type == BNET_INTERNAL_NODE or BNET_OUTPUT_NODE */
672 /* Initialize the sum to logical 0. */
673 func = Cudd_ReadLogicZero(dd);
674 Cudd_Ref(func);
675
676 /* Build a term for each line of the table and add it to the
677 ** accumulator (func).
678 */
679 line = nd->f;
680 while (line != NULL) {
681 #ifdef BNET_DEBUG
682 (void) fprintf(stdout,"line = %s\n", line->values);
683 #endif
684 /* Initialize the product to logical 1. */
685 prod = Cudd_ReadOne(dd);
686 Cudd_Ref(prod);
687 /* Scan the table line. */
688 for (i = 0; i < nd->ninp; i++) {
689 if (line->values[i] == '-') continue;
690 if (!st_lookup(hash,nd->inputs[i],(void **)&auxnd)) {
691 goto failure;
692 }
693 if (params == BNET_LOCAL_DD) {
694 if (auxnd->active == FALSE) {
695 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
696 goto failure;
697 }
698 }
699 var = Cudd_ReadVars(dd,auxnd->var);
700 if (var == NULL) goto failure;
701 Cudd_Ref(var);
702 if (line->values[i] == '0') {
703 var = Cudd_Not(var);
704 }
705 } else { /* params == BNET_GLOBAL_DD */
706 if (auxnd->dd == NULL) {
707 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
708 goto failure;
709 }
710 }
711 if (line->values[i] == '1') {
712 var = auxnd->dd;
713 } else { /* line->values[i] == '0' */
714 var = Cudd_Not(auxnd->dd);
715 }
716 }
717 tmp = Cudd_bddAnd(dd,prod,var);
718 if (tmp == NULL) goto failure;
719 Cudd_Ref(tmp);
720 Cudd_IterDerefBdd(dd,prod);
721 if (params == BNET_LOCAL_DD) {
722 Cudd_IterDerefBdd(dd,var);
723 }
724 prod = tmp;
725 }
726 tmp = Cudd_bddOr(dd,func,prod);
727 if (tmp == NULL) goto failure;
728 Cudd_Ref(tmp);
729 Cudd_IterDerefBdd(dd,func);
730 Cudd_IterDerefBdd(dd,prod);
731 func = tmp;
732 line = line->next;
733 }
734 /* Associate a variable to this node if local BDDs are being
735 ** built. This is done at the end, so that the primary inputs tend
736 ** to get lower indices.
737 */
738 if (params == BNET_LOCAL_DD && nd->active == FALSE) {
739 DdNode *auxfunc = Cudd_bddNewVar(dd);
740 if (auxfunc == NULL) goto failure;
741 Cudd_Ref(auxfunc);
742 nd->var = auxfunc->index;
743 nd->active = TRUE;
744 Cudd_IterDerefBdd(dd,auxfunc);
745 }
746 }
747 if (nd->polarity == 1) {
748 nd->dd = Cudd_Not(func);
749 } else {
750 nd->dd = func;
751 }
752
753 if (params == BNET_GLOBAL_DD && nodrop == FALSE) {
754 /* Decrease counters for all faninis.
755 ** When count reaches 0, the DD is freed.
756 */
757 for (i = 0; i < nd->ninp; i++) {
758 if (!st_lookup(hash,nd->inputs[i],(void **)&auxnd)) {
759 goto failure;
760 }
761 auxnd->count--;
762 if (auxnd->count == 0) {
763 Cudd_IterDerefBdd(dd,auxnd->dd);
764 if (auxnd->type == BNET_INTERNAL_NODE ||
765 auxnd->type == BNET_CONSTANT_NODE) auxnd->dd = NULL;
766 }
767 }
768 }
769 return(1);
770
771 failure:
772 /* Here we should clean up the mess. */
773 return(0);
774
775 } /* end of Bnet_BuildNodeBDD */
776
777
778 /**
779 @brief Orders the %BDD variables by DFS.
780
781 @return 1 in case of success; 0 otherwise.
782
783 @sideeffect Uses the visited flags of the nodes.
784
785 */
786 int
Bnet_DfsVariableOrder(DdManager * dd,BnetNetwork * net)787 Bnet_DfsVariableOrder(
788 DdManager * dd,
789 BnetNetwork * net)
790 {
791 BnetNode **roots;
792 BnetNode *node;
793 int nroots;
794 int i;
795
796 roots = bnetOrderRoots(net,&nroots);
797 if (roots == NULL) return(0);
798 for (i = 0; i < nroots; i++) {
799 if (!bnetDfsOrder(dd,net,roots[i])) {
800 FREE(roots);
801 return(0);
802 }
803 }
804 /* Clear visited flags. */
805 node = net->nodes;
806 while (node != NULL) {
807 node->visited = 0;
808 node = node->next;
809 }
810 FREE(roots);
811 return(1);
812
813 } /* end of Bnet_DfsVariableOrder */
814
815
816 /**
817 @brief Writes the network BDDs to a file in dot, blif, or daVinci
818 format.
819
820 @details If "-" is passed as file name, the BDDs are dumped to the
821 standard output.
822
823 @return 1 in case of success; 0 otherwise.
824
825 @sideeffect None
826
827 */
828 int
Bnet_bddDump(DdManager * dd,BnetNetwork * network,char * dfile,int dumpFmt,int reencoded)829 Bnet_bddDump(
830 DdManager * dd /**< %DD manager */,
831 BnetNetwork * network /**< network whose BDDs should be dumped */,
832 char * dfile /**< file name */,
833 int dumpFmt /**< 0 -> dot */,
834 int reencoded /**< whether variables have been reencoded */)
835 {
836 int noutputs;
837 FILE *dfp = NULL;
838 DdNode **outputs = NULL;
839 char **inames = NULL;
840 char **onames = NULL;
841 char **altnames = NULL;
842 BnetNode *node;
843 int i;
844 int retval = 0; /* 0 -> failure; 1 -> success */
845
846 /* Open dump file. */
847 if (strcmp(dfile, "-") == 0) {
848 dfp = stdout;
849 } else {
850 dfp = fopen(dfile,"w");
851 }
852 if (dfp == NULL) goto endgame;
853
854 /* Initialize data structures. */
855 noutputs = network->noutputs;
856 outputs = ALLOC(DdNode *,noutputs);
857 if (outputs == NULL) goto endgame;
858 onames = ALLOC(char *,noutputs);
859 if (onames == NULL) goto endgame;
860 inames = ALLOC(char *,Cudd_ReadSize(dd));
861 if (inames == NULL) goto endgame;
862
863 /* Find outputs and their names. */
864 for (i = 0; i < network->nlatches; i++) {
865 onames[i] = network->latches[i][0];
866 if (!st_lookup(network->hash,network->latches[i][0],(void **)&node)) {
867 goto endgame;
868 }
869 outputs[i] = node->dd;
870 }
871 for (i = 0; i < network->npos; i++) {
872 onames[i + network->nlatches] = network->outputs[i];
873 if (!st_lookup(network->hash,network->outputs[i],(void **)&node)) {
874 goto endgame;
875 }
876 outputs[i + network->nlatches] = node->dd;
877 }
878
879 /* Find the input names. */
880 for (i = 0; i < network->ninputs; i++) {
881 if (!st_lookup(network->hash,network->inputs[i],(void **)&node)) {
882 goto endgame;
883 }
884 inames[node->var] = network->inputs[i];
885 }
886 for (i = 0; i < network->nlatches; i++) {
887 if (!st_lookup(network->hash,network->latches[i][1],(void **)&node)) {
888 goto endgame;
889 }
890 inames[node->var] = network->latches[i][1];
891 }
892
893 if (reencoded == 1 && dumpFmt == 1) {
894 altnames = bnetGenerateNewNames(network->hash,network->ninputs);
895 if (altnames == NULL) {
896 retval = 0;
897 goto endgame;
898 }
899 retval = bnetDumpReencodingLogic(dd,network->name,noutputs,outputs,
900 inames,altnames,onames,dfp);
901 for (i = 0; i < network->ninputs; i++) {
902 FREE(altnames[i]);
903 }
904 FREE(altnames);
905 if (retval == 0) goto endgame;
906 }
907
908 /* Dump the BDDs. */
909 if (dumpFmt == 1) {
910 retval = Cudd_DumpBlif(dd,noutputs,outputs,
911 (char const * const *) inames,
912 (char const * const *) onames,
913 network->name,dfp,0);
914 } else if (dumpFmt == 2) {
915 retval = Cudd_DumpDaVinci(dd,noutputs,outputs,
916 (char const * const *) inames,
917 (char const * const *) onames,dfp);
918 } else if (dumpFmt == 3) {
919 retval = Cudd_DumpDDcal(dd,noutputs,outputs,
920 (char const * const *) inames,
921 (char const * const *) onames,dfp);
922 } else if (dumpFmt == 4) {
923 retval = Cudd_DumpFactoredForm(dd,noutputs,outputs,
924 (char const * const *) inames,
925 (char const * const *) onames,dfp);
926 } else if (dumpFmt == 5) {
927 retval = Cudd_DumpBlif(dd,noutputs,outputs,
928 (char const * const *) inames,
929 (char const * const *) onames,
930 network->name,dfp,1);
931 } else {
932 retval = Cudd_DumpDot(dd,noutputs,outputs,
933 (char const * const *) inames,
934 (char const * const *) onames,dfp);
935 }
936
937 endgame:
938 if (dfp != stdout && dfp != NULL) {
939 if (fclose(dfp) == EOF) retval = 0;
940 }
941 if (outputs != NULL) FREE(outputs);
942 if (onames != NULL) FREE(onames);
943 if (inames != NULL) FREE(inames);
944
945 return(retval);
946
947 } /* end of Bnet_bddDump */
948
949
950 /**
951 @brief Writes an array of BDDs to a file in dot, blif, DDcal,
952 factored-form, daVinci, or blif-MV format.
953
954 @details The BDDs and their names are passed as arguments. The
955 inputs and their names are taken from the network. If "-" is passed
956 as file name, the BDDs are dumped to the standard output. The encoding
957 of the format is:
958 <ul>
959 <li>0: dot
960 <li>1: blif
961 <li>2: da Vinci
962 <li>3: ddcal
963 <li>4: factored form
964 <li>5: blif-MV
965 </ul>
966
967 @return 1 in case of success; 0 otherwise.
968
969 @sideeffect None
970
971 */
972 int
Bnet_bddArrayDump(DdManager * dd,BnetNetwork * network,char * dfile,DdNode ** outputs,char ** onames,int noutputs,int dumpFmt)973 Bnet_bddArrayDump(
974 DdManager * dd /**< %DD manager */,
975 BnetNetwork * network /**< network whose BDDs should be dumped */,
976 char * dfile /**< file name */,
977 DdNode ** outputs /**< BDDs to be dumped */,
978 char ** onames /**< names of the BDDs to be dumped */,
979 int noutputs /**< number of BDDs to be dumped */,
980 int dumpFmt /**< 0 -> dot */)
981 {
982 FILE *dfp = NULL;
983 char **inames = NULL;
984 BnetNode *node;
985 int i;
986 int retval = 0; /* 0 -> failure; 1 -> success */
987
988 /* Open dump file. */
989 if (strcmp(dfile, "-") == 0) {
990 dfp = stdout;
991 } else {
992 dfp = fopen(dfile,"w");
993 }
994 if (dfp == NULL) goto endgame;
995
996 /* Initialize data structures. */
997 inames = ALLOC(char *,Cudd_ReadSize(dd));
998 if (inames == NULL) goto endgame;
999 for (i = 0; i < Cudd_ReadSize(dd); i++) {
1000 inames[i] = NULL;
1001 }
1002
1003 /* Find the input names. */
1004 for (i = 0; i < network->ninputs; i++) {
1005 if (!st_lookup(network->hash,network->inputs[i],(void **)&node)) {
1006 goto endgame;
1007 }
1008 inames[node->var] = network->inputs[i];
1009 }
1010 for (i = 0; i < network->nlatches; i++) {
1011 if (!st_lookup(network->hash,network->latches[i][1],(void **)&node)) {
1012 goto endgame;
1013 }
1014 inames[node->var] = network->latches[i][1];
1015 }
1016
1017 /* Dump the BDDs. */
1018 if (dumpFmt == 1) {
1019 retval = Cudd_DumpBlif(dd,noutputs,outputs,
1020 (char const * const *) inames,
1021 (char const * const *) onames,
1022 network->name,dfp,0);
1023 } else if (dumpFmt == 2) {
1024 retval = Cudd_DumpDaVinci(dd,noutputs,outputs,
1025 (char const * const *) inames,
1026 (char const * const *) onames,dfp);
1027 } else if (dumpFmt == 3) {
1028 retval = Cudd_DumpDDcal(dd,noutputs,outputs,
1029 (char const * const *) inames,
1030 (char const * const *) onames,dfp);
1031 } else if (dumpFmt == 4) {
1032 retval = Cudd_DumpFactoredForm(dd,noutputs,outputs,
1033 (char const * const *) inames,
1034 (char const * const *) onames,dfp);
1035 } else if (dumpFmt == 5) {
1036 retval = Cudd_DumpBlif(dd,noutputs,outputs,
1037 (char const * const *) inames,
1038 (char const * const *) onames,
1039 network->name,dfp,1);
1040 } else {
1041 retval = Cudd_DumpDot(dd,noutputs,outputs,
1042 (char const * const *) inames,
1043 (char const * const *) onames,dfp);
1044 }
1045
1046 endgame:
1047 if (dfp != stdout && dfp != NULL) {
1048 if (fclose(dfp) == EOF) retval = 0;
1049 }
1050 if (inames != NULL) FREE(inames);
1051
1052 return(retval);
1053
1054 } /* end of Bnet_bddArrayDump */
1055
1056
1057 /**
1058 @brief Reads the variable order from a file.
1059
1060 @return 1 if successful; 0 otherwise.
1061
1062 @sideeffect The BDDs for the primary inputs and present state variables
1063 are built.
1064
1065 */
1066 int
Bnet_ReadOrder(DdManager * dd,char * ordFile,BnetNetwork * net,int locGlob,int nodrop)1067 Bnet_ReadOrder(
1068 DdManager * dd,
1069 char * ordFile,
1070 BnetNetwork * net,
1071 int locGlob,
1072 int nodrop)
1073 {
1074 FILE *fp;
1075 st_table *dict;
1076 int result;
1077 BnetNode *node;
1078 char name[MAXLENGTH];
1079
1080 if (ordFile == NULL) {
1081 return(0);
1082 }
1083
1084 dict = st_init_table((st_compare_t) strcmp,st_strhash);
1085 if (dict == NULL) {
1086 return(0);
1087 }
1088
1089 if ((fp = fopen(ordFile,"r")) == NULL) {
1090 (void) fprintf(stderr,"Unable to open %s\n",ordFile);
1091 st_free_table(dict);
1092 return(0);
1093 }
1094
1095 while (!feof(fp)) {
1096 result = fscanf(fp, "%s", name);
1097 if (result == EOF) {
1098 break;
1099 } else if (result != 1) {
1100 st_free_table(dict);
1101 return(0);
1102 } else if (strlen(name) > MAXLENGTH) {
1103 st_free_table(dict);
1104 return(0);
1105 }
1106 /* There should be a node named "name" in the network. */
1107 if (!st_lookup(net->hash,name,(void **)&node)) {
1108 (void) fprintf(stderr,"Unknown name in order file (%s)\n", name);
1109 st_free_table(dict);
1110 return(0);
1111 }
1112 /* A name should not appear more than once in the order. */
1113 if (st_is_member(dict,name)) {
1114 (void) fprintf(stderr,"Duplicate name in order file (%s)\n", name);
1115 st_free_table(dict);
1116 return(0);
1117 }
1118 /* The name should correspond to a primary input or present state. */
1119 if (node->type != BNET_INPUT_NODE &&
1120 node->type != BNET_PRESENT_STATE_NODE) {
1121 (void) fprintf(stderr,"%s has the wrong type (%d)\n", name,
1122 node->type);
1123 st_free_table(dict);
1124 return(0);
1125 }
1126 /* Insert in table. Use node->name rather than name, because the
1127 ** latter gets overwritten.
1128 */
1129 if (st_insert(dict,node->name,NULL) == ST_OUT_OF_MEM) {
1130 (void) fprintf(stderr,"Out of memory in Bnet_ReadOrder\n");
1131 st_free_table(dict);
1132 return(0);
1133 }
1134 result = Bnet_BuildNodeBDD(dd,node,net->hash,locGlob,nodrop);
1135 if (result == 0) {
1136 (void) fprintf(stderr,"Construction of BDD failed\n");
1137 st_free_table(dict);
1138 return(0);
1139 }
1140 } /* while (!feof(fp)) */
1141 result = fclose(fp);
1142 if (result == EOF) {
1143 (void) fprintf(stderr,"Error closing order file %s\n", ordFile);
1144 st_free_table(dict);
1145 return(0);
1146 }
1147
1148 /* The number of names in the order file should match exactly the
1149 ** number of primary inputs and present states.
1150 */
1151 if (st_count(dict) != net->ninputs) {
1152 (void) fprintf(stderr,"Order incomplete: %d names instead of %d\n",
1153 st_count(dict), net->ninputs);
1154 st_free_table(dict);
1155 return(0);
1156 }
1157
1158 st_free_table(dict);
1159 return(1);
1160
1161 } /* end of Bnet_ReadOrder */
1162
1163
1164 /**
1165 @brief Prints the order of the %DD variables of a network.
1166
1167 @details Only primary inputs and present states are printed.
1168
1169 @return 1 if successful; 0 otherwise.
1170
1171 @sideeffect None
1172
1173 */
1174 int
Bnet_PrintOrder(BnetNetwork * net,DdManager * dd)1175 Bnet_PrintOrder(
1176 BnetNetwork * net,
1177 DdManager *dd)
1178 {
1179 char **names; /* array used to print variable orders */
1180 int level; /* position of a variable in current order */
1181 BnetNode *node; /* auxiliary pointer to network node */
1182 int i,j;
1183 int retval;
1184 int nvars;
1185
1186 nvars = Cudd_ReadSize(dd);
1187 names = ALLOC(char *, nvars);
1188 if (names == NULL) return(0);
1189 for (i = 0; i < nvars; i++) {
1190 names[i] = NULL;
1191 }
1192 for (i = 0; i < net->npis; i++) {
1193 if (!st_lookup(net->hash,net->inputs[i],(void **)&node)) {
1194 FREE(names);
1195 return(0);
1196 }
1197 if (node->dd == NULL) {
1198 FREE(names);
1199 return(0);
1200 }
1201 level = Cudd_ReadPerm(dd,node->var);
1202 names[level] = node->name;
1203 }
1204 for (i = 0; i < net->nlatches; i++) {
1205 if (!st_lookup(net->hash,net->latches[i][1],(void **)&node)) {
1206 FREE(names);
1207 return(0);
1208 }
1209 if (node->dd == NULL) {
1210 FREE(names);
1211 return(0);
1212 }
1213 level = Cudd_ReadPerm(dd,node->var);
1214 names[level] = node->name;
1215 }
1216 for (i = 0, j = 0; i < nvars; i++) {
1217 if (names[i] == NULL) continue;
1218 if ((j%8 == 0)&&j) {
1219 retval = printf("\n");
1220 if (retval == EOF) {
1221 FREE(names);
1222 return(0);
1223 }
1224 }
1225 retval = printf("%s ",names[i]);
1226 if (retval == EOF) {
1227 FREE(names);
1228 return(0);
1229 }
1230 j++;
1231 }
1232 FREE(names);
1233 retval = printf("\n");
1234 if (retval == EOF) {
1235 return(0);
1236 }
1237 return(1);
1238
1239 } /* end of Bnet_PrintOrder */
1240
1241
1242 /*---------------------------------------------------------------------------*/
1243 /* Definition of internal functions */
1244 /*---------------------------------------------------------------------------*/
1245
1246 /*---------------------------------------------------------------------------*/
1247 /* Definition of static functions */
1248 /*---------------------------------------------------------------------------*/
1249
1250
1251 /**
1252 @brief Reads a string from a file.
1253
1254 @details The string can be MAXLENGTH-1 characters at
1255 most. readString allocates memory to hold the string.
1256
1257 @return a pointer to the result string if successful. It returns
1258 NULL otherwise.
1259
1260 @sideeffect None
1261
1262 @see readList
1263
1264 */
1265 static char *
readString(FILE * fp)1266 readString(
1267 FILE * fp /**< pointer to the file from which the string is read */)
1268 {
1269 char *savestring;
1270 int length;
1271
1272 while (!CurPos) {
1273 if (!fgets(BuffLine, MAXLENGTH, fp))
1274 return(NULL);
1275 BuffLine[strlen(BuffLine) - 1] = '\0';
1276 CurPos = strtok(BuffLine, " \t");
1277 if (CurPos && CurPos[0] == '#') CurPos = (char *)NULL;
1278 }
1279 length = strlen(CurPos);
1280 savestring = ALLOC(char,length+1);
1281 if (savestring == NULL)
1282 return(NULL);
1283 strcpy(savestring,CurPos);
1284 CurPos = strtok(NULL, " \t");
1285 return(savestring);
1286
1287 } /* end of readString */
1288
1289
1290 /**
1291 @brief Reads a list of strings from a line of a file.
1292
1293 @details The strings are sequences of characters separated by spaces
1294 or tabs. The total length of the list, white space included, must
1295 not exceed MAXLENGTH-1 characters. readList allocates memory for
1296 the strings and creates an array of pointers to the individual
1297 lists. Only two pieces of memory are allocated by readList: One to
1298 hold all the strings, and one to hold the pointers to
1299 them. Therefore, when freeing the memory allocated by readList, only
1300 the pointer to the list of pointers, and the pointer to the
1301 beginning of the first string should be freed.
1302
1303 @return the pointer to the list of pointers if successful; NULL
1304 otherwise.
1305
1306 @sideeffect n is set to the number of strings in the list.
1307
1308 @see readString printList
1309
1310 */
1311 static char **
readList(FILE * fp,int * n)1312 readList(
1313 FILE * fp /**< pointer to the file from which the list is read */,
1314 int * n /**< on return, number of strings in the list */)
1315 {
1316 char *savestring;
1317 int length;
1318 char *stack[8192];
1319 char **list;
1320 int i, count = 0;
1321
1322 while (CurPos) {
1323 if (strcmp(CurPos, "\\") == 0) {
1324 CurPos = (char *)NULL;
1325 while (!CurPos) {
1326 if (!fgets(BuffLine, MAXLENGTH, fp)) return(NULL);
1327 BuffLine[strlen(BuffLine) - 1] = '\0';
1328 CurPos = strtok(BuffLine, " \t");
1329 }
1330 }
1331 length = strlen(CurPos);
1332 savestring = ALLOC(char,length+1);
1333 if (savestring == NULL) return(NULL);
1334 strcpy(savestring,CurPos);
1335 stack[count] = savestring;
1336 count++;
1337 CurPos = strtok(NULL, " \t");
1338 }
1339 list = ALLOC(char *, count);
1340 for (i = 0; i < count; i++)
1341 list[i] = stack[i];
1342 *n = count;
1343 return(list);
1344
1345 } /* end of readList */
1346
1347
1348 /**
1349 @brief Prints a list of strings to the standard output.
1350
1351 @details The list is in the format created by readList.
1352
1353 @sideeffect None
1354
1355 @see readList Bnet_PrintNetwork
1356
1357 */
1358 static void
printList(char ** list,int n)1359 printList(
1360 char ** list /**< list of pointers to strings */,
1361 int n /**< length of the list */)
1362 {
1363 int i;
1364
1365 for (i = 0; i < n; i++) {
1366 (void) fprintf(stdout," %s",list[i]);
1367 }
1368 (void) fprintf(stdout,"\n");
1369
1370 } /* end of printList */
1371
1372
1373 /**
1374 @brief Generates n names not currently in a symbol table.
1375
1376 @details The pointer to the symbol table may be NULL, in which case
1377 no test is made. The names generated by the procedure are
1378 unique. So, if there is no possibility of conflict with pre-existing
1379 names, NULL can be passed for the hash table.
1380
1381 @return an array of names if succesful; NULL otherwise.
1382
1383 @sideeffect None
1384
1385 @see
1386
1387 */
1388 static char **
bnetGenerateNewNames(st_table * hash,int n)1389 bnetGenerateNewNames(
1390 st_table * hash /* table of existing names (or NULL) */,
1391 int n /* number of names to be generated */)
1392 {
1393 char **list;
1394 char name[256];
1395 int i;
1396
1397 if (n < 1) return(NULL);
1398
1399 list = ALLOC(char *,n);
1400 if (list == NULL) return(NULL);
1401 for (i = 0; i < n; i++) {
1402 do {
1403 sprintf(name, "var%d", newNameNumber);
1404 newNameNumber++;
1405 } while (hash != NULL && st_is_member(hash,name));
1406 list[i] = util_strsav(name);
1407 }
1408
1409 return(list);
1410
1411 } /* bnetGenerateNewNames */
1412
1413
1414 /**
1415 @brief Writes blif for the reencoding logic.
1416
1417 @sideeffect None
1418
1419 */
1420 static int
bnetDumpReencodingLogic(DdManager * dd,char * mname,int noutputs,DdNode ** outputs,char ** inames,char ** altnames,char ** onames,FILE * fp)1421 bnetDumpReencodingLogic(
1422 DdManager * dd /**< %DD manager */,
1423 char * mname /**< model name */,
1424 int noutputs /**< number of outputs */,
1425 DdNode ** outputs /**< array of network outputs */,
1426 char ** inames /**< array of network input names */,
1427 char ** altnames /**< array of names of reencoded inputs */,
1428 char ** onames /**< array of network output names */,
1429 FILE * fp /**< file pointer */)
1430 {
1431 int i;
1432 int retval;
1433 int nvars = Cudd_ReadSize(dd);
1434 int *support = NULL;
1435
1436 support = bnetFindVectorSupport(dd,outputs,noutputs);
1437 if (support == NULL) return(0);
1438
1439 /* Write the header (.model .inputs .outputs). */
1440 retval = fprintf(fp,".model %s.global\n.inputs",mname);
1441 if (retval == EOF) goto failure;
1442
1443 for (i = 0; i < nvars; i++) {
1444 if ((i%8 == 0)&&i) {
1445 retval = fprintf(fp," \\\n");
1446 if (retval == EOF) goto failure;
1447 }
1448 retval = fprintf(fp," %s", inames[i]);
1449 if (retval == EOF) goto failure;
1450 }
1451
1452 /* Write the .output line. */
1453 retval = fprintf(fp,"\n.outputs");
1454 if (retval == EOF) goto failure;
1455 for (i = 0; i < noutputs; i++) {
1456 if ((i%8 == 0)&&i) {
1457 retval = fprintf(fp," \\\n");
1458 if (retval == EOF) goto failure;
1459 }
1460 retval = fprintf(fp," %s", onames[i]);
1461 if (retval == EOF) goto failure;
1462 }
1463 retval = fprintf(fp,"\n");
1464 if (retval == EOF) goto failure;
1465
1466 /* Instantiate main subcircuit. */
1467 retval = fprintf(fp,"\n.subckt %s", mname);
1468 if (retval == EOF) goto failure;
1469 for (i = 0; i < nvars; i++) {
1470 if ((i%8 == 0)&&i) {
1471 retval = fprintf(fp," \\\n");
1472 if (retval == EOF) goto failure;
1473 }
1474 if (support[i] == 1) {
1475 retval = fprintf(fp," %s=%s", inames[i], altnames[i]);
1476 if (retval == EOF) goto failure;
1477 }
1478 }
1479 for (i = 0; i < noutputs; i++) {
1480 if ((i%8 == 0)&&i) {
1481 retval = fprintf(fp," \\\n");
1482 if (retval == EOF) goto failure;
1483 }
1484 retval = fprintf(fp," %s=%s", onames[i], onames[i]);
1485 if (retval == EOF) goto failure;
1486 }
1487 retval = fprintf(fp,"\n");
1488 if (retval == EOF) goto failure;
1489
1490 /* Instantiate reencoding subcircuit. */
1491 retval = fprintf(fp,"\n.subckt %s.reencode",mname);
1492 if (retval == EOF) goto failure;
1493 for (i = 0; i < nvars; i++) {
1494 if ((i%8 == 0)&&i) {
1495 retval = fprintf(fp," \\\n");
1496 if (retval == EOF) goto failure;
1497 }
1498 retval = fprintf(fp," %s=%s", inames[i], inames[i]);
1499 if (retval == EOF) goto failure;
1500 }
1501 retval = fprintf(fp," \\\n");
1502 if (retval == EOF) goto failure;
1503 for (i = 0; i < nvars; i++) {
1504 if ((i%8 == 0)&&i) {
1505 retval = fprintf(fp," \\\n");
1506 if (retval == EOF) goto failure;
1507 }
1508 if (support[i] == 1) {
1509 retval = fprintf(fp," %s=%s", altnames[i],altnames[i]);
1510 if (retval == EOF) goto failure;
1511 }
1512 }
1513 retval = fprintf(fp,"\n");
1514 if (retval == EOF) goto failure;
1515
1516 /* Write trailer. */
1517 retval = fprintf(fp,".end\n\n");
1518 if (retval == EOF) goto failure;
1519
1520 /* Write reencoding subcircuit. */
1521 retval = bnetBlifWriteReencode(dd,mname,inames,altnames,support,fp);
1522 if (retval == EOF) goto failure;
1523
1524 FREE(support);
1525 return(1);
1526
1527 failure:
1528 if (support != NULL) FREE(support);
1529 return(0);
1530
1531 } /* end of bnetDumpReencodingLogic */
1532
1533
1534 /**
1535 @brief Writes blif for the truth table of an n-input xnor.
1536
1537 @return 1 if successful; 0 otherwise.
1538
1539 @sideeffect None
1540
1541 */
1542 #if 0
1543 static int
1544 bnetBlifXnorTable(
1545 FILE * fp /**< file pointer */,
1546 int n /**< number of inputs */)
1547 {
1548 int power; /* 2 to the power n */
1549 int i,j,k;
1550 int nzeroes;
1551 int retval;
1552 char *line;
1553
1554 line = ALLOC(char,n+1);
1555 if (line == NULL) return(0);
1556 line[n] = '\0';
1557
1558 for (i = 0, power = 1; i < n; i++) {
1559 power *= 2;
1560 }
1561
1562 for (i = 0; i < power; i++) {
1563 k = i;
1564 nzeroes = 0;
1565 for (j = 0; j < n; j++) {
1566 if (k & 1) {
1567 line[j] = '1';
1568 } else {
1569 line[j] = '0';
1570 nzeroes++;
1571 }
1572 k >>= 1;
1573 }
1574 if ((nzeroes & 1) == 0) {
1575 retval = fprintf(fp,"%s 1\n",line);
1576 if (retval == 0) return(0);
1577 }
1578 }
1579 return(1);
1580
1581 } /* end of bnetBlifXnorTable */
1582 #endif
1583
1584
1585 /**
1586 @brief Writes blif for the reencoding logic.
1587
1588 @details Exclusive NORs with more than two inputs are decomposed
1589 into cascaded two-input gates.
1590
1591 @return 1 if successful; 0 otherwise.
1592
1593 @sideeffect None
1594
1595 */
1596 static int
bnetBlifWriteReencode(DdManager * dd,char * mname,char ** inames,char ** altnames,int * support,FILE * fp)1597 bnetBlifWriteReencode(
1598 DdManager * dd,
1599 char * mname,
1600 char ** inames,
1601 char ** altnames,
1602 int * support,
1603 FILE * fp)
1604 {
1605 int retval;
1606 int nvars = Cudd_ReadSize(dd);
1607 int i,j;
1608 int ninp;
1609
1610 /* Write the header (.model .inputs .outputs). */
1611 retval = fprintf(fp,".model %s.reencode\n.inputs",mname);
1612 if (retval == EOF) return(0);
1613
1614 for (i = 0; i < nvars; i++) {
1615 if ((i%8 == 0)&&i) {
1616 retval = fprintf(fp," \\\n");
1617 if (retval == EOF) goto failure;
1618 }
1619 retval = fprintf(fp," %s", inames[i]);
1620 if (retval == EOF) goto failure;
1621 }
1622
1623 /* Write the .output line. */
1624 retval = fprintf(fp,"\n.outputs");
1625 if (retval == EOF) goto failure;
1626 for (i = 0; i < nvars; i++) {
1627 if ((i%8 == 0)&&i) {
1628 retval = fprintf(fp," \\\n");
1629 if (retval == EOF) goto failure;
1630 }
1631 if (support[i] == 1) {
1632 retval = fprintf(fp," %s", altnames[i]);
1633 if (retval == EOF) goto failure;
1634 }
1635 }
1636 retval = fprintf(fp,"\n");
1637 if (retval == EOF) goto failure;
1638
1639 /* Instantiate exclusive nors. */
1640 for (i = 0; i < nvars; i++) {
1641 char *in1 = NULL;
1642 char *in2 = NULL;
1643 char **oname;
1644 if (support[i] == 0) continue;
1645 ninp = 0;
1646 for (j = 0; j < nvars; j++) {
1647 if (Cudd_ReadLinear(dd,i,j)) {
1648 switch (ninp) {
1649 case 0:
1650 in1 = inames[j];
1651 ninp++;
1652 break;
1653 case 1:
1654 in2 = inames[j];
1655 ninp++;
1656 break;
1657 case 2:
1658 oname = bnetGenerateNewNames(NULL,1);
1659 retval = fprintf(fp,".names %s %s %s\n11 1\n00 1\n",
1660 in1, in2, oname[0]);
1661 if (retval == EOF) goto failure;
1662 in1 = oname[0];
1663 in2 = inames[j];
1664 FREE(oname);
1665 break;
1666 default:
1667 goto failure;
1668 }
1669 }
1670 }
1671 switch (ninp) {
1672 case 1:
1673 retval = fprintf(fp,".names %s %s\n1 1\n", in1, altnames[i]);
1674 if (retval == EOF) goto failure;
1675 break;
1676 case 2:
1677 retval = fprintf(fp,".names %s %s %s\n11 1\n00 1\n",
1678 in1, in2, altnames[i]);
1679 if (retval == EOF) goto failure;
1680 break;
1681 default:
1682 goto failure;
1683 }
1684 }
1685
1686 /* Write trailer. */
1687 retval = fprintf(fp,"\n.end\n\n");
1688 if (retval == EOF) goto failure;
1689
1690 return(1);
1691
1692 failure:
1693 return(0);
1694
1695 } /* end of bnetBlifWriteReencode */
1696
1697
1698 /**
1699 @brief Finds the support of a list of DDs.
1700
1701 @sideeffect None
1702
1703 */
1704 static int *
bnetFindVectorSupport(DdManager * dd,DdNode ** list,int n)1705 bnetFindVectorSupport(
1706 DdManager * dd,
1707 DdNode ** list,
1708 int n)
1709 {
1710 DdNode *support = NULL;
1711 DdNode *scan;
1712 int *array = NULL;
1713 int nvars = Cudd_ReadSize(dd);
1714 int i;
1715
1716 /* Build an array with the support of the functions in list. */
1717 array = ALLOC(int,nvars);
1718 if (array == NULL) return(NULL);
1719 for (i = 0; i < nvars; i++) {
1720 array[i] = 0;
1721 }
1722
1723 /* Take the union of the supports of each output function. */
1724 for (i = 0; i < n; i++) {
1725 support = Cudd_Support(dd,list[i]);
1726 if (support == NULL) {
1727 FREE(array);
1728 return(NULL);
1729 }
1730 Cudd_Ref(support);
1731 scan = support;
1732 while (!Cudd_IsConstant(scan)) {
1733 array[scan->index] = 1;
1734 scan = Cudd_T(scan);
1735 }
1736 Cudd_IterDerefBdd(dd,support);
1737 }
1738
1739 return(array);
1740
1741 } /* end of bnetFindVectorSupport */
1742
1743
1744 /**
1745 @brief Builds %BDD for a XOR function.
1746
1747 @details Checks whether a function is a XOR with 2 or 3 inputs. If so,
1748 it builds the %BDD.
1749
1750 @return 1 if the %BDD has been built; 0 otherwise.
1751
1752 @sideeffect None
1753
1754 */
1755 static int
buildExorBDD(DdManager * dd,BnetNode * nd,st_table * hash,int params,int nodrop)1756 buildExorBDD(
1757 DdManager * dd,
1758 BnetNode * nd,
1759 st_table * hash,
1760 int params,
1761 int nodrop)
1762 {
1763 int check[8];
1764 int i;
1765 int nlines;
1766 BnetTabline *line;
1767 DdNode *func, *var, *tmp;
1768 BnetNode *auxnd;
1769
1770 if (nd->ninp < 2 || nd->ninp > 3) return(0);
1771
1772 nlines = 1 << (nd->ninp - 1);
1773 for (i = 0; i < 8; i++) check[i] = 0;
1774 line = nd->f;
1775 while (line != NULL) {
1776 int num = 0;
1777 int count = 0;
1778 nlines--;
1779 for (i = 0; i < nd->ninp; i++) {
1780 num <<= 1;
1781 if (line->values[i] == '-') {
1782 return(0);
1783 } else if (line->values[i] == '1') {
1784 count++;
1785 num++;
1786 }
1787 }
1788 if ((count & 1) == 0) return(0);
1789 if (check[num]) return(0);
1790 line = line->next;
1791 }
1792 if (nlines != 0) return(0);
1793
1794 /* Initialize the exclusive sum to logical 0. */
1795 func = Cudd_ReadLogicZero(dd);
1796 Cudd_Ref(func);
1797
1798 /* Scan the inputs. */
1799 for (i = 0; i < nd->ninp; i++) {
1800 if (!st_lookup(hash, nd->inputs[i], (void **) &auxnd)) {
1801 goto failure;
1802 }
1803 if (params == BNET_LOCAL_DD) {
1804 if (auxnd->active == FALSE) {
1805 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1806 goto failure;
1807 }
1808 }
1809 var = Cudd_ReadVars(dd,auxnd->var);
1810 if (var == NULL) goto failure;
1811 Cudd_Ref(var);
1812 } else { /* params == BNET_GLOBAL_DD */
1813 if (auxnd->dd == NULL) {
1814 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1815 goto failure;
1816 }
1817 }
1818 var = auxnd->dd;
1819 }
1820 tmp = Cudd_bddXor(dd,func,var);
1821 if (tmp == NULL) goto failure;
1822 Cudd_Ref(tmp);
1823 Cudd_IterDerefBdd(dd,func);
1824 if (params == BNET_LOCAL_DD) {
1825 Cudd_IterDerefBdd(dd,var);
1826 }
1827 func = tmp;
1828 }
1829 nd->dd = func;
1830
1831 /* Associate a variable to this node if local BDDs are being
1832 ** built. This is done at the end, so that the primary inputs tend
1833 ** to get lower indices.
1834 */
1835 if (params == BNET_LOCAL_DD && nd->active == FALSE) {
1836 DdNode *auxfunc = Cudd_bddNewVar(dd);
1837 if (auxfunc == NULL) goto failure;
1838 Cudd_Ref(auxfunc);
1839 nd->var = auxfunc->index;
1840 nd->active = TRUE;
1841 Cudd_IterDerefBdd(dd,auxfunc);
1842 }
1843
1844 return(1);
1845 failure:
1846 return(0);
1847
1848 } /* end of buildExorBDD */
1849
1850
1851 /**
1852 @brief Builds %BDD for a multiplexer.
1853
1854 @details Checks whether a function is a 2-to-1 multiplexer. If so,
1855 it builds the %BDD.
1856
1857 @return 1 if the %BDD has been built; 0 otherwise.
1858
1859 @sideeffect None
1860
1861 */
1862 static int
buildMuxBDD(DdManager * dd,BnetNode * nd,st_table * hash,int params,int nodrop)1863 buildMuxBDD(
1864 DdManager * dd,
1865 BnetNode * nd,
1866 st_table * hash,
1867 int params,
1868 int nodrop)
1869 {
1870 BnetTabline *line;
1871 char *values[2];
1872 int mux[2] = {0, 0};
1873 int phase[2] = {0, 0};
1874 int j;
1875 int nlines = 0;
1876 int controlC = -1;
1877 int controlR = -1;
1878 DdNode *func, *f, *g, *h;
1879 BnetNode *auxnd;
1880
1881 if (nd->ninp != 3 || nd->f == NULL) return(0);
1882
1883 for (line = nd->f; line != NULL; line = line->next) {
1884 int dc = 0;
1885 if (nlines > 1) return(0);
1886 values[nlines] = line->values;
1887 for (j = 0; j < 3; j++) {
1888 if (values[nlines][j] == '-') {
1889 if (dc) return(0);
1890 dc = 1;
1891 }
1892 }
1893 if (!dc) return(0);
1894 nlines++;
1895 }
1896 if (nlines != 2) return(0);
1897 /* At this point we know we have:
1898 ** 3 inputs
1899 ** 2 lines
1900 ** 1 dash in each line
1901 ** If the two dashes are not in the same column, then there is
1902 ** exaclty one column without dashes: the control column.
1903 */
1904 for (j = 0; j < 3; j++) {
1905 if (values[0][j] == '-' && values[1][j] == '-') return(0);
1906 if (values[0][j] != '-' && values[1][j] != '-') {
1907 if (values[0][j] == values[1][j]) return(0);
1908 controlC = j;
1909 controlR = values[0][j] == '0';
1910 }
1911 }
1912 assert(controlC != -1 && controlR != -1);
1913 /* At this point we know that there is indeed no column with two
1914 ** dashes. The control column has been identified, and we know that
1915 ** its two elelments are different. */
1916 for (j = 0; j < 3; j++) {
1917 if (j == controlC) continue;
1918 if (values[controlR][j] == '1') {
1919 mux[0] = j;
1920 phase[0] = 0;
1921 } else if (values[controlR][j] == '0') {
1922 mux[0] = j;
1923 phase[0] = 1;
1924 } else if (values[1-controlR][j] == '1') {
1925 mux[1] = j;
1926 phase[1] = 0;
1927 } else if (values[1-controlR][j] == '0') {
1928 mux[1] = j;
1929 phase[1] = 1;
1930 }
1931 }
1932
1933 /* Get the inputs. */
1934 if (!st_lookup(hash, nd->inputs[controlC], (void **) &auxnd)) {
1935 goto failure;
1936 }
1937 if (params == BNET_LOCAL_DD) {
1938 if (auxnd->active == FALSE) {
1939 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1940 goto failure;
1941 }
1942 }
1943 f = Cudd_ReadVars(dd,auxnd->var);
1944 if (f == NULL) goto failure;
1945 Cudd_Ref(f);
1946 } else { /* params == BNET_GLOBAL_DD */
1947 if (auxnd->dd == NULL) {
1948 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1949 goto failure;
1950 }
1951 }
1952 f = auxnd->dd;
1953 }
1954 if (!st_lookup(hash, nd->inputs[mux[0]], (void **) &auxnd)) {
1955 goto failure;
1956 }
1957 if (params == BNET_LOCAL_DD) {
1958 if (auxnd->active == FALSE) {
1959 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1960 goto failure;
1961 }
1962 }
1963 g = Cudd_ReadVars(dd,auxnd->var);
1964 if (g == NULL) goto failure;
1965 Cudd_Ref(g);
1966 } else { /* params == BNET_GLOBAL_DD */
1967 if (auxnd->dd == NULL) {
1968 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1969 goto failure;
1970 }
1971 }
1972 g = auxnd->dd;
1973 }
1974 g = Cudd_NotCond(g,phase[0]);
1975 if (!st_lookup(hash, nd->inputs[mux[1]], (void **) &auxnd)) {
1976 goto failure;
1977 }
1978 if (params == BNET_LOCAL_DD) {
1979 if (auxnd->active == FALSE) {
1980 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1981 goto failure;
1982 }
1983 }
1984 h = Cudd_ReadVars(dd,auxnd->var);
1985 if (h == NULL) goto failure;
1986 Cudd_Ref(h);
1987 } else { /* params == BNET_GLOBAL_DD */
1988 if (auxnd->dd == NULL) {
1989 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1990 goto failure;
1991 }
1992 }
1993 h = auxnd->dd;
1994 }
1995 h = Cudd_NotCond(h,phase[1]);
1996 func = Cudd_bddIte(dd,f,g,h);
1997 if (func == NULL) goto failure;
1998 Cudd_Ref(func);
1999 if (params == BNET_LOCAL_DD) {
2000 Cudd_IterDerefBdd(dd,f);
2001 Cudd_IterDerefBdd(dd,g);
2002 Cudd_IterDerefBdd(dd,h);
2003 }
2004 nd->dd = func;
2005
2006 /* Associate a variable to this node if local BDDs are being
2007 ** built. This is done at the end, so that the primary inputs tend
2008 ** to get lower indices.
2009 */
2010 if (params == BNET_LOCAL_DD && nd->active == FALSE) {
2011 DdNode *auxfunc = Cudd_bddNewVar(dd);
2012 if (auxfunc == NULL) goto failure;
2013 Cudd_Ref(auxfunc);
2014 nd->var = auxfunc->index;
2015 nd->active = TRUE;
2016 Cudd_IterDerefBdd(dd,auxfunc);
2017 }
2018
2019 return(1);
2020 failure:
2021 return(0);
2022
2023 } /* end of buildExorBDD */
2024
2025
2026 /**
2027 @brief Sets the level of each node.
2028
2029 @return 1 if successful; 0 otherwise.
2030
2031 @sideeffect Changes the level and visited fields of the nodes it
2032 visits.
2033
2034 @see bnetLevelDFS
2035
2036 */
2037 static int
bnetSetLevel(BnetNetwork * net)2038 bnetSetLevel(
2039 BnetNetwork * net)
2040 {
2041 BnetNode *node;
2042
2043 /* Recursively visit nodes. This is pretty inefficient, because we
2044 ** visit all nodes in this loop, and most of them in the recursive
2045 ** calls to bnetLevelDFS. However, this approach guarantees that
2046 ** all nodes will be reached ven if there are dangling outputs. */
2047 node = net->nodes;
2048 while (node != NULL) {
2049 if (!bnetLevelDFS(net,node)) return(0);
2050 node = node->next;
2051 }
2052
2053 /* Clear visited flags. */
2054 node = net->nodes;
2055 while (node != NULL) {
2056 node->visited = 0;
2057 node = node->next;
2058 }
2059 return(1);
2060
2061 } /* end of bnetSetLevel */
2062
2063
2064 /**
2065 @brief Does a DFS from a node setting the level field.
2066
2067 @return 1 if successful; 0 otherwise.
2068
2069 @sideeffect Changes the level and visited fields of the nodes it
2070 visits.
2071
2072 @see bnetSetLevel
2073
2074 */
2075 static int
bnetLevelDFS(BnetNetwork * net,BnetNode * node)2076 bnetLevelDFS(
2077 BnetNetwork * net,
2078 BnetNode * node)
2079 {
2080 int i;
2081 BnetNode *auxnd;
2082
2083 if (node->visited == 1) {
2084 return(1);
2085 }
2086
2087 node->visited = 1;
2088
2089 /* Graphical sources have level 0. This is the final value if the
2090 ** node has no fan-ins. Otherwise the successive loop will
2091 ** increase the level. */
2092 node->level = 0;
2093 for (i = 0; i < node->ninp; i++) {
2094 if (!st_lookup(net->hash, node->inputs[i], (void **) &auxnd)) {
2095 return(0);
2096 }
2097 if (!bnetLevelDFS(net,auxnd)) {
2098 return(0);
2099 }
2100 if (auxnd->level >= node->level) node->level = 1 + auxnd->level;
2101 }
2102 return(1);
2103
2104 } /* end of bnetLevelDFS */
2105
2106
2107 /**
2108 @brief Orders network roots for variable ordering.
2109
2110 @return an array with the ordered outputs and next state variables
2111 if successful; NULL otherwise.
2112
2113 @sideeffect None
2114
2115 */
2116 static BnetNode **
bnetOrderRoots(BnetNetwork * net,int * nroots)2117 bnetOrderRoots(
2118 BnetNetwork * net,
2119 int * nroots)
2120 {
2121 int i, noutputs;
2122 BnetNode *node;
2123 BnetNode **nodes = NULL;
2124
2125 /* Initialize data structures. */
2126 noutputs = net->noutputs;
2127 nodes = ALLOC(BnetNode *, noutputs);
2128 if (nodes == NULL) goto endgame;
2129
2130 /* Find output names and levels. */
2131 for (i = 0; i < net->noutputs; i++) {
2132 if (!st_lookup(net->hash,net->outputs[i],(void **)&node)) {
2133 goto endgame;
2134 }
2135 nodes[i] = node;
2136 }
2137
2138 util_qsort(nodes, noutputs, sizeof(BnetNode *),
2139 (DD_QSFP)bnetLevelCompare);
2140 *nroots = noutputs;
2141 return(nodes);
2142
2143 endgame:
2144 if (nodes != NULL) FREE(nodes);
2145 return(NULL);
2146
2147 } /* end of bnetOrderRoots */
2148
2149
2150 /**
2151 @brief Comparison function used by qsort.
2152
2153 @details Used to order the variables according to the number of keys
2154 in the subtables.
2155
2156 @return the difference in number of keys between the two variables
2157 being compared.
2158
2159 @sideeffect None
2160
2161 */
2162 static int
bnetLevelCompare(BnetNode ** x,BnetNode ** y)2163 bnetLevelCompare(
2164 BnetNode ** x,
2165 BnetNode ** y)
2166 {
2167 return((*y)->level - (*x)->level);
2168
2169 } /* end of bnetLevelCompare */
2170
2171
2172 /**
2173 @brief Does a DFS from a node ordering the inputs.
2174
2175 @return 1 if successful; 0 otherwise.
2176
2177 @sideeffect Changes visited fields of the nodes it visits.
2178
2179 @see Bnet_DfsVariableOrder
2180
2181 */
2182 static int
bnetDfsOrder(DdManager * dd,BnetNetwork * net,BnetNode * node)2183 bnetDfsOrder(
2184 DdManager * dd,
2185 BnetNetwork * net,
2186 BnetNode * node)
2187 {
2188 int i;
2189 BnetNode *auxnd;
2190 BnetNode **fanins;
2191
2192 if (node->visited == 1) {
2193 return(1);
2194 }
2195
2196 node->visited = 1;
2197 if (node->type == BNET_INPUT_NODE ||
2198 node->type == BNET_PRESENT_STATE_NODE) {
2199 node->dd = Cudd_bddNewVar(dd);
2200 if (node->dd == NULL) return(0);
2201 Cudd_Ref(node->dd);
2202 node->active = TRUE;
2203 node->var = node->dd->index;
2204 return(1);
2205 }
2206
2207 fanins = ALLOC(BnetNode *, node->ninp);
2208 if (fanins == NULL) return(0);
2209
2210 for (i = 0; i < node->ninp; i++) {
2211 if (!st_lookup(net->hash, node->inputs[i], (void **) &auxnd)) {
2212 FREE(fanins);
2213 return(0);
2214 }
2215 fanins[i] = auxnd;
2216 }
2217
2218 util_qsort(fanins, node->ninp, sizeof(BnetNode *),
2219 (DD_QSFP)bnetLevelCompare);
2220 for (i = 0; i < node->ninp; i++) {
2221 /* for (i = node->ninp - 1; i >= 0; i--) { */
2222 int res = bnetDfsOrder(dd,net,fanins[i]);
2223 if (res == 0) {
2224 FREE(fanins);
2225 return(0);
2226 }
2227 }
2228 FREE(fanins);
2229 return(1);
2230
2231 } /* end of bnetLevelDFS */
2232