Biddy  1.8.1
An academic Binary Decision Diagrams package
biddyInOut.c
Go to the documentation of this file.
1 /***************************************************************************/
47 #include "biddyInt.h"
48 
49 /* the following constants and types are used in Biddy_ReadVerilogFile() */
50 #define LINESIZE 999 /* maximum length of each input line read */
51 #define BUFSIZE 99999 /* maximum length of a buffer */
52 #define INOUTNUM 999 /* maximum number of inputs and outputs */
53 #define REGNUM 9999 /* maximum number of registers */
54 #define TOKENNUM 9999 /* maximum number of tokens */
55 #define GATENUM 9999 /* maximum number of gates */
56 #define LINENUM 99999 /* maximum number of lines */
57 #define WIRENUM 99999 /* maximum number of wires */
58 
59 /* recognized Verilog Boolean operators */
60 /* some of them are not very standard but they are used in various benchmarks */
61 /* we are trying to accept everything which is not in direct conflict with the standard */
62 /* https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ite_r_verilog_reserved_words.htm */
63 /* http://sutherland-hdl.com/pdfs/verilog_2001_ref_guide.pdf, page 3 */
64 /* http://www.externsoft.ch/download/verilog.html */
65 #define GATESNUM 9
66 const char* VerilogFileGateName[] = {
67  "buf",
68  "and",
69  "nand",
70  "or",
71  "nor",
72  "xor",
73  "xnor",
74  "not", "inv"
75 };
76 
77 /*----------------------------------------------------------------------------*/
78 /* Static function prototypes */
79 /*----------------------------------------------------------------------------*/
80 
81 /* The following functions are used in Biddy_Eval0(), Biddy_Eval1(), and Biddy_Eval1x(). */
82 
83 static Biddy_Boolean charOK(char c);
84 static void nextCh(Biddy_String s, int *i, Biddy_String *ch);
85 
86 /* Function ReadBDD()is used in Biddy_Eval0(). */
87 
88 static Biddy_Edge ReadBDD(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch);
89 
90 /* The following functions are used in Biddy_Eval1() and Biddy_Eval1x(). */
91 
92 static Biddy_Edge evaluate1(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch, Biddy_LookupFunction lf);
93 static Biddy_Edge evaluateN(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch, Biddy_Edge g, int op, Biddy_LookupFunction lf);
94 static int Op(Biddy_String s, int *i, Biddy_String *ch);
95 
96 /* Functions createVariablesFromBTree and createBddFromBTree() are used in Biddy_Eval2(). */
97 
98 static void createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree);
99 static Biddy_Edge createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i);
100 
101 /* The following functions are used in Biddy_ReadVerilogFile(). */
102 static void parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt);
103 static void createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c);
104 static void createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix);
105 static void parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count);
106 static void printModuleSummary(BiddyVerilogModule *m);
107 static void printCircuitSummary(BiddyVerilogCircuit *c);
108 static Biddy_Boolean isGate(Biddy_String word);
109 static Biddy_Boolean isSignalVector(Biddy_String word);
110 static Biddy_Boolean isEndOfLine(Biddy_String source);
111 static Biddy_Boolean isDefined(BiddyVerilogCircuit *c, Biddy_String name);
112 static void buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name);
113 static void buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name);
114 static int getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name);
115 static BiddyVerilogWire *getWireById(BiddyVerilogCircuit *c, int id);
116 static BiddyVerilogWire *getWireByName(BiddyVerilogCircuit *c, Biddy_String name);
117 static Biddy_String trim(Biddy_String source);
118 static void concat(char **s1, const char *s2);
119 
120 /* Function WriteBDD() is used in Biddy_WriteBDD(). */
121 
122 static void WriteBDD(Biddy_Manager MNG, Biddy_Edge f);
123 
124 /* Function WriteBDDx() is used in Biddy_WriteBDDx(). */
125 
126 static void WriteBDDx(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f, unsigned int *line);
127 
128 /* The following functions are used in Biddy_PrintfSOP() in Biddy_WriteSOP(). */
129 
130 static void WriteProduct(Biddy_Manager MNG, BiddyVarList *l);
131 static void WriteProductx(Biddy_Manager MNG, FILE *s, BiddyVarList *l);
132 static void WriteSOP(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable top, Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize);
133 static void WriteSOPx(Biddy_Manager MNG, FILE *s, Biddy_Edge f, Biddy_Variable top, Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize);
134 
135 /* The following functions are used in Biddy_WriteDot(). */
136 
137 static unsigned int enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n);
138 static void WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd);
139 static void WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd);
140 
141 /* The following functions are used in Biddy_WriteBddview(). */
142 
143 static void WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f);
144 
145 /* Other functions that may be used everywhere */
146 
147 static Biddy_String getname(Biddy_Manager MNG, void *p);
148 static Biddy_String getshortname(Biddy_Manager MNG, void *p, int n);
149 
150 /*----------------------------------------------------------------------------*/
151 /* Definition of exported functions */
152 /*----------------------------------------------------------------------------*/
153 
154 /***************************************************************************/
167 #ifdef __cplusplus
168 extern "C" {
169 #endif
170 
173 {
174  int i;
175  Biddy_String ch;
176  Biddy_String name;
177  Biddy_Edge f;
178 
179  if (!MNG) MNG = biddyAnonymousManager;
180 
181  if ((biddyManagerType == BIDDYTYPEOBDD) || (biddyManagerType == BIDDYTYPEOBDDC)) {
182  /* IMPLEMENTED */
183  } else if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZBDDC) ||
184  (biddyManagerType == BIDDYTYPETZBDD) || (biddyManagerType == BIDDYTYPETZBDDC))
185  {
186  fprintf(stderr,"Biddy_Eval0: this BDD type is not supported, yet!\n");
187  return NULL;
188  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
189  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
190  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
191  {
192  fprintf(stderr,"Biddy_Eval0: this BDD type is not supported, yet!\n");
193  return NULL;
194  } else {
195  fprintf(stderr,"Biddy_Eval0: Unsupported BDD type!\n");
196  return NULL;
197  }
198 
199  ch = (Biddy_String) malloc(255); /* max variable name length */
200 
201  i = 0;
202  nextCh(s,&i,&ch);
203  name = strdup(ch);
204 
205  f = ReadBDD(MNG,s,&i,&ch);
206 
207  if (Biddy_IsNull(f)) {
208  printf("(Biddy_Managed_Eval0) ERROR: char %d\n",i);
209  free(ch);
210  return((Biddy_String)"");
211  } else {
212  Biddy_Managed_AddPersistentFormula(MNG,name,f);
213  }
214 
215  nextCh(s,&i,&ch);
216  if (strcmp(ch,"")) {
217  printf("(Biddy_Managed_Eval0) ERROR: extra characters\n");
218  free(ch);
219  return((Biddy_String)"");
220  }
221 
222  free(ch);
223 
224  return(name);
225 }
226 
227 #ifdef __cplusplus
228 }
229 #endif
230 
231 /***************************************************************************/
244 #ifdef __cplusplus
245 extern "C" {
246 #endif
247 
250 {
251  Biddy_Edge sup;
252  Biddy_String ch;
253  int i;
254 
255  if (!MNG) MNG = biddyAnonymousManager;
256 
257  ch = (Biddy_String) malloc(255);
258 
259  i = 0;
260  nextCh(s,&i,&ch);
261  sup = evaluate1(MNG,s,&i,&ch,lf);
262 
263  free(ch);
264 
265  if (Biddy_IsNull(sup)) {
266  printf("(Biddy_Managed_Eval1x) ERROR: return NULL\n");
267  }
268 
269  return sup;
270 }
271 
272 #ifdef __cplusplus
273 }
274 #endif
275 
276 /***************************************************************************/
294 /* USE THIS FOR DEBUGGING */
295 /*
296 static void
297 printBiddyBTreeContainer(BiddyBTreeContainer *tree)
298 {
299  int i;
300  printf("availableNode=%d\n",tree->availableNode);
301  for (i = tree->availableNode; i >= 0; i--) {
302  printf("[%d]parent=%d,left=%d,right=%d,index=%d,op=%u",i,
303  tree->tnode[i].parent,
304  tree->tnode[i].left,
305  tree->tnode[i].right,
306  tree->tnode[i].index,
307  tree->tnode[i].op
308  );
309  if (tree->tnode[i].name) {
310  printf(",name=%s\n",tree->tnode[i].name);
311  } else {
312  printf("\n");
313  }
314  }
315 }
316 
317 static void
318 printPrefixFromBTree(BiddyBTreeContainer *tree, int i)
319 {
320  if (i == -1) return;
321  if (tree->tnode[i].op == 255) {
322  if (tree->tnode[i].name) {
323  printf("%s",tree->tnode[i].name);
324  } else {
325  printf("NULL");
326  }
327  return;
328  }
329  if (tree->tnode[i].op == 0) printf("(NOT");
330  else if (tree->tnode[i].op == 1) printf("(AND ");
331  else if (tree->tnode[i].op == 2) printf("(BUTNOT ");
332  else if (tree->tnode[i].op == 4) printf("(NOTBUT ");
333  else if (tree->tnode[i].op == 6) printf("(XOR ");
334  else if (tree->tnode[i].op == 7) printf("(OR ");
335  else printf("(? ");
336  printPrefixFromBTree(tree,tree->tnode[i].left);
337  printf(" ");
338  printPrefixFromBTree(tree,tree->tnode[i].right);
339  printf(")");
340 }
341 */
342 
343 #ifdef __cplusplus
344 extern "C" {
345 #endif
346 
349 {
350  /* NOT (~!), AND (&*), OR (|+), XOR (^%) , XNOR(-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (\), AND NOTBUT (/) ARE IMPLEMENTED */
351  char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' };
352  long tempPos,currStringPos,currTreePos,oldTreePos; /* tmp variables */
353  long offset; /* this is used for implementation of parenthesis and operator's priority */
354  char currS;
355  long i,j;
356  BiddyBTreeContainer *tree;
357  Biddy_Edge fbdd; /* result */
358  Biddy_String expression;
359 
360  if (!MNG) MNG = biddyAnonymousManager;
361 
362  i = 0; j = 0;
363  tree = (BiddyBTreeContainer *) calloc(1, sizeof(BiddyBTreeContainer));
364  if (!tree) return biddyNull;
365  tree->tnode = (BiddyBTreeNode*) malloc(1024 * sizeof(BiddyBTreeNode));
366  if (!tree->tnode) return biddyNull;
367  tree->availableNode = -1;
368  for (i = 1023; i > 0; i--) {
369  tree->tnode[i].name = NULL;
370  tree->tnode[i].parent = tree->availableNode;
371  tree->availableNode = i;
372  }
373  tree->tnode[0].index = 0;
374  tree->tnode[0].name = NULL;
375 
376  tempPos = 0;
377  currStringPos = 0;
378  currTreePos = 1;
379  oldTreePos = 0;
380  offset = 0;
381  expression = strdup(boolFunc);
382  currS = expression[currStringPos];
383  while (currS > '\n') {
384  if (currS == ' ') {
385  /* WHITE SPACE */
386  currStringPos++;
387  currS = expression[currStringPos];
388  continue;
389  }
390  currTreePos = tree->availableNode;
391  if (currTreePos != -1) {
392  tree->availableNode = tree->tnode[tree->availableNode].parent;
393  } else {
394  fprintf(stderr,"ERROR: SOMETHING WRONG WITH tree->availableNode\n");
395  return biddyNull;
396  }
397  if (j == 0) {
398  tree->tnode[oldTreePos].right = currTreePos;
399  tree->tnode[currTreePos].parent = oldTreePos;
400  tree->tnode[currTreePos].left = -1;
401  if (currS == '!') currS = '~'; /* operator '!' is also allowed for negation */
402  if (currS == boolOperators[0]) {
403  /* UNARY OPERATOR NOT */
404  tree->tnode[currTreePos].op = 0;
405  tree->tnode[currTreePos].index = offset + 3;
406  }
407  else if ((currS == '(') || (currS == '[') || (currS == '{')) {
408  /* OPEN PARENTHESIS */
409  offset += 4; currStringPos++;
410  currS = expression[currStringPos];
411  continue;
412  }
413  else if ((currS == '_') || ((currS >= '0') && (currS <= '9')) || ((currS >= 'A') && (currS <= 'Z')) || ((currS >= 'a') && (currS <= 'z'))) {
414  /* CONSTANT OR VARIABLE NAME */
415  tree->tnode[currTreePos].right = -1;
416  tree->tnode[currTreePos].op = 255;
417  tree->tnode[currTreePos].index = currStringPos;
418  while ((currS == '_') || ((currS >= '0') && (currS <= '9')) || ((currS >= 'A') && (currS <= 'Z')) || ((currS >= 'a') && (currS <= 'z'))) {
419  currStringPos++;
420  currS = expression[currStringPos];
421  }
422  expression[currStringPos] = 0;
423  tree->tnode[currTreePos].name = strdup(&expression[tree->tnode[currTreePos].index]);
424  tree->tnode[currTreePos].index = (int) strlen(tree->tnode[currTreePos].name); /* length of the variable name */
425  expression[currStringPos] = currS;
426  currStringPos--;
427  j = 1;
428  }
429  else {
430  /* printf("ERROR: MISSING OR INVALID VARIABLE NAME\n"); */
431  break;
432  }
433  }
434  else if (j == 1) {
435  /* CLOSE PARENTHESIS */
436  if ((currS == ')') || (currS == ']') || (currS == '}')) {
437  offset -= 4; currStringPos++;
438  currS = expression[currStringPos];
439  if (offset < 0) {
440  /* printf("ERROR: INVALID CLOSE PARENTHESIS\n"); */
441  j = 0;
442  break;
443  }
444  continue;
445  }
446  else {
447  /* BOOLEAN BINARY OPERATOR */
448  j = 0;
449  if (currS == '*') currS = '&'; /* operator '*' is also allowed for conjunction */
450  if (currS == '+') currS = '|'; /* operator '+' is also allowed for disjunction */
451  if (currS == '%') currS = '^'; /* operator '%' is also allowed for xor */
452  for (i = 0; i < 16; i++) { if (boolOperators[i] == currS) { break; } }
453  if (i == 0) {
454  /* printf("ERROR:INVALID USE OF UNARY OPERATOR ~\n"); */
455  break;
456  }
457  else if ((i < 16) && (boolOperators[i] != '#')) {
458  tree->tnode[currTreePos].op = (char) i;
459  if (i == 1) { tree->tnode[currTreePos].index = offset + 3; }
460  else if ((i == 2) || (i == 4)) { tree->tnode[currTreePos].index = offset + 3; }
461  else if ((i == 6) || (i == 7)) { tree->tnode[currTreePos].index = offset + 2; }
462  else { tree->tnode[currTreePos].index = offset + 1; }
463  oldTreePos = tree->tnode[oldTreePos].parent;
464  while (tree->tnode[oldTreePos].index >= tree->tnode[currTreePos].index) {
465  oldTreePos = tree->tnode[oldTreePos].parent;
466  }
467  tempPos = tree->tnode[oldTreePos].right;
468  tree->tnode[oldTreePos].right = currTreePos;
469  tree->tnode[tempPos].parent = currTreePos;
470  tree->tnode[currTreePos].parent = oldTreePos;
471  tree->tnode[currTreePos].left = tempPos;
472  }
473  else {
474  /* printf("ERROR: MISSING OPERATOR OR INVALID BOOLEAN OPERATOR %c\n",currS); */
475  break;
476  }
477  }
478  }
479  currStringPos++;
480  currS = expression[currStringPos];
481  oldTreePos = currTreePos;
482  }
483 
484  if (j == 0) {
485  /* printf("ERROR: INCORRECT REQUEST\n"); */
486  return biddyNull;
487  }
488 
489  /*
490  printBiddyBTreeContainer(tree);
491  */
492 
493  /*
494  printf("%s\n",expression);
495  printPrefixFromBTree(tree,tree->tnode[0].right);
496  printf("\n");
497  */
498 
499  free(expression);
500 
501  /* FOR SOME BDD TYPES, IT IS NECESSARY TO CREATE ALL VARIABLES IN ADVANCE */
502  /* createBddFromBTree DOES NOT STORE TMP RESULTS AS FORMULAE AND THUS */
503  /* TMP RESULTS BECOME WRONG IF NEW VARIABLES ARE ADDED ON-THE-FLY */
504 
505  createVariablesFromBTree(MNG,tree);
506  fbdd = createBddFromBTree(MNG,tree,tree->tnode[0].right);
507 
508  for (i = 1023; i >= 0; i--) {
509  if (tree->tnode[i].name) free(tree->tnode[i].name);
510  }
511  free(tree->tnode);
512  free(tree);
513 
514  return fbdd;
515 }
516 
517 #ifdef __cplusplus
518 }
519 #endif
520 
521 /***************************************************************************/
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 /***************************************************************************/
1152 #ifdef __cplusplus
1153 extern "C" {
1154 #endif
1155 
1156 void
1158 {
1159  unsigned int variableNumber;
1160  Biddy_Variable* variableTable;
1161  unsigned int i;
1162  int j;
1163  Biddy_Variable k,v;
1164  unsigned int numcomb;
1165 
1166  if (!MNG) MNG = biddyAnonymousManager;
1167 
1168  if (Biddy_IsNull(f)) {
1169  printf("NULL\n");
1170  return;
1171  }
1172 
1173  /* variableNumber is the number of dependent variables in BDD */
1174  variableNumber = Biddy_Managed_DependentVariableNumber(MNG,f,TRUE);
1175 
1176  /* for ZBDD and ZFDD, variables above the top variable */
1177  /* (which are always all dependent) are not counted and not selected! */
1178  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
1179  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
1180  {
1181  for (k = 1; k < biddyVariableTable.num; k++) {
1182  if (BiddyIsSmaller(k,BiddyV(f))) {
1183  variableNumber++;
1184  biddyVariableTable.table[k].selected = TRUE;
1185  }
1186  }
1187  }
1188 
1189  /* DEBUGGING */
1190  /*
1191  printf("DEPENDENT: %u\n",variableNumber);
1192  for (k = 1; k < biddyVariableTable.num; k++) {
1193  if (biddyVariableTable.table[k].selected == TRUE) {
1194  printf("DEPENDENT: %s\n",Biddy_Managed_GetVariableName(MNG,k));
1195  }
1196  }
1197  */
1198 
1199  if (variableNumber > 6) {
1200  printf("Table for %d variables is to large for output.\n",variableNumber);
1201  for (k = 0; k < biddyVariableTable.num; k++) {
1202  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
1203  }
1204  return;
1205  }
1206 
1207  /* variableTable is a table of all dependent variables in BDD */
1208  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
1209  i = 0;
1210  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1211  for (k = 1; k < biddyVariableTable.num; k++) {
1212  if (biddyVariableTable.table[v].selected == TRUE) {
1213  variableTable[i] = v;
1214  printf("|%s",Biddy_Managed_GetVariableName(MNG,v));
1215  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1216  i++;
1217  }
1218  v = biddyVariableTable.table[v].next;
1219  }
1220  printf("|:value\n");
1221 
1222  numcomb = 1;
1223  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
1224  for (i = 0; i < numcomb; i++)
1225  {
1226  for (j = variableNumber - 1; j >= 0; j--) {
1227  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
1228  if (i&(1 << j)) {
1229  printf("%*c",1+(int)strlen(
1230  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1231  ),'1');
1232  } else {
1233  printf("%*c",1+(int)strlen(
1234  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1235  ),'0');
1236  }
1237  }
1238  printf(" :");
1239  if (Biddy_Managed_Eval(MNG,f)) printf("1\n"); else printf("0\n");
1240  }
1241 
1242  free(variableTable);
1243 }
1244 
1245 #ifdef __cplusplus
1246 }
1247 #endif
1248 
1249 
1250 /***************************************************************************/
1261 #ifdef __cplusplus
1262 extern "C" {
1263 #endif
1264 
1265 void
1266 Biddy_Managed_WriteTable(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
1267 {
1268  unsigned int variableNumber;
1269  Biddy_Variable* variableTable;
1270  unsigned int i;
1271  int j;
1272  Biddy_Variable k,v;
1273  unsigned int numcomb;
1274  FILE *s;
1275 
1276  if (!MNG) MNG = biddyAnonymousManager;
1277 
1278  if (filename) {
1279  s = fopen(filename,"w");
1280  } else {
1281  s = stdout;
1282  }
1283  if (!s) return;
1284 
1285  if (Biddy_IsNull(f)) {
1286  fprintf(s,"NULL\n");
1287  fclose(s);
1288  return;
1289  }
1290 
1291  /* variableNumber is the number of dependent variables in BDD */
1292  variableNumber = Biddy_Managed_DependentVariableNumber(MNG,f,TRUE);
1293 
1294  /* for ZBDD and ZFDD, variables above the top variable */
1295  /* (which are always all dependent) are not counted and not selected! */
1296  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
1297  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
1298  {
1299  for (k = 1; k < biddyVariableTable.num; k++) {
1300  if (BiddyIsSmaller(k,BiddyV(f))) {
1301  variableNumber++;
1302  biddyVariableTable.table[k].selected = TRUE;
1303  }
1304  }
1305  }
1306 
1307  if (variableNumber > 6) {
1308  fprintf(s,"Table for %d variables is to large for output.\n",variableNumber);
1309  for (k = 0; k < biddyVariableTable.num; k++) {
1310  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
1311  }
1312  fclose(s);
1313  return;
1314  }
1315 
1316  /* variableTable is a table of all dependent variables in BDD */
1317  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
1318  i = 0;
1319  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1320  for (k = 1; k < biddyVariableTable.num; k++) {
1321  if (biddyVariableTable.table[v].selected == TRUE) {
1322  variableTable[i] = v;
1323  fprintf(s,"|%s",Biddy_Managed_GetVariableName(MNG,v));
1324  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1325  i++;
1326  }
1327  v = biddyVariableTable.table[v].next;
1328  }
1329  fprintf(s,"|:value\n");
1330 
1331  numcomb = 1;
1332  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
1333  for (i = 0; i < numcomb; i++)
1334  {
1335  for (j = variableNumber - 1; j >= 0; j--)
1336  {
1337  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
1338  if (i&(1 << j)) {
1339  fprintf(s,"%*c",1+(int)strlen(
1340  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1341  ),'1');
1342  } else {
1343  fprintf(s,"%*c",1+(int)strlen(
1344  Biddy_Managed_GetVariableName(MNG,variableTable[variableNumber-j-1])
1345  ),'0');
1346  }
1347  }
1348  fprintf(s," :");
1349  if (Biddy_Managed_Eval(MNG,f)) fprintf(s,"1\n"); else fprintf(s,"0\n");
1350  }
1351 
1352  free(variableTable);
1353 
1354  if (filename) {
1355  fclose(s);
1356  }
1357 }
1358 
1359 #ifdef __cplusplus
1360 }
1361 #endif
1362 
1363 /***************************************************************************/
1371 #ifdef __cplusplus
1372 extern "C" {
1373 #endif
1374 
1375 void
1377 {
1378  unsigned int maxsize = 100;
1379  Biddy_Variable top;
1380 
1381  if (!MNG) MNG = biddyAnonymousManager;
1382 
1383  if (Biddy_IsNull(f)) {
1384  printf(" NULL\n");
1385  return;
1386  }
1387 
1388  if (Biddy_IsTerminal(f)) {
1389  if (f == biddyZero) {
1390  printf(" + 0\n");
1391  return;
1392  }
1393  else if (f == biddyOne) {
1394  printf(" + 1\n");
1395  return;
1396  }
1397  }
1398 
1399  top = BiddyV(f);
1400  if (biddyManagerType == BIDDYTYPEOBDD) {
1401  /* IMPLEMENTED */
1402  }
1403  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1404  /* IMPLEMENTED */
1405  }
1406  else if (biddyManagerType == BIDDYTYPEZBDD) {
1407  /* IMPLEMENTED */
1408  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1409  top = biddyVariableTable.table[top].prev;
1410  }
1411  }
1412  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1413  /* IMPLEMENTED */
1414  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1415  top = biddyVariableTable.table[top].prev;
1416  }
1417  }
1418  else if (biddyManagerType == BIDDYTYPETZBDD) {
1419  /* IMPLEMENTED */
1420  top = Biddy_GetTag(f);
1421  }
1422  else if (biddyManagerType == BIDDYTYPETZBDDC)
1423  {
1424  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1425  return;
1426  }
1427  else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1428  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1429  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1430  {
1431  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1432  return;
1433  }
1434  else {
1435  fprintf(stderr,"Biddy_PrintfSOP: Unsupported BDD type!\n");
1436  return;
1437  }
1438 
1439  WriteSOP(MNG,f,top,Biddy_GetMark(f),NULL,&maxsize);
1440  printf("\n");
1441 }
1442 
1443 #ifdef __cplusplus
1444 }
1445 #endif
1446 
1447 /***************************************************************************/
1455 #ifdef __cplusplus
1456 extern "C" {
1457 #endif
1458 
1459 void
1460 Biddy_Managed_WriteSOP(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
1461 {
1462  unsigned int maxsize = 100;
1463  Biddy_Variable top;
1464  FILE *s;
1465 
1466  if (!MNG) MNG = biddyAnonymousManager;
1467 
1468  if (filename) {
1469  s = fopen(filename,"w");
1470  } else {
1471  s = stdout;
1472  }
1473  if (!s) return;
1474 
1475  if (Biddy_IsNull(f)) {
1476  fprintf(s," NULL\n");
1477  if (filename) {
1478  fclose(s);
1479  }
1480  return;
1481  }
1482 
1483  if (Biddy_IsTerminal(f)) {
1484  if (f == biddyZero) {
1485  fprintf(s," + 0\n");
1486  if (filename) {
1487  fclose(s);
1488  }
1489  }
1490  else if (f == biddyOne) {
1491  fprintf(s," + 1\n");
1492  if (filename) {
1493  fclose(s);
1494  }
1495  }
1496  }
1497 
1498  top = BiddyV(f);
1499  if (biddyManagerType == BIDDYTYPEOBDD) {
1500  /* IMPLEMENTED */
1501  }
1502  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1503  /* IMPLEMENTED */
1504  }
1505  else if (biddyManagerType == BIDDYTYPEZBDD) {
1506  /* IMPLEMENTED */
1507  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1508  top = biddyVariableTable.table[top].prev;
1509  }
1510  }
1511  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1512  /* IMPLEMENTED */
1513  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
1514  top = biddyVariableTable.table[top].prev;
1515  }
1516  }
1517  else if (biddyManagerType == BIDDYTYPETZBDD) {
1518  /* IMPLEMENTED */
1519  top = Biddy_GetTag(f);
1520  }
1521  else if (biddyManagerType == BIDDYTYPETZBDDC)
1522  {
1523  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1524  if (filename) {
1525  fclose(s);
1526  }
1527  return;
1528  }
1529  else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1530  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1531  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1532  {
1533  fprintf(stderr,"Biddy_PrintfSOP: this BDD type is not supported, yet!\n");
1534  if (filename) {
1535  fclose(s);
1536  }
1537  return;
1538  }
1539  else {
1540  fprintf(stderr,"Biddy_PrintfSOP: Unsupported BDD type!\n");
1541  if (filename) {
1542  fclose(s);
1543  }
1544  return;
1545  }
1546 
1547  WriteSOPx(MNG,s,f,top,Biddy_GetMark(f),NULL,&maxsize);
1548 
1549  if (filename) {
1550  fclose(s);
1551  }
1552 
1553 }
1554 
1555 #ifdef __cplusplus
1556 }
1557 #endif
1558 
1559 /***************************************************************************/
1576 #ifdef __cplusplus
1577 extern "C" {
1578 #endif
1579 
1580 unsigned int
1581 Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f,
1582  const char label[], int id, Biddy_Boolean cudd)
1583 {
1584  unsigned int n;
1585  char *label1;
1586  char *hash;
1587  FILE *s;
1588  Biddy_Variable tag;
1589  BiddyLocalInfo *li;
1590  Biddy_Variable v;
1591  Biddy_String name;
1592 
1593  if (!MNG) MNG = biddyAnonymousManager;
1594 
1595  /* if (id != -1) use it instead of <...> */
1596 
1597  if (Biddy_IsNull(f)) {
1598  printf("WARNING (Biddy_Managed_WriteDot): Function is null!\n");
1599  return 0;
1600  }
1601 
1602  if (filename) {
1603  s = fopen(filename,"w");
1604  } else {
1605  s = stdout;
1606  }
1607  if (!s) return 0;
1608 
1609  if (Biddy_IsTerminal(f)) {
1610  n = 1; /* there is only one terminal node */
1611  } else {
1612  BiddyCreateLocalInfo(MNG,f);
1613  n = enumerateNodes(MNG,f,0); /* this will select all nodes except terminal node */
1615  }
1616 
1617  label1 = strdup(label);
1618  while ((hash=strchr(label1,'#'))) hash[0]='_'; /* avoid hashes in the name */
1619 
1620  if (cudd) {
1621  fprintf(s,"//GENERATED WITH BIDDY - biddy.meolic.com\n");
1622  if (filename) {
1623  fprintf(s,"//USE 'dot -y -Tpng -O %s' TO VISUALIZE %s\n",filename,biddyManagerName);
1624  }
1625  fprintf(s,"digraph \"DD\" {\n");
1626  /* fprintf(s,"size = \"7.5,10\"\n"); */
1627  fprintf(s,"center=true;\nedge [dir=none];\n");
1628  fprintf(s,"{ node [shape=plaintext];\n");
1629  fprintf(s," edge [style=invis];\n");
1630  fprintf(s," \"CONST NODES\" [style = invis];\n");
1631 
1632  if (!Biddy_IsTerminal(f)) {
1633  li = (BiddyLocalInfo *)(BiddyN(f)->list);
1635  while (li->back) {
1636  v = BiddyV(li->back);
1637  if (biddyVariableTable.table[v].value == biddyZero) {
1638  biddyVariableTable.table[v].value = biddyOne;
1639  /* variable names containing # are adpated */
1640  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
1641  while ((hash = strchr(name,'#'))) hash[0] = '_';
1642  fprintf(s,"\" %s \" -> ",name);
1643  free(name);
1644  }
1645  li = &li[1]; /* next field in the array */
1646  }
1648  }
1649 
1650  fprintf(s,"\"CONST NODES\"; \n}\n");
1651  fprintf(s,"{ rank=same; node [shape=box]; edge [style=invis];\n");
1652  fprintf(s,"\"%s\"",label1);
1653  fprintf(s,"; }\n");
1654  } else {
1655  fprintf(s,"//GENERATED WITH BIDDY - biddy.meolic.com\n");
1656  if (filename) {
1657  fprintf(s,"//USE 'dot -y -Tpng -O %s' TO VISUALIZE %s\n",filename,biddyManagerName);
1658  }
1659  fprintf(s,"digraph ");
1660  if (biddyManagerType == BIDDYTYPEOBDD) fprintf(s,"ROBDD");
1661  else if (biddyManagerType == BIDDYTYPEZBDD) fprintf(s,"ZBDD");
1662  else if (biddyManagerType == BIDDYTYPETZBDD) fprintf(s,"TZBDD");
1663  else if (biddyManagerType == BIDDYTYPEOBDDC) fprintf(s,"ROBDDCE");
1664  else if (biddyManagerType == BIDDYTYPEZBDDC) fprintf(s,"ZBDDCE");
1665  else if (biddyManagerType == BIDDYTYPETZBDDC) fprintf(s,"TZBDDCE");
1666  else fprintf(s,"BDD");
1667  fprintf(s," {\n");
1668  fprintf(s," ordering=out;\n");
1669 #ifdef LEGACY_DOT
1670 #else
1671  fprintf(s," edge [dir=\"both\"];\n");
1672 #endif
1673  fprintf(s," edge [arrowhead=\"none\"]\n");
1674  fprintf(s," node [shape=none, label=\"%s\"] 0;\n",label1);
1675  }
1676 
1677  WriteDotNodes(MNG,s,f,id,cudd);
1678 
1679  if (((biddyManagerType == BIDDYTYPEOBDD) ||
1680  (biddyManagerType == BIDDYTYPEZBDD) ||
1681  (biddyManagerType == BIDDYTYPETZBDD) ||
1682  !(Biddy_GetMark(f))))
1683  {
1684  if ((f != biddyZero) && (tag = Biddy_GetTag(f))) {
1685  if (cudd) {
1686  fprintf(s,"\"%s\"",label1);
1687  if (Biddy_IsTerminal(f)) {
1688  fprintf(s," -> \"1\" [style=solid label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1689  } else {
1690  fprintf(s," -> \"%p\" [style=solid label=\"%s\"];\n",BiddyP(f),Biddy_Managed_GetVariableName(MNG,tag));
1691  }
1692  } else {
1693 #ifdef LEGACY_DOT
1694  fprintf(s," 0 -> 1 [style=solid label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1695 #else
1696  fprintf(s," 0 -> 1 [arrowtail=\"none\" label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1697 #endif
1698  }
1699  } else {
1700  if (cudd) {
1701  fprintf(s,"\"%s\"",label1);
1702  if (Biddy_IsTerminal(f)) {
1703  fprintf(s," -> \"1\" [style=solid];\n");
1704  } else {
1705  fprintf(s," -> \"%p\" [style=solid];\n",BiddyP(f));
1706  }
1707  } else {
1708 #ifdef LEGACY_DOT
1709  fprintf(s," 0 -> 1 [style=solid];\n");
1710 #else
1711  fprintf(s," 0 -> 1 [arrowtail=\"none\"];\n");
1712 #endif
1713  }
1714  }
1715  } else {
1716  if ((f != biddyZero) && (tag = Biddy_GetTag(f))) {
1717  if (cudd) {
1718  fprintf(s,"\"%s\"",label1);
1719  if (Biddy_IsTerminal(f)) {
1720  fprintf(s," -> \"1\" [style=dotted label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1721  } else {
1722  fprintf(s," -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),Biddy_Managed_GetVariableName(MNG,tag));
1723  }
1724  } else {
1725 #ifdef LEGACY_DOT
1726  fprintf(s," 0 -> 1 [style=dotted label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1727 #else
1728  fprintf(s," 0 -> 1 [arrowtail=\"none\" arrowhead=\"dot\" label=\"%s\"];\n",Biddy_Managed_GetVariableName(MNG,tag));
1729 #endif
1730  }
1731  } else {
1732  if (cudd) {
1733  fprintf(s,"\"%s\"",label1);
1734  if (Biddy_IsTerminal(f)) {
1735  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1736  fprintf(s," -> \"1\" [style=dotted];\n");
1737  } else {
1738  fprintf(s," -> \"1\" [style=bold];\n");
1739  }
1740  } else {
1741  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1742  fprintf(s," -> \"%p\" [style=dotted];\n",BiddyP(f));
1743  } else {
1744  fprintf(s," -> \"%p\" [style=bold];\n",BiddyP(f));
1745  }
1746  }
1747  } else {
1748 #ifdef LEGACY_DOT
1749  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1750  fprintf(s," 0 -> 1 [style=dotted];\n");
1751  } else {
1752  fprintf(s," 0 -> 1 [style=bold];\n");
1753  }
1754 #else
1755  fprintf(s," 0 -> 1 [arrowtail=\"none\" arrowhead=\"dot\"];\n");
1756 #endif
1757  }
1758  }
1759  }
1760 
1761  free(label1);
1762 
1763  WriteDotEdges(MNG,s,f,cudd); /* this will select all nodes except terminal node */
1764 
1765  if (!Biddy_IsTerminal(f)) {
1766  BiddyDeleteLocalInfo(MNG,f);
1767  }
1768 
1769  fprintf(s,"}\n");
1770 
1771  if (filename) {
1772  fclose(s);
1773  }
1774 
1775  return n;
1776 }
1777 
1778 #ifdef __cplusplus
1779 }
1780 #endif
1781 
1782 /***************************************************************************/
1799 #ifdef __cplusplus
1800 extern "C" {
1801 #endif
1802 
1803 unsigned int
1804 Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[],
1805  Biddy_Edge f, const char label[], void *xytable)
1806 {
1807  FILE *s;
1808  unsigned int i,n;
1809  Biddy_Boolean useCoordinates;
1810  BiddyLocalInfo *li;
1811  Biddy_Variable v,k,tag;
1812  char *hash;
1813  Biddy_String name;
1814  BiddyXY *table;
1815 
1816  if (!MNG) MNG = biddyAnonymousManager;
1817 
1818  if (Biddy_IsNull(f)) {
1819  /* printf("ERROR Biddy_Managed_WriteBddview: Function is null!\n"); */
1820  return 0 ;
1821  }
1822 
1823  if (filename) {
1824  s = fopen(filename,"w");
1825  } else {
1826  s = stdout;
1827  }
1828  if (!s) {
1829  printf("ERROR: s = 0\n");
1830  return(0);
1831  }
1832 
1833  table = (BiddyXY *)xytable;
1834 
1835  fprintf(s,"#GENERATED WITH BIDDY - biddy.meolic.com\n");
1836 
1837  /* WRITE BDD TYPE */
1838 
1839  if (biddyManagerType == BIDDYTYPEOBDD) {
1840  fprintf(s,"type ROBDD\n");
1841  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1842  fprintf(s,"type ROBDDCE\n");
1843  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1844  fprintf(s,"type ZBDD\n");
1845  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1846  fprintf(s,"type ZBDDCE\n");
1847  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1848  fprintf(s,"type TZBDD\n");
1849  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
1850  fprintf(s,"type TZBDDCE\n");
1851  } else if (biddyManagerType == BIDDYTYPEOFDD) {
1852  fprintf(s,"type ROFDD\n");
1853  } else if (biddyManagerType == BIDDYTYPEOFDDC) {
1854  fprintf(s,"type ROFDDCE\n");
1855  } else if (biddyManagerType == BIDDYTYPEZFDD) {
1856  fprintf(s,"type ZFDD\n");
1857  } else if (biddyManagerType == BIDDYTYPEZFDDC) {
1858  fprintf(s,"type ZFDDCE\n");
1859  } else if (biddyManagerType == BIDDYTYPETZFDD) {
1860  fprintf(s,"type TZFDD\n");
1861  } else if (biddyManagerType == BIDDYTYPETZFDDC) {
1862  fprintf(s,"type TZFDDCE\n");
1863  }
1864 
1865  /* WRITE VARIABLES */
1866  /* A conservative approach to list all the existing variables */
1867  /* in the manager (and not only the dependent ones) is used. */
1868 
1869  fprintf(s,"var");
1870  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1871  for (k = 1; k < biddyVariableTable.num; k++) {
1872  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
1873 
1874  /* variable names containing # are adpated */
1875  while ((hash = strchr(name,'#'))) hash[0] = '_';
1876  /* to support EST, also variable names containing <> are adapted */
1877  for (i=0; i<strlen(name); i++) {
1878  if (name[i] == '<') name[i] = '_';
1879  if (name[i] == '>') name[i] = 0;
1880  }
1881 
1882  fprintf(s," \"%s\"",name);
1883  free(name);
1884  v = biddyVariableTable.table[v].next;
1885  }
1886  fprintf(s,"\n");
1887 
1888  /* PREPARE CALCULATION */
1889 
1890  useCoordinates = FALSE;
1891  if (Biddy_IsTerminal(f)) {
1892 
1893  n = 1; /* for all BDD types, in memory there is only one terminal node */
1894  if (table) {
1895  /* use table of nodes given by the user */
1896  useCoordinates = TRUE;
1897  } else {
1898  n = 1; /* there is one terminal node */
1899  table = (BiddyXY *) malloc((n+1) * sizeof(BiddyXY)); /* n = nodes, add one label */
1900  if (!table) return 0;
1901  table[0].id = 0;
1902  table[0].label = strdup(label);
1903  table[0].x = 0;
1904  table[0].y = 0;
1905  table[0].isConstant = FALSE;
1906  table[1].id = 1;
1907  table[1].label = getname(MNG,f);
1908  table[1].x = 0;
1909  table[1].y = 0;
1910  table[1].isConstant = TRUE;
1911  }
1912 
1913  } else {
1914 
1915  BiddyCreateLocalInfo(MNG,f);
1916  n = enumerateNodes(MNG,f,0); /* this will select all nodes except terminal node */
1918 
1919  if (table) {
1920  /* use table of nodes given by the user */
1921  useCoordinates = TRUE;
1922  } else {
1923  /* generate table of nodes */
1924  /* TO DO: coordinates are not calculated, how to do this without graphviz/dot? */
1925  table = (BiddyXY *) malloc((n+1) * sizeof(BiddyXY)); /* n = nodes, add one label */
1926  if (!table) return 0;
1927  table[0].id = 0;
1928  table[0].label = strdup(label);
1929  table[0].x = 0;
1930  table[0].y = 0;
1931  table[0].isConstant = FALSE;
1932  li = (BiddyLocalInfo *)(BiddyN(f)->list);
1933  while (li->back) {
1934 
1935  /* add one node */
1936  table[li->data.enumerator].id = li->data.enumerator;
1937  table[li->data.enumerator].label = getname(MNG,li->back);
1938  table[li->data.enumerator].x = 0;
1939  table[li->data.enumerator].y = 0;
1940  table[li->data.enumerator].isConstant = FALSE;
1941 
1942  /* if one or both successors are terminal node then extra nodes must be added */
1943  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
1944  if (((biddyManagerType == BIDDYTYPEOBDD) ||
1945  (biddyManagerType == BIDDYTYPEZBDD) ||
1946  (biddyManagerType == BIDDYTYPETZBDD)
1947  ) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back))))
1948  {
1949  /* two terminal nodes only if complemented edges are not used and they are different */
1950  unsigned int num;
1951  num = 0;
1952  if (Biddy_IsTerminal(BiddyE(li->back))) {
1953  num = 1;
1954  table[li->data.enumerator+1].id = li->data.enumerator+1;
1955  if (BiddyE(li->back) == biddyZero) {
1956  table[li->data.enumerator+1].label = strdup("0");
1957  } else {
1958  table[li->data.enumerator+1].label = strdup("1");
1959  }
1960  table[li->data.enumerator+1].x = 0;
1961  table[li->data.enumerator+1].y = 0;
1962  table[li->data.enumerator+1].isConstant = TRUE;
1963  }
1964  if (Biddy_IsTerminal(BiddyT(li->back))) {
1965  table[li->data.enumerator+num+1].id = li->data.enumerator+num+1;
1966  if (BiddyT(li->back) == biddyZero) {
1967  table[li->data.enumerator+num+1].label = strdup("0");
1968  } else {
1969  table[li->data.enumerator+num+1].label = strdup("1");
1970  }
1971  table[li->data.enumerator+num+1].x = 0;
1972  table[li->data.enumerator+num+1].y = 0;
1973  table[li->data.enumerator+num+1].isConstant = TRUE;
1974  }
1975  } else {
1976  /* only one terminal node */
1977  table[li->data.enumerator+1].id = li->data.enumerator+1;
1978  table[li->data.enumerator+1].label = strdup("1");
1979  table[li->data.enumerator+1].x = 0;
1980  table[li->data.enumerator+1].y = 0;
1981  table[li->data.enumerator+1].isConstant = TRUE;
1982  }
1983  }
1984 
1985  li = &li[1]; /* next field in the array */
1986  }
1987  }
1988 
1989  }
1990 
1991  /* WRITE bddview NODES */
1992 
1993  if (useCoordinates) {
1994  fprintf(s,"label %d %s %d %d\n",table[0].id,table[0].label,table[0].x,table[0].y);
1995  } else {
1996  fprintf(s,"label %d %s\n",table[0].id,table[0].label);
1997  }
1998  for (i=1;i<(n+1);i++) {
1999  if (table[i].isConstant) {
2000  fprintf(s,"terminal ");
2001  } else {
2002  fprintf(s,"node ");
2003  }
2004  if (useCoordinates) {
2005  fprintf(s,"%d %s %d %d\n",table[i].id,table[i].label,table[i].x,table[i].y);
2006  } else {
2007  fprintf(s,"%d %s\n",table[i].id,table[i].label);
2008  }
2009  }
2010 
2011  if (!useCoordinates) {
2012  for (i=1;i<(n+1);i++) {
2013  free(table[i].label);
2014  }
2015  free(table);
2016  }
2017 
2018  /* WRITE bddview CONNECTIONS */
2019 
2020  fprintf(s,"connect 0 1 ");
2021  if ((biddyManagerType == BIDDYTYPEOBDD) ||
2022  (biddyManagerType == BIDDYTYPEZBDD) ||
2023  (biddyManagerType == BIDDYTYPETZBDD))
2024  {
2025  fprintf(s,"s");
2026  }
2027  else {
2028  if (Biddy_GetMark(f)) {
2029  fprintf(s,"si");
2030  } else {
2031  fprintf(s,"s");
2032  }
2033  }
2034 
2035  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2036  {
2037  tag = Biddy_GetTag(f);
2038  fprintf(s," %s\n",Biddy_Managed_GetVariableName(MNG,tag));
2039  } else {
2040  fprintf(s,"\n");
2041  }
2042 
2043  if (!Biddy_IsTerminal(f)) {
2044  WriteBddviewConnections(MNG,s,f); /* this will select all nodes except terminal node */
2045  BiddyDeleteLocalInfo(MNG,f);
2046  }
2047 
2048  if (filename) {
2049  fclose(s);
2050  }
2051 
2052  return n;
2053 }
2054 
2055 #ifdef __cplusplus
2056 }
2057 #endif
2058 
2059 /*----------------------------------------------------------------------------*/
2060 /* Definition of internal functions */
2061 /*----------------------------------------------------------------------------*/
2062 
2063 /*----------------------------------------------------------------------------*/
2064 /* Definition of static functions */
2065 /*----------------------------------------------------------------------------*/
2066 
2067 /* Some of these were implemented long time ago (1995). */
2068 /* Not comprehensible. */
2069 
2070 #define oAND 1
2071 #define oOR 2
2072 #define oEXOR 3
2073 
2074 static Biddy_Boolean
2075 charOK(char c)
2076 {
2077  return (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z') || c == '_' ||
2078  (c >= '0' && c <= '9') || c == '[' || c == ']' ||
2079  c == '+' || c == '-' || c == '*' || c == '\'' ||
2080  c == '$' || c == '&' || c == '%' || c == '#' ||
2081  c == '?' || c == '!' || c == ':' || c == '.' ;
2082 }
2083 
2084 static void
2085 nextCh(Biddy_String s, int *i, Biddy_String *ch)
2086 {
2087  char c;
2088  int j;
2089 
2090  while (s[*i] == ' ' || s[*i] == '\t' || s[*i] == '\n') (*i)++;
2091  j = *i;
2092  c = s[*i];
2093 
2094  /* DEBUGGING */
2095  /*
2096  printf("%c",c);
2097  */
2098 
2099  if (c == '(') {
2100  (*i)++;
2101  strcpy(*ch,"(");
2102  return;
2103  }
2104 
2105  if (c == ')') {
2106  (*i)++;
2107  strcpy(*ch,")");
2108  return;
2109  }
2110 
2111  if (c == '*') {
2112  (*i)++;
2113  strcpy(*ch,"*");
2114  return;
2115  }
2116 
2117  if (charOK(c)) {
2118  (*i)++;
2119  while (charOK(s[*i])) (*i)++;
2120  c = s[*i];
2121 
2122  /* DEBUGGING */
2123  /*
2124  printf("%c",c);
2125  */
2126 
2127  if ( (c == ' ') || (c == '\t') || (c == '\n') || (c == '(') || (c == ')') ) {
2128  strncpy(*ch, &(s[j]), *i-j);
2129  (*ch)[*i-j] = 0;
2130  return;
2131  }
2132  }
2133 
2134  strcpy(*ch,"");
2135  return;
2136 }
2137 
2138 static Biddy_Edge
2139 ReadBDD(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch)
2140 {
2141  Biddy_Boolean inv;
2142  Biddy_String varname;
2143  Biddy_Edge f,n,e,t;
2144 
2145  assert( (biddyManagerType == BIDDYTYPEOBDD) || (biddyManagerType == BIDDYTYPEOBDDC) );
2146 
2147  nextCh(s,i,ch);
2148 
2149  if (strcmp(*ch,"*")) {
2150  inv = FALSE;
2151  } else {
2152  inv = TRUE;
2153  /* printf("<*>\n"); */
2154  nextCh(s,i,ch);
2155  }
2156 
2157  /* printf("<%s>\n",*ch); */
2158 
2159  if (!strcmp(*ch,"0")) {
2160  if (inv) {
2161  f = biddyOne;
2162  } else {
2163  f = biddyZero;
2164  }
2165  } else if (!strcmp(*ch,"1")) {
2166  if (inv) {
2167  f = biddyZero;
2168  } else {
2169  f = biddyOne;
2170  }
2171  } else {
2172  varname = strdup(*ch);
2173  n = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_GetVariable(MNG,varname)); /* variables should already exist */
2174  nextCh(s,i,ch);
2175  if (strcmp(*ch,"(")) {
2176  printf("ERROR: <%s>\n",*ch);
2177  return biddyNull;
2178  }
2179  e = ReadBDD(MNG,s,i,ch);
2180  nextCh(s,i,ch);
2181  if (strcmp(*ch,")")) {
2182  printf("ERROR: <%s>\n",*ch);
2183  return biddyNull;
2184  }
2185  nextCh(s,i,ch);
2186  if (strcmp(*ch,"(")) {
2187  printf("ERROR: <%s>\n",*ch);
2188  return biddyNull;
2189  }
2190  t = ReadBDD(MNG,s,i,ch);
2191  nextCh(s,i,ch);
2192  if (strcmp(*ch,")")) {
2193  printf("ERROR: <%s>\n",*ch);
2194  return biddyNull;
2195  }
2196  if (inv) {
2197  f = Biddy_Managed_Not(MNG,Biddy_Managed_ITE(MNG,n,t,e));
2198  } else {
2199  f = Biddy_Managed_ITE(MNG,n,t,e);
2200  }
2201  free(varname);
2202  }
2203 
2204  return f;
2205 }
2206 
2207 static Biddy_Edge
2208 evaluate1(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch,
2210 {
2211  unsigned int idx;
2212  Biddy_Edge f;
2213  int op;
2214 
2215  /* DEBUGGING */
2216  /*
2217  printf("evaluate1: %s\n",s);
2218  printf("evaluate1 i = %d\n",*i);
2219  printf("evaluate1 ch = %s\n",*ch);
2220  */
2221 
2222  if (!strcmp(*ch,"(")) {
2223  nextCh(s,i,ch);
2224 
2225  if (!strcasecmp(*ch, "NOT")) {
2226  nextCh(s,i,ch);
2227  f = Biddy_Managed_Not(MNG,evaluate1(MNG,s,i,ch,lf));
2228  } else {
2229  if ((op = Op(s,i,ch))) {
2230  f = evaluateN(MNG,s,i,ch,evaluate1(MNG,s,i,ch,lf),op,lf);
2231  } else {
2232  f = evaluate1(MNG,s,i,ch,lf);
2233  }
2234  }
2235 
2236  if (!strcmp(*ch, ")")) nextCh(s,i,ch);
2237 
2238  return f;
2239  }
2240 
2241  /* evaluate1 will always check Biddy's formula table */
2242  /* if (lf != NULL) then user's formula table will be checked, too */
2243  /* user's formula table will be checked before Biddy's formula table */
2244  /* entries in user's formula should not be obsolete */
2245 
2246  if (charOK(*ch[0])) {
2247  if (!lf) {
2248  if (!Biddy_Managed_FindFormula(MNG,*ch,&idx,&f)) {
2250  }
2251  } else {
2252  if ((!(lf(*ch,&f))) &&
2253  (!Biddy_Managed_FindFormula(MNG,*ch,&idx,&f))) {
2255  }
2256  }
2257  nextCh(s,i,ch);
2258 
2259  assert( f != biddyNull );
2260 
2261  return f;
2262  }
2263 
2264  return biddyNull;
2265 }
2266 
2267 static Biddy_Edge
2268 evaluateN(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch,
2269  Biddy_Edge g, int op, Biddy_LookupFunction lf)
2270 {
2271  Biddy_Edge f, h;
2272 
2273  /* DEBUGGING */
2274  /*
2275  printf("evaluateN: %s\n",s);
2276  printf("evaluateN i = %d\n",*i);
2277  printf("evaluateN ch = %s\n",*ch);
2278  */
2279 
2280  h = evaluate1(MNG,s,i,ch,lf);
2281  if (!Biddy_IsNull(h)) {
2282  f = biddyNull;
2283  switch (op) {
2284  case oAND: f = Biddy_Managed_And(MNG,g,h);
2285  break;
2286  case oOR: f = Biddy_Managed_Or(MNG,g,h);
2287  break;
2288  case oEXOR: f = Biddy_Managed_Xor(MNG,g,h);
2289  }
2290  return evaluateN(MNG,s,i,ch,f,op,lf);
2291  }
2292  return g;
2293 }
2294 
2295 static int
2296 Op(Biddy_String s, int *i, Biddy_String *ch)
2297 {
2298 
2299  /* DEBUGGING */
2300  /*
2301  printf("Op ch = %s\n",*ch);
2302  */
2303 
2304  if (!strcasecmp(*ch, "AND")) {
2305  nextCh(s,i,ch);
2306  return oAND;
2307  }
2308 
2309  if (!strcasecmp(*ch, "OR")) {
2310  nextCh(s,i,ch);
2311  return oOR;
2312  }
2313 
2314  if (!strcasecmp(*ch, "EXOR")) {
2315  nextCh(s,i,ch);
2316  return oEXOR;
2317  }
2318 
2319  return 0;
2320 }
2321 
2322 static void
2323 createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree)
2324 {
2325  int i;
2326  unsigned int idx;
2327  Biddy_Edge tmp;
2328 
2329  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
2330  {
2331  for (i = 0; i <= tree->availableNode; i++) {
2332  if (tree->tnode[i].op == 255) {
2333  if (tree->tnode[i].name) {
2334  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&tmp))) {
2335  Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2336  }
2337  }
2338  }
2339  }
2340  }
2341 
2342  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2343  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2344  {
2345  for (i = tree->availableNode; i >= 0; i--) {
2346  if (tree->tnode[i].op == 255) {
2347  if (tree->tnode[i].name) {
2348  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&tmp))) {
2349  Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2350  }
2351  }
2352  }
2353  }
2354  }
2355 }
2356 
2357 static Biddy_Edge
2358 createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i)
2359 {
2360  unsigned int idx;
2361  Biddy_Edge lbdd,rbdd,fbdd;
2362 
2363  if (i == -1) return biddyNull;
2364  if (tree->tnode[i].op == 255) {
2365  if (tree->tnode[i].name) {
2366  if (!strcmp(tree->tnode[i].name,"0")) fbdd = biddyZero;
2367  else if (!strcmp(tree->tnode[i].name,"1")) fbdd = biddyOne;
2368  else {
2369  if (!(Biddy_Managed_FindFormula(MNG,tree->tnode[i].name,&idx,&fbdd))) {
2370  fbdd = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,tree->tnode[i].name));
2371  }
2372  }
2373  } else {
2374  fbdd = biddyNull;
2375  }
2376 
2377  /* DEBUGGING */
2378  /*
2379  printf("createBddFromBTree: op == 255\n");
2380  printPrefixFromBTree(tree,i);
2381  printf("\n");
2382  printf("HERE IS fbdd:\n");
2383  Biddy_PrintfBDD(fbdd);
2384  Biddy_PrintfSOP(fbdd);
2385  */
2386 
2387  return fbdd;
2388  }
2389  lbdd = createBddFromBTree(MNG,tree,tree->tnode[i].left);
2390  rbdd = createBddFromBTree(MNG,tree,tree->tnode[i].right);
2391 
2392  /* NOT (~!), AND (&*), OR (|+), XOR (^%) , XNOR(-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (\), AND NOTBUT (/) ARE IMPLEMENTED */
2393  /* char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' }; */
2394  if (tree->tnode[i].op == 0) fbdd = Biddy_Managed_Not(MNG,rbdd); /* NOT */
2395  else if (tree->tnode[i].op == 1) fbdd = Biddy_Managed_And(MNG,lbdd,rbdd); /* AND */
2396  else if (tree->tnode[i].op == 2) fbdd = Biddy_Managed_Gt(MNG,lbdd,rbdd); /* BUTNOT */
2397  else if (tree->tnode[i].op == 4) fbdd = Biddy_Managed_Gt(MNG,rbdd,lbdd); /* NOTBUT */
2398  else if (tree->tnode[i].op == 6) fbdd = Biddy_Managed_Xor(MNG,lbdd,rbdd); /* XOR */
2399  else if (tree->tnode[i].op == 7) fbdd = Biddy_Managed_Or(MNG,lbdd,rbdd); /* OR */
2400  else if (tree->tnode[i].op == 8) fbdd = Biddy_Managed_Nor(MNG,lbdd,rbdd); /* NOR */
2401  else if (tree->tnode[i].op == 9) fbdd = Biddy_Managed_Xnor(MNG,lbdd,rbdd); /* XNOR */
2402  else if (tree->tnode[i].op == 11) fbdd = Biddy_Managed_Leq(MNG,rbdd,lbdd); /* IMPLIES <= */
2403  else if (tree->tnode[i].op == 13) fbdd = Biddy_Managed_Leq(MNG,lbdd,rbdd); /* IMPLIES => */
2404  else if (tree->tnode[i].op == 14) fbdd = Biddy_Managed_Nand(MNG,lbdd,rbdd); /* NAND */
2405  else fbdd = biddyNull;
2406 
2407  /* DEBUGGING */
2408  /*
2409  printf("createBddFromBTree: op == %u\n",tree->tnode[i].op);
2410  printPrefixFromBTree(tree,i);
2411  printf("\n");
2412  printf("HERE IS lbdd:\n");
2413  Biddy_PrintfBDD(lbdd);
2414  Biddy_PrintfSOP(lbdd);
2415  printf("HERE IS rbdd:\n");
2416  Biddy_PrintfBDD(rbdd);
2417  Biddy_PrintfSOP(rbdd);
2418  printf("HERE IS fbdd:\n");
2419  Biddy_PrintfBDD(fbdd);
2420  Biddy_PrintfSOP(fbdd);
2421  */
2422 
2423  return fbdd;
2424 }
2425 
2426 static void
2427 parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt)
2428 {
2429  unsigned int activemodule=0;
2430  BiddyVerilogLine *ln;
2431  BiddyVerilogModule *md;
2432  unsigned int i=0, j=0, k=0; /* indexes */
2433  char ch, linebuf[LINESIZE]; /* buffer for single line from the verilog file */
2434  Biddy_String buffer; /* buffer for complete verilog statements */
2435  Biddy_String token[TOKENNUM]; /* array to hold tokens for the line */
2436  Biddy_String keyword; /* keyword from verilog line */
2437  Biddy_Boolean comment, noname, ok, acceptable;
2438  Biddy_String t,tc;
2439  unsigned int tn;
2440 
2441  (*l) = 0;
2442  (*lt) = NULL;
2443  (*n) = 0;
2444  (*mt) = NULL;
2445 
2446  keyword = NULL;
2447  buffer = NULL;
2448  md = NULL;
2449  while (fgets(linebuf,LINESIZE,verilogfile) != NULL) {
2450 
2451  if (keyword) free(keyword);
2452  tn = (unsigned int) strspn(linebuf," ");
2453 
2454  if (tn == strlen(linebuf)) {
2455  continue; /* skip empty lines and white space */
2456  }
2457 
2458  /* get 1st word from the line */
2459  tn += (unsigned int) strcspn(&linebuf[tn]," ");
2460  ch = 0;
2461  if (tn < strlen(linebuf)) {
2462  ch = linebuf[tn];
2463  linebuf[tn] = 0;
2464  }
2465  tn = (unsigned int) strspn(linebuf," ");
2466  keyword = strdup(&linebuf[tn]);
2467  if (ch) {
2468  tn += (unsigned int) strcspn(&linebuf[tn]," ");
2469  linebuf[tn] = ch;
2470  }
2471  keyword = trim(keyword);
2472 
2473  if (!strlen(keyword)) {
2474  continue; /* skip white space not recognised before */
2475  }
2476 
2477  if (!strcmp(keyword,"//")) {
2478  continue; /* skip comment lines */
2479  }
2480 
2481  if (buffer) free(buffer);
2482  buffer = strdup("");
2483  if (!strcmp(keyword,"endmodule")) { /* endmodule keyword does not use ';' */
2484  concat(&buffer,keyword);
2485  } else {
2486  concat(&buffer,linebuf);
2487  while (!isEndOfLine(linebuf)) { /* check if the line ends with a ';' character (multiple lines statement) */
2488  if (fgets(linebuf,LINESIZE,verilogfile) != NULL) {/* otherwise, append all the following lines */
2489  concat(&buffer,linebuf);
2490  if ((strlen(buffer) + LINESIZE) > BUFSIZE) printf("ERROR (parseVerilogFile): BUFFER TO SMALL\n");
2491  }
2492  }
2493  }
2494 
2495  /* tokenize the line to extract data */
2496  noname = FALSE;
2497  if (strcmp(keyword,"module") && strcmp(keyword,"endmodule") &&
2498  strcmp(keyword,"input") && strcmp(keyword,"output") &&
2499  strcmp(keyword,"wire") && strcmp(keyword,"reg") &&
2500  strcmp(keyword,"assign"))
2501  {
2502  tn = (unsigned int) strspn(buffer," ");
2503  tn += (unsigned int) strcspn(&buffer[tn]," ");
2504  tn += (unsigned int) strspn(&buffer[tn]," ");
2505  if (buffer[tn] == '(') noname = TRUE;
2506  }
2507  i=0;
2508  comment = FALSE;
2509  t = strtok(buffer," ");
2510  token[i++] = strdup(t); /* full keyword */
2511  if (noname) {
2512  sprintf(linebuf,"NONAME%d",(*l));
2513  token[i++] = strdup(linebuf); /* add NONAME */
2514  }
2515  while ((t = strtok(NULL," (),;\r\n")) && (strcmp(t,"//"))) {
2516  if (!strcmp(t,"/*")) comment = TRUE;
2517  if (!comment) {
2518  if (strlen(t)>1) {
2519  tn = (unsigned int) strcspn(t,"{}");
2520  while (tn != strlen(t)) {
2521  tc = NULL;
2522  if (t[tn] == '{') tc = strdup("{");
2523  if (t[tn] == '}') tc = strdup("}");
2524  if (tn) {
2525  t[tn] = 0;
2526  token[i++] = strdup(t);
2527  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2528  }
2529  token[i++] = tc;
2530  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2531  t = &t[tn+1];
2532  tn = (unsigned int) strcspn(t,"{}");
2533  }
2534  }
2535  if (strlen(t)) {
2536  token[i++] = strdup(t);
2537  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
2538  }
2539  }
2540  if (comment && !strcmp(t,"*/")) comment = FALSE;
2541  }
2542  token[i] = NULL;
2543 
2544  if (!strcmp(keyword,"module")) { /* START OF MODULE */
2545  (*n)++;
2546  (*mt) = (BiddyVerilogModule **) realloc((*mt), (*n) * sizeof(BiddyVerilogModule *)); /* create or enlarge table of modules */
2547  md = (BiddyVerilogModule *) calloc(1, sizeof(BiddyVerilogModule)); /* declare an instance of a module */
2548  (*mt)[(*n)-1] = md;
2549  md->name = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for module name string */
2550  strcpy(md->name,token[1]); /* set module name */
2551  activemodule = (*n);
2552  /* DEBUGGING */
2553  /*
2554  printf("MODULE: %s (#%d)\n",token[1],activemodule);
2555  */
2556  md->outputFirst = TRUE; /* TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3), FALSE iff N3 = NAND(N1,N2) */
2557  }
2558 
2559  if (!strcmp(keyword,"endmodule")) { /* END OF MODULE */
2560  /* DEBUGGING */
2561  /*
2562  printf("ENDMODULE: #%d\n",activemodule);
2563  */
2564  activemodule = 0;
2565  md = NULL;
2566  } else {
2567  if (!activemodule) {
2568  printf("ERROR (parseVerilogFile): statement <%s> is outside of module\n",keyword);
2569  continue;
2570  }
2571  }
2572 
2573  acceptable = FALSE;
2574  if ((activemodule == 1) || !strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
2575  /* TO DO: MULTIPLE MODULES ARE NOT SUPPORTED, YET */
2576 
2577  if (!strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
2578  acceptable = TRUE;
2579  }
2580 
2581  else if (!strcmp(keyword,"input")) { /* PRIMARY INPUTS */
2582  acceptable = TRUE;
2583  for (j = 1; j < i; j++) { /* parse all the words in the line */
2584  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2585  parseSignalVector(md->inputs, token, &j, &md->inputcount);
2586  else { /* not a vector of signal */
2587  md->inputs[md->inputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for input string */
2588  strcpy(md->inputs[md->inputcount],token[j]); /* add the input name to the array of inputs */
2589  (md->inputcount)++; /* update the number of inputs in the circuit */
2590  if (md->inputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
2591  }
2592  }
2593  }
2594 
2595  else if (!strcmp(keyword,"output")) { /* PRIMARY OUTPUTS */
2596  acceptable = TRUE;
2597  for (j = 1; j < i; j++) { /* parse all the words in the line */
2598  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2599  parseSignalVector(md->outputs, token, &j, &md->outputcount);
2600  else { /* not a vector of signal */
2601  md->outputs[md->outputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for output string */
2602  strcpy(md->outputs[md->outputcount],token[j]); /* add the output name to the array of outputs */
2603  (md->outputcount)++; /* update the number of outputs in the circuit */
2604  if (md->outputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
2605  }
2606  }
2607  }
2608 
2609  else if (!strcmp(keyword,"wire")) { /* WIRES */
2610  for (j = 1; j < i; j++) { /* parse all the words in the line */
2611  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2612  parseSignalVector(md->wires, token, &j, &md->wirecount);
2613  else { /* not a vector of signal */
2614  /* check if this wire has not already been stated as input or output */
2615  ok = TRUE;
2616  for (k=0; k < md->inputcount; k++) {
2617  if (!strcmp(md->inputs[k],token[j])) ok = FALSE;
2618  }
2619  for (k=0; k < md->outputcount; k++) {
2620  if (!strcmp(md->outputs[k],token[j])) ok = FALSE;
2621  }
2622  if (ok) {
2623  acceptable = TRUE;
2624  md->wires[md->wirecount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for wire string */
2625  strcpy(md->wires[md->wirecount],token[j]); /* add the wire name to the array of wires */
2626  (md->wirecount)++; /* update the number of wires in the circuit */
2627  if (md->wirecount >= WIRENUM) printf("ERROR (parseVerilogFile): WIRENUM TO SMALL\n");
2628  } else {
2629  /* DEBUGGING */
2630  /*
2631  printf("WARNING (parseVerilogFile): wire %s already defined as input/output\n",token[j]);
2632  */
2633  }
2634  }
2635  }
2636  }
2637 
2638  else if (!strcmp(keyword,"reg")) { /* REGS */
2639  acceptable = TRUE;
2640  for (j = 1; j < i; j++) { /* parse all the words in the line */
2641  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
2642  parseSignalVector (md->regs, token, &j, &md->regcount);
2643  else { /* not a vector of signal */
2644  md->regs[md->regcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for reg string */
2645  strcpy(md->regs [md->regcount],token[j]); /* add the reg name to the array of regs */
2646  (md->regcount)++; /* update the number of regs in the circuit */
2647  if (md->regcount >= REGNUM) printf("ERROR (parseVerilogFile): REGNUM TO SMALL\n");
2648  }
2649  }
2650  }
2651 
2652  else if (isGate(keyword)) { /* BASIC GATES */
2653  acceptable = TRUE;
2654  md->gates[md->gatecount] = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for gate name string */
2655  strcpy(md->gates[md->gatecount],token[1]); /* add the gate name to the array of gates */
2656  if (!md->gatecount) { /* use the first gate to determine md->outputFirst */
2657  for (j=0; md->inputs[j] != NULL; j++) if (!strcmp(md->inputs[j],token[2])) md->outputFirst = FALSE;
2658  }
2659  (md->gatecount)++; /* update the number of gates in the circuit */
2660  if (md->gatecount >= GATENUM) printf("ERROR (parseVerilogFile): GATENUM TO SMALL\n");
2661  }
2662 
2663  else {
2664  /* AN UNIMPLEMENTED KEYWORD */
2665  /* GATES DEFINED BY OTHER MODULES ARE NOT RESOLVED */
2666  }
2667 
2668  }
2669 
2670  /* add this line to the table of acceptable lines */
2671  if (acceptable) {
2672  (*l)++;
2673  (*lt) = (BiddyVerilogLine **) realloc((*lt), (*l) * sizeof(BiddyVerilogLine *)); /* create or enlarge table of lines */
2674  ln = (BiddyVerilogLine *) calloc(1, sizeof(BiddyVerilogLine)); /* declare an instance of a line */
2675  ln->keyword = strdup(keyword);
2676  ln->line = strdup(token[0]);
2677  for (j=1; j<i; j++) concat(&(ln->line),token[j]);
2678  (*lt)[(*l)-1] = ln;
2679  }
2680 
2681  }
2682 
2683  if (keyword) free(keyword);
2684  if (buffer) free(buffer);
2685 
2686  /* DEBUGGING - print summary of the module */
2687  /*
2688  printModuleSummary(m);
2689  */
2690 }
2691 
2696 static void
2697 createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c)
2698 {
2699  BiddyVerilogModule *m;
2700  unsigned int i=0, j=0, k=0, l=0;
2701  int in=0, id=0, index=0;
2702  unsigned int activemodule=0;
2703  Biddy_String keyword, buffer;
2704  Biddy_String token[TOKENNUM]; /* array to hold tokens for one line */
2705  Biddy_Boolean ok;
2706  Biddy_String tmptoken;
2707 
2708  memset(token, 0, sizeof(char*) * TOKENNUM);
2709 
2710  m = mt[0]; /* target module is the first one in the table */
2711 
2712  /* initialization of the circuit */
2713  c->inputcount = m->inputcount; /* set the number of inputs for the ciruit */
2714  c->outputcount = m->outputcount; /* set the number of outputs for the circuit */
2715  c->wirecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of wires for the circuit */
2716  c->nodecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of nodes for the circuit */
2717  c->wires = (BiddyVerilogWire **) calloc(c->wirecount,sizeof(BiddyVerilogWire *)); /* allocate a contiguous array to index every wire */
2718  c->nodes = (BiddyVerilogNode **) calloc(c->nodecount,sizeof(BiddyVerilogNode *)); /* allocate a contiguous array to index every node */
2719 
2720  id = 0;
2721  for (i=0; i < m->inputcount; i++) { /* store the names of primary inputs */
2722  c->inputs[i] = (Biddy_String) calloc(strlen(m->inputs[i]) + 1, sizeof (char));
2723  strcpy(c->inputs[i],m->inputs[i]);
2724  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2725  buildNode(c->nodes[id],(Biddy_String)"input", m->inputs[i]);
2726  id++;
2727  }
2728  for (i=0; i < m->outputcount; i++) { /* store the names of primary outputs */
2729  c->outputs[i] = (Biddy_String) calloc(strlen(m->outputs[i]) + 1, sizeof(char));
2730  strcpy(c->outputs[i],m->outputs[i]);
2731  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2732  buildNode(c->nodes[id],(Biddy_String)"output",m->outputs[i]);
2733  id++;
2734  }
2735  for (i=0; i < m->wirecount; i++) { /* store the names of wires */
2736  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2737  buildNode(c->nodes[id],(Biddy_String)"wire",m->wires[i]);
2738  id++;
2739  }
2740  for (i=0; i < m->gatecount; i++) { /* store the names of gates */
2741  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
2742  buildNode(c->nodes[id],(Biddy_String)"gate",m->gates[i]);
2743  id++;
2744  }
2745 
2746  index = 0;
2747  for (l=0; l<linecount;l++) {
2748  keyword = lt[l]->keyword;
2749  buffer = lt[l]->line;
2750 
2751  if (!strcmp(keyword,"module")) {
2752  activemodule++;
2753  continue;
2754  }
2755 
2756  if (!strcmp(keyword,"endmodule")) {
2757  continue;
2758  }
2759 
2760  if (activemodule > 1) {
2761  /* TO DO: MULTIPLE MODULES ARE NOT FULLY SUPPORTED, YET */
2762  continue;
2763  }
2764 
2765  if (!strcmp(keyword,"input")) {
2766  continue;
2767  }
2768  if (!strcmp(keyword,"output")) {
2769  continue;
2770  }
2771  if (!strcmp(keyword,"wire")) {
2772  continue;
2773  }
2774  if (!strcmp(keyword,"reg")) {
2775  continue;
2776  }
2777  if (!strcmp(keyword,"assign")) {
2778  continue;
2779  }
2780 
2781  /* tokenize the line to extract data */
2782  i=0;
2783  token[0] = strtok(buffer," ");
2784  while(token[i]!= NULL) {
2785  /* DEBUGGING */
2786  /*
2787  printf("(#%d) TOKENIZE: <%s>\n",i,token[i]);
2788  */
2789  i++;
2790  token[i] = strtok(NULL," ");
2791  }
2792 
2793  if (!isGate(keyword)) {
2794  printf("WARNING (createVerilogCircuit): SKIP <%s>\n",buffer);
2795  continue;
2796  }
2797 
2798  if (!m->outputFirst) {
2799  /* m->outputFirst == FALSE iff "nand NAND2_1 (N1, N2, N3);" defines N3 = NAND(N1,N2) */
2800  /* m->outputFirst == TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3) */
2801  /* exchange token[2] and token[i-1] */
2802  tmptoken = token[2];
2803  token[2] = token[i-1];
2804  token[i-1] = tmptoken;
2805  }
2806 
2807  /* A. Check or create wires for all the gate inputs */
2808  /* if wire is not known it will be treated as a primary input */
2809  for (j = 3; j < i; j++) {
2810  if (!isDefined(c,token[j])) {
2811  ok = FALSE;
2812  for (k=0; k < m->wirecount; k++) { /* check the names of wires */
2813  if (!strcmp(m->wires[k],token[j])) {
2814  printf("ERROR (createVerilogCircuit): wire %s used before defined!\n",token[j]);
2815  exit(1);
2816  }
2817  }
2818  for (k=0; !ok && k < m->inputcount; k++) { /* check the names of primary inputs */
2819  if (!strcmp(m->inputs[k],token[j])) ok = TRUE;
2820  }
2821  if (!ok) {
2822  printf("WARNING (createVerilogCircuit): wire %s treated as primary input!\n",token[j]);
2823  }
2824  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2825  buildWire(c,c->wires[index],(Biddy_String)"I",token[j]);
2826  /* assign inputs to the wires representing gate inputs */
2827  /* NOT NEEDED */
2828  /* assign outputs to the wires representing gate inputs */
2829  /* NOT USED */
2830  index++;
2831  }
2832  }
2833 
2834  /* B. Create a wire for the gate */
2835  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2836  buildWire(c,c->wires[index],keyword,token[1]);
2837  /* assign inputs to the wire representing gate */
2838  in = 0;
2839  for (j = 3; j < i; j++) {
2840  c->wires[index]->inputs[in] = getNodeIdByName(c,token[j]);
2841  c->wires[index]->inputcount++;
2842  in++;
2843  }
2844  /* assign outputs to the wire representing gate */
2845  /* NOT USED */
2846  index++;
2847 
2848  /* C. Check or create a wire for the gate output */
2849  if (!isDefined(c,token[2])) { /* if wire is not already defined */
2850  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
2851  buildWire(c,c->wires[index],(Biddy_String)"W",token[2]);
2852  /* assign inputs to the wire representing gate ouput */
2853  c->wires[index]->inputs[0] = getNodeIdByName(c,token[1]);
2854  c->wires[index]->inputcount = 1;
2855  /* assign outputs to the wire representing gate ouput */
2856  /* NOT USED */
2857  index++;
2858  } else { /* if wire is already defined */
2859  getWireByName(c,token[2])->inputs[0] = getNodeIdByName(c,token[1]); /* find the wire and attach an input to it */
2860  getWireByName(c,token[2])->inputcount = 1;
2861  }
2862 
2863  }
2864 
2865  c->wirecount = index;
2866 
2867  /* c->wires[i]->fanout is the count of gates (and wires), where */
2868  /* this wire is used as an input */
2869  i=0;
2870  while (i<c->wirecount && c->wires[i] != NULL) {
2871  for (j=0; j<c->wires[i]->inputcount; j++) {
2872  (getWireById(c,c->wires[i]->inputs[j])->fanout)++;
2873  /* DEBUGGING */
2874  /*
2875  printf("Increment TTL for wire %d\n",c->wires[i]->inputs[j]);
2876  */
2877  }
2878  i++;
2879  }
2880 
2881  /* DEBUGGING - print summary of the circuit */
2882  /*
2883  printCircuitSummary(c);
2884  */
2885 }
2886 
2895 static void
2896 createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix)
2897 {
2898  unsigned int i,j;
2899  BiddyVerilogWire *w;
2900  Biddy_Edge f;
2901 
2902  /* DEBUGGING */
2903  /*
2904  printf("Creating %d primary inputs\n",c->inputcount);
2905  */
2906 
2907  /* DEBUGGING */
2908  /*
2909  for (i = 0; i < c->inputcount; i++) {
2910  printf("%s ",c->inputs[i]);
2911  }
2912  if (c->inputcount) printf("\n");
2913  */
2914 
2915  /* DEBUGGING */
2916  /*
2917  printf("Creating %d primary outputs\n",c->outputcount);
2918  */
2919 
2920  /* DEBUGGING */
2921  /*
2922  for (i = 0; i < c->outputcount; i++) {
2923  printf("%s ",c->outputs[i]);
2924  }
2925  if (c->outputcount) printf("\n");
2926  */
2927 
2928  /* DEBUGGING */
2929  /*
2930  printf("Creating %d wires\n",c->wirecount);
2931  */
2932 
2933  /* create all BDD variables - important for ZBDD and TZBDD */
2934  for (i = 0; i < c->nodecount; i++) {
2935  if (!strcmp(c->nodes[i]->type,"input")) {
2936  Biddy_Managed_FoaVariable(MNG,c->nodes[i]->name,TRUE); /* TO DO: add prefix */
2937  }
2938  if (!strcmp(c->nodes[i]->type,"extern")) {
2939  Biddy_Managed_FoaVariable(MNG,c->nodes[i]->name,TRUE); /* TO DO: add prefix */
2940  }
2941  }
2942 
2943  /* prepare c->wires[i]->ttl which will be used to guide GC */
2944  for (i = 0; i < c->wirecount; i++) {
2945  c->wires[i]->ttl = 0;
2946  }
2947  for (i = 0; i < c->wirecount; i++) {
2948  for (j = 0; j < c->wires[i]->inputcount; j++) {
2949  w = getWireById(c,c->wires[i]->inputs[j]);
2950  (w->ttl)++;
2951  if (w->ttl == w->fanout) {
2952  w->ttl = i;
2953  }
2954  }
2955  }
2956  for (i = 0; i < c->outputcount; i++) {
2957  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
2958  if (w) {
2959  w->ttl = c->wirecount - 1;
2960  }
2961  }
2962  for (i = 0; i < c->wirecount; i++) {
2963  if (c->wires[i]->ttl) c->wires[i]->ttl = c->wires[i]->ttl - i;
2964  }
2965 
2966  for (i = 0; i < c->wirecount; i++) {
2967 
2968  /* REPORT PROGRESS */
2969 
2970  printf("#%d",i);
2971  if (i == c->wirecount-1) printf("\n");
2972 
2973 
2974  /* DEBUGGING */
2975  /*
2976  printf("Creating c->wire[%d], ",i);
2977  printf("ID: %d, ",c->wires[i]->id);
2978  printf("name: %s, ",c->nodes[c->wires[i]->id]->name);
2979  printf("type: %s, ",c->wires[i]->type);
2980  printf("fanout: %d, ",c->wires[i]->fanout);
2981  printf("ttl: %d, ",c->wires[i]->ttl);
2982  printf("Inputs (%d): ",c->wires[i]->inputcount);
2983  if (strcmp(c->wires[i]->type,"I")) {
2984  if (c->wires[i]->inputcount) {
2985  for (j=0;j<c->wires[i]->inputcount;j++) {
2986  printf("%d ",c->wires[i]->inputs[j]);
2987  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
2988  printf("ERROR (gate ordering is wrong)");
2989  }
2990  }
2991  } else {
2992  printf("ERROR (wire must be a primary input or it must have some inputs)");
2993  }
2994  } else {
2995  if (c->wires[i]->inputcount) {
2996  printf("ERROR (primary input cannot have additional inputs)");
2997  } else {
2998  printf("/");
2999  }
3000  }
3001  printf("\n");
3002  */
3003 
3004  f = biddyNull;
3005 
3006  if (!strcmp(c->wires[i]->type,"I")) {
3007  if (c->wires[i]->inputcount) {
3008  printf("ERROR (primary input cannot have additional inputs)\n");
3009  } else {
3010  f = Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_GetVariable(MNG,c->nodes[c->wires[i]->id]->name)); /* TO DO: add prefix */
3011  }
3012  }
3013  else if (!strcmp(c->wires[i]->type,"M")) {
3014  /* TO DO: this will be used for gates defined by other modules */
3015  }
3016  else {
3017  if (c->wires[i]->inputcount) {
3018  for (j=0; j<c->wires[i]->inputcount; j++) {
3019  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3020  printf("ERROR (gate ordering is wrong)\n");
3021  }
3022  }
3023 
3024  if (!strcmp(c->wires[i]->type,"W")) {
3025  if (c->wires[i]->inputcount == 1) {
3026  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3027  } else {
3028  printf("ERROR (internal wire must have exactly one input)\n");
3029  }
3030  }
3031 
3032  else if (!strcmp(c->wires[i]->type,"buf"))
3033  {
3034  if (c->wires[i]->inputcount != 1) {
3035  printf("ERROR (buf gate must have exactly 1 input)\n");
3036  } else {
3037  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3038  }
3039  }
3040 
3041  else if (!strcmp(c->wires[i]->type,"and"))
3042  {
3043  f = biddyOne;
3044  for (j=0; j<c->wires[i]->inputcount; j++) {
3045  f = Biddy_Managed_And(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3046  }
3047  }
3048 
3049  else if (!strcmp(c->wires[i]->type,"nand"))
3050  {
3051  f = biddyOne;
3052  for (j=0; j<c->wires[i]->inputcount; j++) {
3053  f = Biddy_Managed_And(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3054  }
3055  f = Biddy_Managed_Not(MNG,f);
3056  }
3057 
3058  else if (!strcmp(c->wires[i]->type,"or"))
3059  {
3060  f = biddyZero;
3061  for (j=0; j<c->wires[i]->inputcount; j++) {
3062  f = Biddy_Managed_Or(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3063  }
3064  }
3065 
3066  else if (!strcmp(c->wires[i]->type,"nor"))
3067  {
3068  f = biddyZero;
3069  for (j=0; j<c->wires[i]->inputcount; j++) {
3070  f = Biddy_Managed_Or(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3071  }
3072  f = Biddy_Managed_Not(MNG,f);
3073  }
3074 
3075  else if (!strcmp(c->wires[i]->type,"xor"))
3076  {
3077  if (c->wires[i]->inputcount != 2) {
3078  printf("ERROR (xor gate not having exactly 2 inputs is not supported)\n");
3079  } else {
3080  f = Biddy_Managed_Xor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3081  getWireById(c,c->wires[i]->inputs[1])->bdd);
3082  }
3083  }
3084 
3085  else if (!strcmp(c->wires[i]->type,"xnor"))
3086  {
3087  if (c->wires[i]->inputcount != 2) {
3088  printf("ERROR (xnor gate not having exactly 2 inputs is not supported)\n");
3089  } else {
3090  f = Biddy_Managed_Xor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3091  getWireById(c,c->wires[i]->inputs[1])->bdd);
3092  f = Biddy_Managed_Not(MNG,f);
3093  }
3094  }
3095 
3096  else if (!strcmp(c->wires[i]->type,"not") ||
3097  !strcmp(c->wires[i]->type,"inv"))
3098  {
3099  if (c->wires[i]->inputcount != 1) {
3100  printf("ERROR (not gate must have exactly 1 input)\n");
3101  } else {
3102  f = Biddy_Managed_Not(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd);
3103  }
3104  }
3105 
3106  else {
3107  printf("ERROR (unimplemented type: %s)\n",c->wires[i]->type);
3108  }
3109 
3110  } else {
3111  printf("ERROR (wire must be a primary input or it must have some inputs)\n");
3112  }
3113  }
3114 
3115  c->wires[i]->bdd = f;
3116 
3117  Biddy_Managed_KeepFormulaProlonged(MNG,f,c->wires[i]->ttl);
3118  Biddy_Managed_Clean(MNG);
3119  }
3120 
3121  for (i = 0; i < c->outputcount; i++) {
3122  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3123  if (w) {
3124  f = w->bdd;
3125  } else {
3126  f = biddyZero; /* undefined outputs are represented with biddyZero */
3127  }
3128  Biddy_Managed_AddFormula(MNG,c->outputs[i],f,1); /* TO DO: add prefix */
3129  }
3130  Biddy_Managed_Clean(MNG);
3131 
3132  /*
3133  printf("Report on primary outputs\n");
3134  for (i = 0; i < c->outputcount; i++) {
3135  f = getWireByName(c,c->outputs[i])->bdd;
3136  printf("%s - %d nodes / %d nodes without complement edge\n",
3137  c->outputs[i],
3138  Biddy_Managed_CountNodes(MNG,f),
3139  Biddy_Managed_CountNodesPlain(MNG,f)
3140  );
3141  }
3142  */
3143 
3144 
3145  j = 0;
3146  for (i = 0; i < c->outputcount; i++) {
3147  f = getWireByName(c,c->outputs[i])->bdd;
3148  j = j + Biddy_Managed_CountNodes(MNG,f);
3149  }
3150  printf("The sum of BDD sizes for all outputs: %u\n",j);
3151 
3152 
3153 }
3154 
3159 static void
3160 parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count)
3161 {
3162  int v,v1,v2;
3163  char *sig_vector; /* array to hold tokens for the line */
3164 
3165  sig_vector = strtok(token[*index],":"); /* tokenize the vector to extract vector width */
3166  v1 = atoi(sig_vector); /* starting index for the vector */
3167  sig_vector = strtok(NULL, ":");
3168  v2 = atoi(sig_vector); /* ending index for the vector */
3169  (*index)++; /* get vector name from the next token */
3170  for (v = v2; v <= v1; v++) { /* add the vector signals to the array of signals */
3171  int wordsize = (int) strlen(token[*index]); /* size of the string read from the line */
3172  signal_arr [*count] = (Biddy_String) calloc(wordsize + 1, sizeof(char)); /* allocating memory for signal string */
3173  strcpy(signal_arr [*count], token[*index]); /* add the signal name to the array of signals */
3174  (*count)++; /* update the number of signals in the circuit */
3175  }
3176 }
3177 
3178 static void
3179 printModuleSummary(BiddyVerilogModule *m)
3180 {
3181  unsigned int i;
3182 
3183  printf("************** Module %s statistical results *************\n", m->name);
3184 
3185  printf("Number of primary inputs: %d\n", m->inputcount);
3186  for (i = 0; i < m->inputcount; i++)
3187  printf("%s ", m->inputs[i]);
3188  if (m->inputcount) printf("\n");
3189 
3190  printf("Number of primary outputs: %d\n", m->outputcount);
3191  for (i = 0; i < m->outputcount; i++)
3192  printf("%s ", m->outputs[i]);
3193  if ( m->outputcount) printf("\n");
3194 
3195  printf("Number of gates: %d\n", m->gatecount);
3196  for (i = 0; i < m->gatecount; i++)
3197  printf("%s ", m->gates[i]);
3198  if (m->gatecount) printf("\n");
3199 
3200  printf("Number of wires: %d\n", m->wirecount);
3201  for (i = 0; i < m->wirecount; i++)
3202  printf("%s ", m->wires[i]);
3203  if (m->wirecount) printf("\n");
3204 
3205  printf("Number of regs: %d\n", m->regcount);
3206  for (i = 0; i < m->regcount; i++)
3207  printf("%s ", m->regs[i]);
3208  if (m->regcount) printf("\n");
3209 
3210  printf("*************************** END **************************\n");
3211 }
3212 
3217 static void
3218 printCircuitSummary(BiddyVerilogCircuit *c)
3219 {
3220  unsigned int i,j;
3221 
3222  printf("************** Circuit %s statistical results *************\n", c->name);
3223 
3224  printf("Circuit size: %d\n", c->nodecount);
3225 
3226  printf("Number of primary inputs: %d\n", c->inputcount);
3227  for (i = 0; i < c->inputcount; i++)
3228  printf("%s ", c->inputs[i]);
3229  if (c->inputcount) printf("\n");
3230 
3231  printf("Number of primary outputs: %d\n", c->outputcount);
3232  for (i = 0; i < c->outputcount; i++)
3233  printf("%s ", c->outputs[i]);
3234  if (c->outputcount) printf("\n");
3235 
3236  i=0;
3237  while (i<c->wirecount && c->wires[i] != NULL) {
3238  printf ("c->wire[%d]->type: %s, ",i, c->wires[i]->type);
3239  printf ("ID: %d, ", c->wires[i]->id);
3240  printf ("name: %s, ", c->nodes[c->wires[i]->id]->name);
3241 
3242  printf ("\nInputs (%d): ", c->wires[i]->inputcount); /* wire inputs */
3243  for (j=0; j<c->wires[i]->inputcount; j++)
3244  printf ("%d ",c->wires[i]->inputs[j]);
3245 
3246  printf ("\nOutputs (%d): ", c->wires[i]->outputcount); /* wire outputs */
3247  for (j=0; j<c->wires[i]->outputcount; j++)
3248  printf ("%d ",c->wires[i]->outputs[j]);
3249 
3250  i++;
3251  printf ("\n");
3252  }
3253 
3254  printf("*************************** END **************************\n");
3255 }
3256 
3262 static Biddy_Boolean
3263 isGate(Biddy_String word)
3264 {
3265  int i;
3266  for (i = 0; i < GATESNUM; i++)
3267  if (strcmp(word,VerilogFileGateName[i]) == 0)
3268  return TRUE;
3269  return FALSE;
3270 }
3271 
3277 static Biddy_Boolean
3278 isSignalVector(Biddy_String word)
3279 {
3280  unsigned int i;
3281  for (i = 0; i < strlen(word); i++)
3282  if (word[i] == ':')
3283  return TRUE;
3284  return FALSE;
3285 }
3286 
3292 static Biddy_Boolean
3293 isEndOfLine(Biddy_String source)
3294 {
3295  Biddy_String pchar = strchr(source, ';');
3296  return (pchar == NULL) ? FALSE : TRUE;
3297 }
3298 
3304 static Biddy_Boolean
3305 isDefined(BiddyVerilogCircuit *c, Biddy_String name)
3306 {
3307  unsigned int i;
3308  for (i=0; (i < c->wirecount) && c->wires[i]; i++) {
3309  if (strcmp(c->nodes[c->wires[i]->id]->name, name) == 0) return TRUE;
3310  }
3311  return FALSE;
3312 }
3313 
3318 static void
3319 buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name)
3320 {
3321  n->type = strdup(type);
3322  n->name = strdup(name);
3323 }
3324 
3329 static void
3330 buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name)
3331 {
3332  int id;
3333 
3334  /* TO DO: check if wire with the same name does not already exists */
3335 
3336  if ((id = getNodeIdByName(c,name)) == -1) {
3337  printf("ERROR (buildWire): node %s does not exists!\n",name);
3338  exit(1);
3339  }
3340  w->id = id; /* wire ID */
3341  w->type = strdup(type); /* wire type */
3342  w->inputcount = 0; /* initial number of inputs */
3343  w->outputcount = 0; /* initial number of outputs */
3344  w->fanout = 0;
3345  w->ttl = 0;
3346  w->bdd = biddyNull;
3347 
3348  /* DEBUGGING */
3349  /*
3350  printf("Creating wire: id: %d, type: %s\n", w->id, w->type);
3351  */
3352 }
3353 
3359 static int
3360 getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name)
3361 {
3362  unsigned int i;
3363  if (strcmp(name,c->nodes[c->nodecount-1]->name) == 0) return (int) c->nodecount-1;
3364  for (i=0; i < c->nodecount; i++) {
3365  if (strcmp(name,c->nodes[i]->name) == 0) return (int) i;
3366  }
3367  return -1;
3368 }
3369 
3375 static BiddyVerilogWire *
3376 getWireById(BiddyVerilogCircuit *c, int id)
3377 {
3378  unsigned int i;
3379  for (i=0; i < c->wirecount; i++) {
3380  if (c->wires[i]->id == id) return c->wires[i];
3381  }
3382  return NULL;
3383 }
3384 
3390 static BiddyVerilogWire *
3391 getWireByName(BiddyVerilogCircuit *c, Biddy_String name)
3392 {
3393  unsigned int i;
3394  for (i=0; i < c->wirecount; i++) {
3395  if (strcmp(name, c->nodes[c->wires[i]->id]->name) == 0) return c->wires[i];
3396  }
3397  return NULL;
3398 }
3399 
3404 static Biddy_String
3405 trim(Biddy_String source)
3406 {
3407  unsigned int sr_length;
3408 
3409  sr_length = (unsigned int) strlen(source);
3410  while (sr_length && ((source[sr_length-1] == ' ') ||
3411  (source[sr_length-1] == '\t') ||
3412  (source[sr_length-1] == 10) ||
3413  (source[sr_length-1] == 13)))
3414  {
3415  source[sr_length-1] = 0;
3416  sr_length = (unsigned int) strlen(source);
3417  }
3418 
3419  return source;
3420 }
3421 
3422 static void
3423 concat(char **s1, const char *s2)
3424 {
3425  if (s2) {
3426  *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1+1);
3427  strcat(*s1," ");
3428  strcat(*s1,s2);
3429  }
3430 }
3431 
3432 static void
3433 WriteBDD(Biddy_Manager MNG, Biddy_Edge f)
3434 {
3435  Biddy_Variable v;
3436  Biddy_String var;
3437 
3438  if (Biddy_GetMark(f)) {
3439  printf("*");
3440  }
3441  if ((v = Biddy_GetTag(f))) {
3442  printf("<%s>",Biddy_Managed_GetVariableName(MNG,v));
3443  }
3444 
3445  var = Biddy_Managed_GetTopVariableName(MNG,f);
3446  printf("%s",var);
3447 
3448  if (!Biddy_IsTerminal(f)) {
3449  printf("(");
3450  WriteBDD(MNG,BiddyE(f));
3451  printf(")(");
3452  WriteBDD(MNG,BiddyT(f));
3453  printf(")");
3454  }
3455 }
3456 
3457 static void
3458 WriteBDDx(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f, unsigned int *line)
3459 {
3460  Biddy_String var;
3461 
3462  if (Biddy_GetMark(f)) {
3463  fprintf(funfile,"* ");
3464  }
3465 
3466  *line = *line + 2;
3467 
3468  var = Biddy_Managed_GetTopVariableName(MNG,f);
3469  fprintf(funfile,"%s",var);
3470 
3471  *line = *line + (unsigned int)strlen(var);
3472 
3473  if (!Biddy_IsTerminal(f)) {
3474  if (*line >= 80) {
3475  fprintf(funfile,"\n");
3476  *line = 0;
3477  }
3478  fprintf(funfile," (");
3479  *line = *line + 2;
3480  WriteBDDx(MNG,funfile,BiddyE(f),line);
3481  if (*line >= 80) {
3482  fprintf(funfile,"\n");
3483  *line = 0;
3484  }
3485  fprintf(funfile,") (");
3486  *line = *line + 3;
3487  WriteBDDx(MNG,funfile,BiddyT(f),line);
3488  if (*line >= 80) {
3489  fprintf(funfile,"\n");
3490  *line = 0;
3491  }
3492  fprintf(funfile,")");
3493  *line = *line + 1;
3494  }
3495 }
3496 
3497 static void
3498 WriteProduct(Biddy_Manager MNG, BiddyVarList *l)
3499 {
3500  if (l) {
3501  WriteProduct(MNG,l->next);
3502  printf(" ");
3503  if (l->negative) {
3504  printf("*");
3505  }
3506  printf("%s",Biddy_Managed_GetVariableName(MNG,l->v));
3507  }
3508 }
3509 
3510 static void
3511 WriteProductx(Biddy_Manager MNG, FILE *s, BiddyVarList *l)
3512 {
3513  if (l) {
3514  WriteProductx(MNG,s,l->next);
3515  fprintf(s," ");
3516  if (l->negative) {
3517  fprintf(s,"*");
3518  }
3519  fprintf(s,"%s",Biddy_Managed_GetVariableName(MNG,l->v));
3520  }
3521 }
3522 
3523 static void
3524 WriteSOP(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable top,
3525  Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize)
3526 {
3527  BiddyVarList tmp;
3528  Biddy_Variable v;
3529 
3530  if (*maxsize == 0) return; /* SOP to large */
3531 
3532  v = BiddyV(f);
3533 
3534  /* DEBUGGING */
3535  /*
3536  printf("WriteSOP: top = %u (%s), v = %u (%s)\n",top,Biddy_Managed_GetVariableName(MNG,top),v,Biddy_Managed_GetVariableName(MNG,v));
3537  */
3538 
3539  assert( !(BiddyIsSmaller(BiddyV(f),top)) );
3540 
3541  if ((top != v) && (f != biddyZero)) {
3542 
3543  if (biddyManagerType == BIDDYTYPEOBDD) {
3544  /* IMPLEMENTED */
3545  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3546  /* IMPLEMENTED */
3547  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3548  /* IMPLEMENTED */
3549  tmp.next = l;
3550  tmp.v = top;
3551  tmp.negative = TRUE; /* left successor */
3552  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize);
3553  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3554  /* IMPLEMENTED */
3555  tmp.next = l;
3556  tmp.v = top;
3557  tmp.negative = TRUE; /* left successor */
3558  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize);
3559  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3560  /* IMPLEMENTED */
3561  tmp.next = l;
3562  tmp.v = top;
3563  tmp.negative = TRUE; /* left successor */
3564  WriteSOP(MNG,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize);
3565  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3566  {
3567  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3568  return;
3569  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
3570  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
3571  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
3572  {
3573  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3574  return;
3575  } else {
3576  fprintf(stderr,"WriteSOP: Unsupported BDD type!\n");
3577  return;
3578  }
3579 
3580  } else if (v == 0) {
3581 
3582  if (!mark) {
3583  printf(" + ");
3584  if (l) {
3585  WriteProduct(MNG,l);
3586  printf("\n");
3587  (*maxsize)--;
3588  } else {
3589  printf(" 1");
3590  }
3591  } else {
3592  if (!l) {
3593  printf(" + 0");
3594  }
3595  }
3596 
3597  } else {
3598 
3599  tmp.next = l;
3600  tmp.v = v;
3601  tmp.negative = TRUE; /* left successor */
3602 
3603  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3604  WriteSOP(MNG,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize);
3605  }
3606  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3607  WriteSOP(MNG,BiddyE(f),biddyVariableTable.table[v].next,mark,&tmp,maxsize);
3608  }
3609  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3610  WriteSOP(MNG,BiddyE(f),Biddy_GetTag(BiddyE(f)),Biddy_GetMark(BiddyE(f)),&tmp,maxsize);
3611  }
3612 
3613  tmp.negative = FALSE; /* right successor */
3614 
3615  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3616  WriteSOP(MNG,BiddyT(f),BiddyV(BiddyT(f)),mark,&tmp,maxsize);
3617  }
3618  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3619  WriteSOP(MNG,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize);
3620  }
3621  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3622  WriteSOP(MNG,BiddyT(f),Biddy_GetTag(BiddyT(f)),Biddy_GetMark(BiddyT(f)),&tmp,maxsize);
3623  }
3624 
3625  }
3626 }
3627 
3628 static void
3629 WriteSOPx(Biddy_Manager MNG, FILE *s, Biddy_Edge f, Biddy_Variable top,
3630  Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize)
3631 {
3632  BiddyVarList tmp;
3633  Biddy_Variable v;
3634 
3635  if (*maxsize == 0) return; /* SOP to large */
3636 
3637  v = BiddyV(f);
3638 
3639  /* DEBUGGING */
3640  /*
3641  printf("WriteSOPx: top = %u (%s), v = %u (%s)\n",top,Biddy_Managed_GetVariableName(MNG,top),v,Biddy_Managed_GetVariableName(MNG,v));
3642  */
3643 
3644  assert( !(BiddyIsSmaller(BiddyV(f),top)) );
3645 
3646  if ((top != v) && (f != biddyZero)) {
3647 
3648  if (biddyManagerType == BIDDYTYPEOBDD) {
3649  /* IMPLEMENTED */
3650  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3651  /* IMPLEMENTED */
3652  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3653  /* IMPLEMENTED */
3654  tmp.next = l;
3655  tmp.v = top;
3656  tmp.negative = TRUE; /* left successor */
3657  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize);
3658  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3659  /* IMPLEMENTED */
3660  tmp.next = l;
3661  tmp.v = top;
3662  tmp.negative = TRUE; /* left successor */
3663  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize);
3664  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3665  /* IMPLEMENTED */
3666  tmp.next = l;
3667  tmp.v = top;
3668  tmp.negative = TRUE; /* left successor */
3669  WriteSOPx(MNG,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize);
3670  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3671  {
3672  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3673  return;
3674  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
3675  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
3676  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
3677  {
3678  fprintf(stderr,"WriteSOP: this BDD type is not supported, yet!\n");
3679  return;
3680  } else {
3681  fprintf(stderr,"WriteSOP: Unsupported BDD type!\n");
3682  return;
3683  }
3684 
3685  } else if (v == 0) {
3686 
3687  if (!mark) {
3688  fprintf(s," + ");
3689  if (l) {
3690  WriteProductx(MNG,s,l);
3691  fprintf(s,"\n");
3692  (*maxsize)--;
3693  } else {
3694  fprintf(s," 1");
3695  }
3696  } else {
3697  if (!l) {
3698  fprintf(s," + 0");
3699  }
3700  }
3701 
3702  } else {
3703 
3704  tmp.next = l;
3705  tmp.v = v;
3706  tmp.negative = TRUE; /* left successor */
3707 
3708  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3709  WriteSOPx(MNG,s,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ Biddy_GetMark(BiddyE(f))),&tmp,maxsize);
3710  }
3711  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3712  WriteSOPx(MNG,s,BiddyE(f),biddyVariableTable.table[v].next,mark,&tmp,maxsize);
3713  }
3714  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3715  WriteSOPx(MNG,s,BiddyE(f),Biddy_GetTag(BiddyE(f)),Biddy_GetMark(BiddyE(f)),&tmp,maxsize);
3716  }
3717 
3718  tmp.negative = FALSE; /* right successor */
3719 
3720  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3721  WriteSOPx(MNG,s,BiddyT(f),BiddyV(BiddyT(f)),mark,&tmp,maxsize);
3722  }
3723  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3724  WriteSOPx(MNG,s,BiddyT(f),biddyVariableTable.table[v].next,Biddy_GetMark(BiddyT(f)),&tmp,maxsize);
3725  }
3726  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
3727  WriteSOPx(MNG,s,BiddyT(f),Biddy_GetTag(BiddyT(f)),Biddy_GetMark(BiddyT(f)),&tmp,maxsize);
3728  }
3729 
3730  }
3731 }
3732 
3733 static unsigned int
3734 enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n)
3735 {
3736  if (!Biddy_Managed_IsSelected(MNG,f)) {
3737  if (Biddy_IsTerminal(f)) {
3738  } else {
3739  Biddy_Managed_SelectNode(MNG,f);
3740  n++;
3741  BiddySetEnumerator(f,n);
3742 
3743  /* one or both are terminal node */
3744  /* every instance of terminal node is enumerated */
3745  if (Biddy_IsTerminal(BiddyE(f)) || Biddy_IsTerminal(BiddyT(f))) {
3746 
3747  if (((biddyManagerType == BIDDYTYPEOBDD) ||
3748  (biddyManagerType == BIDDYTYPEZBDD) ||
3749  (biddyManagerType == BIDDYTYPETZBDD)
3750  ) && (Biddy_GetMark(BiddyE(f)) != Biddy_GetMark(BiddyT(f))))
3751  {
3752  /* two terminal nodes only if complemented edges are not used and they are different */
3753  if (Biddy_IsTerminal(BiddyE(f))) {
3754  n++;
3755  }
3756  if (Biddy_IsTerminal(BiddyT(f))) {
3757  n++;
3758  }
3759  }
3760  else {
3761  /* only one terminal node */
3762  n++;
3763  }
3764 
3765  }
3766 
3767  if (!Biddy_IsTerminal(BiddyE(f))) {
3768  n = enumerateNodes(MNG,BiddyE(f),n);
3769  }
3770  if (!Biddy_IsTerminal(BiddyT(f))) {
3771  n = enumerateNodes(MNG,BiddyT(f),n);
3772  }
3773  }
3774  }
3775  return n;
3776 }
3777 
3778 static void
3779 WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd)
3780 {
3781  BiddyLocalInfo *li;
3782  Biddy_String name,hash;
3783  Biddy_Variable v;
3784  BiddyLocalInfo *li2;
3785 
3786  if (Biddy_IsTerminal(f)) {
3787  if (cudd) {
3788 
3789  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
3790  /*
3791  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
3792  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
3793  fprintf(dotfile,"\"%p\";\n",biddyOne);
3794  */
3795 
3796  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
3797 
3798  fprintf(dotfile,"{ \"CONST NODES\";\n");
3799  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
3800  fprintf(dotfile,"\"1\";\n");
3801 
3802 
3803  fprintf(dotfile,"}\n}\n");
3804  } else {
3805  if ((biddyManagerType == BIDDYTYPEOBDD) ||
3806  (biddyManagerType == BIDDYTYPEZBDD) ||
3807  (biddyManagerType == BIDDYTYPETZBDD))
3808  {
3809  if (f == biddyZero) {
3810  fprintf(dotfile, " node [shape = none, label = \"0\"] %u;\n",1);
3811  } else {
3812  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
3813  }
3814  }
3815  else {
3816  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
3817  }
3818  }
3819  return;
3820  }
3821  if (cudd) {
3823  li = (BiddyLocalInfo *)(BiddyN(f)->list);
3824  while (li->back) {
3825  v = BiddyV(li->back);
3826  if (biddyVariableTable.table[v].value == biddyZero) {
3827  biddyVariableTable.table[v].value = biddyOne;
3828  name = strdup(Biddy_Managed_GetVariableName(MNG,v));
3829  while ((hash = strchr(name,'#'))) hash[0] = '_';
3830  fprintf(dotfile,"{ rank = same; ");
3831  fprintf(dotfile,"\" %s \";\n",name);
3832  free(name);
3833  li2 = li;
3834  while (li2->back) {
3835  if (BiddyV(li2->back) == v) {
3836  fprintf(dotfile,"\"%p\";\n",li2->back);
3837  }
3838  li2 = &li2[1]; /* next field in the array */
3839  }
3840  fprintf(dotfile,"}\n");
3841  }
3842  li = &li[1]; /* next field in the array */
3843  }
3845 
3846  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
3847  /*
3848  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
3849  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
3850  fprintf(dotfile,"\"%p\";\n",biddyOne);
3851  */
3852 
3853  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
3854 
3855  fprintf(dotfile,"{ \"CONST NODES\";\n");
3856  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
3857  li = (BiddyLocalInfo *)(BiddyN(f)->list);
3858  while (li->back) {
3859  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
3860  fprintf(dotfile,"\"%u\";\n",li->data.enumerator+1);
3861  }
3862  li = &li[1];
3863  }
3864 
3865 
3866  fprintf(dotfile,"}\n}\n");
3867  } else {
3868  li = (BiddyLocalInfo *)(BiddyN(f)->list);
3869  while (li->back) {
3870  if (id == -1) {
3871  name = getname(MNG,li->back);
3872  } else {
3873  name = getshortname(MNG,li->back,id);
3874  }
3875  while ((hash = strchr(name,'#'))) hash[0] = '_';
3876  fprintf(dotfile," node [shape = circle, label = \"%s\"] %u;\n",name,li->data.enumerator);
3877  free(name);
3878  if ((biddyManagerType == BIDDYTYPEOBDD) ||
3879  (biddyManagerType == BIDDYTYPEZBDD) ||
3880  (biddyManagerType == BIDDYTYPETZBDD))
3881  {
3882  if (BiddyE(li->back) == biddyZero) {
3883  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
3884  }
3885  else if (Biddy_IsTerminal(BiddyE(li->back))) {
3886  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
3887  }
3888  if (BiddyT(li->back) == biddyZero) {
3889  if (Biddy_IsTerminal(BiddyE(li->back)) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back)))) {
3890  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+2);
3891  } else {
3892  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
3893  }
3894  }
3895  else if (Biddy_IsTerminal(BiddyT(li->back))) {
3896  if (Biddy_IsTerminal(BiddyE(li->back)) && (Biddy_GetMark(BiddyE(li->back)) != Biddy_GetMark(BiddyT(li->back)))) {
3897  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+2);
3898  } else {
3899  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
3900  }
3901  }
3902  }
3903  else {
3904  if (Biddy_IsTerminal(BiddyE(li->back)) || Biddy_IsTerminal(BiddyT(li->back))) {
3905  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
3906  }
3907  }
3908  li = &li[1]; /* next field in the array */
3909  }
3910  }
3911 }
3912 
3913 static void
3914 WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd)
3915 {
3916  unsigned int n1,n2;
3917  Biddy_Variable tag;
3918 
3919  if (!Biddy_IsTerminal(f) && !Biddy_Managed_IsSelected(MNG,f)) {
3920  Biddy_Managed_SelectNode(MNG,f);
3921  n1 = BiddyGetEnumerator(f);
3922 
3923  if (Biddy_IsTerminal(BiddyE(f))) {
3924  n2 = n1 + 1;
3925  } else {
3926  n2 = BiddyGetEnumerator(BiddyE(f));
3927  }
3928  if (Biddy_GetMark(BiddyE(f))) {
3929  if ((BiddyE(f) != biddyZero) && (tag = Biddy_GetTag(BiddyE(f)))) {
3930  if (cudd) {
3931 
3932  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
3933  /*
3934  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
3935  */
3936 
3937  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
3938 
3939  if (Biddy_IsTerminal(BiddyE(f))) {
3940  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
3941  } else {
3942  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
3943  }
3944 
3945 
3946  } else {
3947 #ifdef LEGACY_DOT
3948  fprintf(dotfile," %u -> %u [style=dotted label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
3949 #else
3950  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
3951 #endif
3952  }
3953  } else {
3954  if (cudd) {
3955 
3956  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
3957  /*
3958  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
3959  */
3960 
3961  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
3962 
3963  if (Biddy_IsTerminal(BiddyE(f))) {
3964  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted];\n",BiddyP(f),n2);
3965  } else {
3966  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
3967  }
3968 
3969 
3970  } else {
3971  if ((biddyManagerType == BIDDYTYPEOBDD) ||
3972  (biddyManagerType == BIDDYTYPEZBDD) ||
3973  (biddyManagerType == BIDDYTYPETZBDD))
3974  {
3975 #ifdef LEGACY_DOT
3976  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
3977 #else
3978  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
3979 #endif
3980  }
3981  else {
3982 #ifdef LEGACY_DOT
3983  fprintf(dotfile," %u -> %u [style=dotted];\n",n1,n2);
3984 #else
3985  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\"];\n",n1,n2);
3986 #endif
3987  }
3988  }
3989  }
3990  } else {
3991  if ((BiddyE(f) != biddyZero) && (tag = Biddy_GetTag(BiddyE(f)))) {
3992  if (cudd) {
3993 
3994  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
3995  /*
3996  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
3997  */
3998 
3999  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4000 
4001  if (Biddy_IsTerminal(BiddyE(f))) {
4002  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4003  } else {
4004  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),Biddy_Managed_GetVariableName(MNG,tag));
4005  }
4006 
4007 
4008  } else {
4009 #ifdef LEGACY_DOT
4010  fprintf(dotfile," %u -> %u [style=dashed label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4011 #else
4012  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4013 #endif
4014  }
4015  } else {
4016  if (cudd) {
4017 
4018  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4019  /*
4020  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
4021  */
4022 
4023  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4024 
4025  if (Biddy_IsTerminal(BiddyE(f))) {
4026  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed];\n",BiddyP(f),n2);
4027  } else {
4028  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
4029  }
4030 
4031 
4032  } else {
4033 #ifdef LEGACY_DOT
4034  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
4035 #else
4036  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
4037 #endif
4038  }
4039  }
4040  }
4041 
4042  if (Biddy_IsTerminal(BiddyT(f))) {
4043  if (((biddyManagerType == BIDDYTYPEOBDD) ||
4044  (biddyManagerType == BIDDYTYPEZBDD) ||
4045  (biddyManagerType == BIDDYTYPETZBDD))
4046  && (Biddy_IsTerminal(BiddyE(f)))
4047  && (Biddy_GetMark(BiddyE(f)) != Biddy_GetMark(BiddyT(f))))
4048  {
4049  n2 = n1 + 2;
4050  }
4051  else {
4052  n2 = n1 + 1;
4053  }
4054  } else {
4055  n2 = BiddyGetEnumerator(BiddyT(f));
4056  }
4057  if (Biddy_GetMark(BiddyT(f))) {
4058  if ((BiddyT(f) != biddyZero) && (tag = Biddy_GetTag(BiddyT(f)))) {
4059  if (cudd) {
4060 
4061  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4062  /*
4063  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4064  */
4065 
4066  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4067 
4068  if (Biddy_IsTerminal(BiddyT(f))) {
4069  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4070  } else {
4071  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4072  }
4073 
4074 
4075  } else {
4076 #ifdef LEGACY_DOT
4077  fprintf(dotfile," %d -> %d [style=bold label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4078 #else
4079  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4080 #endif
4081  }
4082  } else {
4083  if (cudd) {
4084 
4085  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4086  /*
4087  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
4088  */
4089 
4090  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4091 
4092  if (Biddy_IsTerminal(BiddyT(f))) {
4093  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold];\n",BiddyP(f),n2);
4094  } else {
4095  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
4096  }
4097 
4098 
4099  } else {
4100  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4101  (biddyManagerType == BIDDYTYPEZBDD) ||
4102  (biddyManagerType == BIDDYTYPETZBDD))
4103  {
4104 #ifdef LEGACY_DOT
4105  fprintf(dotfile," %d -> %d;\n",n1,n2);
4106 #else
4107  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
4108 #endif
4109  }
4110  else {
4111 #ifdef LEGACY_DOT
4112  fprintf(dotfile," %d -> %d [style=bold];\n",n1,n2);
4113 #else
4114  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\"];\n",n1,n2);
4115 #endif
4116  }
4117  }
4118  }
4119  } else {
4120  if ((BiddyT(f) != biddyZero) && (tag = Biddy_GetTag(BiddyT(f)))) {
4121  if (cudd) {
4122 
4123  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4124  /*
4125  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4126  */
4127 
4128  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4129 
4130  if (Biddy_IsTerminal(BiddyT(f))) {
4131  fprintf(dotfile,"\"%p\" -> \"%u\" [label=\"%s\"];\n",BiddyP(f),n2,Biddy_Managed_GetVariableName(MNG,tag));
4132  } else {
4133  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),Biddy_Managed_GetVariableName(MNG,tag));
4134  }
4135 
4136 
4137  } else {
4138 #ifdef LEGACY_DOT
4139  fprintf(dotfile," %d -> %d [label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4140 #else
4141  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" label=\"%s\"];\n",n1,n2,Biddy_Managed_GetVariableName(MNG,tag));
4142 #endif
4143  }
4144  } else {
4145  if (cudd) {
4146 
4147  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4148  /*
4149  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
4150  */
4151  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4152 
4153 
4154  if (Biddy_IsTerminal(BiddyT(f))) {
4155  fprintf(dotfile,"\"%p\" -> \"%u\";\n",BiddyP(f),n2);
4156  } else {
4157  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
4158  }
4159 
4160 
4161  } else {
4162 #ifdef LEGACY_DOT
4163  fprintf(dotfile," %d -> %d [style=solid];\n",n1,n2);
4164 #else
4165  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
4166 #endif
4167  }
4168  }
4169  }
4170 
4171  WriteDotEdges(MNG,dotfile,BiddyE(f),cudd);
4172  WriteDotEdges(MNG,dotfile,BiddyT(f),cudd);
4173  }
4174 }
4175 
4176 static void
4177 WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f)
4178 {
4179  int n1,n2;
4180  Biddy_Variable tag1,tag2;
4181 
4182  if (!Biddy_IsTerminal(f) && !Biddy_Managed_IsSelected(MNG,f)) {
4183  Biddy_Managed_SelectNode(MNG,f);
4184  n1 = BiddyGetEnumerator(f);
4185 
4186  /* if successors are equal then double line is possible */
4187  if ((BiddyP(BiddyE(f)) != BiddyP(BiddyT(f))) ||
4188  (((biddyManagerType == BIDDYTYPEOBDD) ||
4189  (biddyManagerType == BIDDYTYPEZBDD) ||
4190  (biddyManagerType == BIDDYTYPETZBDD))
4191  &&
4192  (Biddy_GetMark((BiddyE(f))) != Biddy_GetMark((BiddyT(f)))))
4193  )
4194  {
4195 
4196  unsigned int num;
4197 
4198  /* SINGLE LINE */
4199 
4200  num = 0;
4201  if (Biddy_IsTerminal(BiddyE(f))) {
4202  n2 = n1 + 1;
4203  num = 1;
4204  } else {
4205  n2 = BiddyGetEnumerator(BiddyE(f));
4206  }
4207  fprintf(funfile,"connect %d %d ",n1,n2);
4208  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4209  (biddyManagerType == BIDDYTYPEZBDD) ||
4210  (biddyManagerType == BIDDYTYPETZBDD))
4211  {
4212  fprintf(funfile,"l");
4213  }
4214  else {
4215  if (Biddy_GetMark((BiddyE(f)))) {
4216  fprintf(funfile,"li");
4217  } else {
4218  fprintf(funfile,"l");
4219  }
4220  }
4221  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4222  {
4223  if (BiddyE(f) == biddyZero) {
4224  fprintf(funfile," 0\n");
4225  } else {
4226  tag1 = Biddy_GetTag(BiddyE(f));
4227  fprintf(funfile," %s\n",Biddy_Managed_GetVariableName(MNG,tag1));
4228  }
4229  } else {
4230  fprintf(funfile,"\n");
4231  }
4232 
4233  if (Biddy_IsTerminal(BiddyT(f))) {
4234  n2 = n1 + num + 1;
4235  } else {
4236  n2 = BiddyGetEnumerator(BiddyT(f));
4237  }
4238  fprintf(funfile,"connect %d %d ",n1,n2);
4239  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4240  (biddyManagerType == BIDDYTYPEZBDD) ||
4241  (biddyManagerType == BIDDYTYPETZBDD))
4242  {
4243  fprintf(funfile,"r");
4244  }
4245  else {
4246  if (Biddy_GetMark((BiddyT(f)))) {
4247  fprintf(funfile,"ri");
4248  } else {
4249  fprintf(funfile,"r");
4250  }
4251  }
4252  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4253  {
4254  if (BiddyT(f) == biddyZero) {
4255  fprintf(funfile," 0\n");
4256  } else {
4257  tag2 = Biddy_GetTag(BiddyT(f));
4258  fprintf(funfile," %s\n",Biddy_Managed_GetVariableName(MNG,tag2));
4259  }
4260  } else {
4261  fprintf(funfile,"\n");
4262  }
4263 
4264  } else {
4265 
4266  /* DOUBLE LINE */
4267 
4268  if (Biddy_IsTerminal(BiddyE(f))) {
4269  n2 = n1 + 1;
4270  } else {
4271  n2 = BiddyGetEnumerator(BiddyE(f));
4272  }
4273 
4274  fprintf(funfile,"connect %d %d ",n1,n2);
4275  if (Biddy_GetMark((BiddyE(f)))) {
4276  if (Biddy_GetMark((BiddyT(f)))) {
4277  fprintf(funfile,"ei");
4278  } else {
4279  fprintf(funfile,"d");
4280  }
4281  } else {
4282  if (Biddy_GetMark((BiddyT(f)))) {
4283  fprintf(funfile,"di");
4284  } else {
4285  fprintf(funfile,"e");
4286  }
4287  }
4288  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
4289  {
4290  tag1 = Biddy_GetTag(BiddyE(f));
4291  tag2 = Biddy_GetTag(BiddyT(f));
4292  fprintf(funfile," %s %s\n",Biddy_Managed_GetVariableName(MNG,tag1),Biddy_Managed_GetVariableName(MNG,tag2));
4293  } else {
4294  fprintf(funfile,"\n");
4295  }
4296 
4297  }
4298 
4299  WriteBddviewConnections(MNG,funfile,BiddyE(f));
4300  WriteBddviewConnections(MNG,funfile,BiddyT(f));
4301  }
4302 }
4303 
4304 static Biddy_String
4305 getname(Biddy_Manager MNG, void *p) {
4306  unsigned int i;
4307  Biddy_String newname;
4308 
4309  if ((p == biddyZero) &&
4310  ((biddyManagerType == BIDDYTYPEOBDD) ||
4311  (biddyManagerType == BIDDYTYPEZBDD) ||
4312  (biddyManagerType == BIDDYTYPETZBDD)))
4313  {
4314  newname = strdup("0");
4315  return (newname);
4316  }
4317 
4318  newname = strdup(Biddy_Managed_GetTopVariableName(MNG,(Biddy_Edge) p));
4319  for (i=0; i<strlen(newname); ++i) {
4320  if (newname[i] == '<') newname[i] = '_';
4321  if (newname[i] == '>') newname[i] = 0;
4322  }
4323 
4324  return (newname);
4325 }
4326 
4327 static Biddy_String
4328 getshortname(Biddy_Manager MNG, void *p, int n) {
4329  unsigned int i;
4330  Biddy_String name;
4331  Biddy_String shortname;
4332 
4333  name = strdup(Biddy_Managed_GetTopVariableName(MNG,(Biddy_Edge) p));
4334  i = (unsigned int)strcspn(name,"<");
4335  name[i]=0;
4336  shortname = strdup(name);
4337  free(name);
4338 
4339  return (shortname);
4340 }
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:1379
EXTERN void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1515
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:1712
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:348
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:1951
#define Biddy_GetMark(f)
Definition: biddy.h:168
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:249
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:4759
EXTERN void Biddy_Managed_ResetVariablesValue(Biddy_Manager MNG)
Function Biddy_Managed_ResetVariablesValue sets all variable&#39;s value to biddyZero.
Definition: biddyMain.c:2064
EXTERN Biddy_Variable Biddy_Managed_GetLowestVariable(Biddy_Manager MNG)
Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering...
Definition: biddyMain.c:1766
EXTERN unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean select)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:1279
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:1376
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:1581
EXTERN Biddy_Variable Biddy_Managed_AddVariableByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddVariableByName adds variable.
Definition: biddyMain.c:2871
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:1804
void Biddy_Managed_PrintfTable(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfTable writes truth table using printf.
Definition: biddyInOut.c:1157
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:2234
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:1266
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:4480
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:2007
#define Biddy_GetTag(f)
Definition: biddy.h:199
#define Biddy_IsNull(f)
Definition: biddy.h:150
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:2551
Biddy_String Biddy_Managed_Eval0(Biddy_Manager MNG, Biddy_String s)
Function Biddy_Managed_Eval0 evaluates raw format.
Definition: biddyInOut.c:172
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:1901
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:4252
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:1460
#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:1431
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