VIS
|
00001 00017 #include "synthInt.h" 00018 00019 static char rcsid[] UNUSED = "$Id: synthUtil.c,v 1.13 1998/08/19 22:51:49 mooni Exp $"; 00020 00021 /*---------------------------------------------------------------------------*/ 00022 /* Constant declarations */ 00023 /*---------------------------------------------------------------------------*/ 00024 00025 00026 /*---------------------------------------------------------------------------*/ 00027 /* Type declarations */ 00028 /*---------------------------------------------------------------------------*/ 00029 00030 00031 /*---------------------------------------------------------------------------*/ 00032 /* Structure declarations */ 00033 /*---------------------------------------------------------------------------*/ 00034 00035 00036 /*---------------------------------------------------------------------------*/ 00037 /* Variable declarations */ 00038 /*---------------------------------------------------------------------------*/ 00039 00042 /*---------------------------------------------------------------------------*/ 00043 /* Static function prototypes */ 00044 /*---------------------------------------------------------------------------*/ 00045 00046 static int GetChildTree(bdd_manager *dd, bdd_node *f, char *eq); 00047 static int GetChildMlTree(bdd_manager *dd, MlTree *tree, char *eq); 00048 static bdd_node * FindNodeWithIndex(bdd_node *node, int index); 00049 static void GetZddCoverWithNameRecur(Ntk_Network_t *net, bdd_manager *dd, bdd_node *node, char *cover); 00050 00054 /*---------------------------------------------------------------------------*/ 00055 /* Definition of exported functions */ 00056 /*---------------------------------------------------------------------------*/ 00057 00058 00059 /*---------------------------------------------------------------------------*/ 00060 /* Definition of internal functions */ 00061 /*---------------------------------------------------------------------------*/ 00062 00075 void 00076 SynthPrintZddTree(bdd_manager *dd, 00077 bdd_node *f) 00078 { 00079 char eq[MAX_EQ_LEN]; 00080 00081 GetChildTree(dd, f, eq); 00082 fprintf(vis_stdout, "%s\n", eq); 00083 } 00084 00085 00100 void 00101 SynthPrintZddTreeMessage(bdd_manager *dd, 00102 bdd_node *f, 00103 char *mess) 00104 { 00105 char eq[MAX_EQ_LEN]; 00106 00107 GetChildTree(dd, f, eq); 00108 fprintf(vis_stdout, "%s%s\n", mess, eq); 00109 } 00110 00111 00126 void 00127 SynthPrintMlTreeMessage(bdd_manager *dd, 00128 MlTree *tree, 00129 char *mess) 00130 { 00131 char eq[MAX_EQ_LEN]; 00132 00133 if (MlTree_IsComplement(tree)) { 00134 tree = MlTree_Regular(tree); 00135 GetChildMlTree(dd, tree, eq); 00136 (void) fprintf(vis_stdout, "%s%s'\n", mess, eq); 00137 } else { 00138 GetChildMlTree(dd, tree, eq); 00139 (void) fprintf(vis_stdout, "%s%s\n", mess, eq); 00140 } 00141 } 00142 00143 00156 void 00157 SynthFreeMlTree(MlTree *tree, 00158 int flag) 00159 { 00160 if (!tree) 00161 return; 00162 00163 if (tree->ref) { 00164 FREE(tree); 00165 return; 00166 } 00167 00168 if (tree->support) 00169 FREE(tree->support); 00170 00171 if (flag && tree->leaf == 0) { 00172 if (tree->q_ref == 0) 00173 SynthFreeMlTree(tree->q, flag); 00174 if (tree->d_ref == 0) 00175 SynthFreeMlTree(tree->d, flag); 00176 if (tree->r_ref == 0) 00177 SynthFreeMlTree(tree->r, flag); 00178 } 00179 00180 FREE(tree); 00181 } 00182 00183 00198 void 00199 SynthPrintMlTreeWithName(Ntk_Network_t *net, 00200 bdd_manager *dd, 00201 MlTree *tree, 00202 char *mess) 00203 { 00204 char eq[MAX_EQ_LEN]; 00205 00206 SynthGetChildMlTreeWithName(net, dd, tree, eq); 00207 fprintf(vis_stdout, "%s%s\n", mess, eq); 00208 } 00209 00210 00222 int 00223 SynthGetChildMlTreeWithName(Ntk_Network_t *net, 00224 bdd_manager *dd, 00225 MlTree *tree, 00226 char *eq) 00227 { 00228 char q_eq[MAX_EQ_LEN]; 00229 char d_eq[MAX_EQ_LEN]; 00230 char r_eq[MAX_EQ_LEN]; 00231 char qd_eq[MAX_EQ_LEN]; 00232 bdd_node *one = bdd_read_one(dd); 00233 bdd_node *zero = bdd_read_zero(dd); 00234 bdd_node *f; 00235 int flag; 00236 00237 f = tree->node; 00238 if (tree->leaf) { 00239 flag = SynthGetChildTreeWithName(net, dd, f, eq); 00240 return(flag); 00241 } 00242 00243 if (f == one) { 00244 sprintf(eq, "one"); 00245 return(0); 00246 } else if (f == zero) { 00247 sprintf(eq, "zero"); 00248 return(0); 00249 } 00250 00251 flag = SynthGetChildMlTreeWithName(net, dd, tree->q, q_eq); 00252 if (tree->q_comp) 00253 SynthMakeComplementString(q_eq); 00254 if (flag) 00255 return(1); 00256 flag = SynthGetChildMlTreeWithName(net, dd, tree->d, d_eq); 00257 if (tree->d_comp) 00258 SynthMakeComplementString(d_eq); 00259 if (flag) 00260 return(1); 00261 flag = SynthGetChildMlTreeWithName(net, dd, tree->r, r_eq); 00262 if (tree->r_comp) 00263 SynthMakeComplementString(r_eq); 00264 if (flag) 00265 return(1); 00266 00267 if (strcmp(q_eq, "one") == 0) 00268 sprintf(qd_eq, "%s", d_eq); 00269 else if (strcmp(q_eq, "zero") == 0) 00270 sprintf(qd_eq, "zero"); 00271 else if (strcmp(d_eq, "one") == 0) 00272 sprintf(qd_eq, "%s", q_eq); 00273 else if (strcmp(d_eq, "zero") == 0) 00274 sprintf(qd_eq, "zero"); 00275 else { 00276 if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) { 00277 sprintf(eq, "%s", q_eq); 00278 if (strlen(eq) == MAX_EQ_LEN - 1) { 00279 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00280 eq[MAX_EQ_LEN - 1] = '\0'; 00281 } else { 00282 eq[strlen(eq)] = '#'; /* truncated */ 00283 eq[strlen(eq) + 1] = '\0'; 00284 } 00285 return(1); 00286 } 00287 sprintf(qd_eq, "%s%s", q_eq, d_eq); 00288 } 00289 00290 if (strcmp(r_eq, "zero") == 0) 00291 sprintf(eq, "%s", qd_eq); 00292 else { 00293 if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) { 00294 sprintf(eq, "%s", qd_eq); 00295 if (strlen(eq) == MAX_EQ_LEN - 1) { 00296 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00297 eq[MAX_EQ_LEN - 1] = '\0'; 00298 } else { 00299 eq[strlen(eq)] = '#'; /* truncated */ 00300 eq[strlen(eq) + 1] = '\0'; 00301 } 00302 return(1); 00303 } 00304 sprintf(eq, "(%s + %s)", qd_eq, r_eq); 00305 } 00306 return(0); 00307 } 00308 00309 00323 int 00324 SynthGetChildTreeWithName(Ntk_Network_t *net, 00325 bdd_manager *dd, 00326 bdd_node *f, 00327 char *eq) 00328 { 00329 char left[MAX_EQ_LEN]; 00330 char right[MAX_EQ_LEN]; 00331 bdd_node *one = bdd_read_one(dd); 00332 bdd_node *zero = bdd_read_zero(dd); 00333 int id, comp; 00334 char name[MAX_NAME_LEN]; 00335 int flag; 00336 00337 if (f == one) { 00338 sprintf(eq, "one"); 00339 return(0); 00340 } else if (f == zero) { 00341 sprintf(eq, "zero"); 00342 return(0); 00343 } 00344 00345 flag = SynthGetChildTreeWithName(net, dd, bdd_bdd_T(f), left); 00346 if (flag) 00347 return(1); 00348 flag = SynthGetChildTreeWithName(net, dd, bdd_bdd_E(f), right); 00349 if (flag) 00350 return(1); 00351 00352 id = bdd_node_read_index(f); 00353 comp = id & 0x1; 00354 id = id >> 1; 00355 00356 sprintf(name, "%s", Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id))); 00357 00358 if (comp) 00359 strcat(name, "'"); 00360 00361 if (strcmp(left, "one") == 0) { 00362 if (strcmp(right, "zero") == 0) 00363 sprintf(eq, "%s", name); 00364 else { 00365 if (strlen(right) + strlen(name) + 6 > MAX_EQ_LEN) { 00366 sprintf(eq, "%s", right); 00367 if (strlen(eq) == MAX_EQ_LEN - 1) { 00368 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00369 eq[MAX_EQ_LEN - 1] = '\0'; 00370 } else { 00371 eq[strlen(eq)] = '#'; /* truncated */ 00372 eq[strlen(eq) + 1] = '\0'; 00373 } 00374 return(1); 00375 } 00376 sprintf(eq, "(%s + %s)", name, right); 00377 } 00378 } else { 00379 if (strcmp(right, "zero") == 0) { 00380 if (strlen(left) + strlen(name) + 1 > MAX_EQ_LEN) { 00381 sprintf(eq, "%s", left); 00382 if (strlen(eq) == MAX_EQ_LEN - 1) { 00383 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00384 eq[MAX_EQ_LEN - 1] = '\0'; 00385 } else { 00386 eq[strlen(eq)] = '#'; /* truncated */ 00387 eq[strlen(eq) + 1] = '\0'; 00388 } 00389 return(1); 00390 } 00391 sprintf(eq, "%s%s", name, left); 00392 } else { 00393 if (strlen(right) + strlen(left) + strlen(name) + 6 > 00394 MAX_EQ_LEN) { 00395 sprintf(eq, "%s", right); 00396 if (strlen(eq) == MAX_EQ_LEN - 1) { 00397 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00398 eq[MAX_EQ_LEN - 1] = '\0'; 00399 } else { 00400 eq[strlen(eq)] = '#'; /* truncated */ 00401 eq[strlen(eq) + 1] = '\0'; 00402 } 00403 return(1); 00404 } 00405 sprintf(eq, "(%s%s + %s)", name, left, right); 00406 } 00407 } 00408 return(0); 00409 } 00410 00411 00424 int 00425 SynthGetPrimaryNodeName(Ntk_Network_t *net, 00426 bdd_node *node, 00427 char *name) 00428 { 00429 int id; 00430 int comp; 00431 char *ntk_name; 00432 00433 id = bdd_node_read_index(node); 00434 comp = id % 2; 00435 id = id >> 1; 00436 00437 ntk_name = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id)); 00438 sprintf(name, "%s", ntk_name); 00439 00440 return(comp); 00441 } 00442 00443 00455 void 00456 SynthGetPrimaryIndexName(Ntk_Network_t *net, 00457 int index, 00458 char *name) 00459 { 00460 int id; 00461 00462 id = index >> 1; 00463 sprintf(name, "%s", Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id))); 00464 } 00465 00466 00479 void 00480 SynthPrintZddCoverWithName(Ntk_Network_t *net, 00481 bdd_manager *dd, 00482 bdd_node *node) 00483 { 00484 char cover[MAX_EQ_LEN]; 00485 00486 fprintf(vis_stdout, "cover ="); 00487 cover[0] = '\0'; 00488 GetZddCoverWithNameRecur(net, dd, node, cover); 00489 fprintf(vis_stdout, "\n"); 00490 } 00491 00492 00504 void 00505 SynthMakeComplementString(char *eq) 00506 { 00507 int len; 00508 00509 if (strcmp(eq, "zero") == 0) { 00510 sprintf(eq, "one"); 00511 return; 00512 } else if (strcmp(eq, "one") == 0) { 00513 sprintf(eq, "zero"); 00514 return; 00515 } 00516 len = strlen(eq); 00517 if (eq[len - 1] == '\'') 00518 eq[len - 1] = '\0'; 00519 else { 00520 if (len == MAX_EQ_LEN - 1) { 00521 eq[len - 2] = '#'; /* truncated */ 00522 eq[len - 1] = '\''; 00523 } else 00524 strcat(eq, "'"); 00525 } 00526 } 00527 00528 00529 /*---------------------------------------------------------------------------*/ 00530 /* Definition of static functions */ 00531 /*---------------------------------------------------------------------------*/ 00532 00545 static int 00546 GetChildTree(bdd_manager *dd, 00547 bdd_node *f, 00548 char *eq) 00549 { 00550 char left[MAX_EQ_LEN]; 00551 char right[MAX_EQ_LEN]; 00552 char tmp[MAX_NAME_LEN]; 00553 bdd_node *one = bdd_read_one(dd); 00554 bdd_node *zero = bdd_read_zero(dd); 00555 int flag; /* truncated */ 00556 00557 if (f == one) { 00558 sprintf(eq, "one"); 00559 return(0); 00560 } else if (f == zero) { 00561 sprintf(eq, "zero"); 00562 return(0); 00563 } 00564 00565 flag = GetChildTree(dd, bdd_bdd_T(f), left); 00566 if (flag) 00567 return(1); 00568 flag = GetChildTree(dd, bdd_bdd_E(f), right); 00569 if (flag) 00570 return(1); 00571 00572 sprintf(tmp, "v%d", bdd_node_read_index(f)); 00573 if (strcmp(left, "one") == 0) { 00574 if (strcmp(right, "zero") == 0) 00575 sprintf(eq, "%s", tmp); 00576 else { 00577 if (strlen(right) + strlen(tmp) + 6 > MAX_EQ_LEN) { 00578 sprintf(eq, "%s", right); 00579 if (strlen(eq) == MAX_EQ_LEN - 1) { 00580 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00581 eq[MAX_EQ_LEN - 1] = '\0'; 00582 } else { 00583 eq[strlen(eq)] = '#'; /* truncated */ 00584 eq[strlen(eq) + 1] = '\0'; 00585 } 00586 return(1); 00587 } 00588 sprintf(eq, "(%s + %s)", tmp, right); 00589 } 00590 } else { 00591 if (strcmp(right, "zero") == 0) { 00592 if (strlen(left) + strlen(tmp) + 1 > MAX_EQ_LEN) { 00593 sprintf(eq, "%s", left); 00594 if (strlen(eq) == MAX_EQ_LEN - 1) { 00595 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00596 eq[MAX_EQ_LEN - 1] = '\0'; 00597 } else { 00598 eq[strlen(eq)] = '#'; /* truncated */ 00599 eq[strlen(eq) + 1] = '\0'; 00600 } 00601 return(1); 00602 } 00603 sprintf(eq, "%s%s", tmp, left); 00604 } else { 00605 if (strlen(right) + strlen(left) + strlen(tmp) + 6 > MAX_EQ_LEN) { 00606 sprintf(eq, "%s", right); 00607 if (strlen(eq) == MAX_EQ_LEN - 1) { 00608 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00609 eq[MAX_EQ_LEN - 1] = '\0'; 00610 } else { 00611 eq[strlen(eq)] = '#'; /* truncated */ 00612 eq[strlen(eq) + 1] = '\0'; 00613 } 00614 return(1); 00615 } 00616 sprintf(eq, "(%s%s + %s)", tmp, left, right); 00617 } 00618 } 00619 return(0); 00620 } 00621 00622 00635 static int 00636 GetChildMlTree(bdd_manager *dd, 00637 MlTree *tree, 00638 char *eq) 00639 { 00640 char q_eq[MAX_EQ_LEN]; 00641 char d_eq[MAX_EQ_LEN]; 00642 char r_eq[MAX_EQ_LEN]; 00643 char qd_eq[MAX_EQ_LEN]; 00644 bdd_node *one = bdd_read_one(dd); 00645 bdd_node *zero = bdd_read_zero(dd); 00646 bdd_node *f; 00647 int flag; 00648 00649 f = tree->node; 00650 if (tree->leaf) { 00651 flag = GetChildTree(dd, f, eq); 00652 return(flag); 00653 } 00654 00655 if (f == one) { 00656 sprintf(eq, "one"); 00657 return(0); 00658 } else if (f == zero) { 00659 sprintf(eq, "zero"); 00660 return(0); 00661 } 00662 00663 flag = GetChildMlTree(dd, tree->q, q_eq); 00664 if (tree->q_comp) 00665 SynthMakeComplementString(q_eq); 00666 if (flag) 00667 return(1); 00668 flag = GetChildMlTree(dd, tree->d, d_eq); 00669 if (tree->d_comp) 00670 SynthMakeComplementString(d_eq); 00671 if (flag) 00672 return(1); 00673 flag = GetChildMlTree(dd, tree->r, r_eq); 00674 if (tree->r_comp) 00675 SynthMakeComplementString(r_eq); 00676 if (flag) 00677 return(1); 00678 00679 if (strcmp(q_eq, "one") == 0) 00680 sprintf(qd_eq, "%s", d_eq); 00681 else if (strcmp(q_eq, "zero") == 0) 00682 sprintf(qd_eq, "zero"); 00683 else if (strcmp(d_eq, "one") == 0) 00684 sprintf(qd_eq, "%s", q_eq); 00685 else if (strcmp(d_eq, "zero") == 0) 00686 sprintf(qd_eq, "zero"); 00687 else { 00688 if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) { 00689 sprintf(eq, "%s", q_eq); 00690 if (strlen(eq) == MAX_EQ_LEN - 1) { 00691 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00692 eq[MAX_EQ_LEN - 1] = '\0'; 00693 } else { 00694 eq[strlen(eq)] = '#'; /* truncated */ 00695 eq[strlen(eq) + 1] = '\0'; 00696 } 00697 return(1); 00698 } 00699 sprintf(qd_eq, "%s%s", q_eq, d_eq); 00700 } 00701 00702 if (strcmp(r_eq, "zero") == 0) 00703 sprintf(eq, "%s", qd_eq); 00704 else { 00705 if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) { 00706 sprintf(eq, "%s", qd_eq); 00707 if (strlen(eq) == MAX_EQ_LEN - 1) { 00708 eq[MAX_EQ_LEN - 2] = '#'; /* truncated */ 00709 eq[MAX_EQ_LEN - 1] = '\0'; 00710 } else { 00711 eq[strlen(eq)] = '#'; /* truncated */ 00712 eq[strlen(eq) + 1] = '\0'; 00713 } 00714 return(1); 00715 } 00716 sprintf(eq, "(%s + %s)", qd_eq, r_eq); 00717 } 00718 return(0); 00719 } 00720 00721 00735 static bdd_node * 00736 FindNodeWithIndex(bdd_node *node, 00737 int index) 00738 { 00739 bdd_node *tmp; 00740 00741 if (bdd_is_constant(node)) 00742 return(NULL); 00743 if (bdd_node_read_index(node) == index) 00744 return(node); 00745 00746 tmp = FindNodeWithIndex(bdd_bdd_T(node), index); 00747 if (tmp) 00748 return(tmp); 00749 return(FindNodeWithIndex(bdd_bdd_E(node), index)); 00750 } 00751 00752 00764 static void 00765 GetZddCoverWithNameRecur(Ntk_Network_t *net, 00766 bdd_manager *dd, 00767 bdd_node *node, 00768 char *cover) 00769 { 00770 bdd_node *one = bdd_read_one(dd); 00771 bdd_node *zero = bdd_read_zero(dd); 00772 int len, index; 00773 char name[MAX_NAME_LEN], *varName; 00774 00775 if (node == zero) 00776 return; 00777 00778 if (node == one) { 00779 fprintf(vis_stdout, " + %s", cover); 00780 return; 00781 } 00782 00783 len = strlen(cover); 00784 index = bdd_node_read_index(node); 00785 varName = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, index / 2)); 00786 if (index % 2 == 0) 00787 sprintf(name, "%s", varName); 00788 else 00789 sprintf(name, "%s'", varName); 00790 strcat(cover, name); 00791 GetZddCoverWithNameRecur(net, dd, bdd_bdd_T(node), cover); 00792 cover[len] = '\0'; 00793 GetZddCoverWithNameRecur(net, dd, bdd_bdd_E(node), cover); 00794 cover[len] = '\0'; 00795 } 00796 00797