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  nextCh(s,i,ch);
2287  if (strcmp(*ch,"(")) {
2288  printf("ERROR: <%s>\n",*ch);
2289  return biddyNull;
2290  }
2291  e = ReadBDD(MNG,s,i,ch);
2292  nextCh(s,i,ch);
2293  if (strcmp(*ch,")")) {
2294  printf("ERROR: <%s>\n",*ch);
2295  return biddyNull;
2296  }
2297  nextCh(s,i,ch);
2298  if (strcmp(*ch,"(")) {
2299  printf("ERROR: <%s>\n",*ch);
2300  return biddyNull;
2301  }
2302  t = ReadBDD(MNG,s,i,ch);
2303  nextCh(s,i,ch);
2304  if (strcmp(*ch,")")) {
2305  printf("ERROR: <%s>\n",*ch);
2306  return biddyNull;
2307  }
2308  if (inv) {
2309  f = Biddy_Managed_Not(MNG,Biddy_Managed_ITE(MNG,n,t,e));
2310  } else {
2311  f = Biddy_Managed_ITE(MNG,n,t,e);
2312  }
2313  free(varname);
2314  }
2315 
2316  return f;
2317 }
2318 
2319 static Biddy_Edge
2320 evaluate1(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch,
2322 {
2323  unsigned int idx;
2324  Biddy_Edge f;
2325  int op;
2326 
2327  /* DEBUGGING */
2328  /*
2329  printf("evaluate1: %s\n",s);
2330  printf("evaluate1 i = %d\n",*i);
2331  printf("evaluate1 ch = %s\n",*ch);
2332  */
2333 
2334  if (!strcmp(*ch,"(")) {
2335  nextCh(s,i,ch);
2336 
2337  if (!strcasecmp(*ch, "NOT")) {
2338  nextCh(s,i,ch);
2339  f = Biddy_Managed_Not(MNG,evaluate1(MNG,s,i,ch,lf));
2340  } else {
2341  if ((op = Op(s,i,ch))) {
2342  f = evaluateN(MNG,s,i,ch,evaluate1(MNG,s,i,ch,lf),op,lf);
2343  } else {
2344  f = evaluate1(MNG,s,i,ch,lf);
2345  }
2346  }
2347 
2348  if (!strcmp(*ch, ")")) nextCh(s,i,ch);
2349 
2350  return f;
2351  }
2352 
2353  /* evaluate1 will always check Biddy's formula table */
2354  /* if (lf != NULL) then user's formula table will be checked, too */
2355  /* user's formula table will be checked before Biddy's formula table */
2356  /* entries in user's formula should not be obsolete */
2357 
2358  if (charOK(*ch[0])) {
2359  if (!lf) {
2360  if (!Biddy_Managed_FindFormula(MNG,*ch,&idx,&f)) {
2362  }
2363  } else {
2364  if ((!(lf(*ch,&f))) &&
2365  (!Biddy_Managed_FindFormula(MNG,*ch,&idx,&f))) {
2367  }
2368  }
2369  nextCh(s,i,ch);
2370 
2371  assert( f != biddyNull );
2372 
2373  return f;
2374  }
2375 
2376  return biddyNull;
2377 }
2378 
2379 static Biddy_Edge
2380 evaluateN(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch,
2381  Biddy_Edge g, int op, Biddy_LookupFunction lf)
2382 {
2383  Biddy_Edge f, h;
2384 
2385  /* DEBUGGING */
2386  /*
2387  printf("evaluateN: %s\n",s);
2388  printf("evaluateN i = %d\n",*i);
2389  printf("evaluateN ch = %s\n",*ch);
2390  */
2391 
2392  h = evaluate1(MNG,s,i,ch,lf);
2393  if (!Biddy_IsNull(h)) {
2394  f = biddyNull;
2395  switch (op) {
2396  case oAND: f = Biddy_Managed_And(MNG,g,h);
2397  break;
2398  case oOR: f = Biddy_Managed_Or(MNG,g,h);
2399  break;
2400  case oEXOR: f = Biddy_Managed_Xor(MNG,g,h);
2401  }
2402  return evaluateN(MNG,s,i,ch,f,op,lf);
2403  }
2404  return g;
2405 }
2406 
2407 static int
2408 Op(Biddy_String s, int *i, Biddy_String *ch)
2409 {
2410 
2411  /* DEBUGGING */
2412  /*
2413  printf("Op ch = %s\n",*ch);
2414  */
2415 
2416  if (!strcasecmp(*ch, "AND")) {
2417  nextCh(s,i,ch);
2418  return oAND;
2419  }
2420 
2421  if (!strcasecmp(*ch, "OR")) {
2422  nextCh(s,i,ch);
2423  return oOR;
2424  }
2425 
2426  if (!strcasecmp(*ch, "EXOR")) {
2427  nextCh(s,i,ch);
2428  return oEXOR;
2429  }
2430 
2431  return 0;
2432 }
2433 
2434 static void
2435 createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree)
2436 {
2437  int i;
2438  unsigned int idx;
2439  Biddy_Edge tmp;
2440 
2441  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
2442  {
2443  for (i = 0; i <= tree->availableNode; i++) {
2444  if (tree->tnode[i].op == 255) {
2445  if (tree->tnode[i].name) {
2446  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&tmp))) {
2447  Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2448  }
2449  }
2450  }
2451  }
2452  }
2453 
2454  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2455  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2456  {
2457  for (i = tree->availableNode; i >= 0; i--) {
2458  if (tree->tnode[i].op == 255) {
2459  if (tree->tnode[i].name) {
2460  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&tmp))) {
2461  Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2462  }
2463  }
2464  }
2465  }
2466  }
2467 }
2468 
2469 static Biddy_Edge
2470 createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i)
2471 {
2472  unsigned int idx;
2473  Biddy_Edge lbdd,rbdd,fbdd;
2474 
2475  if (i == -1) return biddyNull;
2476  if (tree->tnode[i].op == 255) {
2477  if (tree->tnode[i].name) {
2478  if (!strcmp(tree->tnode[i].name,"0")) fbdd = biddyZero;
2479  else if (!strcmp(tree->tnode[i].name,"1")) fbdd = biddyOne;
2480  else {
2481  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&fbdd))) {
2482  fbdd = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2483  }
2484  }
2485  } else {
2486  fbdd = biddyNull;
2487  }
2488 
2489  /* DEBUGGING */
2490  /*
2491  printf("createBddFromBTree: op == 255\n");
2492  printPrefixFromBTree(tree,i);
2493  printf("\n");
2494  printf("HERE IS fbdd:\n");
2495  Biddy_PrintfBDD(fbdd);
2496  Biddy_PrintfSOP(fbdd);
2497  */
2498 
2499  return fbdd;
2500  }
2501  lbdd = createBddFromBTree(MNG,tree,tree->tnode[i].left);
2502  rbdd = createBddFromBTree(MNG,tree,tree->tnode[i].right);
2503 
2504  /* NOT (~!), AND (&*), OR (|+), XOR (^%) , XNOR(-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (\), AND NOTBUT (/) ARE IMPLEMENTED */
2505  /* char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' }; */
2506  if (tree->tnode[i].op == 0) fbdd = Biddy_Managed_Not(MNG,rbdd); /* NOT */
2507  else if (tree->tnode[i].op == 1) fbdd = Biddy_Managed_And(MNG,lbdd,rbdd); /* AND */
2508  else if (tree->tnode[i].op == 2) fbdd = Biddy_Managed_Gt(MNG,lbdd,rbdd); /* BUTNOT */
2509  else if (tree->tnode[i].op == 4) fbdd = Biddy_Managed_Gt(MNG,rbdd,lbdd); /* NOTBUT */
2510  else if (tree->tnode[i].op == 6) fbdd = Biddy_Managed_Xor(MNG,lbdd,rbdd); /* XOR */
2511  else if (tree->tnode[i].op == 7) fbdd = Biddy_Managed_Or(MNG,lbdd,rbdd); /* OR */
2512  else if (tree->tnode[i].op == 8) fbdd = Biddy_Managed_Nor(MNG,lbdd,rbdd); /* NOR */
2513  else if (tree->tnode[i].op == 9) fbdd = Biddy_Managed_Xnor(MNG,lbdd,rbdd); /* XNOR */
2514  else if (tree->tnode[i].op == 11) fbdd = Biddy_Managed_Leq(MNG,rbdd,lbdd); /* IMPLIES <= */
2515  else if (tree->tnode[i].op == 13) fbdd = Biddy_Managed_Leq(MNG,lbdd,rbdd); /* IMPLIES => */
2516  else if (tree->tnode[i].op == 14) fbdd = Biddy_Managed_Nand(MNG,lbdd,rbdd); /* NAND */
2517  else fbdd = biddyNull;
2518 
2519  /* DEBUGGING */
2520  /*
2521  printf("createBddFromBTree: op == %u\n",tree->tnode[i].op);
2522  printPrefixFromBTree(tree,i);
2523  printf("\n");
2524  printf("HERE IS lbdd:\n");
2525  Biddy_PrintfBDD(lbdd);
2526  Biddy_PrintfSOP(lbdd);
2527  printf("HERE IS rbdd:\n");
2528  Biddy_PrintfBDD(rbdd);
2529  Biddy_PrintfSOP(rbdd);
2530  printf("HERE IS fbdd:\n");
2531  Biddy_PrintfBDD(fbdd);
2532  Biddy_PrintfSOP(fbdd);
2533  */
2534 
2535  return fbdd;
2536 }
2537 
2538 static void
2539 parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt)
2540 {
2541  unsigned int activemodule=0;
2542  BiddyVerilogLine *ln;
2543  BiddyVerilogModule *md;
2544  unsigned int i=0, j=0, k=0; /* indexes */
2545  char ch, linebuf[LINESIZE]; /* buffer for single line from the verilog file */
2546  Biddy_String buffer; /* buffer for complete verilog statements */
2547  Biddy_String token[TOKENNUM]; /* array to hold tokens for the line */
2548  Biddy_String keyword; /* keyword from verilog line */
2549  Biddy_Boolean comment, noname, ok, acceptable;
2550  Biddy_String t,tc;
2551  unsigned int tn;
2552 
2553  (*l) = 0;
2554  (*lt) = NULL;
2555  (*n) = 0;
2556  (*mt) = NULL;
2557 
2558  keyword = NULL;
2559  buffer = NULL;
2560  md = NULL;
2561  while (fgets(linebuf,LINESIZE,verilogfile) != NULL) {
2562 
2563  if (keyword) free(keyword);
2564  tn = (unsigned int) strspn(linebuf," ");
2565 
2566  if (tn == strlen(linebuf)) {
2567  continue; /* skip empty lines and white space */
2568  }
2569 
2570  /* get 1st word from the line */
2571  tn += (unsigned int) strcspn(&linebuf[tn]," ");
2572  ch = 0;
2573  if (tn < strlen(linebuf)) {
2574  ch = linebuf[tn];
2575  linebuf[tn] = 0;
2576  }
2577  tn = (unsigned int) strspn(linebuf," ");
2578  keyword = strdup(&linebuf[tn]);
2579  if (ch) {
2580  tn += (unsigned int) strcspn(&linebuf[tn]," ");
2581  linebuf[tn] = ch;
2582  }
2583  keyword = trim(keyword);
2584 
2585  if (!strlen(keyword)) {
2586  continue; /* skip white space not recognised before */
2587  }
2588 
2589  if (!strcmp(keyword,"//")) {
2590  continue; /* skip comment lines */
2591  }
2592 
2593  if (buffer) free(buffer);
2594  buffer = strdup("");
2595  if (!strcmp(keyword,"endmodule")) { /* endmodule keyword does not use ';' */
2596  concat(&buffer,keyword);
2597  } else {
2598  concat(&buffer,linebuf);
2599  while (!isEndOfLine(linebuf)) { /* check if the line ends with a ';' character (multiple lines statement) */
2600  if (fgets(linebuf,LINESIZE,verilogfile) != NULL) {/* otherwise, append all the following lines */
2601  concat(&buffer,linebuf);
2602  if ((strlen(buffer) + LINESIZE) > BUFSIZE) printf("ERROR (parseVerilogFile): BUFFER TO SMALL\n");
2603  }
2604  }
2605  }
2606 
2607  /* tokenize the line to extract data */
2608  noname = FALSE;
2609  if (strcmp(keyword,"module") && strcmp(keyword,"endmodule") &&
2610  strcmp(keyword,"input") && strcmp(keyword,"output") &&
2611  strcmp(keyword,"wire") && strcmp(keyword,"reg") &&
2612  strcmp(keyword,"assign"))
2613  {
2614  tn = (unsigned int) strspn(buffer," ");
2615  tn += (unsigned int) strcspn(&buffer[tn]," ");
2616  tn += (unsigned int) strspn(&buffer[tn]," ");
2617  if (buffer[tn] == '(') noname = TRUE;
2618  }
2619  i=0;
2620  comment = FALSE;
2621  t = strtok(buffer," ");
2622  token[i++] = strdup(t); /* full keyword */
2623  if (noname) {
2624  sprintf(linebuf,"NONAME%d",(*l));
2625  token[i++] = strdup(linebuf); /* add NONAME */
2626  }
2627  while ((t = strtok(NULL," (),;\r\n")) && (strcmp(t,"//"))) {
2628  if (!strcmp(t,"/*")) comment = TRUE;
2629  if (!comment) {
2630  if (strlen(t)>1) {
2631  tn = (unsigned int) strcspn(t,"{}");
2632  while (tn != strlen(t)) {
2633  tc = NULL;
2634  if (t[tn] == '{') tc = strdup("{");
2635  if (t[tn] == '}') tc = strdup("}");
2636  if (tn) {
2637  t[tn] = 0;
2638  token[i++] = strdup(t);
2639  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2640  }
2641  token[i++] = tc;
2642  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2643  t = &t[tn+1];
2644  tn = (unsigned int) strcspn(t,"{}");
2645  }
2646  }
2647  if (strlen(t)) {
2648  token[i++] = strdup(t);
2649  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2650  }
2651  }
2652  if (comment && !strcmp(t,"*/")) comment = FALSE;
2653  }
2654  token[i] = NULL;
2655 
2656  if (!strcmp(keyword,"module")) { /* START OF MODULE */
2657  (*n)++;
2658  (*mt) = (BiddyVerilogModule **) realloc((*mt), (*n) * sizeof(BiddyVerilogModule *)); /* create or enlarge table of modules */
2659  md = (BiddyVerilogModule *) calloc(1, sizeof(BiddyVerilogModule)); /* declare an instance of a module */
2660  (*mt)[(*n)-1] = md;
2661  md->name = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for module name string */
2662  strcpy(md->name,token[1]); /* set module name */
2663  activemodule = (*n);
2664  /* DEBUGGING */
2665  /*
2666  printf("MODULE: %s (#%d)\n",token[1],activemodule);
2667  */
2668  md->outputFirst = TRUE; /* TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3), FALSE iff N3 = NAND(N1,N2) */
2669  }
2670 
2671  if (!strcmp(keyword,"endmodule")) { /* END OF MODULE */
2672  /* DEBUGGING */
2673  /*
2674  printf("ENDMODULE: #%d\n",activemodule);
2675  */
2676  activemodule = 0;
2677  md = NULL;
2678  } else {
2679  if (!activemodule) {
2680  printf("ERROR (parseVerilogFile): statement <%s> is outside of module\n",keyword);
2681  continue;
2682  }
2683  }
2684 
2685  acceptable = FALSE;
2686  if ((activemodule == 1) || !strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
2687  /* TO DO: MULTIPLE MODULES ARE NOT SUPPORTED, YET */
2688 
2689  if (!strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
2690  acceptable = TRUE;
2691  }
2692 
2693  else if (!strcmp(keyword,"input")) { /* PRIMARY INPUTS */
2694  acceptable = TRUE;
2695  for (j = 1; j < i; j++) { /* parse all the words in the line */
2696  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2697  parseSignalVector(md->inputs, token, &j, &md->inputcount);
2698  else { /* not a vector of signal */
2699  md->inputs[md->inputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for input string */
2700  strcpy(md->inputs[md->inputcount],token[j]); /* add the input name to the array of inputs */
2701  (md->inputcount)++; /* update the number of inputs in the circuit */
2702  if (md->inputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
2703  }
2704  }
2705  }
2706 
2707  else if (!strcmp(keyword,"output")) { /* PRIMARY OUTPUTS */
2708  acceptable = TRUE;
2709  for (j = 1; j < i; j++) { /* parse all the words in the line */
2710  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2711  parseSignalVector(md->outputs, token, &j, &md->outputcount);
2712  else { /* not a vector of signal */
2713  md->outputs[md->outputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for output string */
2714  strcpy(md->outputs[md->outputcount],token[j]); /* add the output name to the array of outputs */
2715  (md->outputcount)++; /* update the number of outputs in the circuit */
2716  if (md->outputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
2717  }
2718  }
2719  }
2720 
2721  else if (!strcmp(keyword,"wire")) { /* WIRES */
2722  for (j = 1; j < i; j++) { /* parse all the words in the line */
2723  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2724  parseSignalVector(md->wires, token, &j, &md->wirecount);
2725  else { /* not a vector of signal */
2726  /* check if this wire has not already been stated as input or output */
2727  ok = TRUE;
2728  for (k=0; k < md->inputcount; k++) {
2729  if (!strcmp(md->inputs[k],token[j])) ok = FALSE;
2730  }
2731  for (k=0; k < md->outputcount; k++) {
2732  if (!strcmp(md->outputs[k],token[j])) ok = FALSE;
2733  }
2734  if (ok) {
2735  acceptable = TRUE;
2736  md->wires[md->wirecount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for wire string */
2737  strcpy(md->wires[md->wirecount],token[j]); /* add the wire name to the array of wires */
2738  (md->wirecount)++; /* update the number of wires in the circuit */
2739  if (md->wirecount >= WIRENUM) printf("ERROR (parseVerilogFile): WIRENUM TO SMALL\n");
2740  } else {
2741  /* DEBUGGING */
2742  /*
2743  printf("WARNING (parseVerilogFile): wire %s already defined as input/output\n",token[j]);
2744  */
2745  }
2746  }
2747  }
2748  }
2749 
2750  else if (!strcmp(keyword,"reg")) { /* REGS */
2751  acceptable = TRUE;
2752  for (j = 1; j < i; j++) { /* parse all the words in the line */
2753  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2754  parseSignalVector (md->regs, token, &j, &md->regcount);
2755  else { /* not a vector of signal */
2756  md->regs[md->regcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for reg string */
2757  strcpy(md->regs [md->regcount],token[j]); /* add the reg name to the array of regs */
2758  (md->regcount)++; /* update the number of regs in the circuit */
2759  if (md->regcount >= REGNUM) printf("ERROR (parseVerilogFile): REGNUM TO SMALL\n");
2760  }
2761  }
2762  }
2763 
2764  else if (isGate(keyword)) { /* BASIC GATES */
2765  acceptable = TRUE;
2766  md->gates[md->gatecount] = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for gate name string */
2767  strcpy(md->gates[md->gatecount],token[1]); /* add the gate name to the array of gates */
2768  if (!md->gatecount) { /* use the first gate to determine md->outputFirst */
2769  for (j=0; md->inputs[j] != NULL; j++) if (!strcmp(md->inputs[j],token[2])) md->outputFirst = FALSE;
2770  }
2771  (md->gatecount)++; /* update the number of gates in the circuit */
2772  if (md->gatecount >= GATENUM) printf("ERROR (parseVerilogFile): GATENUM TO SMALL\n");
2773  }
2774 
2775  else {
2776  /* AN UNIMPLEMENTED KEYWORD */
2777  /* GATES DEFINED BY OTHER MODULES ARE NOT RESOLVED */
2778  }
2779 
2780  }
2781 
2782  /* add this line to the table of acceptable lines */
2783  if (acceptable) {
2784  (*l)++;
2785  (*lt) = (BiddyVerilogLine **) realloc((*lt), (*l) * sizeof(BiddyVerilogLine *)); /* create or enlarge table of lines */
2786  ln = (BiddyVerilogLine *) calloc(1, sizeof(BiddyVerilogLine)); /* declare an instance of a line */
2787  ln->keyword = strdup(keyword);
2788  ln->line = strdup(token[0]);
2789  for (j=1; j<i; j++) concat(&(ln->line),token[j]);
2790  (*lt)[(*l)-1] = ln;
2791  }
2792 
2793  }
2794 
2795  if (keyword) free(keyword);
2796  if (buffer) free(buffer);
2797 
2798  /* DEBUGGING - print summary of the module */
2799  /*
2800  printModuleSummary(m);
2801  */
2802 }
2803 
2808 static void
2809 createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c)
2810 {
2811  BiddyVerilogModule *m;
2812  unsigned int i=0, j=0, k=0, l=0;
2813  int in=0, id=0, index=0;
2814  unsigned int activemodule=0;
2815  Biddy_String keyword, buffer;
2816  Biddy_String token[TOKENNUM]; /* array to hold tokens for one line */
2817  Biddy_Boolean ok;
2818  Biddy_String tmptoken;
2819 
2820  memset(token, 0, sizeof(char*) * TOKENNUM);
2821 
2822  m = mt[0]; /* target module is the first one in the table */
2823 
2824  /* initialization of the circuit */
2825  c->inputcount = m->inputcount; /* set the number of inputs for the ciruit */
2826  c->outputcount = m->outputcount; /* set the number of outputs for the circuit */
2827  c->wirecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of wires for the circuit */
2828  c->nodecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of nodes for the circuit */
2829  c->wires = (BiddyVerilogWire **) calloc(c->wirecount,sizeof(BiddyVerilogWire *)); /* allocate a contiguous array to index every wire */
2830  c->nodes = (BiddyVerilogNode **) calloc(c->nodecount,sizeof(BiddyVerilogNode *)); /* allocate a contiguous array to index every node */
2831 
2832  id = 0;
2833  for (i=0; i < m->inputcount; i++) { /* store the names of primary inputs */
2834  c->inputs[i] = (Biddy_String) calloc(strlen(m->inputs[i]) + 1, sizeof (char));
2835  strcpy(c->inputs[i],m->inputs[i]);
2836  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2837  buildNode(c->nodes[id],(Biddy_String)"input", m->inputs[i]);
2838  id++;
2839  }
2840  for (i=0; i < m->outputcount; i++) { /* store the names of primary outputs */
2841  c->outputs[i] = (Biddy_String) calloc(strlen(m->outputs[i]) + 1, sizeof(char));
2842  strcpy(c->outputs[i],m->outputs[i]);
2843  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2844  buildNode(c->nodes[id],(Biddy_String)"output",m->outputs[i]);
2845  id++;
2846  }
2847  for (i=0; i < m->wirecount; i++) { /* store the names of wires */
2848  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2849  buildNode(c->nodes[id],(Biddy_String)"wire",m->wires[i]);
2850  id++;
2851  }
2852  for (i=0; i < m->gatecount; i++) { /* store the names of gates */
2853  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2854  buildNode(c->nodes[id],(Biddy_String)"gate",m->gates[i]);
2855  id++;
2856  }
2857 
2858  index = 0;
2859  for (l=0; l<linecount;l++) {
2860  keyword = lt[l]->keyword;
2861  buffer = lt[l]->line;
2862 
2863  if (!strcmp(keyword,"module")) {
2864  activemodule++;
2865  continue;
2866  }
2867 
2868  if (!strcmp(keyword,"endmodule")) {
2869  continue;
2870  }
2871 
2872  if (activemodule > 1) {
2873  /* TO DO: MULTIPLE MODULES ARE NOT FULLY SUPPORTED, YET */
2874  continue;
2875  }
2876 
2877  if (!strcmp(keyword,"input")) {
2878  continue;
2879  }
2880  if (!strcmp(keyword,"output")) {
2881  continue;
2882  }
2883  if (!strcmp(keyword,"wire")) {
2884  continue;
2885  }
2886  if (!strcmp(keyword,"reg")) {
2887  continue;
2888  }
2889  if (!strcmp(keyword,"assign")) {
2890  continue;
2891  }
2892 
2893  /* tokenize the line to extract data */
2894  i=0;
2895  token[0] = strtok(buffer," ");
2896  while(token[i]!= NULL) {
2897  /* DEBUGGING */
2898  /*
2899  printf("(#%d) TOKENIZE: <%s>\n",i,token[i]);
2900  */
2901  i++;
2902  token[i] = strtok(NULL," ");
2903  }
2904 
2905  if (!isGate(keyword)) {
2906  printf("WARNING (createVerilogCircuit): SKIP <%s>\n",buffer);
2907  continue;
2908  }
2909 
2910  if (!m->outputFirst) {
2911  /* m->outputFirst == FALSE iff "nand NAND2_1 (N1, N2, N3);" defines N3 = NAND(N1,N2) */
2912  /* m->outputFirst == TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3) */
2913  /* exchange token[2] and token[i-1] */
2914  tmptoken = token[2];
2915  token[2] = token[i-1];
2916  token[i-1] = tmptoken;
2917  }
2918 
2919  /* A. Check or create wires for all the gate inputs */
2920  /* if wire is not known it will be treated as a primary input */
2921  for (j = 3; j < i; j++) {
2922  if (!isDefined(c,token[j])) {
2923  ok = FALSE;
2924  for (k=0; k < m->wirecount; k++) { /* check the names of wires */
2925  if (!strcmp(m->wires[k],token[j])) {
2926  printf("ERROR (createVerilogCircuit): wire %s used before defined!\n",token[j]);
2927  exit(1);
2928  }
2929  }
2930  for (k=0; !ok && k < m->inputcount; k++) { /* check the names of primary inputs */
2931  if (!strcmp(m->inputs[k],token[j])) ok = TRUE;
2932  }
2933  if (!ok) {
2934  printf("WARNING (createVerilogCircuit): wire %s treated as primary input!\n",token[j]);
2935  }
2936  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2937  buildWire(c,c->wires[index],(Biddy_String)"I",token[j]);
2938  /* assign inputs to the wires representing gate inputs */
2939  /* NOT NEEDED */
2940  /* assign outputs to the wires representing gate inputs */
2941  /* NOT USED */
2942  index++;
2943  }
2944  }
2945 
2946  /* B. Create a wire for the gate */
2947  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2948  buildWire(c,c->wires[index],keyword,token[1]);
2949  /* assign inputs to the wire representing gate */
2950  in = 0;
2951  for (j = 3; j < i; j++) {
2952  c->wires[index]->inputs[in] = getNodeIdByName(c,token[j]);
2953  c->wires[index]->inputcount++;
2954  in++;
2955  }
2956  /* assign outputs to the wire representing gate */
2957  /* NOT USED */
2958  index++;
2959 
2960  /* C. Check or create a wire for the gate output */
2961  if (!isDefined(c,token[2])) { /* if wire is not already defined */
2962  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2963  buildWire(c,c->wires[index],(Biddy_String)"W",token[2]);
2964  /* assign inputs to the wire representing gate ouput */
2965  c->wires[index]->inputs[0] = getNodeIdByName(c,token[1]);
2966  c->wires[index]->inputcount = 1;
2967  /* assign outputs to the wire representing gate ouput */
2968  /* NOT USED */
2969  index++;
2970  } else { /* if wire is already defined */
2971  getWireByName(c,token[2])->inputs[0] = getNodeIdByName(c,token[1]); /* find the wire and attach an input to it */
2972  getWireByName(c,token[2])->inputcount = 1;
2973  }
2974 
2975  }
2976 
2977  c->wirecount = index;
2978 
2979  /* c->wires[i]->fanout is the count of gates (and wires), where */
2980  /* this wire is used as an input */
2981  i=0;
2982  while (i<c->wirecount && c->wires[i] != NULL) {
2983  for (j=0; j<c->wires[i]->inputcount; j++) {
2984  (getWireById(c,c->wires[i]->inputs[j])->fanout)++;
2985  /* DEBUGGING */
2986  /*
2987  printf("Increment TTL for wire %d\n",c->wires[i]->inputs[j]);
2988  */
2989  }
2990  i++;
2991  }
2992 
2993  /* DEBUGGING - print summary of the circuit */
2994  /*
2995  printCircuitSummary(c);
2996  */
2997 }
2998 
3007 static void
3008 createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix)
3009 {
3010  unsigned int i,j;
3011  BiddyVerilogWire *w;
3012  Biddy_Edge f;
3013 
3014  /* DEBUGGING */
3015  /*
3016  printf("Creating %d primary inputs\n",c->inputcount);
3017  */
3018 
3019  /* DEBUGGING */
3020  /*
3021  for (i = 0; i < c->inputcount; i++) {
3022  printf("%s ",c->inputs[i]);
3023  }
3024  if (c->inputcount) printf("\n");
3025  */
3026 
3027  /* DEBUGGING */
3028  /*
3029  printf("Creating %d primary outputs\n",c->outputcount);
3030  */
3031 
3032  /* DEBUGGING */
3033  /*
3034  for (i = 0; i < c->outputcount; i++) {
3035  printf("%s ",c->outputs[i]);
3036  }
3037  if (c->outputcount) printf("\n");
3038  */
3039 
3040  /* DEBUGGING */
3041  /*
3042  printf("Creating %d wires\n",c->wirecount);
3043  */
3044 
3045  /* create all BDD variables - important for ZBDD and TZBDD */
3046  for (i = 0; i < c->nodecount; i++) {
3047  if (!strcmp(c->nodes[i]->type,"input")) {
3048  Biddy_Managed_FoaVariable(MNG,c->nodes[i]->name,TRUE); /* TO DO: add prefix */
3049  }
3050  if (!strcmp(c->nodes[i]->type,"extern")) {
3051  Biddy_Managed_FoaVariable(MNG,c->nodes[i]->name,TRUE); /* TO DO: add prefix */
3052  }
3053  }
3054 
3055  /* prepare c->wires[i]->ttl which will be used to guide GC */
3056  for (i = 0; i < c->wirecount; i++) {
3057  c->wires[i]->ttl = 0;
3058  }
3059  for (i = 0; i < c->wirecount; i++) {
3060  for (j = 0; j < c->wires[i]->inputcount; j++) {
3061  w = getWireById(c,c->wires[i]->inputs[j]);
3062  (w->ttl)++;
3063  if (w->ttl == w->fanout) {
3064  w->ttl = i;
3065  }
3066  }
3067  }
3068  for (i = 0; i < c->outputcount; i++) {
3069  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3070  if (w) {
3071  w->ttl = c->wirecount - 1;
3072  }
3073  }
3074  for (i = 0; i < c->wirecount; i++) {
3075  if (c->wires[i]->ttl) c->wires[i]->ttl = c->wires[i]->ttl - i;
3076  }
3077 
3078  for (i = 0; i < c->wirecount; i++) {
3079 
3080  /* REPORT PROGRESS */
3081 
3082  printf("#%d",i);
3083  if (i == c->wirecount-1) printf("\n");
3084 
3085 
3086  /* DEBUGGING */
3087  /*
3088  printf("Creating c->wire[%d], ",i);
3089  printf("ID: %d, ",c->wires[i]->id);
3090  printf("name: %s, ",c->nodes[c->wires[i]->id]->name);
3091  printf("type: %s, ",c->wires[i]->type);
3092  printf("fanout: %d, ",c->wires[i]->fanout);
3093  printf("ttl: %d, ",c->wires[i]->ttl);
3094  printf("Inputs (%d): ",c->wires[i]->inputcount);
3095  if (strcmp(c->wires[i]->type,"I")) {
3096  if (c->wires[i]->inputcount) {
3097  for (j=0;j<c->wires[i]->inputcount;j++) {
3098  printf("%d ",c->wires[i]->inputs[j]);
3099  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3100  printf("ERROR (gate ordering is wrong)");
3101  }
3102  }
3103  } else {
3104  printf("ERROR (wire must be a primary input or it must have some inputs)");
3105  }
3106  } else {
3107  if (c->wires[i]->inputcount) {
3108  printf("ERROR (primary input cannot have additional inputs)");
3109  } else {
3110  printf("/");
3111  }
3112  }
3113  printf("\n");
3114  */
3115 
3116  f = biddyNull;
3117 
3118  if (!strcmp(c->wires[i]->type,"I")) {
3119  if (c->wires[i]->inputcount) {
3120  printf("ERROR (primary input cannot have additional inputs)\n");
3121  } else {
3122  f = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_GetVariable(MNG,c->nodes[c->wires[i]->id]->name)); /* TO DO: add prefix */
3123  }
3124  }
3125  else if (!strcmp(c->wires[i]->type,"M")) {
3126  /* TO DO: this will be used for gates defined by other modules */
3127  }
3128  else {
3129  if (c->wires[i]->inputcount) {
3130  for (j=0; j<c->wires[i]->inputcount; j++) {
3131  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3132  printf("ERROR (gate ordering is wrong)\n");
3133  }
3134  }
3135 
3136  if (!strcmp(c->wires[i]->type,"W")) {
3137  if (c->wires[i]->inputcount == 1) {
3138  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3139  } else {
3140  printf("ERROR (internal wire must have exactly one input)\n");
3141  }
3142  }
3143 
3144  else if (!strcmp(c->wires[i]->type,"buf"))
3145  {
3146  if (c->wires[i]->inputcount != 1) {
3147  printf("ERROR (buf gate must have exactly 1 input)\n");
3148  } else {
3149  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3150  }
3151  }
3152 
3153  else if (!strcmp(c->wires[i]->type,"and"))
3154  {
3155  f = biddyOne;
3156  for (j=0; j<c->wires[i]->inputcount; j++) {
3157  f = Biddy_Managed_And(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3158  }
3159  }
3160 
3161  else if (!strcmp(c->wires[i]->type,"nand"))
3162  {
3163  f = biddyOne;
3164  for (j=0; j<c->wires[i]->inputcount; j++) {
3165  f = Biddy_Managed_And(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3166  }
3167  f = Biddy_Managed_Not(MNG,f);
3168  }
3169 
3170  else if (!strcmp(c->wires[i]->type,"or"))
3171  {
3172  f = biddyZero;
3173  for (j=0; j<c->wires[i]->inputcount; j++) {
3174  f = Biddy_Managed_Or(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3175  }
3176  }
3177 
3178  else if (!strcmp(c->wires[i]->type,"nor"))
3179  {
3180  f = biddyZero;
3181  for (j=0; j<c->wires[i]->inputcount; j++) {
3182  f = Biddy_Managed_Or(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3183  }
3184  f = Biddy_Managed_Not(MNG,f);
3185  }
3186 
3187  else if (!strcmp(c->wires[i]->type,"xor"))
3188  {
3189  if (c->wires[i]->inputcount != 2) {
3190  printf("ERROR (xor gate not having exactly 2 inputs is not supported)\n");
3191  } else {
3192  f = Biddy_Managed_Xor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3193  getWireById(c,c->wires[i]->inputs[1])->bdd);
3194  }
3195  }
3196 
3197  else if (!strcmp(c->wires[i]->type,"xnor"))
3198  {
3199  if (c->wires[i]->inputcount != 2) {
3200  printf("ERROR (xnor gate not having exactly 2 inputs is not supported)\n");
3201  } else {
3202  f = Biddy_Managed_Xor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3203  getWireById(c,c->wires[i]->inputs[1])->bdd);
3204  f = Biddy_Managed_Not(MNG,f);
3205  }
3206  }
3207 
3208  else if (!strcmp(c->wires[i]->type,"not") ||
3209  !strcmp(c->wires[i]->type,"inv"))
3210  {
3211  if (c->wires[i]->inputcount != 1) {
3212  printf("ERROR (not gate must have exactly 1 input)\n");
3213  } else {
3214  f = Biddy_Managed_Not(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd);
3215  }
3216  }
3217 
3218  else {
3219  printf("ERROR (unimplemented type: %s)\n",c->wires[i]->type);
3220  }
3221 
3222  } else {
3223  printf("ERROR (wire must be a primary input or it must have some inputs)\n");
3224  }
3225  }
3226 
3227  c->wires[i]->bdd = f;
3228 
3229  Biddy_Managed_KeepFormulaProlonged(MNG,f,c->wires[i]->ttl);
3230  Biddy_Managed_Clean(MNG);
3231  }
3232 
3233  for (i = 0; i < c->outputcount; i++) {
3234  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3235  if (w) {
3236  f = w->bdd;
3237  } else {
3238  f = biddyZero; /* undefined outputs are represented with biddyZero */
3239  }
3240  Biddy_Managed_AddFormula(MNG,c->outputs[i],f,1); /* TO DO: add prefix */
3241  }
3242  Biddy_Managed_Clean(MNG);
3243 
3244  /*
3245  printf("Report on primary outputs\n");
3246  for (i = 0; i < c->outputcount; i++) {
3247  f = getWireByName(c,c->outputs[i])->bdd;
3248  printf("%s - %d nodes / %d nodes without complement edge\n",
3249  c->outputs[i],
3250  Biddy_Managed_CountNodes(MNG,f),
3251  Biddy_Managed_CountNodesPlain(MNG,f)
3252  );
3253  }
3254  */
3255 
3256 
3257  j = 0;
3258  for (i = 0; i < c->outputcount; i++) {
3259  f = getWireByName(c,c->outputs[i])->bdd;
3260  j = j + Biddy_Managed_CountNodes(MNG,f);
3261  }
3262  printf("The sum of BDD sizes for all outputs: %u\n",j);
3263 
3264 
3265 }
3266 
3271 static void
3272 parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count)
3273 {
3274  int v,v1,v2;
3275  char *sig_vector; /* array to hold tokens for the line */
3276 
3277  sig_vector = strtok(token[*index],":"); /* tokenize the vector to extract vector width */
3278  v1 = atoi(sig_vector); /* starting index for the vector */
3279  sig_vector = strtok(NULL, ":");
3280  v2 = atoi(sig_vector); /* ending index for the vector */
3281  (*index)++; /* get vector name from the next token */
3282  for (v = v2; v <= v1; v++) { /* add the vector signals to the array of signals */
3283  int wordsize = (int) strlen(token[*index]); /* size of the string read from the line */
3284  signal_arr [*count] = (Biddy_String) calloc(wordsize + 1, sizeof(char)); /* allocating memory for signal string */
3285  strcpy(signal_arr [*count], token[*index]); /* add the signal name to the array of signals */
3286  (*count)++; /* update the number of signals in the circuit */
3287  }
3288 }
3289 
3290 static void
3291 printModuleSummary(BiddyVerilogModule *m)
3292 {
3293  unsigned int i;
3294 
3295  printf("************** Module %s statistical results *************\n", m->name);
3296 
3297  printf("Number of primary inputs: %d\n", m->inputcount);
3298  for (i = 0; i < m->inputcount; i++)
3299  printf("%s ", m->inputs[i]);
3300  if (m->inputcount) printf("\n");
3301 
3302  printf("Number of primary outputs: %d\n", m->outputcount);
3303  for (i = 0; i < m->outputcount; i++)
3304  printf("%s ", m->outputs[i]);
3305  if ( m->outputcount) printf("\n");
3306 
3307  printf("Number of gates: %d\n", m->gatecount);
3308  for (i = 0; i < m->gatecount; i++)
3309  printf("%s ", m->gates[i]);
3310  if (m->gatecount) printf("\n");
3311 
3312  printf("Number of wires: %d\n", m->wirecount);
3313  for (i = 0; i < m->wirecount; i++)
3314  printf("%s ", m->wires[i]);
3315  if (m->wirecount) printf("\n");
3316 
3317  printf("Number of regs: %d\n", m->regcount);
3318  for (i = 0; i < m->regcount; i++)
3319  printf("%s ", m->regs[i]);
3320  if (m->regcount) printf("\n");
3321 
3322  printf("*************************** END **************************\n");
3323 }
3324 
3329 static void
3330 printCircuitSummary(BiddyVerilogCircuit *c)
3331 {
3332  unsigned int i,j;
3333 
3334  printf("************** Circuit %s statistical results *************\n", c->name);
3335 
3336  printf("Circuit size: %d\n", c->nodecount);
3337 
3338  printf("Number of primary inputs: %d\n", c->inputcount);
3339  for (i = 0; i < c->inputcount; i++)
3340  printf("%s ", c->inputs[i]);
3341  if (c->inputcount) printf("\n");
3342 
3343  printf("Number of primary outputs: %d\n", c->outputcount);
3344  for (i = 0; i < c->outputcount; i++)
3345  printf("%s ", c->outputs[i]);
3346  if (c->outputcount) printf("\n");
3347 
3348  i=0;
3349  while (i<c->wirecount && c->wires[i] != NULL) {
3350  printf ("c->wire[%d]->type: %s, ",i, c->wires[i]->type);
3351  printf ("ID: %d, ", c->wires[i]->id);
3352  printf ("name: %s, ", c->nodes[c->wires[i]->id]->name);
3353 
3354  printf ("\nInputs (%d): ", c->wires[i]->inputcount); /* wire inputs */
3355  for (j=0; j<c->wires[i]->inputcount; j++)
3356  printf ("%d ",c->wires[i]->inputs[j]);
3357 
3358  printf ("\nOutputs (%d): ", c->wires[i]->outputcount); /* wire outputs */
3359  for (j=0; j<c->wires[i]->outputcount; j++)
3360  printf ("%d ",c->wires[i]->outputs[j]);
3361 
3362  i++;
3363  printf ("\n");
3364  }
3365 
3366  printf("*************************** END **************************\n");
3367 }
3368 
3374 static Biddy_Boolean
3375 isGate(Biddy_String word)
3376 {
3377  int i;
3378  for (i = 0; i < GATESNUM; i++)
3379  if (strcmp(word,VerilogFileGateName[i]) == 0)
3380  return TRUE;
3381  return FALSE;
3382 }
3383 
3389 static Biddy_Boolean
3390 isSignalVector(Biddy_String word)
3391 {
3392  unsigned int i;
3393  for (i = 0; i < strlen(word); i++)
3394  if (word[i] == ':')
3395  return TRUE;
3396  return FALSE;
3397 }
3398 
3404 static Biddy_Boolean
3405 isEndOfLine(Biddy_String source)
3406 {
3407  Biddy_String pchar = strchr(source, ';');
3408  return (pchar == NULL) ? FALSE : TRUE;
3409 }
3410 
3416 static Biddy_Boolean
3417 isDefined(BiddyVerilogCircuit *c, Biddy_String name)
3418 {
3419  unsigned int i;
3420  for (i=0; (i < c->wirecount) && c->wires[i]; i++) {
3421  if (strcmp(c->nodes[c->wires[i]->id]->name, name) == 0) return TRUE;
3422  }
3423  return FALSE;
3424 }
3425 
3430 static void
3431 buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name)
3432 {
3433  n->type = strdup(type);
3434  n->name = strdup(name);
3435 }
3436 
3441 static void
3442 buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name)
3443 {
3444  int id;
3445 
3446  /* TO DO: check if wire with the same name does not already exists */
3447 
3448  if ((id = getNodeIdByName(c,name)) == -1) {
3449  printf("ERROR (buildWire): node %s does not exists!\n",name);
3450  exit(1);
3451  }
3452  w->id = id; /* wire ID */
3453  w->type = strdup(type); /* wire type */
3454  w->inputcount = 0; /* initial number of inputs */
3455  w->outputcount = 0; /* initial number of outputs */
3456  w->fanout = 0;
3457  w->ttl = 0;
3458  w->bdd = biddyNull;
3459 
3460  /* DEBUGGING */
3461  /*
3462  printf("Creating wire: id: %d, type: %s\n", w->id, w->type);
3463  */
3464 }
3465 
3471 static int
3472 getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name)
3473 {
3474  unsigned int i;
3475  if (strcmp(name,c->nodes[c->nodecount-1]->name) == 0) return (int) c->nodecount-1;
3476  for (i=0; i < c->nodecount; i++) {
3477  if (strcmp(name,c->nodes[i]->name) == 0) return (int) i;
3478  }
3479  return -1;
3480 }
3481 
3487 static BiddyVerilogWire *
3488 getWireById(BiddyVerilogCircuit *c, int id)
3489 {
3490  unsigned int i;
3491  for (i=0; i < c->wirecount; i++) {
3492  if (c->wires[i]->id == id) return c->wires[i];
3493  }
3494  return NULL;
3495 }
3496 
3502 static BiddyVerilogWire *
3503 getWireByName(BiddyVerilogCircuit *c, Biddy_String name)
3504 {
3505  unsigned int i;
3506  for (i=0; i < c->wirecount; i++) {
3507  if (strcmp(name, c->nodes[c->wires[i]->id]->name) == 0) return c->wires[i];
3508  }
3509  return NULL;
3510 }
3511 
3516 static Biddy_String
3517 trim(Biddy_String source)
3518 {
3519  unsigned int sr_length;
3520 
3521  sr_length = (unsigned int) strlen(source);
3522  while (sr_length && ((source[sr_length-1] == ' ') ||
3523  (source[sr_length-1] == '\t') ||
3524  (source[sr_length-1] == 10) ||
3525  (source[sr_length-1] == 13)))
3526  {
3527  source[sr_length-1] = 0;
3528  sr_length = (unsigned int) strlen(source);
3529  }
3530 
3531  return source;
3532 }
3533 
3534 static void
3535 concat(char **s1, const char *s2)
3536 {
3537  if (s2) {
3538  *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1+1);
3539  strcat(*s1," ");
3540  strcat(*s1,s2);
3541  }
3542 }
3543 
3544 static void
3545 WriteBDD(Biddy_Manager MNG, Biddy_Edge f)
3546 {
3547  Biddy_Variable v;
3548  Biddy_String var;
3549 
3550  if (Biddy_GetMark(f)) {
3551  printf("*");
3552  }
3553  if ((v = Biddy_GetTag(f))) {
3554  printf("<%s>",Biddy_Managed_GetVariableName(MNG,v));
3555  }
3556 
3557  var = Biddy_Managed_GetTopVariableName(MNG,f);
3558  printf("%s",var);
3559 
3560  if (!Biddy_IsTerminal(f)) {
3561  printf("(");
3562  WriteBDD(MNG,BiddyE(f));
3563  printf(")(");
3564  WriteBDD(MNG,BiddyT(f));
3565  printf(")");
3566  }
3567 }
3568 
3569 static void
3570 WriteBDDx(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f, unsigned int *line)
3571 {
3572  Biddy_String var;
3573 
3574  if (Biddy_GetMark(f)) {
3575  fprintf(funfile,"* ");
3576  }
3577 
3578  *line = *line + 2;
3579 
3580  var = Biddy_Managed_GetTopVariableName(MNG,f);
3581  fprintf(funfile,"%s",var);
3582 
3583  *line = *line + (unsigned int)strlen(var);
3584 
3585  if (!Biddy_IsTerminal(f)) {
3586  if (*line >= 80) {
3587  fprintf(funfile,"\n");
3588  *line = 0;
3589  }
3590  fprintf(funfile," (");
3591  *line = *line + 2;
3592  WriteBDDx(MNG,funfile,BiddyE(f),line);
3593  if (*line >= 80) {
3594  fprintf(funfile,"\n");
3595  *line = 0;
3596  }
3597  fprintf(funfile,") (");
3598  *line = *line + 3;
3599  WriteBDDx(MNG,funfile,BiddyT(f),line);
3600  if (*line >= 80) {
3601  fprintf(funfile,"\n");
3602  *line = 0;
3603  }
3604  fprintf(funfile,")");
3605  *line = *line + 1;
3606  }
3607 }
3608 
3609 static Biddy_Boolean
3610 WriteProduct(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
3611 {
3612  /* DEBUGGING */
3613  /*
3614  typedef struct LIMIT {
3615  unsigned int part;
3616  unsigned int w;
3617  } LIMIT;
3618  void *data;
3619  */
3620 
3621  /* ITERATIVE VARIANT */
3622  /* LITERALS ARE ADDED IN REVERSE ORDERING */
3623  /*
3624  while (l) {
3625  if (combinationset) {
3626  if (!l->negative) {
3627  if (first) first = FALSE; else printf(",");
3628  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3629  } else {
3630  printf(" ");
3631  if (l->negative) {
3632  printf("*");
3633  }
3634  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3635  }
3636  l = l->next;
3637  }
3638  */
3639 
3640  /* RECURSIVE VARIANT */
3641  /* LITERALS ARE ADDED IN REVERSE ORDERING BUT THIS WILL REVERSE THE OUTPUT */
3642 
3643  if (l) {
3644  if (combinationset) {
3645  first = WriteProduct(MNG,l->next,combinationset,first);
3646  if (!l->negative) {
3647  if (first) first = FALSE; else printf(" ");
3648  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3649 
3650  /* DEBUGGING */
3651  /*
3652  if ((data = Biddy_Managed_GetVariableData(MNG,l->v))) {
3653  printf("<%u>",((LIMIT *) data)->w);
3654  }
3655  */
3656 
3657  }
3658  } else {
3659  WriteProduct(MNG,l->next,combinationset,first);
3660  printf(" ");
3661  if (l->negative) {
3662  printf("*");
3663  }
3664  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3665  }
3666  }
3667 
3668 
3669  return first;
3670 }
3671 
3672 static Biddy_Boolean
3673 WriteProductx(Biddy_Manager MNG, FILE *s, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
3674 {
3675  if (l) {
3676  if (combinationset) {
3677  first = WriteProductx(MNG,s,l->next,combinationset,first);
3678  if (!l->negative) {
3679  if (!first) fprintf(s,","); else first = FALSE;
3680  fprintf(s,"%s",Biddy_Managed_GetVariableName(MNG,l->v));
3681  }
3682  } else {
3683  WriteProductx(MNG,s,l->next,combinationset,first);
3684  fprintf(s," ");
3685  if (l->negative) {
3686  fprintf(s,"*");
3687  }
3688  fprintf(s,"%s",Biddy_Managed_GetVariableName(MNG,l->v));
3689  }
3690  }
3691  return first;
3692 }
3693 
3694 static void
3695 WriteProductAlphabetic(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
3696 {
3697  BiddyVarList *tmp;
3698  Biddy_String tmpname,minname,prevname;
3699 
3700  if (l) {
3701  if (combinationset) {
3702  prevname = NULL;
3703  do {
3704  tmp = l;
3705  minname = NULL;
3706  while (tmp) {
3707  if (!tmp->negative) {
3708  tmpname = Biddy_Managed_GetVariableName(MNG,tmp->v);
3709  if ((!minname || (strcmp(tmpname,minname)<0)) && (!prevname || (strcmp(tmpname,prevname)>0))) {
3710  minname = tmpname;
3711  }
3712  }
3713  tmp = tmp->next;
3714  }
3715  if (minname) {
3716  if (!first) printf(","); else first = FALSE;
3717  printf("%s",minname);
3718  prevname = minname;
3719  }
3720  } while (minname);
3721  } else {
3722  /* NOT IMPLEMENTED, YET */
3723  }
3724  }
3725 }
3726 
3727 static void
3728 WriteSOP(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable top,
3729  Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize,
3730  Biddy_Boolean combinationset)
3731 {
3732  BiddyVarList tmp;
3733  Biddy_Variable v;
3734 
3735  /* parameter combinationset is meaningful for ZBDDs and TZBDDs, only */
3736 
3737  if ((!combinationset) && (*maxsize == 0)) return; /* SOP to large */
3738 
3739  v = BiddyV(f);
3740 
3741  /* DEBUGGING */
3742  /*
3743  printf("WriteSOP: top = %u (%s), v = %u (%s)\n",top,Biddy_Managed_GetVariableName(MNG,top),v,Biddy_Managed_GetVariableName(MNG,v));
3744  */
3745 
3746  assert( !(BiddyIsSmaller(BiddyV(f),top)) );
3747 
3748  if ((top != v) && (f != biddyZero)) {
3749 
3750  if (biddyManagerType == BIDDYTYPEOBDD) {
3751  /* NO ACTION IS NEEDED */
3752  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3753  /* NO ACTION IS NEEDED */
3754  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3755  tmp.next = l;
3756  tmp.v = top;
3757  tmp.negative = TRUE; /* negative literal */
3758  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3759  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3760  tmp.next = l;
3761  tmp.v = top;
3762  tmp.negative = TRUE; /* negative literal */
3763  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3764  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3765  tmp.next = l;
3766  tmp.v = top;
3767  tmp.negative = TRUE; /* negative literal */
3768  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3769  if (combinationset && Biddy_Managed_IsSmaller(MNG,top,Biddy_GetTag(f))) {
3770  tmp.negative = FALSE; /* positive literal */
3771  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3772  }
3773  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3774  {
3775  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3776  return;
3777  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
3778  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
3779  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
3780  {
3781  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3782  return;
3783  } else {
3784  fprintf(stderr,"WriteSOP: Unsupported BDD type!\n");
3785  return;
3786  }
3787 
3788  } else if (v == 0) {
3789 
3790  if (combinationset) {
3791  if (!mark) {
3792  if (l) {
3793  /* printf("{"); */
3794  /* WriteProductAlphabetic(MNG,l,combinationset,TRUE); */
3795  WriteProduct(MNG,l,combinationset,TRUE);
3796  /* printf("}"); */
3797  printf(" ; ");
3798  (*maxsize)--;
3799  } else {
3800  /* printf("{}"); */
3801  printf(",");
3802  }
3803  } else {
3804  if (!l) {
3805  printf("EMPTY");
3806  }
3807  }
3808  } else {
3809  if (!mark) {
3810  printf(" + ");
3811  if (l) {
3812  WriteProduct(MNG,l,combinationset,TRUE);
3813  printf("\n");
3814  (*maxsize)--;
3815  } else {
3816  printf(" 1");
3817  }
3818  } else {
3819  if (!l) {
3820  printf(" + 0");
3821  }
3822  }
3823  }
3824 
3825  } else {
3826 
3827  tmp.next = l;
3828  tmp.v = v;
3829 
3830  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3831  tmp.negative = TRUE; /* left successor */
3832  WriteSOP(MNG,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3833  }
3834  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3835  if (combinationset) {
3836  tmp.negative = FALSE; /* right successor for combination sets */
3837  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3838  } else {
3839  tmp.negative = TRUE; /* left successor for Boolean function */
3840  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3841  }
3842  }
3843  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3844  if (combinationset) {
3845  tmp.negative = FALSE; /* right successor for combination sets */
3846  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3847  } else {
3848  tmp.negative = TRUE; /* left successor for Boolean function */
3849  WriteSOP(MNG,BiddyE(f),Biddy_GetTag(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3850  }
3851  }
3852 
3853  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3854  tmp.negative = FALSE; /* right successor */
3855  WriteSOP(MNG,BiddyT(f),BiddyV(BiddyT(f)),(mark ^ Biddy_GetMark(BiddyT(f))),&tmp,maxsize,combinationset);
3856  }
3857  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3858  if (combinationset) {
3859  tmp.negative = TRUE; /* left successor for combination sets */
3860  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3861  } else {
3862  tmp.negative = FALSE; /* right successor for Boolean function */
3863  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3864  }
3865  }
3866  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3867  if (combinationset) {
3868  tmp.negative = TRUE; /* left successor for combination sets */
3869  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3870  } else {
3871  tmp.negative = FALSE; /* right successor for Boolean function */
3872  WriteSOP(MNG,BiddyT(f),Biddy_GetTag(BiddyT(f)),Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3873  }
3874  }
3875 
3876  }
3877 }
3878 
3879 static void
3880 WriteSOPx(Biddy_Manager MNG, FILE *s, Biddy_Edge f, Biddy_Variable top,
3881  Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize,
3882  Biddy_Boolean combinationset)
3883 {
3884  BiddyVarList tmp;
3885  Biddy_Variable v;
3886 
3887  if ((!combinationset) && (*maxsize == 0)) return; /* SOP to large */
3888 
3889  v = BiddyV(f);
3890 
3891  /* DEBUGGING */
3892  /*
3893  printf("WriteSOPx: top = %u (%s), v = %u (%s)\n",top,Biddy_Managed_GetVariableName(MNG,top),v,Biddy_Managed_GetVariableName(MNG,v));
3894  */
3895 
3896  assert( !(BiddyIsSmaller(BiddyV(f),top)) );
3897 
3898  if ((top != v) && (f != biddyZero)) {
3899 
3900  if (biddyManagerType == BIDDYTYPEOBDD) {
3901  /* IMPLEMENTED */
3902  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3903  /* IMPLEMENTED */
3904  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3905  /* IMPLEMENTED */
3906  tmp.next = l;
3907  tmp.v = top;
3908  tmp.negative = TRUE; /* left successor */
3909  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3910  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3911  /* IMPLEMENTED */
3912  tmp.next = l;
3913  tmp.v = top;
3914  tmp.negative = TRUE; /* left successor */
3915  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3916  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3917  /* IMPLEMENTED */
3918  tmp.next = l;
3919  tmp.v = top;
3920  tmp.negative = TRUE; /* left successor */
3921  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
3922  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3923  {
3924  fprintf(stderr,"WriteSOPx: this BDD type is not supported, yet!\n");
3925  return;
3926  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
3927  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
3928  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
3929  {
3930  fprintf(stderr,"WriteSOPx: this BDD type is not supported, yet!\n");
3931  return;
3932  } else {
3933  fprintf(stderr,"WriteSOPx: Unsupported BDD type!\n");
3934  return;
3935  }
3936 
3937  } else if (v == 0) {
3938 
3939  if (combinationset) {
3940  } else {
3941  if (!mark) {
3942  fprintf(s," + ");
3943  if (l) {
3944  WriteProductx(MNG,s,l,combinationset,TRUE);
3945  fprintf(s,"\n");
3946  (*maxsize)--;
3947  } else {
3948  fprintf(s," 1");
3949  }
3950  } else {
3951  if (!l) {
3952  fprintf(s," + 0");
3953  }
3954  }
3955  }
3956 
3957  } else {
3958 
3959  tmp.next = l;
3960  tmp.v = v;
3961  tmp.negative = TRUE; /* left successor */
3962 
3963  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3964  WriteSOPx(MNG,s,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3965  }
3966  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3967  WriteSOPx(MNG,s,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3968  }
3969  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3970  WriteSOPx(MNG,s,BiddyE(f),Biddy_GetTag(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize,combinationset);
3971  }
3972 
3973  tmp.negative = FALSE; /* right successor */
3974 
3975  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3976  WriteSOPx(MNG,s,BiddyT(f),BiddyV(BiddyT(f)),(mark ^ Biddy_GetMark(BiddyT(f))),&tmp,maxsize,combinationset);
3977  }
3978  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3979  WriteSOPx(MNG,s,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3980  }
3981  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3982  WriteSOPx(MNG,s,BiddyT(f),Biddy_GetTag(BiddyT(f)),Biddy_GetMark(BiddyT(f)),&tmp,maxsize,combinationset);
3983  }
3984 
3985  }
3986 }
3987 
3988 static unsigned int
3989 enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n)
3990 {
3991  if (!Biddy_Managed_IsSelected(MNG,f)) {
3992  if (Biddy_IsTerminal(f)) {
3993  } else {
3994  Biddy_Managed_SelectNode(MNG,f);
3995  n++;
3996  BiddySetEnumerator(f,n);
3997 
3998  /* one or both are terminal node */
3999  /* every instance of terminal node is enumerated */
4000  if (Biddy_IsTerminal(BiddyE(f)) || Biddy_IsTerminal(BiddyT(f))) {
4001 
4002  if (((biddyManagerType == BIDDYTYPEOBDD) ||
4003  (biddyManagerType == BIDDYTYPEZBDD) ||
4004  (biddyManagerType == BIDDYTYPETZBDD)
4005  ) && (Biddy_GetMark(BiddyE(f)) != Biddy_GetMark(BiddyT(f))))
4006  {
4007  /* two terminal nodes only if complemented edges are not used and they are different */
4008  if (Biddy_IsTerminal(BiddyE(f))) {
4009  n++;
4010  }
4011  if (Biddy_IsTerminal(BiddyT(f))) {
4012  n++;
4013  }
4014  }
4015  else {
4016  /* only one terminal node */
4017  n++;
4018  }
4019 
4020  }
4021 
4022  if (!Biddy_IsTerminal(BiddyE(f))) {
4023  n = enumerateNodes(MNG,BiddyE(f),n);
4024  }
4025  if (!Biddy_IsTerminal(BiddyT(f))) {
4026  n = enumerateNodes(MNG,BiddyT(f),n);
4027  }
4028  }
4029  }
4030  return n;
4031 }
4032 
4033 static void
4034 WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd)
4035 {
4036  BiddyLocalInfo *li;
4037  Biddy_String name,hash;
4038  Biddy_Variable v;
4039  BiddyLocalInfo *li2;
4040 
4041  if (Biddy_IsTerminal(f)) {
4042  if (cudd) {
4043 
4044  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
4045  /*
4046  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
4047  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
4048  fprintf(dotfile,"\"%p\";\n",biddyOne);
4049  */
4050 
4051  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
4052 
4053  fprintf(dotfile,"{ \"CONST NODES\";\n");
4054  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
4055  fprintf(dotfile,"\"1\";\n");
4056 
4057 
4058  fprintf(dotfile,"}\n}\n");
4059  } else {
4060  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4061  (biddyManagerType == BIDDYTYPEZBDD) ||
4062  (biddyManagerType == BIDDYTYPETZBDD))
4063  {
4064  if (f == biddyZero) {
4065  fprintf(dotfile, " node [shape = none, label = \"0\"] %u;\n",1);
4066  } else {
4067  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
4068  }
4069  }
4070  else {
4071  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
4072  }
4073  }
4074  return;
4075  }
4076  if (cudd) {
4078  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4079  while (li->back) {
4080  v = BiddyV(li->back);
4081  if (biddyVariableTable.table[v].value == biddyZero) {
4082  biddyVariableTable.table[v].value = biddyOne;
4083  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
4084  while ((hash = strchr(name,'#'))) hash[0] = '_';
4085  fprintf(dotfile,"{ rank = same; ");
4086  fprintf(dotfile,"\" %s \";\n",name);
4087  free(name);
4088  li2 = li;
4089  while (li2->back) {
4090  if (BiddyV(li2->back) == v) {
4091  fprintf(dotfile,"\"%p\";\n",li2->back);
4092  }
4093  li2 = &li2[1]; /* next field in the array */
4094  }
4095  fprintf(dotfile,"}\n");
4096  }
4097  li = &li[1]; /* next field in the array */
4098  }
4100 
4101  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
4102  /*
4103  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
4104  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
4105  fprintf(dotfile,"\"%p\";\n",biddyOne);
4106  */
4107 
4108  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
4109 
4110  fprintf(dotfile,"{ \"CONST NODES\";\n");
4111  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
4112  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4113  while (li->back) {
4114  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
4115  fprintf(dotfile,"\"%u\";\n",li->data.enumerator+1);
4116  }
4117  li = &li[1];
4118  }
4119 
4120 
4121  fprintf(dotfile,"}\n}\n");
4122  } else {
4123  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4124  while (li->back) {
4125  if (id == -1) {
4126  name = getname(MNG,li->back);
4127  } else {
4128  name = getshortname(MNG,li->back,id);
4129  }
4130  while ((hash = strchr(name,'#'))) hash[0] = '_';
4131  fprintf(dotfile," node [shape = circle, label = \"%s\"] %u;\n",name,li->data.enumerator);
4132  free(name);
4133  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4134  (biddyManagerType == BIDDYTYPEZBDD) ||
4135  (biddyManagerType == BIDDYTYPETZBDD))
4136  {
4137  if (BiddyE(li->back) == biddyZero) {
4138  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
4139  }
4140  else if (Biddy_IsTerminal(BiddyE(li->back))) {
4141  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4142  }
4143  if (BiddyT(li->back) == biddyZero) {
4144  if (Biddy_IsTerminal(BiddyE(li->back)) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back)))) {
4145  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+2);
4146  } else {
4147  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
4148  }
4149  }
4150  else if (Biddy_IsTerminal(BiddyT(li->back))) {
4151  if (Biddy_IsTerminal(BiddyE(li->back)) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back)))) {
4152  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+2);
4153  } else {
4154  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4155  }
4156  }
4157  }
4158  else {
4159  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
4160  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4161  }
4162  }
4163  li = &li[1]; /* next field in the array */
4164  }
4165  }
4166 }
4167 
4168 static void
4169 WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd)
4170 {
4171  unsigned int n1,n2;
4172  Biddy_Variable tag;
4173 
4174  if (!Biddy_IsTerminal(f) && !Biddy_Managed_IsSelected(MNG,f)) {
4175  Biddy_Managed_SelectNode(MNG,f);
4176  n1 = BiddyGetEnumerator(f);
4177 
4178  if (Biddy_IsTerminal(BiddyE(f))) {
4179  n2 = n1 + 1;
4180  } else {
4181  n2 = BiddyGetEnumerator(BiddyE(f));
4182  }
4183  if (Biddy_GetMark(BiddyE(f))) {
4184  if ((BiddyE(f) != biddyZero) && (tag = Biddy_GetTag(BiddyE(f)))) {
4185  if (cudd) {
4186 
4187  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4188  /*
4189  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4190  */
4191 
4192  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4193 
4194  if (Biddy_IsTerminal(BiddyE(f))) {
4195  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4196  } else {
4197  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4198  }
4199 
4200 
4201  } else {
4202 #ifdef LEGACY_DOT
4203  fprintf(dotfile," %u -> %u [style=dotted label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4204 #else
4205  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4206 #endif
4207  }
4208  } else {
4209  if (cudd) {
4210 
4211  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4212  /*
4213  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
4214  */
4215 
4216  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4217 
4218  if (Biddy_IsTerminal(BiddyE(f))) {
4219  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted];\n",BiddyP(f),n2);
4220  } else {
4221  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
4222  }
4223 
4224 
4225  } else {
4226  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4227  (biddyManagerType == BIDDYTYPEZBDD) ||
4228  (biddyManagerType == BIDDYTYPETZBDD))
4229  {
4230 #ifdef LEGACY_DOT
4231  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
4232 #else
4233  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
4234 #endif
4235  }
4236  else {
4237 #ifdef LEGACY_DOT
4238  fprintf(dotfile," %u -> %u [style=dotted];\n",n1,n2);
4239 #else
4240  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\"];\n",n1,n2);
4241 #endif
4242  }
4243  }
4244  }
4245  } else {
4246  if ((BiddyE(f) != biddyZero) && (tag = Biddy_GetTag(BiddyE(f)))) {
4247  if (cudd) {
4248 
4249  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4250  /*
4251  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4252  */
4253 
4254  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4255 
4256  if (Biddy_IsTerminal(BiddyE(f))) {
4257  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4258  } else {
4259  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4260  }
4261 
4262 
4263  } else {
4264 #ifdef LEGACY_DOT
4265  fprintf(dotfile," %u -> %u [style=dashed label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4266 #else
4267  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4268 #endif
4269  }
4270  } else {
4271  if (cudd) {
4272 
4273  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4274  /*
4275  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
4276  */
4277 
4278  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4279 
4280  if (Biddy_IsTerminal(BiddyE(f))) {
4281  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed];\n",BiddyP(f),n2);
4282  } else {
4283  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
4284  }
4285 
4286 
4287  } else {
4288 #ifdef LEGACY_DOT
4289  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
4290 #else
4291  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
4292 #endif
4293  }
4294  }
4295  }
4296 
4297  if (Biddy_IsTerminal(BiddyT(f))) {
4298  if (((biddyManagerType == BIDDYTYPEOBDD) ||
4299  (biddyManagerType == BIDDYTYPEZBDD) ||
4300  (biddyManagerType == BIDDYTYPETZBDD))
4301  && (Biddy_IsTerminal(BiddyE(f)))
4302  && (Biddy_GetMark(BiddyE(f)) != Biddy_GetMark(BiddyT(f))))
4303  {
4304  n2 = n1 + 2;
4305  }
4306  else {
4307  n2 = n1 + 1;
4308  }
4309  } else {
4310  n2 = BiddyGetEnumerator(BiddyT(f));
4311  }
4312  if (Biddy_GetMark(BiddyT(f))) {
4313  if ((BiddyT(f) != biddyZero) && (tag = Biddy_GetTag(BiddyT(f)))) {
4314  if (cudd) {
4315 
4316  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4317  /*
4318  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4319  */
4320 
4321  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4322 
4323  if (Biddy_IsTerminal(BiddyT(f))) {
4324  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4325  } else {
4326  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4327  }
4328 
4329 
4330  } else {
4331 #ifdef LEGACY_DOT
4332  fprintf(dotfile," %d -> %d [style=bold label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4333 #else
4334  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4335 #endif
4336  }
4337  } else {
4338  if (cudd) {
4339 
4340  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4341  /*
4342  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
4343  */
4344 
4345  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4346 
4347  if (Biddy_IsTerminal(BiddyT(f))) {
4348  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold];\n",BiddyP(f),n2);
4349  } else {
4350  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
4351  }
4352 
4353 
4354  } else {
4355  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4356  (biddyManagerType == BIDDYTYPEZBDD) ||
4357  (biddyManagerType == BIDDYTYPETZBDD))
4358  {
4359 #ifdef LEGACY_DOT
4360  fprintf(dotfile," %d -> %d;\n",n1,n2);
4361 #else
4362  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
4363 #endif
4364  }
4365  else {
4366 #ifdef LEGACY_DOT
4367  fprintf(dotfile," %d -> %d [style=bold];\n",n1,n2);
4368 #else
4369  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\"];\n",n1,n2);
4370 #endif
4371  }
4372  }
4373  }
4374  } else {
4375  if ((BiddyT(f) != biddyZero) && (tag = Biddy_GetTag(BiddyT(f)))) {
4376  if (cudd) {
4377 
4378  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4379  /*
4380  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4381  */
4382 
4383  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4384 
4385  if (Biddy_IsTerminal(BiddyT(f))) {
4386  fprintf(dotfile,"\"%p\" -> \"%u\" [label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4387  } else {
4388  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4389  }
4390 
4391 
4392  } else {
4393 #ifdef LEGACY_DOT
4394  fprintf(dotfile," %d -> %d [label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4395 #else
4396  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4397 #endif
4398  }
4399  } else {
4400  if (cudd) {
4401 
4402  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4403  /*
4404  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
4405  */
4406  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4407 
4408 
4409  if (Biddy_IsTerminal(BiddyT(f))) {
4410  fprintf(dotfile,"\"%p\" -> \"%u\";\n",BiddyP(f),n2);
4411  } else {
4412  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
4413  }
4414 
4415 
4416  } else {
4417 #ifdef LEGACY_DOT
4418  fprintf(dotfile," %d -> %d [style=solid];\n",n1,n2);
4419 #else
4420  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
4421 #endif
4422  }
4423  }
4424  }
4425 
4426  WriteDotEdges(MNG,dotfile,BiddyE(f),cudd);
4427  WriteDotEdges(MNG,dotfile,BiddyT(f),cudd);
4428  }
4429 }
4430 
4431 static void
4432 WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f)
4433 {
4434  int n1,n2;
4435  Biddy_Variable tag1,tag2;
4436 
4437  if (!Biddy_IsTerminal(f) && !Biddy_Managed_IsSelected(MNG,f)) {
4438  Biddy_Managed_SelectNode(MNG,f);
4439  n1 = BiddyGetEnumerator(f);
4440 
4441  /* if successors are equal then double line is possible */
4442  if ((BiddyP(BiddyE(f)) != BiddyP(BiddyT(f))) ||
4443  (((biddyManagerType == BIDDYTYPEOBDD) ||
4444  (biddyManagerType == BIDDYTYPEZBDD) ||
4445  (biddyManagerType == BIDDYTYPETZBDD))
4446  &&
4447  (Biddy_GetMark((BiddyE(f))) != Biddy_GetMark((BiddyT(f)))))
4448  )
4449  {
4450 
4451  unsigned int num;
4452 
4453  /* SINGLE LINE */
4454 
4455  num = 0;
4456  if (Biddy_IsTerminal(BiddyE(f))) {
4457  n2 = n1 + 1;
4458  num = 1;
4459  } else {
4460  n2 = BiddyGetEnumerator(BiddyE(f));
4461  }
4462  fprintf(funfile,"connect %d %d ",n1,n2);
4463  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4464  (biddyManagerType == BIDDYTYPEZBDD) ||
4465  (biddyManagerType == BIDDYTYPETZBDD))
4466  {
4467  fprintf(funfile,"l");
4468  }
4469  else {
4470  if (Biddy_GetMark((BiddyE(f)))) {
4471  fprintf(funfile,"li");
4472  } else {
4473  fprintf(funfile,"l");
4474  }
4475  }
4476  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4477  {
4478  if (BiddyE(f) == biddyZero) {
4479  fprintf(funfile," 0\n");
4480  } else {
4481  tag1 = Biddy_GetTag(BiddyE(f));
4482  fprintf(funfile," %s\n",Biddy_Managed_GetVariableName(MNG,tag1));
4483  }
4484  } else {
4485  fprintf(funfile,"\n");
4486  }
4487 
4488  if (Biddy_IsTerminal(BiddyT(f))) {
4489  n2 = n1 + num + 1;
4490  } else {
4491  n2 = BiddyGetEnumerator(BiddyT(f));
4492  }
4493  fprintf(funfile,"connect %d %d ",n1,n2);
4494  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4495  (biddyManagerType == BIDDYTYPEZBDD) ||
4496  (biddyManagerType == BIDDYTYPETZBDD))
4497  {
4498  fprintf(funfile,"r");
4499  }
4500  else {
4501  if (Biddy_GetMark((BiddyT(f)))) {
4502  fprintf(funfile,"ri");
4503  } else {
4504  fprintf(funfile,"r");
4505  }
4506  }
4507  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4508  {
4509  if (BiddyT(f) == biddyZero) {
4510  fprintf(funfile," 0\n");
4511  } else {
4512  tag2 = Biddy_GetTag(BiddyT(f));
4513  fprintf(funfile," %s\n",Biddy_Managed_GetVariableName(MNG,tag2));
4514  }
4515  } else {
4516  fprintf(funfile,"\n");
4517  }
4518 
4519  } else {
4520 
4521  /* DOUBLE LINE */
4522 
4523  if (Biddy_IsTerminal(BiddyE(f))) {
4524  n2 = n1 + 1;
4525  } else {
4526  n2 = BiddyGetEnumerator(BiddyE(f));
4527  }
4528 
4529  fprintf(funfile,"connect %d %d ",n1,n2);
4530  if (Biddy_GetMark((BiddyE(f)))) {
4531  if (Biddy_GetMark((BiddyT(f)))) {
4532  fprintf(funfile,"ei");
4533  } else {
4534  fprintf(funfile,"d");
4535  }
4536  } else {
4537  if (Biddy_GetMark((BiddyT(f)))) {
4538  fprintf(funfile,"di");
4539  } else {
4540  fprintf(funfile,"e");
4541  }
4542  }
4543  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4544  {
4545  tag1 = Biddy_GetTag(BiddyE(f));
4546  tag2 = Biddy_GetTag(BiddyT(f));
4547  fprintf(funfile," %s %s\n",Biddy_Managed_GetVariableName(MNG,tag1),Biddy_Managed_GetVariableName(MNG,tag2));
4548  } else {
4549  fprintf(funfile,"\n");
4550  }
4551 
4552  }
4553 
4554  WriteBddviewConnections(MNG,funfile,BiddyE(f));
4555  WriteBddviewConnections(MNG,funfile,BiddyT(f));
4556  }
4557 }
4558 
4559 static Biddy_String
4560 getname(Biddy_Manager MNG, void *p)
4561 {
4562  unsigned int i;
4563  Biddy_String newname;
4564 
4565  if ((p == biddyZero) &&
4566  ((biddyManagerType == BIDDYTYPEOBDD) ||
4567  (biddyManagerType == BIDDYTYPEZBDD) ||
4568  (biddyManagerType == BIDDYTYPETZBDD)))
4569  {
4570  newname = strdup("0");
4571  return (newname);
4572  }
4573 
4574  newname = strdup(Biddy_Managed_GetTopVariableName(MNG,(Biddy_Edge) p));
4575  for (i=0; i<strlen(newname); ++i) {
4576  if (newname[i] == '<') newname[i] = '_';
4577  if (newname[i] == '>') newname[i] = 0;
4578  }
4579 
4580  return (newname);
4581 }
4582 
4583 static Biddy_String
4584 getshortname(Biddy_Manager MNG, void *p, int n)
4585 {
4586  unsigned int i;
4587  Biddy_String name;
4588  Biddy_String shortname;
4589 
4590  name = strdup(Biddy_Managed_GetTopVariableName(MNG,(Biddy_Edge) p));
4591  i = (unsigned int)strcspn(name,"<");
4592  name[i]=0;
4593  shortname = strdup(name);
4594  free(name);
4595 
4596  return (shortname);
4597 }
4598 
4599 static void
4600 reportOrdering()
4601 {
4602  Biddy_Variable var;
4603 
4604  printf("Variable ordering:\n");
4605  var = Biddy_GetLowestVariable();
4606  while (var != 0) {
4607  printf("(%s)",Biddy_GetVariableName(var));
4608  var = Biddy_GetNextVariable(var);
4609  }
4610  printf("\n");
4611 }
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