Biddy  1.8.2
An academic Binary Decision Diagrams package
biddyInOut.c
Go to the documentation of this file.
1 /***************************************************************************/
45 #include "biddyInt.h"
46 
47 /* the following constants and types are used in Biddy_ReadVerilogFile() */
48 #define LINESIZE 999 /* maximum length of each input line read */
49 #define BUFSIZE 99999 /* maximum length of a buffer */
50 #define INOUTNUM 999 /* maximum number of inputs and outputs */
51 #define REGNUM 9999 /* maximum number of registers */
52 #define TOKENNUM 9999 /* maximum number of tokens */
53 #define GATENUM 9999 /* maximum number of gates */
54 #define LINENUM 99999 /* maximum number of lines */
55 #define WIRENUM 99999 /* maximum number of wires */
56 
57 /* recognized Verilog Boolean operators */
58 /* some of them are not very standard but they are used in various benchmarks */
59 /* we are trying to accept everything which is not in direct conflict with the standard */
60 /* https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ite_r_verilog_reserved_words.htm */
61 /* http://sutherland-hdl.com/pdfs/verilog_2001_ref_guide.pdf, page 3 */
62 /* http://www.externsoft.ch/download/verilog.html */
63 #define GATESNUM 9
64 const char* VerilogFileGateName[] = {
65  "buf",
66  "and",
67  "nand",
68  "or",
69  "nor",
70  "xor",
71  "xnor",
72  "not", "inv"
73 };
74 
75 /*----------------------------------------------------------------------------*/
76 /* Static function prototypes */
77 /*----------------------------------------------------------------------------*/
78 
79 /* The following functions are used in Biddy_Eval0(), Biddy_Eval1(), and Biddy_Eval1x(). */
80 
81 static Biddy_Boolean charOK(char c);
82 static void nextCh(Biddy_String s, int *i, Biddy_String *ch);
83 
84 /* Function ReadBDD()is used in Biddy_Eval0(). */
85 
86 static Biddy_Edge ReadBDD(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch);
87 
88 /* The following functions are used in Biddy_Eval1() and Biddy_Eval1x(). */
89 
90 static Biddy_Edge evaluate1(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch, Biddy_LookupFunction lf);
91 static Biddy_Edge evaluateN(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch, Biddy_Edge g, int op, Biddy_LookupFunction lf);
92 static int Op(Biddy_String s, int *i, Biddy_String *ch);
93 
94 /* Functions createVariablesFromBTree and createBddFromBTree() are used in Biddy_Eval2(). */
95 
96 static void createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree);
97 static Biddy_Edge createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i);
98 
99 /* The following functions are used in Biddy_ReadVerilogFile(). */
100 static void parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt);
101 static void createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c);
102 static void createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix);
103 static void parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count);
104 static void printModuleSummary(BiddyVerilogModule *m);
105 static void printCircuitSummary(BiddyVerilogCircuit *c);
106 static Biddy_Boolean isGate(Biddy_String word);
107 static Biddy_Boolean isSignalVector(Biddy_String word);
108 static Biddy_Boolean isEndOfLine(Biddy_String source);
109 static Biddy_Boolean isDefined(BiddyVerilogCircuit *c, Biddy_String name);
110 static void buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name);
111 static void buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name);
112 static int getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name);
113 static BiddyVerilogWire *getWireById(BiddyVerilogCircuit *c, int id);
114 static BiddyVerilogWire *getWireByName(BiddyVerilogCircuit *c, Biddy_String name);
115 static Biddy_String trim(Biddy_String source);
116 static void concat(char **s1, const char *s2);
117 
118 /* Function WriteBDD() is used in Biddy_WriteBDD(). */
119 
120 static void WriteBDD(Biddy_Manager MNG, Biddy_Edge f);
121 
122 /* Function WriteBDDx() is used in Biddy_WriteBDDx(). */
123 
124 static void WriteBDDx(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f, unsigned int *line);
125 
126 /* The following functions are used in Biddy_PrintfSOP() in Biddy_WriteSOP(). */
127 
128 static Biddy_Boolean WriteProduct(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first);
129 static Biddy_Boolean WriteProductx(Biddy_Manager MNG, FILE *s, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first);
130 static void WriteProductAlphabetic(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first);
131 static void WriteSOP(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable top, Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize, Biddy_Boolean combinationset);
132 static void WriteSOPx(Biddy_Manager MNG, FILE *s, Biddy_Edge f, Biddy_Variable top, Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize, Biddy_Boolean combinationset);
133 
134 /* The following functions are used in Biddy_WriteDot(). */
135 
136 static unsigned int enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n);
137 static void WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd);
138 static void WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd);
139 
140 /* The following functions are used in Biddy_WriteBddview(). */
141 
142 static void WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f);
143 
144 /* Other functions that may be used everywhere */
145 
146 static Biddy_String getname(Biddy_Manager MNG, void *p);
147 static Biddy_String getshortname(Biddy_Manager MNG, void *p, int n);
148 
149 /*----------------------------------------------------------------------------*/
150 /* Definition of exported functions */
151 /*----------------------------------------------------------------------------*/
152 
153 /***************************************************************************/
166 #ifdef __cplusplus
167 extern "C" {
168 #endif
169 
172 {
173  int i;
174  Biddy_String ch;
175  Biddy_String name;
176  Biddy_Edge f;
177 
178  if (!MNG) MNG = biddyAnonymousManager;
179 
180  if ((biddyManagerType == BIDDYTYPEOBDD) || (biddyManagerType == BIDDYTYPEOBDDC)) {
181  /* IMPLEMENTED */
182  } else if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZBDDC) ||
183  (biddyManagerType == BIDDYTYPETZBDD) || (biddyManagerType == BIDDYTYPETZBDDC))
184  {
185  fprintf(stderr,"Biddy_Eval0: this BDD type is not supported, yet!\n");
186  return NULL;
187  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
188  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
189  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
190  {
191  fprintf(stderr,"Biddy_Eval0: this BDD type is not supported, yet!\n");
192  return NULL;
193  } else {
194  fprintf(stderr,"Biddy_Eval0: Unsupported BDD type!\n");
195  return NULL;
196  }
197 
198  ch = (Biddy_String) malloc(255); /* max variable name length */
199 
200  i = 0;
201  nextCh(s,&i,&ch);
202  name = strdup(ch);
203 
204  f = ReadBDD(MNG,s,&i,&ch);
205 
206  if (Biddy_IsNull(f)) {
207  printf("(Biddy_Managed_Eval0) ERROR: char %d\n",i);
208  free(ch);
209  return((Biddy_String)"");
210  } else {
211  Biddy_Managed_AddPersistentFormula(MNG,name,f);
212  }
213 
214  nextCh(s,&i,&ch);
215  if (strcmp(ch,"")) {
216  printf("(Biddy_Managed_Eval0) ERROR: extra characters\n");
217  free(ch);
218  return((Biddy_String)"");
219  }
220 
221  free(ch);
222 
223  return(name);
224 }
225 
226 #ifdef __cplusplus
227 }
228 #endif
229 
230 /***************************************************************************/
243 #ifdef __cplusplus
244 extern "C" {
245 #endif
246 
249 {
250  Biddy_Edge sup;
251  Biddy_String ch;
252  int i;
253 
254  if (!MNG) MNG = biddyAnonymousManager;
255 
256  ch = (Biddy_String) malloc(255);
257 
258  i = 0;
259  nextCh(s,&i,&ch);
260  sup = evaluate1(MNG,s,&i,&ch,lf);
261 
262  free(ch);
263 
264  if (Biddy_IsNull(sup)) {
265  printf("(Biddy_Managed_Eval1x) ERROR: return NULL\n");
266  }
267 
268  return sup;
269 }
270 
271 #ifdef __cplusplus
272 }
273 #endif
274 
275 /***************************************************************************/
293 /* USE THIS FOR DEBUGGING */
294 /*
295 static void
296 printBiddyBTreeContainer(BiddyBTreeContainer *tree)
297 {
298  int i;
299  printf("availableNode=%d\n",tree->availableNode);
300  for (i = tree->availableNode; i >= 0; i--) {
301  printf("[%d]parent=%d,left=%d,right=%d,index=%d,op=%u",i,
302  tree->tnode[i].parent,
303  tree->tnode[i].left,
304  tree->tnode[i].right,
305  tree->tnode[i].index,
306  tree->tnode[i].op
307  );
308  if (tree->tnode[i].name) {
309  printf(",name=%s\n",tree->tnode[i].name);
310  } else {
311  printf("\n");
312  }
313  }
314 }
315 
316 static void
317 printPrefixFromBTree(BiddyBTreeContainer *tree, int i)
318 {
319  if (i == -1) return;
320  if (tree->tnode[i].op == 255) {
321  if (tree->tnode[i].name) {
322  printf("%s",tree->tnode[i].name);
323  } else {
324  printf("NULL");
325  }
326  return;
327  }
328  if (tree->tnode[i].op == 0) printf("(NOT");
329  else if (tree->tnode[i].op == 1) printf("(AND ");
330  else if (tree->tnode[i].op == 2) printf("(BUTNOT ");
331  else if (tree->tnode[i].op == 4) printf("(NOTBUT ");
332  else if (tree->tnode[i].op == 6) printf("(XOR ");
333  else if (tree->tnode[i].op == 7) printf("(OR ");
334  else printf("(? ");
335  printPrefixFromBTree(tree,tree->tnode[i].left);
336  printf(" ");
337  printPrefixFromBTree(tree,tree->tnode[i].right);
338  printf(")");
339 }
340 */
341 
342 #ifdef __cplusplus
343 extern "C" {
344 #endif
345 
348 {
349  /* NOT (~!), AND (&*), OR (|+), XOR (^%) , XNOR(-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (\), AND NOTBUT (/) ARE IMPLEMENTED */
350  char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' };
351  long tempPos,currStringPos,currTreePos,oldTreePos; /* tmp variables */
352  long offset; /* this is used for implementation of parenthesis and operator's priority */
353  char currS;
354  long i,j;
355  BiddyBTreeContainer *tree;
356  Biddy_Edge fbdd; /* result */
357  Biddy_String expression;
358 
359  if (!MNG) MNG = biddyAnonymousManager;
360 
361  i = 0; j = 0;
362  tree = (BiddyBTreeContainer *) calloc(1, sizeof(BiddyBTreeContainer));
363  if (!tree) return biddyNull;
364  tree->tnode = (BiddyBTreeNode*) malloc(1024 * sizeof(BiddyBTreeNode));
365  if (!tree->tnode) return biddyNull;
366  tree->availableNode = -1;
367  for (i = 1023; i > 0; i--) {
368  tree->tnode[i].name = NULL;
369  tree->tnode[i].parent = tree->availableNode;
370  tree->availableNode = i;
371  }
372  tree->tnode[0].index = 0;
373  tree->tnode[0].name = NULL;
374 
375  tempPos = 0;
376  currStringPos = 0;
377  currTreePos = 1;
378  oldTreePos = 0;
379  offset = 0;
380  expression = strdup(boolFunc);
381  currS = expression[currStringPos];
382  while (currS > '\n') {
383  if (currS == ' ') {
384  /* WHITE SPACE */
385  currStringPos++;
386  currS = expression[currStringPos];
387  continue;
388  }
389  currTreePos = tree->availableNode;
390  if (currTreePos != -1) {
391  tree->availableNode = tree->tnode[tree->availableNode].parent;
392  } else {
393  fprintf(stderr,"ERROR: SOMETHING WRONG WITH tree->availableNode\n");
394  return biddyNull;
395  }
396  if (j == 0) {
397  tree->tnode[oldTreePos].right = currTreePos;
398  tree->tnode[currTreePos].parent = oldTreePos;
399  tree->tnode[currTreePos].left = -1;
400  if (currS == '!') currS = '~'; /* operator '!' is also allowed for negation */
401  if (currS == boolOperators[0]) {
402  /* UNARY OPERATOR NOT */
403  tree->tnode[currTreePos].op = 0;
404  tree->tnode[currTreePos].index = offset + 3;
405  }
406  else if ((currS == '(') || (currS == '[') || (currS == '{')) {
407  /* OPEN PARENTHESIS */
408  offset += 4; currStringPos++;
409  currS = expression[currStringPos];
410  continue;
411  }
412  else if ((currS == '_') || ((currS >= '0') && (currS <= '9')) || ((currS >= 'A') && (currS <= 'Z')) || ((currS >= 'a') && (currS <= 'z'))) {
413  /* CONSTANT OR VARIABLE NAME */
414  tree->tnode[currTreePos].right = -1;
415  tree->tnode[currTreePos].op = 255;
416  tree->tnode[currTreePos].index = currStringPos;
417  while ((currS == '_') || ((currS >= '0') && (currS <= '9')) || ((currS >= 'A') && (currS <= 'Z')) || ((currS >= 'a') && (currS <= 'z'))) {
418  currStringPos++;
419  currS = expression[currStringPos];
420  }
421  expression[currStringPos] = 0;
422  tree->tnode[currTreePos].name = strdup(&expression[tree->tnode[currTreePos].index]);
423  tree->tnode[currTreePos].index = (int) strlen(tree->tnode[currTreePos].name); /* length of the variable name */
424  expression[currStringPos] = currS;
425  currStringPos--;
426  j = 1;
427  }
428  else {
429  /* printf("ERROR: MISSING OR INVALID VARIABLE NAME\n"); */
430  break;
431  }
432  }
433  else if (j == 1) {
434  /* CLOSE PARENTHESIS */
435  if ((currS == ')') || (currS == ']') || (currS == '}')) {
436  offset -= 4; currStringPos++;
437  currS = expression[currStringPos];
438  if (offset < 0) {
439  /* printf("ERROR: INVALID CLOSE PARENTHESIS\n"); */
440  j = 0;
441  break;
442  }
443  continue;
444  }
445  else {
446  /* BOOLEAN BINARY OPERATOR */
447  j = 0;
448  if (currS == '*') currS = '&'; /* operator '*' is also allowed for conjunction */
449  if (currS == '+') currS = '|'; /* operator '+' is also allowed for disjunction */
450  if (currS == '%') currS = '^'; /* operator '%' is also allowed for xor */
451  for (i = 0; i < 16; i++) { if (boolOperators[i] == currS) { break; } }
452  if (i == 0) {
453  /* printf("ERROR:INVALID USE OF UNARY OPERATOR ~\n"); */
454  break;
455  }
456  else if ((i < 16) && (boolOperators[i] != '#')) {
457  tree->tnode[currTreePos].op = (char) i;
458  if (i == 1) { tree->tnode[currTreePos].index = offset + 3; }
459  else if ((i == 2) || (i == 4)) { tree->tnode[currTreePos].index = offset + 3; }
460  else if ((i == 6) || (i == 7)) { tree->tnode[currTreePos].index = offset + 2; }
461  else { tree->tnode[currTreePos].index = offset + 1; }
462  oldTreePos = tree->tnode[oldTreePos].parent;
463  while (tree->tnode[oldTreePos].index >= tree->tnode[currTreePos].index) {
464  oldTreePos = tree->tnode[oldTreePos].parent;
465  }
466  tempPos = tree->tnode[oldTreePos].right;
467  tree->tnode[oldTreePos].right = currTreePos;
468  tree->tnode[tempPos].parent = currTreePos;
469  tree->tnode[currTreePos].parent = oldTreePos;
470  tree->tnode[currTreePos].left = tempPos;
471  }
472  else {
473  /* printf("ERROR: MISSING OPERATOR OR INVALID BOOLEAN OPERATOR %c\n",currS); */
474  break;
475  }
476  }
477  }
478  currStringPos++;
479  currS = expression[currStringPos];
480  oldTreePos = currTreePos;
481  }
482 
483  if (j == 0) {
484  /* printf("ERROR: INCORRECT REQUEST\n"); */
485  return biddyNull;
486  }
487 
488  /*
489  printBiddyBTreeContainer(tree);
490  */
491 
492  /*
493  printf("%s\n",expression);
494  printPrefixFromBTree(tree,tree->tnode[0].right);
495  printf("\n");
496  */
497 
498  free(expression);
499 
500  /* FOR SOME BDD TYPES, IT IS NECESSARY TO CREATE ALL VARIABLES IN ADVANCE */
501  /* createBddFromBTree DOES NOT STORE TMP RESULTS AS FORMULAE AND THUS */
502  /* TMP RESULTS BECOME WRONG IF NEW VARIABLES ARE ADDED ON-THE-FLY */
503 
504  createVariablesFromBTree(MNG,tree);
505  fbdd = createBddFromBTree(MNG,tree,tree->tnode[0].right);
506 
507  for (i = 1023; i >= 0; i--) {
508  if (tree->tnode[i].name) free(tree->tnode[i].name);
509  }
510  free(tree->tnode);
511  free(tree);
512 
513  return fbdd;
514 }
515 
516 #ifdef __cplusplus
517 }
518 #endif
519 
520 /***************************************************************************/
538 #ifdef __cplusplus
539 extern "C" {
540 #endif
541 
543 Biddy_Managed_ReadBddview(Biddy_Manager MNG, const char filename[],
544  Biddy_String name)
545 {
546  FILE *bddfile;
547  char buffer[65536]; /* line with variables can be very long! */
548  char buffer2[256];
549  char code[4];
550  Biddy_String word,word2,line;
551  BiddyVariableOrder *tableV;
552  BiddyNodeList *tableN;
553  int numV,numN;
554  int i,n,m; /* this must be signed because of the used for loop */
555  Biddy_Boolean typeOK,varOK,labelOK;
556  Biddy_Edge r;
557 
558  if (!MNG) MNG = biddyAnonymousManager;
559 
560  bddfile = fopen(filename,"r");
561  if (!bddfile) {
562  printf("Biddy_ReadBddview: File error (%s)!\n",filename);
563  return NULL;
564  }
565 
566  numV = 0;
567  numN = 0;
568  tableV = NULL;
569  tableN = NULL;
570 
571  typeOK = FALSE;
572  varOK = FALSE;
573  labelOK = FALSE;
574 
575  /* PARSE FILE */
576 
577  line = fgets(buffer,65535,bddfile);
578  while (line) {
579 
580  line = trim(line);
581 
582  /* DEBUGGING */
583  /*
584  printf("<%s>\n",line);
585  */
586 
587  if (line[0] == '#') { /* skip the comment line */
588  line = fgets(buffer,65535,bddfile);
589  continue;
590  }
591  else if ((line[0] == 'c') && !strncmp(line,"connect",7)) { /* parsing line with a connection */
592  line = &line[8];
593  word = word2 = NULL;
594  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
595  buffer[0] = buffer2[0] = 0;
596  sscanf(line,"%u %u %s %s",&n,&m,code,buffer);
597  if ((code[0] == 'e') || (code[0] == 'd'))
598  {
599  sscanf(line,"%u %u %s %s %s",&n,&m,code,buffer,buffer2);
600  }
601  if (buffer[0] == '"') {
602  buffer[strlen(buffer)-1] = 0;
603  word = &buffer[1];
604  } else {
605  if (buffer[0]) word = &buffer[0];
606  }
607  if (buffer2[0] == '"') {
608  buffer2[strlen(buffer2)-1] = 0;
609  word2= &buffer2[1];
610  } else {
611  if (buffer2[0]) word2 = &buffer2[0];
612  }
613  } else {
614  sscanf(line,"%u %u %s",&n,&m,code);
615  }
616  if (word2) {
617  tableN[n].ltag = Biddy_Managed_GetVariable(MNG,word);
618  tableN[n].rtag = Biddy_Managed_GetVariable(MNG,word2);
619  } else if (word) {
620  /* if (!strcmp(code,"l") || !strcmp(code,"s") || !strcmp(code,"si")) */
621  if ((code[0] == 'l') || (code[0] == 's'))
622  {
623  tableN[n].ltag = Biddy_Managed_GetVariable(MNG,word);
624  }
625  /* else if (!strcmp(code,"r") || !strcmp(code,"ri")) */
626  else if (code[0] == 'r')
627  {
628  tableN[n].rtag = Biddy_Managed_GetVariable(MNG,word);
629  }
630  /* else if (!strcmp(code,"e") || !strcmp(code,"di")) */
631  else if ((code[0] == 'e') || (code[0] == 'd'))
632  {
633  tableN[n].ltag = tableN[n].rtag = Biddy_Managed_GetVariable(MNG,word);
634  }
635  }
636  /* if (!strcmp(code,"s")) */
637  if ((code[0] == 's') && (code[1] == 0))
638  { /* regular label */
639  /* this is default type for all bdd types */
640  tableN[n].l = m;
641  }
642  /* else if (!strcmp(code,"si")) */
643  else if ((code[0] == 's') && (code[1] != 0))
644  { /* complemented label */
645  /* for OBDD, this is not allowed */
646  /* for OBDDC, this is type 3 */
647  /* for ZBDD, this is not allowed */
648  /* for ZBDDC, this is type 3 */
649  /* for TZBDD, this is not allowed */
650  /* for TZBDDC, this is type 3 */
651  tableN[n].l = m;
652  if (biddyManagerType == BIDDYTYPEOBDDC) {
653  tableN[n].type = 3;
654  }
655  else if (biddyManagerType == BIDDYTYPEZBDDC) {
656  tableN[n].type = 3;
657  }
658  else if (biddyManagerType == BIDDYTYPETZBDDC) {
659  tableN[n].type = 3;
660  } else {
661  printf("Biddy_ReadBddview: Problem with connection - wrong code\n");
662  return NULL;
663  }
664  }
665  /* else if (!strcmp(code,"l")) */
666  else if ((code[0] == 'l') && (code[1] == 0))
667  { /* regular left successor */
668  /* this is default type for all bdd types, this can be changed by right successor */
669  tableN[n].l = m;
670  }
671  /* else if (!strcmp(code,"li")) */
672  else if ((code[0] == 'l') && (code[1] != 0))
673  { /* complemented left successor */
674  /* for OBDD, this is not allowed */
675  /* for OBDDC, this is type 5 */
676  /* for ZBDD, this is not allowed */
677  /* for ZBDDC, this is not allowed */
678  /* for TZBDD, this is not allowed */
679  /* for TZBDDC, this is not allowed */
680  tableN[n].l = m;
681  if (biddyManagerType == BIDDYTYPEOBDDC) {
682  tableN[n].type = 5;
683  } else {
684  printf("Biddy_ReadBddview: Problem with connection - wrong code\n");
685  return NULL;
686  }
687  }
688  /* else if (!strcmp(code,"r")) */
689  else if ((code[0] == 'r') && (code[1] == 0))
690  { /* regular right successor */
691  /* this is default type for all bdd types, this can be changed by left successor */
692  tableN[n].r = m;
693  }
694  /* else if (!strcmp(code,"ri")) */
695  else if ((code[0] == 'r') && (code[1] != 0))
696  { /* complemented right successor */
697  tableN[n].r = m;
698  /* for OBDD, this is not allowed */
699  /* for OBDDC, this is not allowed */
700  /* for ZBDD, this is not allowed */
701  /* for ZBDDC, this is type 5 */
702  /* for TZBDD, this is not allowed */
703  /* for TZBDDC, this is type 5 */
704  if (biddyManagerType == BIDDYTYPEZBDDC) {
705  tableN[n].type = 5;
706  }
707  else if (biddyManagerType == BIDDYTYPETZBDDC) {
708  tableN[n].type = 5;
709  } else {
710  printf("Biddy_ReadBddview: Problem with connection - wrong code\n");
711  return NULL;
712  }
713  }
714  /* else if (!strcmp(code,"d")) */
715  else if ((code[0] == 'd') && (code[1] == 0))
716  { /* double line, type 'd' */
717  tableN[n].l = tableN[n].r = m;
718  /* for OBDD, this is not allowed */
719  /* for OBDDC, this is type 5 */
720  /* for ZBDD, this is not allowed */
721  /* for ZBDDC, this is not allowed */
722  /* for TZBDD, this is not allowed */
723  /* for TZBDDC, this is not allowed */
724  if (biddyManagerType == BIDDYTYPEOBDDC) {
725  tableN[n].type = 5;
726  } else {
727  printf("Biddy_ReadBddview: Problem with connection - wrong code\n");
728  return NULL;
729  }
730  }
731  /* else if (!strcmp(code,"di")) */
732  else if ((code[0] == 'd') && (code[1] != 0))
733  { /* double line, type 'di' */
734  /* for OBDD, this is not allowed */
735  /* for OBDDC, this is not allowed */
736  /* for ZBDD, this is not allowed */
737  /* for ZBDDC, this is type 5 */
738  /* for TZBDD, this is not allowed */
739  /* for TZBDDC, this is type 5 */
740  tableN[n].l = tableN[n].r = m;
741  if (biddyManagerType == BIDDYTYPEZBDDC) {
742  tableN[n].type = 5;
743  }
744  else if (biddyManagerType == BIDDYTYPETZBDDC) {
745  tableN[n].type = 5;
746  } else {
747  printf("Biddy_ReadBddview: Problem with connection - wrong code\n");
748  return NULL;
749  }
750  }
751  /* else if (!strcmp(code,"e")) */
752  else if ((code[0] == 'e') && (code[1] == 0))
753  { /* double line, type 'e' */
754  /* this is default type for all allowed bdd types */
755  tableN[n].l = tableN[n].r = m;
756  }
757  /* else if (!strcmp(code,"ei")) */
758  else if ((code[0] == 'e') && (code[1] != 0))
759  { /* double line, type 'ei' */
760  /* for OBDD, this is not allowed */
761  /* for OBDDC, this is not allowed */
762  /* for ZBDD, this is not allowed */
763  /* for ZBDDC, this is not allowed */
764  /* for TZBDD, this is not allowed */
765  /* for TZBDDC, this is not allowed */
766  tableN[n].l = tableN[n].r = m;
767  printf("Biddy_ReadBddview: Problem with connection - wrong code\n");
768  return NULL;
769  } else {
770  printf("Biddy_ReadBddview: Problem with connection - unknown code\n");
771  return NULL;
772  }
773  /* printf("CONNECT: <%u><%u><%s><%s><%s>\n",n,m,code,word,word2); */
774  }
775  else if ((line[0] == 'n') && !strncmp(line,"node",4)) { /* parsing line with node */
776  line = &line[5];
777  word = NULL;
778  sscanf(line,"%u %s",&n,buffer);
779  if (buffer[0]=='"') {
780  buffer[strlen(buffer)-1] = 0;
781  word = &buffer[1];
782  } else {
783  word = &buffer[0];
784  }
785  if (!numN) {
786  tableN = (BiddyNodeList *) malloc(sizeof(BiddyNodeList));
787  if (!tableN) return NULL;
788  } else if (numN <= n) {
789  tableN = (BiddyNodeList *) realloc(tableN,(n+1)*sizeof(BiddyNodeList));
790  if (!tableN) return NULL;
791  }
792  tableN[n].name = strdup(word);
793  tableN[n].id = n;
794  tableN[n].type = 4; /* 4 is for regular node, this may change to type 5 later */
795  tableN[n].l = tableN[n].r = -1;
796  tableN[n].ltag = tableN[n].rtag = 0;
797  tableN[n].f = NULL;
798  tableN[n].created = FALSE;
799  numN++;
800  /* printf("NODE: <%u><%s>\n",n,word); */
801  }
802  else if ((line[0] == 't') && !strncmp(line,"terminal",8)) { /* parsing line with terminal */
803  line = &line[9];
804  word = NULL;
805  sscanf(line,"%u %s",&n,buffer);
806  if (buffer[0]=='"') {
807  buffer[strlen(buffer)-1] = 0;
808  word = &buffer[1];
809  } else {
810  word = &buffer[0];
811  }
812  if (!numN) {
813  tableN = (BiddyNodeList *) malloc(sizeof(BiddyNodeList));
814  if (!tableN) return NULL;
815  } else if (numN <= n) {
816  tableN = (BiddyNodeList *) realloc(tableN,(n+1)*sizeof(BiddyNodeList));
817  if (!tableN) return NULL;
818  }
819  tableN[n].name = strdup(word);
820  tableN[n].id = n;
821  if (!strcmp(word,"0")) {
822  tableN[n].type = 0;
823  } else if (!strcmp(word,"1")) {
824  tableN[n].type = 1;
825  } else {
826  printf("Biddy_ReadBddview: Problem with terminal\n");
827  return NULL;
828  }
829  tableN[n].l = tableN[n].r = -1;
830  tableN[n].ltag = tableN[n].rtag = 0;
831  tableN[n].f = NULL;
832  tableN[n].created = FALSE;
833  numN++;
834  /* printf("TERMINAL: <%u><%s>\n",n,word); */
835  }
836  else if (!typeOK && !strncmp(line,"type",4)) { /* parsing line with type */
837  typeOK = TRUE;
838  line = &line[5];
839  /* printf("TYPE: %s\n",line); */
840  if (((biddyManagerType == BIDDYTYPEOBDD) && strcmp(line,"robdd") && strcmp(line,"ROBDD")) ||
841  ((biddyManagerType == BIDDYTYPEOBDDC) && strcmp(line,"robddce") && strcmp(line,"ROBDDCE")) ||
842  ((biddyManagerType == BIDDYTYPEZBDD) && strcmp(line,"zbdd") && strcmp(line,"ZBDD")) ||
843  ((biddyManagerType == BIDDYTYPEZBDDC) && strcmp(line,"zbddce") && strcmp(line,"ZBDDCE")) ||
844  ((biddyManagerType == BIDDYTYPETZBDD) && strcmp(line,"tzbdd") && strcmp(line,"TZBDD")) ||
845  ((biddyManagerType == BIDDYTYPETZBDDC) && strcmp(line,"tzbddce") && strcmp(line,"TZBDDCE")))
846  {
847  fprintf(stderr,"Biddy_ReadBddview: Wrong BDD type!\n");
848  return NULL;
849  }
850  }
851  else if (!varOK && !strncmp(line,"var",3)) { /* parsing line with variables */
852  varOK = TRUE;
853  line = &line[4];
854  word = strtok(line," ");
855  while (word) {
856  if (word[0]=='"') {
857  word[strlen(word)-1] = 0;
858  word = &word[1];
859  }
860  if (!numV) {
861  tableV = (BiddyVariableOrder *) malloc(sizeof(BiddyVariableOrder));
862  if (!tableV) return NULL;
863  } else {
864  tableV = (BiddyVariableOrder *) realloc(tableV,(numV+1)*sizeof(BiddyVariableOrder));
865  if (!tableV) return NULL;
866  }
867  tableV[numV].name = strdup(word);
868  tableV[numV].order = numV;
869  numV++;
870  /* printf("<%s>\n",word); */
871  word = strtok(NULL," ");
872  }
873  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
874  {
875  for (i=0; i<numV; i++) {
876  Biddy_Managed_AddVariableByName(MNG,tableV[i].name);
877  }
878  }
879  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
880  {
881  for (i=numV-1; i>=0; i--) {
882  Biddy_Managed_AddVariableByName(MNG,tableV[i].name);
883  }
884  }
885  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
886  {
887  for (i=numV-1; i>=0; i--) {
888  Biddy_Managed_AddVariableByName(MNG,tableV[i].name);
889  }
890  }
891  else {
892  fprintf(stderr,"Biddy_ReadBddview: Unknown BDD type!\n");
893  return NULL;
894  }
895  }
896  else if (!labelOK && !strncmp(line,"label",5)) { /* parsing line with label */
897  labelOK = TRUE;
898  line = &line[6];
899  word = NULL;
900  sscanf(line,"%u %s",&n,buffer);
901  if (buffer[0]=='"') {
902  buffer[strlen(buffer)-1] = 0;
903  word = &buffer[1];
904  } else {
905  word = &buffer[0];
906  }
907  if (!numN) {
908  tableN = (BiddyNodeList *) malloc(sizeof(BiddyNodeList));
909  if (!tableN) return NULL;
910  } else if (numN <= n) {
911  tableN = (BiddyNodeList *) realloc(tableN,(n+1)*sizeof(BiddyNodeList));
912  if (!tableN) return NULL;
913  }
914  tableN[n].name = strdup(word);
915  tableN[n].id = n;
916  tableN[n].type = 2; /* 2 is for regular label, this may change to type 3 later */
917  tableN[n].l = tableN[n].r = -1;
918  tableN[n].ltag = tableN[n].rtag = 0;
919  tableN[n].f = NULL;
920  tableN[n].created = FALSE;
921  numN++;
922  if (!name) name = strdup(word); /* only one label is supported */
923  /* printf("LABEL: <%u><%s>\n",n,word); */
924  }
925 
926  line = fgets(buffer,65535,bddfile);
927  }
928 
929  fclose(bddfile);
930 
931  /* CONSTRUCT BDD */
932 
933  /* DEBUGGING */
934  /*
935  for (i=0; i<numN; i++) {
936  printf("tableN[%d]: %s, type:%d, l:%d, ltag:%u<%s>, r:%d, rtag:%u<%s>\n",
937  tableN[i].id,tableN[i].name,tableN[i].type,
938  tableN[i].l,tableN[i].ltag,Biddy_Managed_GetVariableName(MNG,tableN[i].ltag),
939  tableN[i].r,tableN[i].rtag,Biddy_Managed_GetVariableName(MNG,tableN[i].rtag));
940  }
941  */
942 
943  r = BiddyConstructBDD(MNG,numN,tableN);
944  Biddy_Managed_AddFormula(MNG,name,r,-1);
945 
946  /* DEBUGGING */
947  /*
948  printf("BDD %s CONSTRUCTED\n",name);
949  */
950 
951  return name;
952 }
953 
954 #ifdef __cplusplus
955 }
956 #endif
957 
958 /***************************************************************************/
974 #ifdef __cplusplus
975 extern "C" {
976 #endif
977 
978 void
979 Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[],
980  Biddy_String prefix)
981 {
982  FILE *s;
983  BiddyVerilogCircuit *c;
984  unsigned int linecount, modulecount;
985  BiddyVerilogLine **lt;
986  BiddyVerilogModule **mt;
987  BiddyVerilogModule *md;
988  BiddyVerilogLine *ln;
989  unsigned int i,j;
990 
991  if (!MNG) MNG = biddyAnonymousManager;
992 
993  s = fopen(filename,"r");
994  if (!s) return;
995 
996  printf("PARSING FILE %s\n",filename);
997  c = (BiddyVerilogCircuit *) calloc(1,sizeof(BiddyVerilogCircuit)); /* declare an instance of a circuit */
998  c->name = strdup("CIRCUIT"); /* set circuit name */
999  parseVerilogFile(s,&linecount,&lt,&modulecount,&mt); /* read all modules from the file */
1000 
1001  fclose(s);
1002 
1003  printf("TARGET MODULE: %s\n",(mt[0])->name);
1004 
1005  /* DEBUGGING */
1006  /*
1007  for (i = 0; i < modulecount; i++) {
1008  printf("MODULE: %s\n",(mt[i])->name);
1009  }
1010  printf("ACCEPTABLE LINES\n");
1011  for (i = 0; i < linecount; i++) {
1012  printf("<%s> %s\n",(lt[i])->keyword,(lt[i])->line);
1013  }
1014  */
1015 
1016  createVerilogCircuit(linecount,lt,modulecount,mt,c); /* create circuit object for the given table of acceptable lines and table of modules */
1017  createBddFromVerilogCircuit(MNG,c,prefix); /* create BDDs for all primary outputs */
1018 
1019  for (i = 0; i < linecount; i++) {
1020  ln = lt[i];
1021  free(ln->keyword);
1022  free(ln->line);
1023  free(ln);
1024  }
1025  free(lt);
1026 
1027  for (i = 0; i < modulecount; i++) {
1028  md = mt[i];
1029  for (j = 0; j < md->outputcount; j++) free (md->outputs[j]);
1030  for (j = 0; j < md->inputcount; j++) free (md->inputs[j]);
1031  for (j = 0; j < md->wirecount; j++) free (md->wires[j]);
1032  for (j = 0; j < md->gatecount; j++) free (md->gates[j]);
1033  free(md->name);
1034  free(md);
1035  }
1036  free(mt);
1037 
1038  for (i=0; i < c->outputcount; i++) free (c->outputs[i]);
1039 
1040  for (i=0; i < c->inputcount; i++) free (c->inputs[i]);
1041 
1042  for (i=0; i < c->nodecount; i++) {
1043  free(c->nodes[i]->type);
1044  free(c->nodes[i]->name);
1045  free(c->nodes[i]);
1046  }
1047  free(c->nodes);
1048 
1049  for (i=0; i < c->wirecount; i++) {
1050  free (c->wires[i]->type);
1051  free (c->wires[i]);
1052  }
1053  free(c->wires);
1054 
1055  free(c->name);
1056  free(c);
1057 }
1058 
1059 #ifdef __cplusplus
1060 }
1061 #endif
1062 
1063 /***************************************************************************/
1075 #ifdef __cplusplus
1076 extern "C" {
1077 #endif
1078 
1079 void
1081 {
1082  if (!MNG) MNG = biddyAnonymousManager;
1083 
1084  if (Biddy_IsNull(f)) {
1085  printf("NULL\n");
1086  } else {
1087  WriteBDD(MNG,f);
1088  printf("\n");
1089  }
1090 }
1091 
1092 #ifdef __cplusplus
1093 }
1094 #endif
1095 
1096 /***************************************************************************/
1105 #ifdef __cplusplus
1106 extern "C" {
1107 #endif
1108 
1109 void
1110 Biddy_Managed_WriteBDD(Biddy_Manager MNG, const char filename[], Biddy_Edge f,
1111  Biddy_String label)
1112 {
1113  unsigned int line;
1114  FILE *s;
1115 
1116  if (!MNG) MNG = biddyAnonymousManager;
1117 
1118  s = fopen(filename,"w");
1119  if (!s) return;
1120 
1121  fprintf(s,"%s ",label);
1122 
1123  if (Biddy_IsNull(f)) {
1124  fprintf(s,"NULL\n");
1125  } else {
1126  line = 0;
1127  WriteBDDx(MNG,s,f,&line);
1128  if (line != 0) fprintf(s,"\n");
1129  }
1130 
1131  fclose(s);
1132 }
1133 
1134 #ifdef __cplusplus
1135 }
1136 #endif
1137 
1138 /***************************************************************************/
1151 #ifdef __cplusplus
1152 extern "C" {
1153 #endif
1154 
1155 void
1157 {
1158  unsigned int variableNumber;
1159  Biddy_Variable* variableTable;
1160  unsigned int i;
1161  int j;
1162  Biddy_Variable k,v;
1163  unsigned int numcomb;
1164 
1165  if (!MNG) MNG = biddyAnonymousManager;
1166 
1167  if (Biddy_IsNull(f)) {
1168  printf("NULL\n");
1169  return;
1170  }
1171 
1172  /* variableNumber is the number of dependent variables in BDD */
1173  variableNumber = Biddy_Managed_DependentVariableNumber(MNG,f,TRUE);
1174 
1175  /* DEBUGGING */
1176  /*
1177  reportOrdering();
1178  printf("DEPENDENT: %u\n",variableNumber);
1179  printf("TOP VARIABLE: %s\n",Biddy_Managed_GetVariableName(MNG,BiddyV(f)));
1180  for (k = 1; k < biddyVariableTable.num; k++) {
1181  if (biddyVariableTable.table[k].selected == TRUE) {
1182  printf("SELECTED: %s\n",Biddy_Managed_GetVariableName(MNG,k));
1183  }
1184  }
1185  */
1186 
1187  if (variableNumber > 6) {
1188  printf("Table for %d variables is to large for output.\n",variableNumber);
1189  for (k = 0; k < biddyVariableTable.num; k++) {
1190  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
1191  }
1192  return;
1193  }
1194 
1195  /* variableTable is a table of all dependent variables in BDD */
1196  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
1197  i = 0;
1198  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1199  for (k = 1; k < biddyVariableTable.num; k++) {
1200  if (biddyVariableTable.table[v].selected == TRUE) {
1201  variableTable[i] = v;
1202  printf("|%s",Biddy_Managed_GetVariableName(MNG,v));
1203  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1204  i++;
1205  }
1206  v = biddyVariableTable.table[v].next;
1207  }
1208  printf("|:value\n");
1209 
1210  numcomb = 1;
1211  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
1212  for (i = 0; i < numcomb; i++)
1213  {
1214  for (j = variableNumber - 1; j >= 0; j--) {
1215  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
1216  if (i&(1 << j)) {
1217  printf("%*c",1+(int)strlen(
1218  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1219  ),'1');
1220  } else {
1221  printf("%*c",1+(int)strlen(
1222  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1223  ),'0');
1224  }
1225  }
1226  printf(" :");
1227  if (Biddy_Managed_Eval(MNG,f)) printf("1\n"); else printf("0\n");
1228  }
1229 
1230  free(variableTable);
1231 }
1232 
1233 #ifdef __cplusplus
1234 }
1235 #endif
1236 
1237 
1238 /***************************************************************************/
1248 #ifdef __cplusplus
1249 extern "C" {
1250 #endif
1251 
1252 void
1253 Biddy_Managed_WriteTable(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
1254 {
1255  unsigned int variableNumber;
1256  Biddy_Variable* variableTable;
1257  unsigned int i;
1258  int j;
1259  Biddy_Variable k,v;
1260  unsigned int numcomb;
1261  FILE *s;
1262 
1263  if (!MNG) MNG = biddyAnonymousManager;
1264 
1265  if (filename) {
1266  s = fopen(filename,"w");
1267  } else {
1268  s = stdout;
1269  }
1270  if (!s) return;
1271 
1272  if (Biddy_IsNull(f)) {
1273  fprintf(s,"NULL\n");
1274  fclose(s);
1275  return;
1276  }
1277 
1278  /* variableNumber is the number of dependent variables in BDD */
1279  variableNumber = Biddy_Managed_DependentVariableNumber(MNG,f,TRUE);
1280 
1281  if (variableNumber > 6) {
1282  fprintf(s,"Table for %d variables is to large for output.\n",variableNumber);
1283  for (k = 0; k < biddyVariableTable.num; k++) {
1284  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
1285  }
1286  fclose(s);
1287  return;
1288  }
1289 
1290  /* variableTable is a table of all dependent variables in BDD */
1291  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
1292  i = 0;
1293  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1294  for (k = 1; k < biddyVariableTable.num; k++) {
1295  if (biddyVariableTable.table[v].selected == TRUE) {
1296  variableTable[i] = v;
1297  fprintf(s,"|%s",Biddy_Managed_GetVariableName(MNG,v));
1298  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1299  i++;
1300  }
1301  v = biddyVariableTable.table[v].next;
1302  }
1303  fprintf(s,"|:value\n");
1304 
1305  numcomb = 1;
1306  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
1307  for (i = 0; i < numcomb; i++)
1308  {
1309  for (j = variableNumber - 1; j >= 0; j--)
1310  {
1311  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
1312  if (i&(1 << j)) {
1313  fprintf(s,"%*c",1+(int)strlen(
1314  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1315  ),'1');
1316  } else {
1317  fprintf(s,"%*c",1+(int)strlen(
1318  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1319  ),'0');
1320  }
1321  }
1322  fprintf(s," :");
1323  if (Biddy_Managed_Eval(MNG,f)) fprintf(s,"1\n"); else fprintf(s,"0\n");
1324  }
1325 
1326  free(variableTable);
1327 
1328  if (filename) {
1329  fclose(s);
1330  }
1331 }
1332 
1333 #ifdef __cplusplus
1334 }
1335 #endif
1336 
1337 /***************************************************************************/
1345 #ifdef __cplusplus
1346 extern "C" {
1347 #endif
1348 
1349 void
1351 {
1352  unsigned int maxsize = 100;
1353  Biddy_Variable top;
1354 
1355  if (!MNG) MNG = biddyAnonymousManager;
1356 
1357  if (Biddy_IsNull(f)) {
1358  printf(" NULL\n");
1359  return;
1360  }
1361 
1362  if (Biddy_IsTerminal(f)) {
1363  if (f == biddyZero) {
1364  printf(" + 0\n");
1365  return;
1366  }
1367  else if (f == biddyOne) {
1368  printf(" + 1\n");
1369  return;
1370  }
1371  }
1372 
1373  top = BiddyV(f);
1374  if (biddyManagerType == BIDDYTYPEOBDD) {
1375  /* IMPLEMENTED */
1376  }
1377  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1378  /* IMPLEMENTED */
1379  }
1380  else if (biddyManagerType == BIDDYTYPEZBDD) {
1381  /* IMPLEMENTED */
1382  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1383  top = biddyVariableTable.table[top].prev;
1384  }
1385  }
1386  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1387  /* IMPLEMENTED */
1388  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1389  top = biddyVariableTable.table[top].prev;
1390  }
1391  }
1392  else if (biddyManagerType == BIDDYTYPETZBDD) {
1393  /* IMPLEMENTED */
1394  top = Biddy_GetTag(f);
1395  }
1396  else if (biddyManagerType == BIDDYTYPETZBDDC)
1397  {
1398  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1399  return;
1400  }
1401  else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1402  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1403  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1404  {
1405  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1406  return;
1407  }
1408  else {
1409  fprintf(stderr,"Biddy_PrintfSOP: Unsupported BDD type!\n");
1410  return;
1411  }
1412 
1413  WriteSOP(MNG,f,top,Biddy_GetMark(f),NULL,&maxsize,FALSE);
1414  printf("\n");
1415 }
1416 
1417 #ifdef __cplusplus
1418 }
1419 #endif
1420 
1421 /***************************************************************************/
1429 #ifdef __cplusplus
1430 extern "C" {
1431 #endif
1432 
1433 void
1434 Biddy_Managed_WriteSOP(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
1435 {
1436  unsigned int maxsize = 100;
1437  Biddy_Variable top;
1438  FILE *s;
1439 
1440  if (!MNG) MNG = biddyAnonymousManager;
1441 
1442  if (filename) {
1443  s = fopen(filename,"w");
1444  } else {
1445  s = stdout;
1446  }
1447  if (!s) return;
1448 
1449  if (Biddy_IsNull(f)) {
1450  fprintf(s," NULL\n");
1451  if (filename) {
1452  fclose(s);
1453  }
1454  return;
1455  }
1456 
1457  if (Biddy_IsTerminal(f)) {
1458  if (f == biddyZero) {
1459  fprintf(s," + 0\n");
1460  if (filename) {
1461  fclose(s);
1462  }
1463  }
1464  else if (f == biddyOne) {
1465  fprintf(s," + 1\n");
1466  if (filename) {
1467  fclose(s);
1468  }
1469  }
1470  }
1471 
1472  top = BiddyV(f);
1473  if (biddyManagerType == BIDDYTYPEOBDD) {
1474  /* IMPLEMENTED */
1475  }
1476  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1477  /* IMPLEMENTED */
1478  }
1479  else if (biddyManagerType == BIDDYTYPEZBDD) {
1480  /* IMPLEMENTED */
1481  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1482  top = biddyVariableTable.table[top].prev;
1483  }
1484  }
1485  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1486  /* IMPLEMENTED */
1487  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1488  top = biddyVariableTable.table[top].prev;
1489  }
1490  }
1491  else if (biddyManagerType == BIDDYTYPETZBDD) {
1492  /* IMPLEMENTED */
1493  top = Biddy_GetTag(f);
1494  }
1495  else if (biddyManagerType == BIDDYTYPETZBDDC)
1496  {
1497  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1498  if (filename) {
1499  fclose(s);
1500  }
1501  return;
1502  }
1503  else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1504  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1505  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1506  {
1507  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1508  if (filename) {
1509  fclose(s);
1510  }
1511  return;
1512  }
1513  else {
1514  fprintf(stderr,"Biddy_PrintfSOP: Unsupported BDD type!\n");
1515  if (filename) {
1516  fclose(s);
1517  }
1518  return;
1519  }
1520 
1521  WriteSOPx(MNG,s,f,top,Biddy_GetMark(f),NULL,&maxsize,FALSE);
1522 
1523  if (filename) {
1524  fclose(s);
1525  }
1526 
1527 }
1528 
1529 #ifdef __cplusplus
1530 }
1531 #endif
1532 
1533 
1534 /***************************************************************************/
1552 static void PrintfMintermsOBDD(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean negative);
1553 
1554 #ifdef __cplusplus
1555 extern "C" {
1556 #endif
1557 
1558 void
1559 Biddy_Managed_PrintfMinterms(Biddy_Manager MNG, Biddy_Edge f,
1560  Biddy_Boolean negative)
1561 {
1562  unsigned int maxsize = 0; /* needed for WriteSOP but not used */
1563 
1564  if (!MNG) MNG = biddyAnonymousManager;
1565 
1566  if (Biddy_IsNull(f)) {
1567  printf("NULL\n");
1568  return;
1569  }
1570 
1571  if (f == biddyZero) {
1572  printf("EMPTY\n");
1573  return;
1574  }
1575 
1576  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1577  PrintfMintermsOBDD(MNG,f,negative);
1578  }
1579  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1580  WriteSOP(MNG,f,Biddy_Managed_GetTopVariable(MNG,f),Biddy_GetMark(f),NULL,&maxsize,TRUE);
1581  printf("\n");
1582  }
1583  else if (biddyManagerType == BIDDYTYPETZBDD) {
1584  WriteSOP(MNG,f,Biddy_Managed_GetLowestVariable(MNG),Biddy_GetMark(f),NULL,&maxsize,TRUE);
1585  printf("\n");
1586  }
1587  else if (biddyManagerType == BIDDYTYPETZBDDC)
1588  {
1589  printf("Biddy_PrintfMinterms: this BDD type is not supported, yet!\n");
1590  return;
1591  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
1592  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
1593  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
1594  {
1595  printf("Biddy_PrintfMinterms: this BDD type is not supported, yet!\n");
1596  return;
1597  } else {
1598  printf("Biddy_PrintfMinterms: Unsupported BDD type!\n");
1599  return;
1600  }
1601 }
1602 
1603 #ifdef __cplusplus
1604 }
1605 #endif
1606 
1607 static void
1608 PrintfMintermsOBDD(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean negative)
1609 {
1610  unsigned int variableNumber;
1611  Biddy_Variable* variableTable;
1612  unsigned int i;
1613  int j;
1614  Biddy_Variable k,v;
1615  unsigned int numcomb;
1616  Biddy_Boolean first;
1617 
1618  /* all variables are included into minterms! */
1619  variableNumber = biddyVariableTable.num - 1;
1620 
1621  /* DEBUGGING */
1622  /*
1623  printf("variableNumber = %u\n",variableNumber);
1624  */
1625 
1626  if (variableNumber > 16) {
1627  printf("Biddy_PrintfMinterms: to many variables, variableNumber = %d, max = 16\n",variableNumber);
1628  return;
1629  }
1630 
1631  /* variableTable is a table of all variables - the active ordering is considered */
1632  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
1633  i = 0;
1634  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1635  for (k = 1; k < biddyVariableTable.num; k++) {
1636  variableTable[i] = v;
1637  i++;
1638  v = biddyVariableTable.table[v].next;
1639  }
1640 
1641  numcomb = 1;
1642  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
1643  /* for (i = numcomb - 1; i >= 0; i--) */
1644  for (i = 0; i < numcomb; i++)
1645  {
1646  for (j = variableNumber - 1; j >= 0; j--) {
1647  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
1648  }
1649  if (Biddy_Managed_Eval(MNG,f)) {
1650  printf("{");
1651  first = TRUE;
1652  for (j = variableNumber - 1; j >= 0; j--) {
1653  if (i&(1 << j)) {
1654  if (first) first = FALSE; else printf(",");
1655  printf("%s",Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1]));
1656  } else {
1657  if (negative) {
1658  if (first) first = FALSE; else printf(",");
1659  printf("*%s",Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1]));
1660  }
1661  }
1662  }
1663  printf("}");
1664  }
1665  }
1666  printf("\n");
1667 
1668  free(variableTable);
1669 }
1670 
1671 /***************************************************************************/
1688 #ifdef __cplusplus
1689 extern "C" {
1690 #endif
1691 
1692 unsigned int
1693 Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f,
1694  const char label[], int id, Biddy_Boolean cudd)
1695 {
1696  unsigned int n;
1697  char *label1;
1698  char *hash;
1699  FILE *s;
1700  Biddy_Variable tag;
1701  BiddyLocalInfo *li;
1702  Biddy_Variable v;
1703  Biddy_String name;
1704 
1705  if (!MNG) MNG = biddyAnonymousManager;
1706 
1707  /* if (id != -1) use it instead of <...> */
1708 
1709  if (Biddy_IsNull(f)) {
1710  printf("WARNING (Biddy_Managed_WriteDot): Function is null!\n");
1711  return 0;
1712  }
1713 
1714  if (filename) {
1715  s = fopen(filename,"w");
1716  } else {
1717  s = stdout;
1718  }
1719  if (!s) return 0;
1720 
1721  if (Biddy_IsTerminal(f)) {
1722  n = 1; /* there is only one terminal node */
1723  } else {
1724  BiddyCreateLocalInfo(MNG,f);
1725  n = enumerateNodes(MNG,f,0); /* this will select all nodes except terminal node */
1727  }
1728 
1729  label1 = strdup(label);
1730  while ((hash=strchr(label1,'#'))) hash[0]='_'; /* avoid hashes in the name */
1731 
1732  if (cudd) {
1733  fprintf(s,"//GENERATED WITH BIDDY - biddy.meolic.com\n");
1734  if (filename) {
1735  fprintf(s,"//USE 'dot -y -Tpng -O %s' TO VISUALIZE %s\n",filename,biddyManagerName);
1736  }
1737  fprintf(s,"digraph \"DD\" {\n");
1738  /* fprintf(s,"size = \"7.5,10\"\n"); */
1739  fprintf(s,"center=true;\nedge [dir=none];\n");
1740  fprintf(s,"{ node [shape=plaintext];\n");
1741  fprintf(s," edge [style=invis];\n");
1742  fprintf(s," \"CONST NODES\" [style = invis];\n");
1743 
1744  if (!Biddy_IsTerminal(f)) {
1745  li = (BiddyLocalInfo *)(BiddyN(f)->list);
1747  while (li->back) {
1748  v = BiddyV(li->back);
1749  if (biddyVariableTable.table[v].value == biddyZero) {
1750  biddyVariableTable.table[v].value = biddyOne;
1751  /* variable names containing # are adpated */
1752  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
1753  while ((hash = strchr(name,'#'))) hash[0] = '_';
1754  fprintf(s,"\" %s \" -> ",name);
1755  free(name);
1756  }
1757  li = &li[1]; /* next field in the array */
1758  }
1760  }
1761 
1762  fprintf(s,"\"CONST NODES\"; \n}\n");
1763  fprintf(s,"{ rank=same; node [shape=box]; edge [style=invis];\n");
1764  fprintf(s,"\"%s\"",label1);
1765  fprintf(s,"; }\n");
1766  } else {
1767  fprintf(s,"//GENERATED WITH BIDDY - biddy.meolic.com\n");
1768  if (filename) {
1769  fprintf(s,"//USE 'dot -y -Tpng -O %s' TO VISUALIZE %s\n",filename,biddyManagerName);
1770  }
1771  fprintf(s,"digraph ");
1772  if (biddyManagerType == BIDDYTYPEOBDD) fprintf(s,"ROBDD");
1773  else if (biddyManagerType == BIDDYTYPEZBDD) fprintf(s,"ZBDD");
1774  else if (biddyManagerType == BIDDYTYPETZBDD) fprintf(s,"TZBDD");
1775  else if (biddyManagerType == BIDDYTYPEOBDDC) fprintf(s,"ROBDDCE");
1776  else if (biddyManagerType == BIDDYTYPEZBDDC) fprintf(s,"ZBDDCE");
1777  else if (biddyManagerType == BIDDYTYPETZBDDC) fprintf(s,"TZBDDCE");
1778  else fprintf(s,"BDD");
1779  fprintf(s," {\n");
1780  fprintf(s," ordering=out;\n");
1781 #ifdef LEGACY_DOT
1782 #else
1783  fprintf(s," edge [dir=\"both\"];\n");
1784 #endif
1785  fprintf(s," edge [arrowhead=\"none\"]\n");
1786  fprintf(s," node [shape=none, label=\"%s\"] 0;\n",label1);
1787  }
1788 
1789  WriteDotNodes(MNG,s,f,id,cudd);
1790 
1791  if (((biddyManagerType == BIDDYTYPEOBDD) ||
1792  (biddyManagerType == BIDDYTYPEZBDD) ||
1793  (biddyManagerType == BIDDYTYPETZBDD) ||
1794  !(Biddy_GetMark(f))))
1795  {
1796  if ((f != biddyZero) && (tag = Biddy_GetTag(f))) {
1797  if (cudd) {
1798  fprintf(s,"\"%s\"",label1);
1799  if (Biddy_IsTerminal(f)) {
1800  fprintf(s," -> \"1\" [style=solid label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1801  } else {
1802  fprintf(s," -> \"%p\" [style=solid label=\"%s\"];\n",BiddyP(f),Biddy_Managed_GetVariableName(MNG,tag));
1803  }
1804  } else {
1805 #ifdef LEGACY_DOT
1806  fprintf(s," 0 -> 1 [style=solid label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1807 #else
1808  fprintf(s," 0 -> 1 [arrowtail=\"none\" label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1809 #endif
1810  }
1811  } else {
1812  if (cudd) {
1813  fprintf(s,"\"%s\"",label1);
1814  if (Biddy_IsTerminal(f)) {
1815  fprintf(s," -> \"1\" [style=solid];\n");
1816  } else {
1817  fprintf(s," -> \"%p\" [style=solid];\n",BiddyP(f));
1818  }
1819  } else {
1820 #ifdef LEGACY_DOT
1821  fprintf(s," 0 -> 1 [style=solid];\n");
1822 #else
1823  fprintf(s," 0 -> 1 [arrowtail=\"none\"];\n");
1824 #endif
1825  }
1826  }
1827  } else {
1828  if ((f != biddyZero) && (tag = Biddy_GetTag(f))) {
1829  if (cudd) {
1830  fprintf(s,"\"%s\"",label1);
1831  if (Biddy_IsTerminal(f)) {
1832  fprintf(s," -> \"1\" [style=dotted label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1833  } else {
1834  fprintf(s," -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),Biddy_Managed_GetVariableName(MNG,tag));
1835  }
1836  } else {
1837 #ifdef LEGACY_DOT
1838  fprintf(s," 0 -> 1 [style=dotted label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1839 #else
1840  fprintf(s," 0 -> 1 [arrowtail=\"none\" arrowhead=\"dot\" label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1841 #endif
1842  }
1843  } else {
1844  if (cudd) {
1845  fprintf(s,"\"%s\"",label1);
1846  if (Biddy_IsTerminal(f)) {
1847  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1848  fprintf(s," -> \"1\" [style=dotted];\n");
1849  } else {
1850  fprintf(s," -> \"1\" [style=bold];\n");
1851  }
1852  } else {
1853  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1854  fprintf(s," -> \"%p\" [style=dotted];\n",BiddyP(f));
1855  } else {
1856  fprintf(s," -> \"%p\" [style=bold];\n",BiddyP(f));
1857  }
1858  }
1859  } else {
1860 #ifdef LEGACY_DOT
1861  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1862  fprintf(s," 0 -> 1 [style=dotted];\n");
1863  } else {
1864  fprintf(s," 0 -> 1 [style=bold];\n");
1865  }
1866 #else
1867  fprintf(s," 0 -> 1 [arrowtail=\"none\" arrowhead=\"dot\"];\n");
1868 #endif
1869  }
1870  }
1871  }
1872 
1873  free(label1);
1874 
1875  WriteDotEdges(MNG,s,f,cudd); /* this will select all nodes except terminal node */
1876 
1877  if (!Biddy_IsTerminal(f)) {
1878  BiddyDeleteLocalInfo(MNG,f);
1879  }
1880 
1881  fprintf(s,"}\n");
1882 
1883  if (filename) {
1884  fclose(s);
1885  }
1886 
1887  return n;
1888 }
1889 
1890 #ifdef __cplusplus
1891 }
1892 #endif
1893 
1894 /***************************************************************************/
1911 #ifdef __cplusplus
1912 extern "C" {
1913 #endif
1914 
1915 unsigned int
1916 Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[],
1917  Biddy_Edge f, const char label[], void *xytable)
1918 {
1919  FILE *s;
1920  unsigned int i,n;
1921  Biddy_Boolean useCoordinates;
1922  BiddyLocalInfo *li;
1923  Biddy_Variable v,k,tag;
1924  char *hash;
1925  Biddy_String name;
1926  BiddyXY *table;
1927 
1928  if (!MNG) MNG = biddyAnonymousManager;
1929 
1930  if (Biddy_IsNull(f)) {
1931  /* printf("ERROR Biddy_Managed_WriteBddview: Function is null!\n"); */
1932  return 0 ;
1933  }
1934 
1935  if (filename) {
1936  s = fopen(filename,"w");
1937  } else {
1938  s = stdout;
1939  }
1940  if (!s) {
1941  printf("ERROR: s = 0\n");
1942  return(0);
1943  }
1944 
1945  table = (BiddyXY *)xytable;
1946 
1947  fprintf(s,"#GENERATED WITH BIDDY - biddy.meolic.com\n");
1948 
1949  /* WRITE BDD TYPE */
1950 
1951  if (biddyManagerType == BIDDYTYPEOBDD) {
1952  fprintf(s,"type ROBDD\n");
1953  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1954  fprintf(s,"type ROBDDCE\n");
1955  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1956  fprintf(s,"type ZBDD\n");
1957  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1958  fprintf(s,"type ZBDDCE\n");
1959  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1960  fprintf(s,"type TZBDD\n");
1961  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
1962  fprintf(s,"type TZBDDCE\n");
1963  } else if (biddyManagerType == BIDDYTYPEOFDD) {
1964  fprintf(s,"type ROFDD\n");
1965  } else if (biddyManagerType == BIDDYTYPEOFDDC) {
1966  fprintf(s,"type ROFDDCE\n");
1967  } else if (biddyManagerType == BIDDYTYPEZFDD) {
1968  fprintf(s,"type ZFDD\n");
1969  } else if (biddyManagerType == BIDDYTYPEZFDDC) {
1970  fprintf(s,"type ZFDDCE\n");
1971  } else if (biddyManagerType == BIDDYTYPETZFDD) {
1972  fprintf(s,"type TZFDD\n");
1973  } else if (biddyManagerType == BIDDYTYPETZFDDC) {
1974  fprintf(s,"type TZFDDCE\n");
1975  }
1976 
1977  /* WRITE VARIABLES */
1978  /* A conservative approach to list all the existing variables */
1979  /* in the manager (and not only the dependent ones) is used. */
1980 
1981  fprintf(s,"var");
1982  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1983  for (k = 1; k < biddyVariableTable.num; k++) {
1984  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
1985 
1986  /* variable names containing # are adpated */
1987  while ((hash = strchr(name,'#'))) hash[0] = '_';
1988  /* to support EST, also variable names containing <> are adapted */
1989  for (i=0; i<strlen(name); i++) {
1990  if (name[i] == '<') name[i] = '_';
1991  if (name[i] == '>') name[i] = 0;
1992  }
1993 
1994  fprintf(s," \"%s\"",name);
1995  free(name);
1996  v = biddyVariableTable.table[v].next;
1997  }
1998  fprintf(s,"\n");
1999 
2000  /* PREPARE CALCULATION */
2001 
2002  useCoordinates = FALSE;
2003  if (Biddy_IsTerminal(f)) {
2004 
2005  n = 1; /* for all BDD types, in memory there is only one terminal node */
2006  if (table) {
2007  /* use table of nodes given by the user */
2008  useCoordinates = TRUE;
2009  } else {
2010  n = 1; /* there is one terminal node */
2011  table = (BiddyXY *) malloc((n+1) * sizeof(BiddyXY)); /* n = nodes, add one label */
2012  if (!table) return 0;
2013  table[0].id = 0;
2014  table[0].label = strdup(label);
2015  table[0].x = 0;
2016  table[0].y = 0;
2017  table[0].isConstant = FALSE;
2018  table[1].id = 1;
2019  table[1].label = getname(MNG,f);
2020  table[1].x = 0;
2021  table[1].y = 0;
2022  table[1].isConstant = TRUE;
2023  }
2024 
2025  } else {
2026 
2027  BiddyCreateLocalInfo(MNG,f);
2028  n = enumerateNodes(MNG,f,0); /* this will select all nodes except terminal node */
2030 
2031  if (table) {
2032  /* use table of nodes given by the user */
2033  useCoordinates = TRUE;
2034  } else {
2035  /* generate table of nodes */
2036  /* TO DO: coordinates are not calculated, how to do this without graphviz/dot? */
2037  table = (BiddyXY *) malloc((n+1) * sizeof(BiddyXY)); /* n = nodes, add one label */
2038  if (!table) return 0;
2039  table[0].id = 0;
2040  table[0].label = strdup(label);
2041  table[0].x = 0;
2042  table[0].y = 0;
2043  table[0].isConstant = FALSE;
2044  li = (BiddyLocalInfo *)(BiddyN(f)->list);
2045  while (li->back) {
2046 
2047  /* add one node */
2048  table[li->data.enumerator].id = li->data.enumerator;
2049  table[li->data.enumerator].label = getname(MNG,li->back);
2050  table[li->data.enumerator].x = 0;
2051  table[li->data.enumerator].y = 0;
2052  table[li->data.enumerator].isConstant = FALSE;
2053 
2054  /* if one or both successors are terminal node then extra nodes must be added */
2055  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
2056  if (((biddyManagerType == BIDDYTYPEOBDD) ||
2057  (biddyManagerType == BIDDYTYPEZBDD) ||
2058  (biddyManagerType == BIDDYTYPETZBDD)
2059  ) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back))))
2060  {
2061  /* two terminal nodes only if complemented edges are not used and they are different */
2062  unsigned int num;
2063  num = 0;
2064  if (Biddy_IsTerminal(BiddyE(li->back))) {
2065  num = 1;
2066  table[li->data.enumerator+1].id = li->data.enumerator+1;
2067  if (BiddyE(li->back) == biddyZero) {
2068  table[li->data.enumerator+1].label = strdup("0");
2069  } else {
2070  table[li->data.enumerator+1].label = strdup("1");
2071  }
2072  table[li->data.enumerator+1].x = 0;
2073  table[li->data.enumerator+1].y = 0;
2074  table[li->data.enumerator+1].isConstant = TRUE;
2075  }
2076  if (Biddy_IsTerminal(BiddyT(li->back))) {
2077  table[li->data.enumerator+num+1].id = li->data.enumerator+num+1;
2078  if (BiddyT(li->back) == biddyZero) {
2079  table[li->data.enumerator+num+1].label = strdup("0");
2080  } else {
2081  table[li->data.enumerator+num+1].label = strdup("1");
2082  }
2083  table[li->data.enumerator+num+1].x = 0;
2084  table[li->data.enumerator+num+1].y = 0;
2085  table[li->data.enumerator+num+1].isConstant = TRUE;
2086  }
2087  } else {
2088  /* only one terminal node */
2089  table[li->data.enumerator+1].id = li->data.enumerator+1;
2090  table[li->data.enumerator+1].label = strdup("1");
2091  table[li->data.enumerator+1].x = 0;
2092  table[li->data.enumerator+1].y = 0;
2093  table[li->data.enumerator+1].isConstant = TRUE;
2094  }
2095  }
2096 
2097  li = &li[1]; /* next field in the array */
2098  }
2099  }
2100 
2101  }
2102 
2103  /* WRITE bddview NODES */
2104 
2105  if (useCoordinates) {
2106  fprintf(s,"label %d %s %d %d\n",table[0].id,table[0].label,table[0].x,table[0].y);
2107  } else {
2108  fprintf(s,"label %d %s\n",table[0].id,table[0].label);
2109  }
2110  for (i=1;i<(n+1);i++) {
2111  if (table[i].isConstant) {
2112  fprintf(s,"terminal ");
2113  } else {
2114  fprintf(s,"node ");
2115  }
2116  if (useCoordinates) {
2117  fprintf(s,"%d %s %d %d\n",table[i].id,table[i].label,table[i].x,table[i].y);
2118  } else {
2119  fprintf(s,"%d %s\n",table[i].id,table[i].label);
2120  }
2121  }
2122 
2123  if (!useCoordinates) {
2124  for (i=1;i<(n+1);i++) {
2125  free(table[i].label);
2126  }
2127  free(table);
2128  }
2129 
2130  /* WRITE bddview CONNECTIONS */
2131 
2132  fprintf(s,"connect 0 1 ");
2133  if ((biddyManagerType == BIDDYTYPEOBDD) ||
2134  (biddyManagerType == BIDDYTYPEZBDD) ||
2135  (biddyManagerType == BIDDYTYPETZBDD))
2136  {
2137  fprintf(s,"s");
2138  }
2139  else {
2140  if (Biddy_GetMark(f)) {
2141  fprintf(s,"si");
2142  } else {
2143  fprintf(s,"s");
2144  }
2145  }
2146 
2147  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2148  {
2149  tag = Biddy_GetTag(f);
2150  fprintf(s," %s\n",Biddy_Managed_GetVariableName(MNG,tag));
2151  } else {
2152  fprintf(s,"\n");
2153  }
2154 
2155  if (!Biddy_IsTerminal(f)) {
2156  WriteBddviewConnections(MNG,s,f); /* this will select all nodes except terminal node */
2157  BiddyDeleteLocalInfo(MNG,f);
2158  }
2159 
2160  if (filename) {
2161  fclose(s);
2162  }
2163 
2164  return n;
2165 }
2166 
2167 #ifdef __cplusplus
2168 }
2169 #endif
2170 
2171 /*----------------------------------------------------------------------------*/
2172 /* Definition of internal functions */
2173 /*----------------------------------------------------------------------------*/
2174 
2175 /*----------------------------------------------------------------------------*/
2176 /* Definition of static functions */
2177 /*----------------------------------------------------------------------------*/
2178 
2179 /* Some of these were implemented long time ago (1995). */
2180 /* Not comprehensible. */
2181 
2182 #define oAND 1
2183 #define oOR 2
2184 #define oEXOR 3
2185 
2186 static Biddy_Boolean
2187 charOK(char c)
2188 {
2189  return (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z') || c == '_' ||
2190  (c >= '0' && c <= '9') || c == '[' || c == ']' ||
2191  c == '+' || c == '-' || c == '*' || c == '\'' ||
2192  c == '$' || c == '&' || c == '%' || c == '#' ||
2193  c == '?' || c == '!' || c == ':' || c == '.' ;
2194 }
2195 
2196 static void
2197 nextCh(Biddy_String s, int *i, Biddy_String *ch)
2198 {
2199  char c;
2200  int j;
2201 
2202  while (s[*i] == ' ' || s[*i] == '\t' || s[*i] == '\n') (*i)++;
2203  j = *i;
2204  c = s[*i];
2205 
2206  /* DEBUGGING */
2207  /*
2208  printf("%c",c);
2209  */
2210 
2211  if (c == '(') {
2212  (*i)++;
2213  strcpy(*ch,"(");
2214  return;
2215  }
2216 
2217  if (c == ')') {
2218  (*i)++;
2219  strcpy(*ch,")");
2220  return;
2221  }
2222 
2223  if (c == '*') {
2224  (*i)++;
2225  strcpy(*ch,"*");
2226  return;
2227  }
2228 
2229  if (charOK(c)) {
2230  (*i)++;
2231  while (charOK(s[*i])) (*i)++;
2232  c = s[*i];
2233 
2234  /* DEBUGGING */
2235  /*
2236  printf("%c",c);
2237  */
2238 
2239  if ( (c == ' ') || (c == '\t') || (c == '\n') || (c == '(') || (c == ')') ) {
2240  strncpy(*ch, &(s[j]), *i-j);
2241  (*ch)[*i-j] = 0;
2242  return;
2243  }
2244  }
2245 
2246  strcpy(*ch,"");
2247  return;
2248 }
2249 
2250 static Biddy_Edge
2251 ReadBDD(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch)
2252 {
2253  Biddy_Boolean inv;
2254  Biddy_String varname;
2255  Biddy_Edge f,n,e,t;
2256 
2257  assert( (biddyManagerType == BIDDYTYPEOBDD) || (biddyManagerType == BIDDYTYPEOBDDC) );
2258 
2259  nextCh(s,i,ch);
2260 
2261  if (strcmp(*ch,"*")) {
2262  inv = FALSE;
2263  } else {
2264  inv = TRUE;
2265  /* printf("<*>\n"); */
2266  nextCh(s,i,ch);
2267  }
2268 
2269  /* printf("<%s>\n",*ch); */
2270 
2271  if (!strcmp(*ch,"0")) {
2272  if (inv) {
2273  f = biddyOne;
2274  } else {
2275  f = biddyZero;
2276  }
2277  } else if (!strcmp(*ch,"1")) {
2278  if (inv) {
2279  f = biddyZero;
2280  } else {
2281  f = biddyOne;
2282  }
2283  } else {
2284  varname = strdup(*ch);
2285  n = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_GetVariable(MNG,varname)); /* variables should already exist */
2286  if (!n) return biddyNull;
2287  nextCh(s,i,ch);
2288  if (strcmp(*ch,"(")) {
2289  printf("ERROR: <%s>\n",*ch);
2290  return biddyNull;
2291  }
2292  e = ReadBDD(MNG,s,i,ch);
2293  nextCh(s,i,ch);
2294  if (strcmp(*ch,")")) {
2295  printf("ERROR: <%s>\n",*ch);
2296  return biddyNull;
2297  }
2298  nextCh(s,i,ch);
2299  if (strcmp(*ch,"(")) {
2300  printf("ERROR: <%s>\n",*ch);
2301  return biddyNull;
2302  }
2303  t = ReadBDD(MNG,s,i,ch);
2304  nextCh(s,i,ch);
2305  if (strcmp(*ch,")")) {
2306  printf("ERROR: <%s>\n",*ch);
2307  return biddyNull;
2308  }
2309  if (inv) {
2310  f = Biddy_Managed_Not(MNG,Biddy_Managed_ITE(MNG,n,t,e));
2311  } else {
2312  f = Biddy_Managed_ITE(MNG,n,t,e);
2313  }
2314  free(varname);
2315  }
2316 
2317  return f;
2318 }
2319 
2320 static Biddy_Edge
2321 evaluate1(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch,
2323 {
2324  unsigned int idx;
2325  Biddy_Edge f;
2326  int op;
2327 
2328  /* DEBUGGING */
2329  /*
2330  printf("evaluate1: %s\n",s);
2331  printf("evaluate1 i = %d\n",*i);
2332  printf("evaluate1 ch = %s\n",*ch);
2333  */
2334 
2335  if (!strcmp(*ch,"(")) {
2336  nextCh(s,i,ch);
2337 
2338  if (!strcasecmp(*ch, "NOT")) {
2339  nextCh(s,i,ch);
2340  f = Biddy_Managed_Not(MNG,evaluate1(MNG,s,i,ch,lf));
2341  } else {
2342  if ((op = Op(s,i,ch))) {
2343  f = evaluateN(MNG,s,i,ch,evaluate1(MNG,s,i,ch,lf),op,lf);
2344  } else {
2345  f = evaluate1(MNG,s,i,ch,lf);
2346  }
2347  }
2348 
2349  if (!strcmp(*ch, ")")) nextCh(s,i,ch);
2350 
2351  return f;
2352  }
2353 
2354  /* evaluate1 will always check Biddy's formula table */
2355  /* if (lf != NULL) then user's formula table will be checked, too */
2356  /* user's formula table will be checked before Biddy's formula table */
2357  /* entries in user's formula should not be obsolete */
2358 
2359  if (charOK(*ch[0])) {
2360  if (!lf) {
2361  if (!Biddy_Managed_FindFormula(MNG,*ch,&idx,&f)) {
2363  }
2364  } else {
2365  if ((!(lf(*ch,&f))) &&
2366  (!Biddy_Managed_FindFormula(MNG,*ch,&idx,&f))) {
2368  }
2369  }
2370  nextCh(s,i,ch);
2371 
2372  assert( f != biddyNull );
2373 
2374  return f;
2375  }
2376 
2377  return biddyNull;
2378 }
2379 
2380 static Biddy_Edge
2381 evaluateN(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch,
2382  Biddy_Edge g, int op, Biddy_LookupFunction lf)
2383 {
2384  Biddy_Edge f, h;
2385 
2386  /* DEBUGGING */
2387  /*
2388  printf("evaluateN: %s\n",s);
2389  printf("evaluateN i = %d\n",*i);
2390  printf("evaluateN ch = %s\n",*ch);
2391  */
2392 
2393  h = evaluate1(MNG,s,i,ch,lf);
2394  if (!Biddy_IsNull(h)) {
2395  f = biddyNull;
2396  switch (op) {
2397  case oAND: f = Biddy_Managed_And(MNG,g,h);
2398  break;
2399  case oOR: f = Biddy_Managed_Or(MNG,g,h);
2400  break;
2401  case oEXOR: f = Biddy_Managed_Xor(MNG,g,h);
2402  }
2403  return evaluateN(MNG,s,i,ch,f,op,lf);
2404  }
2405  return g;
2406 }
2407 
2408 static int
2409 Op(Biddy_String s, int *i, Biddy_String *ch)
2410 {
2411 
2412  /* DEBUGGING */
2413  /*
2414  printf("Op ch = %s\n",*ch);
2415  */
2416 
2417  if (!strcasecmp(*ch, "AND")) {
2418  nextCh(s,i,ch);
2419  return oAND;
2420  }
2421 
2422  if (!strcasecmp(*ch, "OR")) {
2423  nextCh(s,i,ch);
2424  return oOR;
2425  }
2426 
2427  if (!strcasecmp(*ch, "EXOR")) {
2428  nextCh(s,i,ch);
2429  return oEXOR;
2430  }
2431 
2432  return 0;
2433 }
2434 
2435 static void
2436 createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree)
2437 {
2438  int i;
2439  unsigned int idx;
2440  Biddy_Edge tmp;
2441 
2442  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
2443  {
2444  for (i = 0; i <= tree->availableNode; i++) {
2445  if (tree->tnode[i].op == 255) {
2446  if (tree->tnode[i].name) {
2447  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&tmp))) {
2448  Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2449  }
2450  }
2451  }
2452  }
2453  }
2454 
2455  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2456  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2457  {
2458  for (i = tree->availableNode; i >= 0; i--) {
2459  if (tree->tnode[i].op == 255) {
2460  if (tree->tnode[i].name) {
2461  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&tmp))) {
2462  Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2463  }
2464  }
2465  }
2466  }
2467  }
2468 }
2469 
2470 static Biddy_Edge
2471 createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i)
2472 {
2473  unsigned int idx;
2474  Biddy_Edge lbdd,rbdd,fbdd;
2475 
2476  if (i == -1) return biddyNull;
2477  if (tree->tnode[i].op == 255) {
2478  if (tree->tnode[i].name) {
2479  if (!strcmp(tree->tnode[i].name,"0")) fbdd = biddyZero;
2480  else if (!strcmp(tree->tnode[i].name,"1")) fbdd = biddyOne;
2481  else {
2482  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&fbdd))) {
2483  fbdd = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2484  }
2485  }
2486  } else {
2487  fbdd = biddyNull;
2488  }
2489 
2490  /* DEBUGGING */
2491  /*
2492  printf("createBddFromBTree: op == 255\n");
2493  printPrefixFromBTree(tree,i);
2494  printf("\n");
2495  printf("HERE IS fbdd:\n");
2496  Biddy_PrintfBDD(fbdd);
2497  Biddy_PrintfSOP(fbdd);
2498  */
2499 
2500  return fbdd;
2501  }
2502  lbdd = createBddFromBTree(MNG,tree,tree->tnode[i].left);
2503  rbdd = createBddFromBTree(MNG,tree,tree->tnode[i].right);
2504 
2505  /* NOT (~!), AND (&*), OR (|+), XOR (^%) , XNOR(-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (\), AND NOTBUT (/) ARE IMPLEMENTED */
2506  /* char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' }; */
2507  if (tree->tnode[i].op == 0) fbdd = Biddy_Managed_Not(MNG,rbdd); /* NOT */
2508  else if (tree->tnode[i].op == 1) fbdd = Biddy_Managed_And(MNG,lbdd,rbdd); /* AND */
2509  else if (tree->tnode[i].op == 2) fbdd = Biddy_Managed_Gt(MNG,lbdd,rbdd); /* BUTNOT */
2510  else if (tree->tnode[i].op == 4) fbdd = Biddy_Managed_Gt(MNG,rbdd,lbdd); /* NOTBUT */
2511  else if (tree->tnode[i].op == 6) fbdd = Biddy_Managed_Xor(MNG,lbdd,rbdd); /* XOR */
2512  else if (tree->tnode[i].op == 7) fbdd = Biddy_Managed_Or(MNG,lbdd,rbdd); /* OR */
2513  else if (tree->tnode[i].op == 8) fbdd = Biddy_Managed_Nor(MNG,lbdd,rbdd); /* NOR */
2514  else if (tree->tnode[i].op == 9) fbdd = Biddy_Managed_Xnor(MNG,lbdd,rbdd); /* XNOR */
2515  else if (tree->tnode[i].op == 11) fbdd = Biddy_Managed_Leq(MNG,rbdd,lbdd); /* IMPLIES <= */
2516  else if (tree->tnode[i].op == 13) fbdd = Biddy_Managed_Leq(MNG,lbdd,rbdd); /* IMPLIES => */
2517  else if (tree->tnode[i].op == 14) fbdd = Biddy_Managed_Nand(MNG,lbdd,rbdd); /* NAND */
2518  else fbdd = biddyNull;
2519 
2520  /* DEBUGGING */
2521  /*
2522  printf("createBddFromBTree: op == %u\n",tree->tnode[i].op);
2523  printPrefixFromBTree(tree,i);
2524  printf("\n");
2525  printf("HERE IS lbdd:\n");
2526  Biddy_PrintfBDD(lbdd);
2527  Biddy_PrintfSOP(lbdd);
2528  printf("HERE IS rbdd:\n");
2529  Biddy_PrintfBDD(rbdd);
2530  Biddy_PrintfSOP(rbdd);
2531  printf("HERE IS fbdd:\n");
2532  Biddy_PrintfBDD(fbdd);
2533  Biddy_PrintfSOP(fbdd);
2534  */
2535 
2536  return fbdd;
2537 }
2538 
2539 static void
2540 parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt)
2541 {
2542  unsigned int activemodule=0;
2543  BiddyVerilogLine *ln;
2544  BiddyVerilogModule *md;
2545  unsigned int i=0, j=0, k=0; /* indexes */
2546  char ch, linebuf[LINESIZE]; /* buffer for single line from the verilog file */
2547  Biddy_String buffer; /* buffer for complete verilog statements */
2548  Biddy_String token[TOKENNUM]; /* array to hold tokens for the line */
2549  Biddy_String keyword; /* keyword from verilog line */
2550  Biddy_Boolean comment, noname, ok, acceptable;
2551  Biddy_String t,tc;
2552  unsigned int tn;
2553 
2554  (*l) = 0;
2555  (*lt) = NULL;
2556  (*n) = 0;
2557  (*mt) = NULL;
2558 
2559  keyword = NULL;
2560  buffer = NULL;
2561  md = NULL;
2562  while (fgets(linebuf,LINESIZE,verilogfile) != NULL) {
2563 
2564  if (keyword) free(keyword);
2565  tn = (unsigned int) strspn(linebuf," ");
2566 
2567  if (tn == strlen(linebuf)) {
2568  continue; /* skip empty lines and white space */
2569  }
2570 
2571  /* get 1st word from the line */
2572  tn += (unsigned int) strcspn(&linebuf[tn]," ");
2573  ch = 0;
2574  if (tn < strlen(linebuf)) {
2575  ch = linebuf[tn];
2576  linebuf[tn] = 0;
2577  }
2578  tn = (unsigned int) strspn(linebuf," ");
2579  keyword = strdup(&linebuf[tn]);
2580  if (ch) {
2581  tn += (unsigned int) strcspn(&linebuf[tn]," ");
2582  linebuf[tn] = ch;
2583  }
2584  keyword = trim(keyword);
2585 
2586  if (!strlen(keyword)) {
2587  continue; /* skip white space not recognised before */
2588  }
2589 
2590  if (!strcmp(keyword,"//")) {
2591  continue; /* skip comment lines */
2592  }
2593 
2594  if (buffer) free(buffer);
2595  buffer = strdup("");
2596  if (!strcmp(keyword,"endmodule")) { /* endmodule keyword does not use ';' */
2597  concat(&buffer,keyword);
2598  } else {
2599  concat(&buffer,linebuf);
2600  while (!isEndOfLine(linebuf)) { /* check if the line ends with a ';' character (multiple lines statement) */
2601  if (fgets(linebuf,LINESIZE,verilogfile) != NULL) {/* otherwise, append all the following lines */
2602  concat(&buffer,linebuf);
2603  if ((strlen(buffer) + LINESIZE) > BUFSIZE) printf("ERROR (parseVerilogFile): BUFFER TO SMALL\n");
2604  }
2605  }
2606  }
2607 
2608  /* tokenize the line to extract data */
2609  noname = FALSE;
2610  if (strcmp(keyword,"module") && strcmp(keyword,"endmodule") &&
2611  strcmp(keyword,"input") && strcmp(keyword,"output") &&
2612  strcmp(keyword,"wire") && strcmp(keyword,"reg") &&
2613  strcmp(keyword,"assign"))
2614  {
2615  tn = (unsigned int) strspn(buffer," ");
2616  tn += (unsigned int) strcspn(&buffer[tn]," ");
2617  tn += (unsigned int) strspn(&buffer[tn]," ");
2618  if (buffer[tn] == '(') noname = TRUE;
2619  }
2620  i=0;
2621  comment = FALSE;
2622  t = strtok(buffer," ");
2623  token[i++] = strdup(t); /* full keyword */
2624  if (noname) {
2625  sprintf(linebuf,"NONAME%d",(*l));
2626  token[i++] = strdup(linebuf); /* add NONAME */
2627  }
2628  while ((t = strtok(NULL," (),;\r\n")) && (strcmp(t,"//"))) {
2629  if (!strcmp(t,"/*")) comment = TRUE;
2630  if (!comment) {
2631  if (strlen(t)>1) {
2632  tn = (unsigned int) strcspn(t,"{}");
2633  while (tn != strlen(t)) {
2634  tc = NULL;
2635  if (t[tn] == '{') tc = strdup("{");
2636  if (t[tn] == '}') tc = strdup("}");
2637  if (tn) {
2638  t[tn] = 0;
2639  token[i++] = strdup(t);
2640  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2641  }
2642  token[i++] = tc;
2643  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2644  t = &t[tn+1];
2645  tn = (unsigned int) strcspn(t,"{}");
2646  }
2647  }
2648  if (strlen(t)) {
2649  token[i++] = strdup(t);
2650  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2651  }
2652  }
2653  if (comment && !strcmp(t,"*/")) comment = FALSE;
2654  }
2655  token[i] = NULL;
2656 
2657  if (!strcmp(keyword,"module")) { /* START OF MODULE */
2658  (*n)++;
2659  (*mt) = (BiddyVerilogModule **) realloc((*mt), (*n) * sizeof(BiddyVerilogModule *)); /* create or enlarge table of modules */
2660  md = (BiddyVerilogModule *) calloc(1, sizeof(BiddyVerilogModule)); /* declare an instance of a module */
2661  (*mt)[(*n)-1] = md;
2662  md->name = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for module name string */
2663  strcpy(md->name,token[1]); /* set module name */
2664  activemodule = (*n);
2665  /* DEBUGGING */
2666  /*
2667  printf("MODULE: %s (#%d)\n",token[1],activemodule);
2668  */
2669  md->outputFirst = TRUE; /* TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3), FALSE iff N3 = NAND(N1,N2) */
2670  }
2671 
2672  if (!strcmp(keyword,"endmodule")) { /* END OF MODULE */
2673  /* DEBUGGING */
2674  /*
2675  printf("ENDMODULE: #%d\n",activemodule);
2676  */
2677  activemodule = 0;
2678  md = NULL;
2679  } else {
2680  if (!activemodule) {
2681  printf("ERROR (parseVerilogFile): statement <%s> is outside of module\n",keyword);
2682  continue;
2683  }
2684  }
2685 
2686  acceptable = FALSE;
2687  if ((activemodule == 1) || !strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
2688  /* TO DO: MULTIPLE MODULES ARE NOT SUPPORTED, YET */
2689 
2690  if (!strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
2691  acceptable = TRUE;
2692  }
2693 
2694  else if (!strcmp(keyword,"input")) { /* PRIMARY INPUTS */
2695  acceptable = TRUE;
2696  for (j = 1; j < i; j++) { /* parse all the words in the line */
2697  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2698  parseSignalVector(md->inputs, token, &j, &md->inputcount);
2699  else { /* not a vector of signal */
2700  md->inputs[md->inputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for input string */
2701  strcpy(md->inputs[md->inputcount],token[j]); /* add the input name to the array of inputs */
2702  (md->inputcount)++; /* update the number of inputs in the circuit */
2703  if (md->inputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
2704  }
2705  }
2706  }
2707 
2708  else if (!strcmp(keyword,"output")) { /* PRIMARY OUTPUTS */
2709  acceptable = TRUE;
2710  for (j = 1; j < i; j++) { /* parse all the words in the line */
2711  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2712  parseSignalVector(md->outputs, token, &j, &md->outputcount);
2713  else { /* not a vector of signal */
2714  md->outputs[md->outputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for output string */
2715  strcpy(md->outputs[md->outputcount],token[j]); /* add the output name to the array of outputs */
2716  (md->outputcount)++; /* update the number of outputs in the circuit */
2717  if (md->outputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
2718  }
2719  }
2720  }
2721 
2722  else if (!strcmp(keyword,"wire")) { /* WIRES */
2723  for (j = 1; j < i; j++) { /* parse all the words in the line */
2724  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2725  parseSignalVector(md->wires, token, &j, &md->wirecount);
2726  else { /* not a vector of signal */
2727  /* check if this wire has not already been stated as input or output */
2728  ok = TRUE;
2729  for (k=0; k < md->inputcount; k++) {
2730  if (!strcmp(md->inputs[k],token[j])) ok = FALSE;
2731  }
2732  for (k=0; k < md->outputcount; k++) {
2733  if (!strcmp(md->outputs[k],token[j])) ok = FALSE;
2734  }
2735  if (ok) {
2736  acceptable = TRUE;
2737  md->wires[md->wirecount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for wire string */
2738  strcpy(md->wires[md->wirecount],token[j]); /* add the wire name to the array of wires */
2739  (md->wirecount)++; /* update the number of wires in the circuit */
2740  if (md->wirecount >= WIRENUM) printf("ERROR (parseVerilogFile): WIRENUM TO SMALL\n");
2741  } else {
2742  /* DEBUGGING */
2743  /*
2744  printf("WARNING (parseVerilogFile): wire %s already defined as input/output\n",token[j]);
2745  */
2746  }
2747  }
2748  }
2749  }
2750 
2751  else if (!strcmp(keyword,"reg")) { /* REGS */
2752  acceptable = TRUE;
2753  for (j = 1; j < i; j++) { /* parse all the words in the line */
2754  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2755  parseSignalVector (md->regs, token, &j, &md->regcount);
2756  else { /* not a vector of signal */
2757  md->regs[md->regcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for reg string */
2758  strcpy(md->regs [md->regcount],token[j]); /* add the reg name to the array of regs */
2759  (md->regcount)++; /* update the number of regs in the circuit */
2760  if (md->regcount >= REGNUM) printf("ERROR (parseVerilogFile): REGNUM TO SMALL\n");
2761  }
2762  }
2763  }
2764 
2765  else if (isGate(keyword)) { /* BASIC GATES */
2766  acceptable = TRUE;
2767  md->gates[md->gatecount] = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for gate name string */
2768  strcpy(md->gates[md->gatecount],token[1]); /* add the gate name to the array of gates */
2769  if (!md->gatecount) { /* use the first gate to determine md->outputFirst */
2770  for (j=0; md->inputs[j] != NULL; j++) if (!strcmp(md->inputs[j],token[2])) md->outputFirst = FALSE;
2771  }
2772  (md->gatecount)++; /* update the number of gates in the circuit */
2773  if (md->gatecount >= GATENUM) printf("ERROR (parseVerilogFile): GATENUM TO SMALL\n");
2774  }
2775 
2776  else {
2777  /* AN UNIMPLEMENTED KEYWORD */
2778  /* GATES DEFINED BY OTHER MODULES ARE NOT RESOLVED */
2779  }
2780 
2781  }
2782 
2783  /* add this line to the table of acceptable lines */
2784  if (acceptable) {
2785  (*l)++;
2786  (*lt) = (BiddyVerilogLine **) realloc((*lt), (*l) * sizeof(BiddyVerilogLine *)); /* create or enlarge table of lines */
2787  ln = (BiddyVerilogLine *) calloc(1, sizeof(BiddyVerilogLine)); /* declare an instance of a line */
2788  ln->keyword = strdup(keyword);
2789  ln->line = strdup(token[0]);
2790  for (j=1; j<i; j++) concat(&(ln->line),token[j]);
2791  (*lt)[(*l)-1] = ln;
2792  }
2793 
2794  }
2795 
2796  if (keyword) free(keyword);
2797  if (buffer) free(buffer);
2798 
2799  /* DEBUGGING - print summary of the module */
2800  /*
2801  printModuleSummary(m);
2802  */
2803 }
2804 
2809 static void
2810 createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c)
2811 {
2812  BiddyVerilogModule *m;
2813  unsigned int i=0, j=0, k=0, l=0;
2814  int in=0, id=0, index=0;
2815  unsigned int activemodule=0;
2816  Biddy_String keyword, buffer;
2817  Biddy_String token[TOKENNUM]; /* array to hold tokens for one line */
2818  Biddy_Boolean ok;
2819  Biddy_String tmptoken;
2820 
2821  memset(token, 0, sizeof(char*) * TOKENNUM);
2822 
2823  m = mt[0]; /* target module is the first one in the table */
2824 
2825  /* initialization of the circuit */
2826  c->inputcount = m->inputcount; /* set the number of inputs for the ciruit */
2827  c->outputcount = m->outputcount; /* set the number of outputs for the circuit */
2828  c->wirecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of wires for the circuit */
2829  c->nodecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of nodes for the circuit */
2830  c->wires = (BiddyVerilogWire **) calloc(c->wirecount,sizeof(BiddyVerilogWire *)); /* allocate a contiguous array to index every wire */
2831  c->nodes = (BiddyVerilogNode **) calloc(c->nodecount,sizeof(BiddyVerilogNode *)); /* allocate a contiguous array to index every node */
2832 
2833  id = 0;
2834  for (i=0; i < m->inputcount; i++) { /* store the names of primary inputs */
2835  c->inputs[i] = (Biddy_String) calloc(strlen(m->inputs[i]) + 1, sizeof (char));
2836  strcpy(c->inputs[i],m->inputs[i]);
2837  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2838  buildNode(c->nodes[id],(Biddy_String)"input", m->inputs[i]);
2839  id++;
2840  }
2841  for (i=0; i < m->outputcount; i++) { /* store the names of primary outputs */
2842  c->outputs[i] = (Biddy_String) calloc(strlen(m->outputs[i]) + 1, sizeof(char));
2843  strcpy(c->outputs[i],m->outputs[i]);
2844  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2845  buildNode(c->nodes[id],(Biddy_String)"output",m->outputs[i]);
2846  id++;
2847  }
2848  for (i=0; i < m->wirecount; i++) { /* store the names of wires */
2849  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2850  buildNode(c->nodes[id],(Biddy_String)"wire",m->wires[i]);
2851  id++;
2852  }
2853  for (i=0; i < m->gatecount; i++) { /* store the names of gates */
2854  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2855  buildNode(c->nodes[id],(Biddy_String)"gate",m->gates[i]);
2856  id++;
2857  }
2858 
2859  index = 0;
2860  for (l=0; l<linecount;l++) {
2861  keyword = lt[l]->keyword;
2862  buffer = lt[l]->line;
2863 
2864  if (!strcmp(keyword,"module")) {
2865  activemodule++;
2866  continue;
2867  }
2868 
2869  if (!strcmp(keyword,"endmodule")) {
2870  continue;
2871  }
2872 
2873  if (activemodule > 1) {
2874  /* TO DO: MULTIPLE MODULES ARE NOT FULLY SUPPORTED, YET */
2875  continue;
2876  }
2877 
2878  if (!strcmp(keyword,"input")) {
2879  continue;
2880  }
2881  if (!strcmp(keyword,"output")) {
2882  continue;
2883  }
2884  if (!strcmp(keyword,"wire")) {
2885  continue;
2886  }
2887  if (!strcmp(keyword,"reg")) {
2888  continue;
2889  }
2890  if (!strcmp(keyword,"assign")) {
2891  continue;
2892  }
2893 
2894  /* tokenize the line to extract data */
2895  i=0;
2896  token[0] = strtok(buffer," ");
2897  while(token[i]!= NULL) {
2898  /* DEBUGGING */
2899  /*
2900  printf("(#%d) TOKENIZE: <%s>\n",i,token[i]);
2901  */
2902  i++;
2903  token[i] = strtok(NULL," ");
2904  }
2905 
2906  if (!isGate(keyword)) {
2907  printf("WARNING (createVerilogCircuit): SKIP <%s>\n",buffer);
2908  continue;
2909  }
2910 
2911  if (!m->outputFirst) {
2912  /* m->outputFirst == FALSE iff "nand NAND2_1 (N1, N2, N3);" defines N3 = NAND(N1,N2) */
2913  /* m->outputFirst == TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3) */
2914  /* exchange token[2] and token[i-1] */
2915  tmptoken = token[2];
2916  token[2] = token[i-1];
2917  token[i-1] = tmptoken;
2918  }
2919 
2920  /* A. Check or create wires for all the gate inputs */
2921  /* if wire is not known it will be treated as a primary input */
2922  for (j = 3; j < i; j++) {
2923  if (!isDefined(c,token[j])) {
2924  ok = FALSE;
2925  for (k=0; k < m->wirecount; k++) { /* check the names of wires */
2926  if (!strcmp(m->wires[k],token[j])) {
2927  printf("ERROR (createVerilogCircuit): wire %s used before defined!\n",token[j]);
2928  exit(1);
2929  }
2930  }
2931  for (k=0; !ok && k < m->inputcount; k++) { /* check the names of primary inputs */
2932  if (!strcmp(m->inputs[k],token[j])) ok = TRUE;
2933  }
2934  if (!ok) {
2935  printf("WARNING (createVerilogCircuit): wire %s treated as primary input!\n",token[j]);
2936  }
2937  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2938  buildWire(c,c->wires[index],(Biddy_String)"I",token[j]);
2939  /* assign inputs to the wires representing gate inputs */
2940  /* NOT NEEDED */
2941  /* assign outputs to the wires representing gate inputs */
2942  /* NOT USED */
2943  index++;
2944  }
2945  }
2946 
2947  /* B. Create a wire for the gate */
2948  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2949  buildWire(c,c->wires[index],keyword,token[1]);
2950  /* assign inputs to the wire representing gate */
2951  in = 0;
2952  for (j = 3; j < i; j++) {
2953  c->wires[index]->inputs[in] = getNodeIdByName(c,token[j]);
2954  c->wires[index]->inputcount++;
2955  in++;
2956  }
2957  /* assign outputs to the wire representing gate */
2958  /* NOT USED */
2959  index++;
2960 
2961  /* C. Check or create a wire for the gate output */
2962  if (!isDefined(c,token[2])) { /* if wire is not already defined */
2963  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2964  buildWire(c,c->wires[index],(Biddy_String)"W",token[2]);
2965  /* assign inputs to the wire representing gate ouput */
2966  c->wires[index]->inputs[0] = getNodeIdByName(c,token[1]);
2967  c->wires[index]->inputcount = 1;
2968  /* assign outputs to the wire representing gate ouput */
2969  /* NOT USED */
2970  index++;
2971  } else { /* if wire is already defined */
2972  getWireByName(c,token[2])->inputs[0] = getNodeIdByName(c,token[1]); /* find the wire and attach an input to it */
2973  getWireByName(c,token[2])->inputcount = 1;
2974  }
2975 
2976  }
2977 
2978  c->wirecount = index;
2979 
2980  /* c->wires[i]->fanout is the count of gates (and wires), where */
2981  /* this wire is used as an input */
2982  i=0;
2983  while (i<c->wirecount && c->wires[i] != NULL) {
2984  for (j=0; j<c->wires[i]->inputcount; j++) {
2985  (getWireById(c,c->wires[i]->inputs[j])->fanout)++;
2986  /* DEBUGGING */
2987  /*
2988  printf("Increment TTL for wire %d\n",c->wires[i]->inputs[j]);
2989  */
2990  }
2991  i++;
2992  }
2993 
2994  /* DEBUGGING - print summary of the circuit */
2995  /*
2996  printCircuitSummary(c);
2997  */
2998 }
2999 
3008 static void
3009 createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix)
3010 {
3011  unsigned int i,j;
3012  BiddyVerilogWire *w;
3013  Biddy_Edge f;
3014 
3015  /* DEBUGGING */
3016  /*
3017  printf("Creating %d primary inputs\n",c->inputcount);
3018  */
3019 
3020  /* DEBUGGING */
3021  /*
3022  for (i = 0; i < c->inputcount; i++) {
3023  printf("%s ",c->inputs[i]);
3024  }
3025  if (c->inputcount) printf("\n");
3026  */
3027 
3028  /* DEBUGGING */
3029  /*
3030  printf("Creating %d primary outputs\n",c->outputcount);
3031  */
3032 
3033  /* DEBUGGING */
3034  /*
3035  for (i = 0; i < c->outputcount; i++) {
3036  printf("%s ",c->outputs[i]);
3037  }
3038  if (c->outputcount) printf("\n");
3039  */
3040 
3041  /* DEBUGGING */
3042  /*
3043  printf("Creating %d wires\n",c->wirecount);
3044  */
3045 
3046  /* create all BDD variables - important for ZBDD and TZBDD */
3047  for (i = 0; i < c->nodecount; i++) {
3048  if (!strcmp(c->nodes[i]->type,"input")) {
3049  Biddy_Managed_FoaVariable(MNG,c->nodes[i]->name,TRUE); /* TO DO: add prefix */
3050  }
3051  if (!strcmp(c->nodes[i]->type,"extern")) {
3052  Biddy_Managed_FoaVariable(MNG,c->nodes[i]->name,TRUE); /* TO DO: add prefix */
3053  }
3054  }
3055 
3056  /* prepare c->wires[i]->ttl which will be used to guide GC */
3057  for (i = 0; i < c->wirecount; i++) {
3058  c->wires[i]->ttl = 0;
3059  }
3060  for (i = 0; i < c->wirecount; i++) {
3061  for (j = 0; j < c->wires[i]->inputcount; j++) {
3062  w = getWireById(c,c->wires[i]->inputs[j]);
3063  (w->ttl)++;
3064  if (w->ttl == w->fanout) {
3065  w->ttl = i;
3066  }
3067  }
3068  }
3069  for (i = 0; i < c->outputcount; i++) {
3070  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3071  if (w) {
3072  w->ttl = c->wirecount - 1;
3073  }
3074  }
3075  for (i = 0; i < c->wirecount; i++) {
3076  if (c->wires[i]->ttl) c->wires[i]->ttl = c->wires[i]->ttl - i;
3077  }
3078 
3079  for (i = 0; i < c->wirecount; i++) {
3080 
3081  /* REPORT PROGRESS */
3082 
3083  printf("#%d",i);
3084  if (i == c->wirecount-1) printf("\n");
3085 
3086 
3087  /* DEBUGGING */
3088  /*
3089  printf("Creating c->wire[%d], ",i);
3090  printf("ID: %d, ",c->wires[i]->id);
3091  printf("name: %s, ",c->nodes[c->wires[i]->id]->name);
3092  printf("type: %s, ",c->wires[i]->type);
3093  printf("fanout: %d, ",c->wires[i]->fanout);
3094  printf("ttl: %d, ",c->wires[i]->ttl);
3095  printf("Inputs (%d): ",c->wires[i]->inputcount);
3096  if (strcmp(c->wires[i]->type,"I")) {
3097  if (c->wires[i]->inputcount) {
3098  for (j=0;j<c->wires[i]->inputcount;j++) {
3099  printf("%d ",c->wires[i]->inputs[j]);
3100  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3101  printf("ERROR (gate ordering is wrong)");
3102  }
3103  }
3104  } else {
3105  printf("ERROR (wire must be a primary input or it must have some inputs)");
3106  }
3107  } else {
3108  if (c->wires[i]->inputcount) {
3109  printf("ERROR (primary input cannot have additional inputs)");
3110  } else {
3111  printf("/");
3112  }
3113  }
3114  printf("\n");
3115  */
3116 
3117  f = biddyNull;
3118 
3119  if (!strcmp(c->wires[i]->type,"I")) {
3120  if (c->wires[i]->inputcount) {
3121  printf("ERROR (primary input cannot have additional inputs)\n");
3122  } else {
3123  f = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_GetVariable(MNG,c->nodes[c->wires[i]->id]->name)); /* TO DO: add prefix */
3124  }
3125  }
3126  else if (!strcmp(c->wires[i]->type,"M")) {
3127  /* TO DO: this will be used for gates defined by other modules */
3128  }
3129  else {
3130  if (c->wires[i]->inputcount) {
3131  for (j=0; j<c->wires[i]->inputcount; j++) {
3132  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3133  printf("ERROR (gate ordering is wrong)\n");
3134  }
3135  }
3136 
3137  if (!strcmp(c->wires[i]->type,"W")) {
3138  if (c->wires[i]->inputcount == 1) {
3139  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3140  } else {
3141  printf("ERROR (internal wire must have exactly one input)\n");
3142  }
3143  }
3144 
3145  else if (!strcmp(c->wires[i]->type,"buf"))
3146  {
3147  if (c->wires[i]->inputcount != 1) {
3148  printf("ERROR (buf gate must have exactly 1 input)\n");
3149  } else {
3150  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3151  }
3152  }
3153 
3154  else if (!strcmp(c->wires[i]->type,"and"))
3155  {
3156  f = biddyOne;
3157  for (j=0; j<c->wires[i]->inputcount; j++) {
3158  f = Biddy_Managed_And(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3159  }
3160  }
3161 
3162  else if (!strcmp(c->wires[i]->type,"nand"))
3163  {
3164  f = biddyOne;
3165  for (j=0; j<c->wires[i]->inputcount; j++) {
3166  f = Biddy_Managed_And(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3167  }
3168  f = Biddy_Managed_Not(MNG,f);
3169  }
3170 
3171  else if (!strcmp(c->wires[i]->type,"or"))
3172  {
3173  f = biddyZero;
3174  for (j=0; j<c->wires[i]->inputcount; j++) {
3175  f = Biddy_Managed_Or(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3176  }
3177  }
3178 
3179  else if (!strcmp(c->wires[i]->type,"nor"))
3180  {
3181  f = biddyZero;
3182  for (j=0; j<c->wires[i]->inputcount; j++) {
3183  f = Biddy_Managed_Or(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3184  }
3185  f = Biddy_Managed_Not(MNG,f);
3186  }
3187 
3188  else if (!strcmp(c->wires[i]->type,"xor"))
3189  {
3190  if (c->wires[i]->inputcount != 2) {
3191  printf("ERROR (xor gate not having exactly 2 inputs is not supported)\n");
3192  } else {
3193  f = Biddy_Managed_Xor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3194  getWireById(c,c->wires[i]->inputs[1])->bdd);
3195  }
3196  }
3197 
3198  else if (!strcmp(c->wires[i]->type,"xnor"))
3199  {
3200  if (c->wires[i]->inputcount != 2) {
3201  printf("ERROR (xnor gate not having exactly 2 inputs is not supported)\n");
3202  } else {
3203  f = Biddy_Managed_Xor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3204  getWireById(c,c->wires[i]->inputs[1])->bdd);
3205  f = Biddy_Managed_Not(MNG,f);
3206  }
3207  }
3208 
3209  else if (!strcmp(c->wires[i]->type,"not") ||
3210  !strcmp(c->wires[i]->type,"inv"))
3211  {
3212  if (c->wires[i]->inputcount != 1) {
3213  printf("ERROR (not gate must have exactly 1 input)\n");
3214  } else {
3215  f = Biddy_Managed_Not(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd);
3216  }
3217  }
3218 
3219  else {
3220  printf("ERROR (unimplemented type: %s)\n",c->wires[i]->type);
3221  }
3222 
3223  } else {
3224  printf("ERROR (wire must be a primary input or it must have some inputs)\n");
3225  }
3226  }
3227 
3228  c->wires[i]->bdd = f;
3229 
3230  Biddy_Managed_KeepFormulaProlonged(MNG,f,c->wires[i]->ttl);
3231  Biddy_Managed_Clean(MNG);
3232  }
3233 
3234  for (i = 0; i < c->outputcount; i++) {
3235  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3236  if (w) {
3237  f = w->bdd;
3238  } else {
3239  f = biddyZero; /* undefined outputs are represented with biddyZero */
3240  }
3241  Biddy_Managed_AddFormula(MNG,c->outputs[i],f,1); /* TO DO: add prefix */
3242  }
3243  Biddy_Managed_Clean(MNG);
3244 
3245  /*
3246  printf("Report on primary outputs\n");
3247  for (i = 0; i < c->outputcount; i++) {
3248  f = getWireByName(c,c->outputs[i])->bdd;
3249  printf("%s - %d nodes / %d nodes without complement edge\n",
3250  c->outputs[i],
3251  Biddy_Managed_CountNodes(MNG,f),
3252  Biddy_Managed_CountNodesPlain(MNG,f)
3253  );
3254  }
3255  */
3256 
3257 
3258  j = 0;
3259  for (i = 0; i < c->outputcount; i++) {
3260  f = getWireByName(c,c->outputs[i])->bdd;
3261  j = j + Biddy_Managed_CountNodes(MNG,f);
3262  }
3263  printf("The sum of BDD sizes for all outputs: %u\n",j);
3264 
3265 
3266 }
3267 
3272 static void
3273 parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count)
3274 {
3275  int v,v1,v2;
3276  char *sig_vector; /* array to hold tokens for the line */
3277 
3278  sig_vector = strtok(token[*index],":"); /* tokenize the vector to extract vector width */
3279  v1 = atoi(sig_vector); /* starting index for the vector */
3280  sig_vector = strtok(NULL, ":");
3281  v2 = atoi(sig_vector); /* ending index for the vector */
3282  (*index)++; /* get vector name from the next token */
3283  for (v = v2; v <= v1; v++) { /* add the vector signals to the array of signals */
3284  int wordsize = (int) strlen(token[*index]); /* size of the string read from the line */
3285  signal_arr [*count] = (Biddy_String) calloc(wordsize + 1, sizeof(char)); /* allocating memory for signal string */
3286  strcpy(signal_arr [*count], token[*index]); /* add the signal name to the array of signals */
3287  (*count)++; /* update the number of signals in the circuit */
3288  }
3289 }
3290 
3291 static void
3292 printModuleSummary(BiddyVerilogModule *m)
3293 {
3294  unsigned int i;
3295 
3296  printf("************** Module %s statistical results *************\n", m->name);
3297 
3298  printf("Number of primary inputs: %d\n", m->inputcount);
3299  for (i = 0; i < m->inputcount; i++)
3300  printf("%s ", m->inputs[i]);
3301  if (m->inputcount) printf("\n");
3302 
3303  printf("Number of primary outputs: %d\n", m->outputcount);
3304  for (i = 0; i < m->outputcount; i++)
3305  printf("%s ", m->outputs[i]);
3306  if ( m->outputcount) printf("\n");
3307 
3308  printf("Number of gates: %d\n", m->gatecount);
3309  for (i = 0; i < m->gatecount; i++)
3310  printf("%s ", m->gates[i]);
3311  if (m->gatecount) printf("\n");
3312 
3313  printf("Number of wires: %d\n", m->wirecount);
3314  for (i = 0; i < m->wirecount; i++)
3315  printf("%s ", m->wires[i]);
3316  if (m->wirecount) printf("\n");
3317 
3318  printf("Number of regs: %d\n", m->regcount);
3319  for (i = 0; i < m->regcount; i++)
3320  printf("%s ", m->regs[i]);
3321  if (m->regcount) printf("\n");
3322 
3323  printf("*************************** END **************************\n");
3324 }
3325 
3330 static void
3331 printCircuitSummary(BiddyVerilogCircuit *c)
3332 {
3333  unsigned int i,j;
3334 
3335  printf("************** Circuit %s statistical results *************\n", c->name);
3336 
3337  printf("Circuit size: %d\n", c->nodecount);
3338 
3339  printf("Number of primary inputs: %d\n", c->inputcount);
3340  for (i = 0; i < c->inputcount; i++)
3341  printf("%s ", c->inputs[i]);
3342  if (c->inputcount) printf("\n");
3343 
3344  printf("Number of primary outputs: %d\n", c->outputcount);
3345  for (i = 0; i < c->outputcount; i++)
3346  printf("%s ", c->outputs[i]);
3347  if (c->outputcount) printf("\n");
3348 
3349  i=0;
3350  while (i<c->wirecount && c->wires[i] != NULL) {
3351  printf ("c->wire[%d]->type: %s, ",i, c->wires[i]->type);
3352  printf ("ID: %d, ", c->wires[i]->id);
3353  printf ("name: %s, ", c->nodes[c->wires[i]->id]->name);
3354 
3355  printf ("\nInputs (%d): ", c->wires[i]->inputcount); /* wire inputs */
3356  for (j=0; j<c->wires[i]->inputcount; j++)
3357  printf ("%d ",c->wires[i]->inputs[j]);
3358 
3359  printf ("\nOutputs (%d): ", c->wires[i]->outputcount); /* wire outputs */
3360  for (j=0; j<c->wires[i]->outputcount; j++)
3361  printf ("%d ",c->wires[i]->outputs[j]);
3362 
3363  i++;
3364  printf ("\n");
3365  }
3366 
3367  printf("*************************** END **************************\n");
3368 }
3369 
3375 static Biddy_Boolean
3376 isGate(Biddy_String word)
3377 {
3378  int i;
3379  for (i = 0; i < GATESNUM; i++)
3380  if (strcmp(word,VerilogFileGateName[i]) == 0)
3381  return TRUE;
3382  return FALSE;
3383 }
3384 
3390 static Biddy_Boolean
3391 isSignalVector(Biddy_String word)
3392 {
3393  unsigned int i;
3394  for (i = 0; i < strlen(word); i++)
3395  if (word[i] == ':')
3396  return TRUE;
3397  return FALSE;
3398 }
3399 
3405 static Biddy_Boolean
3406 isEndOfLine(Biddy_String source)
3407 {
3408  Biddy_String pchar = strchr(source, ';');
3409  return (pchar == NULL) ? FALSE : TRUE;
3410 }
3411 
3417 static Biddy_Boolean
3418 isDefined(BiddyVerilogCircuit *c, Biddy_String name)
3419 {
3420  unsigned int i;
3421  for (i=0; (i < c->wirecount) && c->wires[i]; i++) {
3422  if (strcmp(c->nodes[c->wires[i]->id]->name, name) == 0) return TRUE;
3423  }
3424  return FALSE;
3425 }
3426 
3431 static void
3432 buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name)
3433 {
3434  n->type = strdup(type);
3435  n->name = strdup(name);
3436 }
3437 
3442 static void
3443 buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name)
3444 {
3445  int id;
3446 
3447  /* TO DO: check if wire with the same name does not already exists */
3448 
3449  if ((id = getNodeIdByName(c,name)) == -1) {
3450  printf("ERROR (buildWire): node %s does not exists!\n",name);
3451  exit(1);
3452  }
3453  w->id = id; /* wire ID */
3454  w->type = strdup(type); /* wire type */
3455  w->inputcount = 0; /* initial number of inputs */
3456  w->outputcount = 0; /* initial number of outputs */
3457  w->fanout = 0;
3458  w->ttl = 0;
3459  w->bdd = biddyNull;
3460 
3461  /* DEBUGGING */
3462  /*
3463  printf("Creating wire: id: %d, type: %s\n", w->id, w->type);
3464  */
3465 }
3466 
3472 static int
3473 getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name)
3474 {
3475  unsigned int i;
3476  if (strcmp(name,c->nodes[c->nodecount-1]->name) == 0) return (int) c->nodecount-1;
3477  for (i=0; i < c->nodecount; i++) {
3478  if (strcmp(name,c->nodes[i]->name) == 0) return (int) i;
3479  }
3480  return -1;
3481 }
3482 
3488 static BiddyVerilogWire *
3489 getWireById(BiddyVerilogCircuit *c, int id)
3490 {
3491  unsigned int i;
3492  for (i=0; i < c->wirecount; i++) {
3493  if (c->wires[i]->id == id) return c->wires[i];
3494  }
3495  return NULL;
3496 }
3497 
3503 static BiddyVerilogWire *
3504 getWireByName(BiddyVerilogCircuit *c, Biddy_String name)
3505 {
3506  unsigned int i;
3507  for (i=0; i < c->wirecount; i++) {
3508  if (strcmp(name, c->nodes[c->wires[i]->id]->name) == 0) return c->wires[i];
3509  }
3510  return NULL;
3511 }
3512 
3517 static Biddy_String
3518 trim(Biddy_String source)
3519 {
3520  unsigned int sr_length;
3521 
3522  sr_length = (unsigned int) strlen(source);
3523  while (sr_length && ((source[sr_length-1] == ' ') ||
3524  (source[sr_length-1] == '\t') ||
3525  (source[sr_length-1] == 10) ||
3526  (source[sr_length-1] == 13)))
3527  {
3528  source[sr_length-1] = 0;
3529  sr_length = (unsigned int) strlen(source);
3530  }
3531 
3532  return source;
3533 }
3534 
3535 static void
3536 concat(char **s1, const char *s2)
3537 {
3538  if (s2) {
3539  *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1+1);
3540  strcat(*s1," ");
3541  strcat(*s1,s2);
3542  }
3543 }
3544 
3545 static void
3546 WriteBDD(Biddy_Manager MNG, Biddy_Edge f)
3547 {
3548  Biddy_Variable v;
3549  Biddy_String var;
3550 
3551  if (Biddy_GetMark(f)) {
3552  printf("*");
3553  }
3554  if ((v = Biddy_GetTag(f))) {
3555  printf("<%s>",Biddy_Managed_GetVariableName(MNG,v));
3556  }
3557 
3558  var = Biddy_Managed_GetTopVariableName(MNG,f);
3559  printf("%s",var);
3560 
3561  if (!Biddy_IsTerminal(f)) {
3562  printf("(");
3563  WriteBDD(MNG,BiddyE(f));
3564  printf(")(");
3565  WriteBDD(MNG,BiddyT(f));
3566  printf(")");
3567  }
3568 }
3569 
3570 static void
3571 WriteBDDx(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f, unsigned int *line)
3572 {
3573  Biddy_String var;
3574 
3575  if (Biddy_GetMark(f)) {
3576  fprintf(funfile,"* ");
3577  }
3578 
3579  *line = *line + 2;
3580 
3581  var = Biddy_Managed_GetTopVariableName(MNG,f);
3582  fprintf(funfile,"%s",var);
3583 
3584  *line = *line + (unsigned int)strlen(var);
3585 
3586  if (!Biddy_IsTerminal(f)) {
3587  if (*line >= 80) {
3588  fprintf(funfile,"\n");
3589  *line = 0;
3590  }
3591  fprintf(funfile," (");
3592  *line = *line + 2;
3593  WriteBDDx(MNG,funfile,BiddyE(f),line);
3594  if (*line >= 80) {
3595  fprintf(funfile,"\n");
3596  *line = 0;
3597  }
3598  fprintf(funfile,") (");
3599  *line = *line + 3;
3600  WriteBDDx(MNG,funfile,BiddyT(f),line);
3601  if (*line >= 80) {
3602  fprintf(funfile,"\n");
3603  *line = 0;
3604  }
3605  fprintf(funfile,")");
3606  *line = *line + 1;
3607  }
3608 }
3609 
3610 static Biddy_Boolean
3611 WriteProduct(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
3612 {
3613  /* DEBUGGING */
3614  /*
3615  typedef struct LIMIT {
3616  unsigned int part;
3617  unsigned int w;
3618  } LIMIT;
3619  void *data;
3620  */
3621 
3622  /* ITERATIVE VARIANT */
3623  /* LITERALS ARE ADDED IN REVERSE ORDERING */
3624  /*
3625  while (l) {
3626  if (combinationset) {
3627  if (!l->negative) {
3628  if (first) first = FALSE; else printf(",");
3629  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3630  } else {
3631  printf(" ");
3632  if (l->negative) {
3633  printf("*");
3634  }
3635  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3636  }
3637  l = l->next;
3638  }
3639  */
3640 
3641  /* RECURSIVE VARIANT */
3642  /* LITERALS ARE ADDED IN REVERSE ORDERING BUT THIS WILL REVERSE THE OUTPUT */
3643 
3644  if (l) {
3645  if (combinationset) {
3646  first = WriteProduct(MNG,l->next,combinationset,first);
3647  if (!l->negative) {
3648  if (first) first = FALSE; else printf(" ");
3649  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3650 
3651  /* DEBUGGING */
3652  /*
3653  if ((data = Biddy_Managed_GetVariableData(MNG,l->v))) {
3654  printf("<%u>",((LIMIT *) data)->w);
3655  }
3656  */
3657 
3658  }
3659  } else {
3660  WriteProduct(MNG,l->next,combinationset,first);
3661  printf(" ");
3662  if (l->negative) {
3663  printf("*");
3664  }
3665  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3666  }
3667  }
3668 
3669 
3670  return first;
3671 }
3672 
3673 static Biddy_Boolean
3674 WriteProductx(Biddy_Manager MNG, FILE *s, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
3675 {
3676  if (l) {
3677  if (combinationset) {
3678  first = WriteProductx(MNG,s,l->next,combinationset,first);
3679  if (!l->negative) {
3680  if (!first) fprintf(s,","); else first = FALSE;
3681  fprintf(s,"%s",Biddy_Managed_GetVariableName(MNG,l->v));
3682  }
3683  } else {
3684  WriteProductx(MNG,s,l->next,combinationset,first);
3685  fprintf(s," ");
3686  if (l->negative) {
3687  fprintf(s,"*");
3688  }
3689  fprintf(s,"%s",Biddy_Managed_GetVariableName(MNG,l->v));
3690  }
3691  }
3692  return first;
3693 }
3694 
3695 static void
3696 WriteProductAlphabetic(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
3697 {
3698  BiddyVarList *tmp;
3699  Biddy_String tmpname,minname,prevname;
3700 
3701  if (l) {
3702  if (combinationset) {
3703  prevname = NULL;
3704  do {
3705  tmp = l;
3706  minname = NULL;
3707  while (tmp) {
3708  if (!tmp->negative) {
3709  tmpname = Biddy_Managed_GetVariableName(MNG,tmp->v);
3710  if ((!minname || (strcmp(tmpname,minname)<0)) && (!prevname || (strcmp(tmpname,prevname)>0))) {
3711  minname = tmpname;
3712  }
3713  }
3714  tmp = tmp->next;
3715  }
3716  if (minname) {
3717  if (!first) printf(","); else first = FALSE;
3718  printf("%s",minname);
3719  prevname = minname;
3720  }
3721  } while (minname);
3722  } else {
3723  /* NOT IMPLEMENTED, YET */
3724  }
3725  }
3726 }
3727 
3728 static void
3729 WriteSOP(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable top,
3730  Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize,
3731  Biddy_Boolean combinationset)
3732 {
3733  BiddyVarList tmp;
3734  Biddy_Variable v;
3735 
3736  /* parameter combinationset is meaningful for ZBDDs and TZBDDs, only */
3737 
3738  if ((!combinationset) && (*maxsize == 0)) return; /* SOP to large */
3739 
3740  v = BiddyV(f);
3741 
3742  /* DEBUGGING */
3743  /*
3744  printf("WriteSOP: top = %u (%s), v = %u (%s)\n",top,Biddy_Managed_GetVariableName(MNG,top),v,Biddy_Managed_GetVariableName(MNG,v));
3745  */
3746 
3747  assert( !(BiddyIsSmaller(BiddyV(f),top)) );
3748 
3749  if ((top != v) && (f != biddyZero)) {
3750 
3751  if (biddyManagerType == BIDDYTYPEOBDD) {
3752  /* NO ACTION IS NEEDED */
3753  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3754  /* NO ACTION IS NEEDED */
3755  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3756  tmp.next = l;
3757  tmp.v = top;
3758  tmp.negative = TRUE; /* negative literal */
3759  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3760  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3761  tmp.next = l;
3762  tmp.v = top;
3763  tmp.negative = TRUE; /* negative literal */
3764  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3765  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3766  tmp.next = l;
3767  tmp.v = top;
3768  tmp.negative = TRUE; /* negative literal */
3769  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3770  if (combinationset && Biddy_Managed_IsSmaller(MNG,top,Biddy_GetTag(f))) {
3771  tmp.negative = FALSE; /* positive literal */
3772  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3773  }
3774  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3775  {
3776  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3777  return;
3778  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
3779  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
3780  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
3781  {
3782  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3783  return;
3784  } else {
3785  fprintf(stderr,"WriteSOP: Unsupported BDD type!\n");
3786  return;
3787  }
3788 
3789  } else if (v == 0) {
3790 
3791  if (combinationset) {
3792  if (!mark) {
3793  if (l) {
3794  /* printf("{"); */
3795  /* WriteProductAlphabetic(MNG,l,combinationset,TRUE); */
3796  WriteProduct(MNG,l,combinationset,TRUE);
3797  /* printf("}"); */
3798  printf(" ; ");
3799  (*maxsize)--;
3800  } else {
3801  /* printf("{}"); */
3802  printf(",");
3803  }
3804  } else {
3805  if (!l) {
3806  printf("EMPTY");
3807  }
3808  }
3809  } else {
3810  if (!mark) {
3811  printf(" + ");
3812  if (l) {
3813  WriteProduct(MNG,l,combinationset,TRUE);
3814  printf("\n");
3815  (*maxsize)--;
3816  } else {
3817  printf(" 1");
3818  }
3819  } else {
3820  if (!l) {
3821  printf(" + 0");
3822  }
3823  }
3824  }
3825 
3826  } else {
3827 
3828  tmp.next = l;
3829  tmp.v = v;
3830 
3831  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3832  tmp.negative = TRUE; /* left successor */
3833  WriteSOP(MNG,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3834  }
3835  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3836  if (combinationset) {
3837  tmp.negative = FALSE; /* right successor for combination sets */
3838  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3839  } else {
3840  tmp.negative = TRUE; /* left successor for Boolean function */
3841  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3842  }
3843  }
3844  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3845  if (combinationset) {
3846  tmp.negative = FALSE; /* right successor for combination sets */
3847  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3848  } else {
3849  tmp.negative = TRUE; /* left successor for Boolean function */
3850  WriteSOP(MNG,BiddyE(f),Biddy_GetTag(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3851  }
3852  }
3853 
3854  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3855  tmp.negative = FALSE; /* right successor */
3856  WriteSOP(MNG,BiddyT(f),BiddyV(BiddyT(f)),(mark ^ Biddy_GetMark(BiddyT(f))),&tmp,maxsize,combinationset);
3857  }
3858  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3859  if (combinationset) {
3860  tmp.negative = TRUE; /* left successor for combination sets */
3861  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3862  } else {
3863  tmp.negative = FALSE; /* right successor for Boolean function */
3864  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3865  }
3866  }
3867  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3868  if (combinationset) {
3869  tmp.negative = TRUE; /* left successor for combination sets */
3870  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3871  } else {
3872  tmp.negative = FALSE; /* right successor for Boolean function */
3873  WriteSOP(MNG,BiddyT(f),Biddy_GetTag(BiddyT(f)),Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3874  }
3875  }
3876 
3877  }
3878 }
3879 
3880 static void
3881 WriteSOPx(Biddy_Manager MNG, FILE *s, Biddy_Edge f, Biddy_Variable top,
3882  Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize,
3883  Biddy_Boolean combinationset)
3884 {
3885  BiddyVarList tmp;
3886  Biddy_Variable v;
3887 
3888  if ((!combinationset) && (*maxsize == 0)) return; /* SOP to large */
3889 
3890  v = BiddyV(f);
3891 
3892  /* DEBUGGING */
3893  /*
3894  printf("WriteSOPx: top = %u (%s), v = %u (%s)\n",top,Biddy_Managed_GetVariableName(MNG,top),v,Biddy_Managed_GetVariableName(MNG,v));
3895  */
3896 
3897  assert( !(BiddyIsSmaller(BiddyV(f),top)) );
3898 
3899  if ((top != v) && (f != biddyZero)) {
3900 
3901  if (biddyManagerType == BIDDYTYPEOBDD) {
3902  /* IMPLEMENTED */
3903  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3904  /* IMPLEMENTED */
3905  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3906  /* IMPLEMENTED */
3907  tmp.next = l;
3908  tmp.v = top;
3909  tmp.negative = TRUE; /* left successor */
3910  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3911  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3912  /* IMPLEMENTED */
3913  tmp.next = l;
3914  tmp.v = top;
3915  tmp.negative = TRUE; /* left successor */
3916  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3917  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3918  /* IMPLEMENTED */
3919  tmp.next = l;
3920  tmp.v = top;
3921  tmp.negative = TRUE; /* left successor */
3922  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3923  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3924  {
3925  fprintf(stderr,"WriteSOPx: this BDD type is not supported, yet!\n");
3926  return;
3927  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
3928  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
3929  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
3930  {
3931  fprintf(stderr,"WriteSOPx: this BDD type is not supported, yet!\n");
3932  return;
3933  } else {
3934  fprintf(stderr,"WriteSOPx: Unsupported BDD type!\n");
3935  return;
3936  }
3937 
3938  } else if (v == 0) {
3939 
3940  if (combinationset) {
3941  } else {
3942  if (!mark) {
3943  fprintf(s," + ");
3944  if (l) {
3945  WriteProductx(MNG,s,l,combinationset,TRUE);
3946  fprintf(s,"\n");
3947  (*maxsize)--;
3948  } else {
3949  fprintf(s," 1");
3950  }
3951  } else {
3952  if (!l) {
3953  fprintf(s," + 0");
3954  }
3955  }
3956  }
3957 
3958  } else {
3959 
3960  tmp.next = l;
3961  tmp.v = v;
3962  tmp.negative = TRUE; /* left successor */
3963 
3964  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3965  WriteSOPx(MNG,s,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3966  }
3967  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3968  WriteSOPx(MNG,s,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3969  }
3970  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3971  WriteSOPx(MNG,s,BiddyE(f),Biddy_GetTag(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3972  }
3973 
3974  tmp.negative = FALSE; /* right successor */
3975 
3976  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3977  WriteSOPx(MNG,s,BiddyT(f),BiddyV(BiddyT(f)),(mark ^ Biddy_GetMark(BiddyT(f))),&tmp,maxsize,combinationset);
3978  }
3979  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3980  WriteSOPx(MNG,s,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3981  }
3982  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3983  WriteSOPx(MNG,s,BiddyT(f),Biddy_GetTag(BiddyT(f)),Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3984  }
3985 
3986  }
3987 }
3988 
3989 static unsigned int
3990 enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n)
3991 {
3992  if (!Biddy_Managed_IsSelected(MNG,f)) {
3993  if (Biddy_IsTerminal(f)) {
3994  } else {
3995  Biddy_Managed_SelectNode(MNG,f);
3996  n++;
3997  BiddySetEnumerator(f,n);
3998 
3999  /* one or both are terminal node */
4000  /* every instance of terminal node is enumerated */
4001  if (Biddy_IsTerminal(BiddyE(f)) || Biddy_IsTerminal(BiddyT(f))) {
4002 
4003  if (((biddyManagerType == BIDDYTYPEOBDD) ||
4004  (biddyManagerType == BIDDYTYPEZBDD) ||
4005  (biddyManagerType == BIDDYTYPETZBDD)
4006  ) && (Biddy_GetMark(BiddyE(f)) != Biddy_GetMark(BiddyT(f))))
4007  {
4008  /* two terminal nodes only if complemented edges are not used and they are different */
4009  if (Biddy_IsTerminal(BiddyE(f))) {
4010  n++;
4011  }
4012  if (Biddy_IsTerminal(BiddyT(f))) {
4013  n++;
4014  }
4015  }
4016  else {
4017  /* only one terminal node */
4018  n++;
4019  }
4020 
4021  }
4022 
4023  if (!Biddy_IsTerminal(BiddyE(f))) {
4024  n = enumerateNodes(MNG,BiddyE(f),n);
4025  }
4026  if (!Biddy_IsTerminal(BiddyT(f))) {
4027  n = enumerateNodes(MNG,BiddyT(f),n);
4028  }
4029  }
4030  }
4031  return n;
4032 }
4033 
4034 static void
4035 WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd)
4036 {
4037  BiddyLocalInfo *li;
4038  Biddy_String name,hash;
4039  Biddy_Variable v;
4040  BiddyLocalInfo *li2;
4041 
4042  if (Biddy_IsTerminal(f)) {
4043  if (cudd) {
4044 
4045  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
4046  /*
4047  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
4048  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
4049  fprintf(dotfile,"\"%p\";\n",biddyOne);
4050  */
4051 
4052  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
4053 
4054  fprintf(dotfile,"{ \"CONST NODES\";\n");
4055  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
4056  fprintf(dotfile,"\"1\";\n");
4057 
4058 
4059  fprintf(dotfile,"}\n}\n");
4060  } else {
4061  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4062  (biddyManagerType == BIDDYTYPEZBDD) ||
4063  (biddyManagerType == BIDDYTYPETZBDD))
4064  {
4065  if (f == biddyZero) {
4066  fprintf(dotfile, " node [shape = none, label = \"0\"] %u;\n",1);
4067  } else {
4068  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
4069  }
4070  }
4071  else {
4072  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
4073  }
4074  }
4075  return;
4076  }
4077  if (cudd) {
4079  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4080  while (li->back) {
4081  v = BiddyV(li->back);
4082  if (biddyVariableTable.table[v].value == biddyZero) {
4083  biddyVariableTable.table[v].value = biddyOne;
4084  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
4085  while ((hash = strchr(name,'#'))) hash[0] = '_';
4086  fprintf(dotfile,"{ rank = same; ");
4087  fprintf(dotfile,"\" %s \";\n",name);
4088  free(name);
4089  li2 = li;
4090  while (li2->back) {
4091  if (BiddyV(li2->back) == v) {
4092  fprintf(dotfile,"\"%p\";\n",li2->back);
4093  }
4094  li2 = &li2[1]; /* next field in the array */
4095  }
4096  fprintf(dotfile,"}\n");
4097  }
4098  li = &li[1]; /* next field in the array */
4099  }
4101 
4102  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
4103  /*
4104  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
4105  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
4106  fprintf(dotfile,"\"%p\";\n",biddyOne);
4107  */
4108 
4109  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
4110 
4111  fprintf(dotfile,"{ \"CONST NODES\";\n");
4112  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
4113  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4114  while (li->back) {
4115  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
4116  fprintf(dotfile,"\"%u\";\n",li->data.enumerator+1);
4117  }
4118  li = &li[1];
4119  }
4120 
4121 
4122  fprintf(dotfile,"}\n}\n");
4123  } else {
4124  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4125  while (li->back) {
4126  if (id == -1) {
4127  name = getname(MNG,li->back);
4128  } else {
4129  name = getshortname(MNG,li->back,id);
4130  }
4131  while ((hash = strchr(name,'#'))) hash[0] = '_';
4132  fprintf(dotfile," node [shape = circle, label = \"%s\"] %u;\n",name,li->data.enumerator);
4133  free(name);
4134  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4135  (biddyManagerType == BIDDYTYPEZBDD) ||
4136  (biddyManagerType == BIDDYTYPETZBDD))
4137  {
4138  if (BiddyE(li->back) == biddyZero) {
4139  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
4140  }
4141  else if (Biddy_IsTerminal(BiddyE(li->back))) {
4142  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4143  }
4144  if (BiddyT(li->back) == biddyZero) {
4145  if (Biddy_IsTerminal(BiddyE(li->back)) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back)))) {
4146  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+2);
4147  } else {
4148  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
4149  }
4150  }
4151  else if (Biddy_IsTerminal(BiddyT(li->back))) {
4152  if (Biddy_IsTerminal(BiddyE(li->back)) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back)))) {
4153  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+2);
4154  } else {
4155  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4156  }
4157  }
4158  }
4159  else {
4160  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
4161  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4162  }
4163  }
4164  li = &li[1]; /* next field in the array */
4165  }
4166  }
4167 }
4168 
4169 static void
4170 WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd)
4171 {
4172  unsigned int n1,n2;
4173  Biddy_Variable tag;
4174 
4175  if (!Biddy_IsTerminal(f) && !Biddy_Managed_IsSelected(MNG,f)) {
4176  Biddy_Managed_SelectNode(MNG,f);
4177  n1 = BiddyGetEnumerator(f);
4178 
4179  if (Biddy_IsTerminal(BiddyE(f))) {
4180  n2 = n1 + 1;
4181  } else {
4182  n2 = BiddyGetEnumerator(BiddyE(f));
4183  }
4184  if (Biddy_GetMark(BiddyE(f))) {
4185  if ((BiddyE(f) != biddyZero) && (tag = Biddy_GetTag(BiddyE(f)))) {
4186  if (cudd) {
4187 
4188  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4189  /*
4190  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4191  */
4192 
4193  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4194 
4195  if (Biddy_IsTerminal(BiddyE(f))) {
4196  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4197  } else {
4198  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4199  }
4200 
4201 
4202  } else {
4203 #ifdef LEGACY_DOT
4204  fprintf(dotfile," %u -> %u [style=dotted label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4205 #else
4206  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4207 #endif
4208  }
4209  } else {
4210  if (cudd) {
4211 
4212  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4213  /*
4214  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
4215  */
4216 
4217  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4218 
4219  if (Biddy_IsTerminal(BiddyE(f))) {
4220  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted];\n",BiddyP(f),n2);
4221  } else {
4222  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
4223  }
4224 
4225 
4226  } else {
4227  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4228  (biddyManagerType == BIDDYTYPEZBDD) ||
4229  (biddyManagerType == BIDDYTYPETZBDD))
4230  {
4231 #ifdef LEGACY_DOT
4232  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
4233 #else
4234  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
4235 #endif
4236  }
4237  else {
4238 #ifdef LEGACY_DOT
4239  fprintf(dotfile," %u -> %u [style=dotted];\n",n1,n2);
4240 #else
4241  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\"];\n",n1,n2);
4242 #endif
4243  }
4244  }
4245  }
4246  } else {
4247  if ((BiddyE(f) != biddyZero) && (tag = Biddy_GetTag(BiddyE(f)))) {
4248  if (cudd) {
4249 
4250  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4251  /*
4252  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4253  */
4254 
4255  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4256 
4257  if (Biddy_IsTerminal(BiddyE(f))) {
4258  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4259  } else {
4260  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4261  }
4262 
4263 
4264  } else {
4265 #ifdef LEGACY_DOT
4266  fprintf(dotfile," %u -> %u [style=dashed label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4267 #else
4268  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4269 #endif
4270  }
4271  } else {
4272  if (cudd) {
4273 
4274  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4275  /*
4276  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
4277  */
4278 
4279  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4280 
4281  if (Biddy_IsTerminal(BiddyE(f))) {
4282  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed];\n",BiddyP(f),n2);
4283  } else {
4284  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
4285  }
4286 
4287 
4288  } else {
4289 #ifdef LEGACY_DOT
4290  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
4291 #else
4292  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
4293 #endif
4294  }
4295  }
4296  }
4297 
4298  if (Biddy_IsTerminal(BiddyT(f))) {
4299  if (((biddyManagerType == BIDDYTYPEOBDD) ||
4300  (biddyManagerType == BIDDYTYPEZBDD) ||
4301  (biddyManagerType == BIDDYTYPETZBDD))
4302  && (Biddy_IsTerminal(BiddyE(f)))
4303  && (Biddy_GetMark(BiddyE(f)) != Biddy_GetMark(BiddyT(f))))
4304  {
4305  n2 = n1 + 2;
4306  }
4307  else {
4308  n2 = n1 + 1;
4309  }
4310  } else {
4311  n2 = BiddyGetEnumerator(BiddyT(f));
4312  }
4313  if (Biddy_GetMark(BiddyT(f))) {
4314  if ((BiddyT(f) != biddyZero) && (tag = Biddy_GetTag(BiddyT(f)))) {
4315  if (cudd) {
4316 
4317  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4318  /*
4319  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4320  */
4321 
4322  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4323 
4324  if (Biddy_IsTerminal(BiddyT(f))) {
4325  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4326  } else {
4327  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4328  }
4329 
4330 
4331  } else {
4332 #ifdef LEGACY_DOT
4333  fprintf(dotfile," %d -> %d [style=bold label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4334 #else
4335  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4336 #endif
4337  }
4338  } else {
4339  if (cudd) {
4340 
4341  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4342  /*
4343  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
4344  */
4345 
4346  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4347 
4348  if (Biddy_IsTerminal(BiddyT(f))) {
4349  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold];\n",BiddyP(f),n2);
4350  } else {
4351  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
4352  }
4353 
4354 
4355  } else {
4356  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4357  (biddyManagerType == BIDDYTYPEZBDD) ||
4358  (biddyManagerType == BIDDYTYPETZBDD))
4359  {
4360 #ifdef LEGACY_DOT
4361  fprintf(dotfile," %d -> %d;\n",n1,n2);
4362 #else
4363  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
4364 #endif
4365  }
4366  else {
4367 #ifdef LEGACY_DOT
4368  fprintf(dotfile," %d -> %d [style=bold];\n",n1,n2);
4369 #else
4370  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\"];\n",n1,n2);
4371 #endif
4372  }
4373  }
4374  }
4375  } else {
4376  if ((BiddyT(f) != biddyZero) && (tag = Biddy_GetTag(BiddyT(f)))) {
4377  if (cudd) {
4378 
4379  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4380  /*
4381  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4382  */
4383 
4384  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4385 
4386  if (Biddy_IsTerminal(BiddyT(f))) {
4387  fprintf(dotfile,"\"%p\" -> \"%u\" [label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4388  } else {
4389  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4390  }
4391 
4392 
4393  } else {
4394 #ifdef LEGACY_DOT
4395  fprintf(dotfile," %d -> %d [label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4396 #else
4397  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4398 #endif
4399  }
4400  } else {
4401  if (cudd) {
4402 
4403  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4404  /*
4405  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
4406  */
4407  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4408 
4409 
4410  if (Biddy_IsTerminal(BiddyT(f))) {
4411  fprintf(dotfile,"\"%p\" -> \"%u\";\n",BiddyP(f),n2);
4412  } else {
4413  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
4414  }
4415 
4416 
4417  } else {
4418 #ifdef LEGACY_DOT
4419  fprintf(dotfile," %d -> %d [style=solid];\n",n1,n2);
4420 #else
4421  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
4422 #endif
4423  }
4424  }
4425  }
4426 
4427  WriteDotEdges(MNG,dotfile,BiddyE(f),cudd);
4428  WriteDotEdges(MNG,dotfile,BiddyT(f),cudd);
4429  }
4430 }
4431 
4432 static void
4433 WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f)
4434 {
4435  int n1,n2;
4436  Biddy_Variable tag1,tag2;
4437 
4438  if (!Biddy_IsTerminal(f) && !Biddy_Managed_IsSelected(MNG,f)) {
4439  Biddy_Managed_SelectNode(MNG,f);
4440  n1 = BiddyGetEnumerator(f);
4441 
4442  /* if successors are equal then double line is possible */
4443  if ((BiddyP(BiddyE(f)) != BiddyP(BiddyT(f))) ||
4444  (((biddyManagerType == BIDDYTYPEOBDD) ||
4445  (biddyManagerType == BIDDYTYPEZBDD) ||
4446  (biddyManagerType == BIDDYTYPETZBDD))
4447  &&
4448  (Biddy_GetMark((BiddyE(f))) != Biddy_GetMark((BiddyT(f)))))
4449  )
4450  {
4451 
4452  unsigned int num;
4453 
4454  /* SINGLE LINE */
4455 
4456  num = 0;
4457  if (Biddy_IsTerminal(BiddyE(f))) {
4458  n2 = n1 + 1;
4459  num = 1;
4460  } else {
4461  n2 = BiddyGetEnumerator(BiddyE(f));
4462  }
4463  fprintf(funfile,"connect %d %d ",n1,n2);
4464  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4465  (biddyManagerType == BIDDYTYPEZBDD) ||
4466  (biddyManagerType == BIDDYTYPETZBDD))
4467  {
4468  fprintf(funfile,"l");
4469  }
4470  else {
4471  if (Biddy_GetMark((BiddyE(f)))) {
4472  fprintf(funfile,"li");
4473  } else {
4474  fprintf(funfile,"l");
4475  }
4476  }
4477  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4478  {
4479  if (BiddyE(f) == biddyZero) {
4480  fprintf(funfile," 0\n");
4481  } else {
4482  tag1 = Biddy_GetTag(BiddyE(f));
4483  fprintf(funfile," %s\n",Biddy_Managed_GetVariableName(MNG,tag1));
4484  }
4485  } else {
4486  fprintf(funfile,"\n");
4487  }
4488 
4489  if (Biddy_IsTerminal(BiddyT(f))) {
4490  n2 = n1 + num + 1;
4491  } else {
4492  n2 = BiddyGetEnumerator(BiddyT(f));
4493  }
4494  fprintf(funfile,"connect %d %d ",n1,n2);
4495  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4496  (biddyManagerType == BIDDYTYPEZBDD) ||
4497  (biddyManagerType == BIDDYTYPETZBDD))
4498  {
4499  fprintf(funfile,"r");
4500  }
4501  else {
4502  if (Biddy_GetMark((BiddyT(f)))) {
4503  fprintf(funfile,"ri");
4504  } else {
4505  fprintf(funfile,"r");
4506  }
4507  }
4508  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4509  {
4510  if (BiddyT(f) == biddyZero) {
4511  fprintf(funfile," 0\n");
4512  } else {
4513  tag2 = Biddy_GetTag(BiddyT(f));
4514  fprintf(funfile," %s\n",Biddy_Managed_GetVariableName(MNG,tag2));
4515  }
4516  } else {
4517  fprintf(funfile,"\n");
4518  }
4519 
4520  } else {
4521 
4522  /* DOUBLE LINE */
4523 
4524  if (Biddy_IsTerminal(BiddyE(f))) {
4525  n2 = n1 + 1;
4526  } else {
4527  n2 = BiddyGetEnumerator(BiddyE(f));
4528  }
4529 
4530  fprintf(funfile,"connect %d %d ",n1,n2);
4531  if (Biddy_GetMark((BiddyE(f)))) {
4532  if (Biddy_GetMark((BiddyT(f)))) {
4533  fprintf(funfile,"ei");
4534  } else {
4535  fprintf(funfile,"d");
4536  }
4537  } else {
4538  if (Biddy_GetMark((BiddyT(f)))) {
4539  fprintf(funfile,"di");
4540  } else {
4541  fprintf(funfile,"e");
4542  }
4543  }
4544  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4545  {
4546  tag1 = Biddy_GetTag(BiddyE(f));
4547  tag2 = Biddy_GetTag(BiddyT(f));
4548  fprintf(funfile," %s %s\n",Biddy_Managed_GetVariableName(MNG,tag1),Biddy_Managed_GetVariableName(MNG,tag2));
4549  } else {
4550  fprintf(funfile,"\n");
4551  }
4552 
4553  }
4554 
4555  WriteBddviewConnections(MNG,funfile,BiddyE(f));
4556  WriteBddviewConnections(MNG,funfile,BiddyT(f));
4557  }
4558 }
4559 
4560 static Biddy_String
4561 getname(Biddy_Manager MNG, void *p)
4562 {
4563  unsigned int i;
4564  Biddy_String newname;
4565 
4566  if ((p == biddyZero) &&
4567  ((biddyManagerType == BIDDYTYPEOBDD) ||
4568  (biddyManagerType == BIDDYTYPEZBDD) ||
4569  (biddyManagerType == BIDDYTYPETZBDD)))
4570  {
4571  newname = strdup("0");
4572  return (newname);
4573  }
4574 
4575  newname = strdup(Biddy_Managed_GetTopVariableName(MNG,(Biddy_Edge) p));
4576  for (i=0; i<strlen(newname); ++i) {
4577  if (newname[i] == '<') newname[i] = '_';
4578  if (newname[i] == '>') newname[i] = 0;
4579  }
4580 
4581  return (newname);
4582 }
4583 
4584 static Biddy_String
4585 getshortname(Biddy_Manager MNG, void *p, int n)
4586 {
4587  unsigned int i;
4588  Biddy_String name;
4589  Biddy_String shortname;
4590 
4591  name = strdup(Biddy_Managed_GetTopVariableName(MNG,(Biddy_Edge) p));
4592  i = (unsigned int)strcspn(name,"<");
4593  name[i]=0;
4594  shortname = strdup(name);
4595  free(name);
4596 
4597  return (shortname);
4598 }
4599 
4600 static void
4601 reportOrdering()
4602 {
4603  Biddy_Variable var;
4604 
4605  printf("Variable ordering:\n");
4606  var = Biddy_GetLowestVariable();
4607  while (var != 0) {
4608  printf("(%s)",Biddy_GetVariableName(var));
4609  var = Biddy_GetNextVariable(var);
4610  }
4611  printf("\n");
4612 }
Biddy_Variable is used for indices in variable table.
EXTERN Biddy_Edge Biddy_Managed_Xnor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xnor calculates Boolean function XNOR.
Definition: biddyOp.c:2354
EXTERN Biddy_Edge Biddy_Managed_Leq(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Leq calculates Boolean implication.
Definition: biddyOp.c:2452
EXTERN void Biddy_Managed_SelectNode(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_SelectNode selects the top node of the given function.
Definition: biddyMain.c:1400
EXTERN void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1536
EXTERN Biddy_Edge Biddy_Managed_ITE(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge h)
Function Biddy_Managed_ITE calculates ITE operation of three Boolean functions.
Definition: biddyOp.c:370
Biddy_String Biddy_Managed_ReadBddview(Biddy_Manager MNG, const char filename[], Biddy_String name)
Function Biddy_Managed_ReadBddview reads bddview file and creates a Boolean function.
Definition: biddyInOut.c:543
EXTERN Biddy_Variable Biddy_Managed_GetVariable(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_GetVariable returns variable with the given name.
Definition: biddyMain.c:1733
Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
void Biddy_Managed_WriteBDD(Biddy_Manager MNG, const char filename[], Biddy_Edge f, Biddy_String label)
Function Biddy_Managed_WriteBDD writes raw format using fprintf.
Definition: biddyInOut.c:1110
Biddy_Edge Biddy_Managed_Eval2(Biddy_Manager MNG, Biddy_String boolFunc)
Function Biddy_Managed_Eval2 evaluates infix format.
Definition: biddyInOut.c:347
void Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[], Biddy_String prefix)
Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary input...
Definition: biddyInOut.c:979
EXTERN Biddy_String Biddy_Managed_GetVariableName(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableName returns the name of a variable.
Definition: biddyMain.c:1972
#define Biddy_GetMark(f)
Definition: biddy.h:168
#define Biddy_GetVariableName(v)
Definition: biddy.h:442
Biddy_Edge Biddy_Managed_Eval1x(Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format.
Definition: biddyInOut.c:248
#define Biddy_GetNextVariable(v)
Definition: biddy.h:427
EXTERN Biddy_Edge Biddy_Managed_Nand(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer).
Definition: biddyOp.c:1718
EXTERN Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f)
Function Biddy_Managed_FindFormula find formula in Formula table.
Definition: biddyMain.c:4790
EXTERN void Biddy_Managed_ResetVariablesValue(Biddy_Manager MNG)
Function Biddy_Managed_ResetVariablesValue sets all variable&#39;s value to biddyZero.
Definition: biddyMain.c:2085
EXTERN Biddy_Variable Biddy_Managed_GetLowestVariable(Biddy_Manager MNG)
Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering...
Definition: biddyMain.c:1787
EXTERN unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean select)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:1283
Biddy_String is used for strings.
void Biddy_Managed_PrintfSOP(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfSOP writes SOP using printf.
Definition: biddyInOut.c:1350
unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf.
Definition: biddyInOut.c:1693
EXTERN Biddy_Variable Biddy_Managed_AddVariableByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddVariableByName adds variable.
Definition: biddyMain.c:2896
unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], void *xytable)
Function Biddy_Managed_WriteBDDView writes bddview format using fprintf.
Definition: biddyInOut.c:1916
void Biddy_Managed_PrintfTable(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfTable writes truth table using printf.
Definition: biddyInOut.c:1156
EXTERN Biddy_Boolean Biddy_Managed_Eval(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Eval returns the value of a Boolean function for a given variable assignment...
Definition: biddyMain.c:2255
Biddy_Boolean is used for boolean values.
Biddy_LookupFunction is used in Biddy_Eval1x to specify user&#39;s function which will lookups in a user&#39;...
void Biddy_Managed_WriteTable(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
Function Biddy_Managed_WriteTable writes truth table using fprintf.
Definition: biddyInOut.c:1253
EXTERN unsigned int Biddy_Managed_AddFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c)
Function Biddy_Managed_AddFormula adds formula to Formula table.
Definition: biddyMain.c:4511
EXTERN Biddy_Boolean Biddy_Managed_IsSmaller(Biddy_Manager MNG, Biddy_Variable fv, Biddy_Variable gv)
Function Biddy_Managed_IsSmaller returns TRUE if the first variable is smaller (= lower = previous = ...
Definition: biddyMain.c:2451
EXTERN Biddy_String Biddy_Managed_GetTopVariableName(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableName returns the name of top variable.
Definition: biddyMain.c:2028
#define Biddy_GetTag(f)
Definition: biddy.h:199
#define Biddy_Managed_GetTopVariable(MNG, f)
Definition: biddy.h:348
#define Biddy_IsNull(f)
Definition: biddy.h:150
#define Biddy_GetLowestVariable()
Definition: biddy.h:412
EXTERN unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodes.
Definition: biddyStat.c:85
EXTERN Biddy_Variable Biddy_Managed_FoaVariable(Biddy_Manager MNG, Biddy_String x, Biddy_Boolean varelem)
Function Biddy_Managed_FoaVariable finds variable/element or adds new variable (i.e. Boolean function f = x) and new element (i.e. it creates set {{x}}).
Definition: biddyMain.c:2573
Biddy_String Biddy_Managed_Eval0(Biddy_Manager MNG, Biddy_String s)
Function Biddy_Managed_Eval0 evaluates raw format.
Definition: biddyInOut.c:171
EXTERN Biddy_Edge Biddy_Managed_Or(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Or calculates Boolean function OR (disjunction).
Definition: biddyOp.c:1243
Biddy_Manager is used to specify manager.
EXTERN Biddy_Edge Biddy_Managed_GetVariableEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableEdge returns variable&#39;s edge.
Definition: biddyMain.c:1922
EXTERN Biddy_Edge Biddy_Managed_Xor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xor calculates Boolean function XOR.
Definition: biddyOp.c:1913
EXTERN void Biddy_Managed_Clean(Biddy_Manager MNG)
Function Biddy_Managed_Clean performs cleaning.
Definition: biddyMain.c:4283
void Biddy_Managed_PrintfBDD(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfBDD writes raw format using printf.
Definition: biddyInOut.c:1080
void Biddy_Managed_WriteSOP(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
Function Biddy_Managed_WriteSOP writes SOP using fprintf.
Definition: biddyInOut.c:1434
#define Biddy_IsTerminal(f)
Definition: biddy.h:160
EXTERN Biddy_Edge Biddy_Managed_Nor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce).
Definition: biddyOp.c:1816
EXTERN Biddy_Edge Biddy_Managed_And(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_And calculates Boolean function AND (conjunction).
Definition: biddyOp.c:812
File biddyInt.h contains declaration of internal data structures.
EXTERN Biddy_Boolean Biddy_Managed_IsSelected(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IsSelected returns TRUE iff the top node of the given function is selected...
Definition: biddyMain.c:1452
EXTERN Biddy_Edge Biddy_Managed_Gt(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Gt calculates the negation of Boolean implication.
Definition: biddyOp.c:2767
EXTERN Biddy_Edge Biddy_Managed_Not(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Not calculates Boolean function NOT.
Definition: biddyOp.c:100