[14] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [ordIo.c] |
---|
| 4 | |
---|
| 5 | PackageName [ord] |
---|
| 6 | |
---|
| 7 | Synopsis [Routines to read and write variable orderings.] |
---|
| 8 | |
---|
| 9 | Author [Adnan Aziz, Tom Shiple] |
---|
| 10 | |
---|
| 11 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
| 12 | All rights reserved. |
---|
| 13 | |
---|
| 14 | Permission is hereby granted, without written agreement and without license |
---|
| 15 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
| 16 | documentation for any purpose, provided that the above copyright notice and |
---|
| 17 | the following two paragraphs appear in all copies of this software. |
---|
| 18 | |
---|
| 19 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
| 20 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
| 21 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
| 22 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
| 23 | |
---|
| 24 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
| 25 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
| 26 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
| 27 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
| 28 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
| 29 | |
---|
| 30 | ******************************************************************************/ |
---|
| 31 | |
---|
| 32 | #include "ordInt.h" |
---|
| 33 | |
---|
| 34 | static char rcsid[] UNUSED = "$Id: ordIo.c,v 1.15 2004/07/28 20:42:10 jinh Exp $"; |
---|
| 35 | |
---|
| 36 | /*---------------------------------------------------------------------------*/ |
---|
| 37 | /* Constant declarations */ |
---|
| 38 | /*---------------------------------------------------------------------------*/ |
---|
| 39 | /* |
---|
| 40 | * States of the state machine used to parse the input node list file. |
---|
| 41 | */ |
---|
| 42 | #define STATE_TEST 0 /* next char is in first column */ |
---|
| 43 | #define STATE_WAIT 1 /* wait until end of line '\n' is reached */ |
---|
| 44 | #define STATE_IN 2 /* parsing a node name */ |
---|
| 45 | |
---|
| 46 | /* |
---|
| 47 | * Maximum permissible length of a node name in the input node list file. |
---|
| 48 | */ |
---|
| 49 | #define MAX_NAME_LENGTH 32768 |
---|
| 50 | |
---|
| 51 | |
---|
| 52 | /**AutomaticStart*************************************************************/ |
---|
| 53 | |
---|
| 54 | /*---------------------------------------------------------------------------*/ |
---|
| 55 | /* Static function prototypes */ |
---|
| 56 | /*---------------------------------------------------------------------------*/ |
---|
| 57 | |
---|
| 58 | static array_t * NodeBuildBddLevelArrayFromNtkNode(Ntk_Node_t * node); |
---|
| 59 | static array_t * NodeBuildBddIdArrayFromNtkNode(Ntk_Node_t * node); |
---|
| 60 | static int IntegersCompare(const void * obj1, const void * obj2); |
---|
| 61 | static int NodesCompareBddLevelArray(lsGeneric node1, lsGeneric node2); |
---|
| 62 | static array_t * NodeReadBddLevelArray(Ntk_Node_t * node); |
---|
| 63 | static void NodeSetBddLevelArray(Ntk_Node_t * node, array_t * bddLevelArray); |
---|
| 64 | static boolean NameStringProcess(char * nameString, Ntk_Network_t * network, lsList nodeList, int verbose); |
---|
| 65 | |
---|
| 66 | /**AutomaticEnd***************************************************************/ |
---|
| 67 | |
---|
| 68 | |
---|
| 69 | /*---------------------------------------------------------------------------*/ |
---|
| 70 | /* Definition of exported functions */ |
---|
| 71 | /*---------------------------------------------------------------------------*/ |
---|
| 72 | |
---|
| 73 | /**Function******************************************************************** |
---|
| 74 | |
---|
| 75 | Synopsis [Prints to a file the current ordering of MDD variables.] |
---|
| 76 | |
---|
| 77 | Description [Prints to a file all the nodes specified by orderType. |
---|
| 78 | OrderType can be one of Ord_All_c, Ord_InputAndLatch_c or |
---|
| 79 | Ord_NextStateNode_c (see ord.h for the meaning of these types). For each |
---|
| 80 | node, prints the following: name, node type, MDD id, number of values in the |
---|
| 81 | range of the node output, and a list of the levels (in the current ordering) |
---|
| 82 | of the BDD variables that constitute this multi-valued variable. The nodes |
---|
| 83 | are printed to the file in ascending order of the lowest level corresponding |
---|
| 84 | BDD variable. If there exists a node in the class specified by orderType |
---|
| 85 | that doesn't have an mddId, then the routine writes a message to |
---|
| 86 | error_string, and returns 0. In all other cases, it writes to the file and |
---|
| 87 | then returns 1. It is the responsibility of the user to close the file.] |
---|
| 88 | |
---|
| 89 | SideEffects [] |
---|
| 90 | |
---|
| 91 | ******************************************************************************/ |
---|
| 92 | int |
---|
| 93 | Ord_NetworkPrintVariableOrder( |
---|
| 94 | FILE * fp, |
---|
| 95 | Ntk_Network_t * network, |
---|
| 96 | Ord_OrderType orderType /* Ord_All_c, Ord_InputAndLatch_c or Ord_NextStateNode_c */) |
---|
| 97 | { |
---|
| 98 | lsGen gen; |
---|
| 99 | lsList nodeList; |
---|
| 100 | Ntk_Node_t *node; |
---|
| 101 | int maxNameLength; |
---|
| 102 | time_t now; |
---|
| 103 | struct tm *nowStructPtr; |
---|
| 104 | char *nowTxt; |
---|
| 105 | |
---|
| 106 | assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c) |
---|
| 107 | || (orderType == Ord_NextStateNode_c)); |
---|
| 108 | |
---|
| 109 | /* |
---|
| 110 | * First, build up a list of all the nodes covered by orderType. |
---|
| 111 | */ |
---|
| 112 | if (orderType == Ord_All_c) { |
---|
| 113 | nodeList = lsCopy(Ntk_NetworkReadNodes(network), |
---|
| 114 | (lsGeneric (*) (lsGeneric)) NULL); |
---|
| 115 | } |
---|
| 116 | else { |
---|
| 117 | nodeList = lsCreate(); |
---|
| 118 | Ntk_NetworkForEachNode(network, gen, node) { |
---|
| 119 | if (Ntk_NodeTestIsNextStateNode(node) |
---|
| 120 | || ((orderType == Ord_InputAndLatch_c) && Ntk_NodeTestIsCombInput(node))) { |
---|
| 121 | (void) lsNewEnd(nodeList, (lsGeneric) node, LS_NH); |
---|
| 122 | } |
---|
| 123 | } |
---|
| 124 | } |
---|
| 125 | |
---|
| 126 | /* |
---|
| 127 | * As a sanity check, make sure that all the variables in orderType have an |
---|
| 128 | * MDD id. |
---|
| 129 | */ |
---|
| 130 | lsForEachItem(nodeList, gen, node) { |
---|
| 131 | if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) { |
---|
| 132 | error_append("node "); |
---|
| 133 | error_append(Ntk_NodeReadName(node)); |
---|
| 134 | error_append(" not ordered\n"); |
---|
| 135 | |
---|
| 136 | (void) lsFinish(gen); |
---|
| 137 | (void) lsDestroy(nodeList, (void (*) (lsGeneric)) NULL); |
---|
| 138 | return (0); |
---|
| 139 | } |
---|
| 140 | } |
---|
| 141 | |
---|
| 142 | /* |
---|
| 143 | * For each node in nodeList, get the array of levels of the BDD variables |
---|
| 144 | * which make up the MDD variable of node. |
---|
| 145 | */ |
---|
| 146 | lsForEachItem(nodeList, gen, node) { |
---|
| 147 | array_t *bddLevelArray = NodeBuildBddLevelArrayFromNtkNode(node); |
---|
| 148 | |
---|
| 149 | NodeSetBddLevelArray(node, bddLevelArray); |
---|
| 150 | } |
---|
| 151 | |
---|
| 152 | /* |
---|
| 153 | * Sort the nodes of nodeList in ascending order of the lowest level BDD |
---|
| 154 | * variable corresponding to a node's MDD variable. |
---|
| 155 | */ |
---|
| 156 | (void) lsSort(nodeList, NodesCompareBddLevelArray); |
---|
| 157 | |
---|
| 158 | /* |
---|
| 159 | * Compute the maximum length of a node name, for pretty printing. |
---|
| 160 | */ |
---|
| 161 | maxNameLength = 0; |
---|
| 162 | lsForEachItem(nodeList, gen, node) { |
---|
| 163 | int nameLength = strlen(Ntk_NodeReadName(node)); |
---|
| 164 | maxNameLength = (nameLength > maxNameLength) ? nameLength : maxNameLength; |
---|
| 165 | } |
---|
| 166 | |
---|
| 167 | /* |
---|
| 168 | * Write out the header for the output file. |
---|
| 169 | */ |
---|
| 170 | now = time(0); |
---|
| 171 | nowStructPtr = localtime(& now); |
---|
| 172 | nowTxt = asctime(nowStructPtr); |
---|
| 173 | |
---|
| 174 | (void) fprintf(fp, "# %s\n", Vm_VisReadVersion()); |
---|
| 175 | (void) fprintf(fp, "# network name: %s\n", Ntk_NetworkReadName(network)); |
---|
| 176 | (void) fprintf(fp, "# generated: %s", nowTxt); |
---|
| 177 | (void) fprintf(fp, "#\n"); |
---|
| 178 | (void) fprintf(fp, "# %-*s type mddId vals levs\n", |
---|
| 179 | maxNameLength, "name"); |
---|
| 180 | |
---|
| 181 | /* |
---|
| 182 | * Write out the nodes in order. |
---|
| 183 | */ |
---|
| 184 | lsForEachItem(nodeList, gen, node) { |
---|
| 185 | int i; |
---|
| 186 | array_t *bddLevelArray = NodeReadBddLevelArray(node); |
---|
| 187 | char *nodeType = Ntk_NodeObtainTypeAsString(node); |
---|
| 188 | |
---|
| 189 | (void) fprintf(fp, "%-*s %-16s %5d %4d ", |
---|
| 190 | maxNameLength, |
---|
| 191 | Ntk_NodeReadName(node), |
---|
| 192 | nodeType, |
---|
| 193 | Ntk_NodeReadMddId(node), |
---|
| 194 | Var_VariableReadNumValues(Ntk_NodeReadVariable(node))); |
---|
| 195 | FREE(nodeType); |
---|
| 196 | |
---|
| 197 | (void) fprintf(fp, "("); |
---|
| 198 | for (i = 0; i < array_n(bddLevelArray); i++) { |
---|
| 199 | int level = array_fetch(int, bddLevelArray, i); |
---|
| 200 | |
---|
| 201 | if (i == 0) { |
---|
| 202 | (void) fprintf(fp, "%d", level); |
---|
| 203 | } |
---|
| 204 | else { |
---|
| 205 | (void) fprintf(fp, ", %d", level); |
---|
| 206 | } |
---|
| 207 | } |
---|
| 208 | (void) fprintf(fp, ")\n"); |
---|
| 209 | array_free(bddLevelArray); |
---|
| 210 | } |
---|
| 211 | |
---|
| 212 | (void) lsDestroy(nodeList, (void (*) (lsGeneric)) NULL); |
---|
| 213 | return (1); |
---|
| 214 | } |
---|
| 215 | |
---|
| 216 | |
---|
| 217 | /**Function******************************************************************** |
---|
| 218 | |
---|
| 219 | Synopsis [Returns a name array of combinational input variables in order.] |
---|
| 220 | |
---|
| 221 | SideEffects [] |
---|
| 222 | |
---|
| 223 | ******************************************************************************/ |
---|
| 224 | char ** |
---|
| 225 | Ord_NetworkGetCombInputNamesInOrder( |
---|
| 226 | Ntk_Network_t *network) |
---|
| 227 | { |
---|
| 228 | lsGen gen; |
---|
| 229 | lsList nodeList; |
---|
| 230 | Ntk_Node_t *node; |
---|
| 231 | int i; |
---|
| 232 | char **names; |
---|
| 233 | |
---|
| 234 | i = 0; |
---|
| 235 | nodeList = lsCreate(); |
---|
| 236 | Ntk_NetworkForEachNode(network, gen, node) { |
---|
| 237 | if (Ntk_NodeTestIsCombInput(node)) { |
---|
| 238 | (void) lsNewEnd(nodeList, (lsGeneric) node, LS_NH); |
---|
| 239 | i++; |
---|
| 240 | } |
---|
| 241 | } |
---|
| 242 | |
---|
| 243 | names = (char **)ALLOC(char *, i); |
---|
| 244 | if (!names) |
---|
| 245 | return(NULL); |
---|
| 246 | |
---|
| 247 | /* |
---|
| 248 | * For each node in nodeList, get the array of levels of the BDD variables |
---|
| 249 | * which make up the MDD variable of node. |
---|
| 250 | */ |
---|
| 251 | lsForEachItem(nodeList, gen, node) { |
---|
| 252 | array_t *bddLevelArray = NodeBuildBddLevelArrayFromNtkNode(node); |
---|
| 253 | |
---|
| 254 | NodeSetBddLevelArray(node, bddLevelArray); |
---|
| 255 | } |
---|
| 256 | |
---|
| 257 | /* |
---|
| 258 | * Sort the nodes of nodeList in ascending order of the lowest level BDD |
---|
| 259 | * variable corresponding to a node's MDD variable. |
---|
| 260 | */ |
---|
| 261 | (void) lsSort(nodeList, NodesCompareBddLevelArray); |
---|
| 262 | |
---|
| 263 | /* |
---|
| 264 | * Write out the nodes in order. |
---|
| 265 | */ |
---|
| 266 | i = 0; |
---|
| 267 | lsForEachItem(nodeList, gen, node) { |
---|
| 268 | names[i] = (char *)malloc(strlen(Ntk_NodeReadName(node)) + 1); |
---|
| 269 | strcpy(names[i], Ntk_NodeReadName(node)); |
---|
| 270 | i++; |
---|
| 271 | } |
---|
| 272 | |
---|
| 273 | (void) lsDestroy(nodeList, (void (*) (lsGeneric)) NULL); |
---|
| 274 | return(names); |
---|
| 275 | } |
---|
| 276 | |
---|
| 277 | |
---|
| 278 | /**Function******************************************************************** |
---|
| 279 | |
---|
| 280 | Synopsis [Returns a list of nodes corresponding to the names in a file.] |
---|
| 281 | |
---|
| 282 | Description [Parses a file and builds a node list corresponding to the names |
---|
| 283 | found in the first "column" of each line of the file. Any line starting |
---|
| 284 | with the comment character '#' or white space is ignored. If a name is |
---|
| 285 | found for which there doesn't exist a corresponding node in network, then a |
---|
| 286 | message is written to error_string, the partial node list is freed, and the |
---|
| 287 | function returns FALSE; otherwise, it returns TRUE, and a pointer to a list |
---|
| 288 | is returned.] |
---|
| 289 | |
---|
| 290 | Comment [The parser consists of 3 states. See the documentation |
---|
| 291 | accompanying the #defines defining the state names.] |
---|
| 292 | |
---|
| 293 | SideEffects [] |
---|
| 294 | |
---|
| 295 | ******************************************************************************/ |
---|
| 296 | boolean |
---|
| 297 | Ord_FileReadNodeList( |
---|
| 298 | FILE * fp, |
---|
| 299 | Ntk_Network_t * network, |
---|
| 300 | lsList * nodeList /* of Ntk_Node_t , for return */, |
---|
| 301 | int verbose) |
---|
| 302 | { |
---|
| 303 | int c; |
---|
| 304 | int state; |
---|
| 305 | int curPosition = 0; |
---|
| 306 | boolean status; |
---|
| 307 | char nameString[MAX_NAME_LENGTH]; |
---|
| 308 | boolean returnFlag = TRUE; |
---|
| 309 | |
---|
| 310 | *nodeList = lsCreate(); |
---|
| 311 | |
---|
| 312 | state = STATE_TEST; |
---|
| 313 | while ((c = fgetc(fp)) != EOF) { |
---|
| 314 | |
---|
| 315 | switch (state) { |
---|
| 316 | case STATE_TEST: |
---|
| 317 | /* At start of a new line. */ |
---|
| 318 | if (c == '#') { |
---|
| 319 | /* Line starting with comment character; wait for newline */ |
---|
| 320 | state = STATE_WAIT; |
---|
| 321 | } |
---|
| 322 | else if ((c == ' ') || (c == '\t')) { |
---|
| 323 | /* Line starting with white space; wait for newline */ |
---|
| 324 | state = STATE_WAIT; |
---|
| 325 | } |
---|
| 326 | else if (c == '\n') { |
---|
| 327 | /* Line starting newline; go to next line */ |
---|
| 328 | state = STATE_TEST; |
---|
| 329 | } |
---|
| 330 | else { |
---|
| 331 | /* Assume starting a node name. */ |
---|
| 332 | curPosition = 0; |
---|
| 333 | nameString[curPosition++] = c; |
---|
| 334 | state = STATE_IN; |
---|
| 335 | } |
---|
| 336 | break; |
---|
| 337 | case STATE_WAIT: |
---|
| 338 | /* |
---|
| 339 | * Waiting for the newline character. |
---|
| 340 | */ |
---|
| 341 | state = (c == '\n') ? STATE_TEST : STATE_WAIT; |
---|
| 342 | break; |
---|
| 343 | case STATE_IN: |
---|
| 344 | /* |
---|
| 345 | * Parsing a node name. If white space reached, then terminate the |
---|
| 346 | * node name and process it. Else, continue parsing. |
---|
| 347 | */ |
---|
| 348 | if ((c == ' ') || (c == '\n') || (c == '\t')) { |
---|
| 349 | nameString[curPosition] = '\0'; |
---|
| 350 | status = NameStringProcess(nameString, network, *nodeList, verbose); |
---|
| 351 | if (status == FALSE) { |
---|
| 352 | returnFlag = FALSE; |
---|
| 353 | } |
---|
| 354 | state = (c == '\n') ? STATE_TEST : STATE_WAIT; |
---|
| 355 | } |
---|
| 356 | else { |
---|
| 357 | nameString[curPosition++] = c; |
---|
| 358 | if (curPosition >= MAX_NAME_LENGTH) { |
---|
| 359 | error_append("maximum node name length exceeded"); |
---|
| 360 | returnFlag = FALSE; |
---|
| 361 | } |
---|
| 362 | state = STATE_IN; /* redundant, but be explicit */ |
---|
| 363 | } |
---|
| 364 | break; |
---|
| 365 | default: |
---|
| 366 | fail("unrecognized state"); |
---|
| 367 | } |
---|
| 368 | } |
---|
| 369 | |
---|
| 370 | /* |
---|
| 371 | * Handle case where EOF terminates a name. |
---|
| 372 | */ |
---|
| 373 | if (state == STATE_IN) { |
---|
| 374 | nameString[curPosition] = '\0'; |
---|
| 375 | status = NameStringProcess(nameString, network, *nodeList, verbose); |
---|
| 376 | if (status == FALSE) { |
---|
| 377 | returnFlag = FALSE; |
---|
| 378 | } |
---|
| 379 | } |
---|
| 380 | |
---|
| 381 | if (returnFlag) { |
---|
| 382 | return TRUE; |
---|
| 383 | } |
---|
| 384 | else { |
---|
| 385 | (void) lsDestroy(*nodeList, (void (*) (lsGeneric)) NULL); |
---|
| 386 | return FALSE; |
---|
| 387 | } |
---|
| 388 | } |
---|
| 389 | |
---|
| 390 | |
---|
| 391 | /*---------------------------------------------------------------------------*/ |
---|
| 392 | /* Definition of internal functions */ |
---|
| 393 | /*---------------------------------------------------------------------------*/ |
---|
| 394 | |
---|
| 395 | |
---|
| 396 | /**Function******************************************************************** |
---|
| 397 | |
---|
| 398 | Synopsis [Makes new variable order.] |
---|
| 399 | |
---|
| 400 | Description [Makes new variable order. Returns 1 if not successful.] |
---|
| 401 | |
---|
| 402 | SideEffects [] |
---|
| 403 | |
---|
| 404 | ******************************************************************************/ |
---|
| 405 | int |
---|
| 406 | OrdMakeNewVariableOrder(mdd_manager *mddMgr, lsList suppliedNodeList, |
---|
| 407 | int group, int verbose) |
---|
| 408 | { |
---|
| 409 | int i, nVars; |
---|
| 410 | int *invPerm = NIL(int); |
---|
| 411 | int *groupInfo = NIL(int); |
---|
| 412 | int length, bddId, mvLen; |
---|
| 413 | lsGen gen; |
---|
| 414 | Ntk_Node_t *node; |
---|
| 415 | array_t *bddIdArray; |
---|
| 416 | char *name = NIL(char), *prevName = NIL(char), *longName; |
---|
| 417 | int len1, len2, minLen; |
---|
| 418 | |
---|
| 419 | nVars = bdd_num_vars(mddMgr); |
---|
| 420 | invPerm = ALLOC(int, nVars); |
---|
| 421 | |
---|
| 422 | length = 0; |
---|
| 423 | if (group) { |
---|
| 424 | prevName = NIL(char); |
---|
| 425 | groupInfo = ALLOC(int, nVars); |
---|
| 426 | memset(groupInfo, 0, sizeof(int) * nVars); |
---|
| 427 | } |
---|
| 428 | lsForEachItem(suppliedNodeList, gen, node) { |
---|
| 429 | bddIdArray = NodeBuildBddIdArrayFromNtkNode(node); |
---|
| 430 | mvLen = array_n(bddIdArray); |
---|
| 431 | if (group) { |
---|
| 432 | name = Ntk_NodeReadName(node); |
---|
| 433 | if (prevName) { |
---|
| 434 | len1 = strlen(prevName); |
---|
| 435 | len2 = strlen(name); |
---|
| 436 | if (len1 < len2) { |
---|
| 437 | minLen = len1; |
---|
| 438 | longName = name; |
---|
| 439 | } else { |
---|
| 440 | minLen = len2; |
---|
| 441 | longName = prevName; |
---|
| 442 | } |
---|
| 443 | if (strncmp(name, prevName, minLen) == 0) { |
---|
| 444 | if (strcmp(longName + minLen, "$NS") == 0) |
---|
| 445 | groupInfo[length - mvLen] = mvLen * 2; |
---|
| 446 | } |
---|
| 447 | } |
---|
| 448 | } |
---|
| 449 | for (i = 0; i < mvLen; i++) { |
---|
| 450 | bddId = array_fetch(int, bddIdArray, i); |
---|
| 451 | invPerm[length] = bddId; |
---|
| 452 | length++; |
---|
| 453 | } |
---|
| 454 | array_free(bddIdArray); |
---|
| 455 | if (group) |
---|
| 456 | prevName = name; |
---|
| 457 | } |
---|
| 458 | |
---|
| 459 | if (length != nVars) { |
---|
| 460 | fprintf(vis_stderr, |
---|
| 461 | "** ord error: the number of variables does not match\n"); |
---|
| 462 | FREE(invPerm); |
---|
| 463 | if (group) |
---|
| 464 | FREE(groupInfo); |
---|
| 465 | return(1); |
---|
| 466 | } |
---|
| 467 | |
---|
| 468 | bdd_discard_all_var_groups(mddMgr); |
---|
| 469 | bdd_shuffle_heap(mddMgr, invPerm); |
---|
| 470 | |
---|
| 471 | if (group) { |
---|
| 472 | mdd_t *var; |
---|
| 473 | |
---|
| 474 | for (i = 0; i < nVars; i++) { |
---|
| 475 | if (groupInfo[i]) { |
---|
| 476 | var = bdd_var_with_index(mddMgr, invPerm[i]); |
---|
| 477 | bdd_new_var_block(var, groupInfo[i]); |
---|
| 478 | i += groupInfo[i] - 1; |
---|
| 479 | } |
---|
| 480 | } |
---|
| 481 | FREE(groupInfo); |
---|
| 482 | } |
---|
| 483 | |
---|
| 484 | FREE(invPerm); |
---|
| 485 | return(0); |
---|
| 486 | } |
---|
| 487 | |
---|
| 488 | |
---|
| 489 | /*---------------------------------------------------------------------------*/ |
---|
| 490 | /* Definition of static functions */ |
---|
| 491 | /*---------------------------------------------------------------------------*/ |
---|
| 492 | |
---|
| 493 | /**Function******************************************************************** |
---|
| 494 | |
---|
| 495 | Synopsis [Gets the levels of the BDD variables corresponding to the MDD |
---|
| 496 | variable of a node.] |
---|
| 497 | |
---|
| 498 | Description [Returns an array (of int's) of the levels of the BDD variables |
---|
| 499 | corresponding to the MDD variable of a node. The level of a BDD variable is |
---|
| 500 | it place in the current variable ordering of the BDD manager. The returned |
---|
| 501 | array is sorted in ascending order. It is the responsibility of the caller |
---|
| 502 | to free this array.] |
---|
| 503 | |
---|
| 504 | SideEffects [] |
---|
| 505 | |
---|
| 506 | ******************************************************************************/ |
---|
| 507 | static array_t * |
---|
| 508 | NodeBuildBddLevelArrayFromNtkNode( |
---|
| 509 | Ntk_Node_t * node) |
---|
| 510 | { |
---|
| 511 | int i; |
---|
| 512 | Ntk_Network_t *network = Ntk_NodeReadNetwork(node); |
---|
| 513 | mdd_manager *mddManager = Ntk_NetworkReadMddManager(network); |
---|
| 514 | array_t *mvarArray = mdd_ret_mvar_list(mddManager); |
---|
| 515 | int mddId = Ntk_NodeReadMddId(node); |
---|
| 516 | mvar_type mv; |
---|
| 517 | array_t *bddLevelArray; |
---|
| 518 | |
---|
| 519 | mv = array_fetch(mvar_type, mvarArray, mddId); |
---|
| 520 | bddLevelArray = array_alloc(int, mv.encode_length); |
---|
| 521 | |
---|
| 522 | for (i = 0; i < mv.encode_length; i++) { |
---|
| 523 | int bddId = mdd_ret_bvar_id(&mv, i); |
---|
| 524 | bdd_t *varBdd = bdd_get_variable((bdd_manager *) mddManager, bddId); |
---|
| 525 | int varLevel = (int) bdd_top_var_level((bdd_manager *) mddManager, varBdd); |
---|
| 526 | |
---|
| 527 | bdd_free(varBdd); |
---|
| 528 | array_insert_last(int, bddLevelArray, varLevel); |
---|
| 529 | } |
---|
| 530 | array_sort(bddLevelArray, IntegersCompare); |
---|
| 531 | |
---|
| 532 | return (bddLevelArray); |
---|
| 533 | } |
---|
| 534 | |
---|
| 535 | |
---|
| 536 | /**Function******************************************************************** |
---|
| 537 | |
---|
| 538 | Synopsis [Gets the indices of the BDD variables corresponding to the MDD |
---|
| 539 | variable of a node.] |
---|
| 540 | |
---|
| 541 | Description [Returns an array (of int's) of the indices of the BDD variables |
---|
| 542 | corresponding to the MDD variable of a node. It is the responsibility of the |
---|
| 543 | caller to free this array.] |
---|
| 544 | |
---|
| 545 | SideEffects [] |
---|
| 546 | |
---|
| 547 | ******************************************************************************/ |
---|
| 548 | static array_t * |
---|
| 549 | NodeBuildBddIdArrayFromNtkNode( |
---|
| 550 | Ntk_Node_t * node) |
---|
| 551 | { |
---|
| 552 | int i, bddId; |
---|
| 553 | Ntk_Network_t *network = Ntk_NodeReadNetwork(node); |
---|
| 554 | mdd_manager *mddManager = Ntk_NetworkReadMddManager(network); |
---|
| 555 | array_t *mvarArray = mdd_ret_mvar_list(mddManager); |
---|
| 556 | int mddId = Ntk_NodeReadMddId(node); |
---|
| 557 | mvar_type mv; |
---|
| 558 | array_t *bddIdArray; |
---|
| 559 | |
---|
| 560 | mv = array_fetch(mvar_type, mvarArray, mddId); |
---|
| 561 | bddIdArray = array_alloc(int, mv.encode_length); |
---|
| 562 | |
---|
| 563 | for (i = 0; i < mv.encode_length; i++) { |
---|
| 564 | bddId = mdd_ret_bvar_id(&mv, i); |
---|
| 565 | array_insert_last(int, bddIdArray, bddId); |
---|
| 566 | } |
---|
| 567 | |
---|
| 568 | return (bddIdArray); |
---|
| 569 | } |
---|
| 570 | |
---|
| 571 | |
---|
| 572 | /**Function******************************************************************** |
---|
| 573 | |
---|
| 574 | Synopsis [Used to sort an array of integers in ascending order.] |
---|
| 575 | |
---|
| 576 | SideEffects [] |
---|
| 577 | |
---|
| 578 | ******************************************************************************/ |
---|
| 579 | static int |
---|
| 580 | IntegersCompare( |
---|
| 581 | const void * obj1, |
---|
| 582 | const void * obj2) |
---|
| 583 | { |
---|
| 584 | int int1 = *(int *) obj1; |
---|
| 585 | int int2 = *(int *) obj2; |
---|
| 586 | |
---|
| 587 | if (int1 < int2) { |
---|
| 588 | return -1; |
---|
| 589 | } |
---|
| 590 | else if (int1 == int2) { |
---|
| 591 | return 0; |
---|
| 592 | } |
---|
| 593 | else { |
---|
| 594 | return 1; |
---|
| 595 | } |
---|
| 596 | } |
---|
| 597 | |
---|
| 598 | |
---|
| 599 | /**Function******************************************************************** |
---|
| 600 | |
---|
| 601 | Synopsis [Used to sort an array of nodes in ascending order of lowest BDD |
---|
| 602 | level.] |
---|
| 603 | |
---|
| 604 | SideEffects [] |
---|
| 605 | |
---|
| 606 | ******************************************************************************/ |
---|
| 607 | static int |
---|
| 608 | NodesCompareBddLevelArray( |
---|
| 609 | lsGeneric node1, |
---|
| 610 | lsGeneric node2) |
---|
| 611 | { |
---|
| 612 | array_t *bddLevelArray1 = NodeReadBddLevelArray((Ntk_Node_t *) node1); |
---|
| 613 | array_t *bddLevelArray2 = NodeReadBddLevelArray((Ntk_Node_t *) node2); |
---|
| 614 | int firstLevel1 = array_fetch(int, bddLevelArray1, 0); |
---|
| 615 | int firstLevel2 = array_fetch(int, bddLevelArray2, 0); |
---|
| 616 | |
---|
| 617 | if (firstLevel1 < firstLevel2) { |
---|
| 618 | return -1; |
---|
| 619 | } |
---|
| 620 | else if (firstLevel1 == firstLevel2) { |
---|
| 621 | return 0; |
---|
| 622 | } |
---|
| 623 | else { |
---|
| 624 | return 1; |
---|
| 625 | } |
---|
| 626 | } |
---|
| 627 | |
---|
| 628 | |
---|
| 629 | /**Function******************************************************************** |
---|
| 630 | |
---|
| 631 | Synopsis [Gets the BDD level array of a node.] |
---|
| 632 | |
---|
| 633 | SideEffects [] |
---|
| 634 | |
---|
| 635 | SeeAlso [NodeSetBddLevelArray NodesCompareBddLevelArray] |
---|
| 636 | |
---|
| 637 | ******************************************************************************/ |
---|
| 638 | static array_t * |
---|
| 639 | NodeReadBddLevelArray( |
---|
| 640 | Ntk_Node_t * node) |
---|
| 641 | { |
---|
| 642 | return ((array_t *) Ntk_NodeReadUndef(node)); |
---|
| 643 | } |
---|
| 644 | |
---|
| 645 | |
---|
| 646 | /**Function******************************************************************** |
---|
| 647 | |
---|
| 648 | Synopsis [Sets the BDD level array of a node.] |
---|
| 649 | |
---|
| 650 | SideEffects [] |
---|
| 651 | |
---|
| 652 | SeeAlso [NodeReadBddLevelArray] |
---|
| 653 | |
---|
| 654 | ******************************************************************************/ |
---|
| 655 | static void |
---|
| 656 | NodeSetBddLevelArray( |
---|
| 657 | Ntk_Node_t * node, |
---|
| 658 | array_t * bddLevelArray) |
---|
| 659 | { |
---|
| 660 | Ntk_NodeSetUndef(node, (void *) bddLevelArray); |
---|
| 661 | } |
---|
| 662 | |
---|
| 663 | |
---|
| 664 | /**Function******************************************************************** |
---|
| 665 | |
---|
| 666 | Synopsis [Processes the name of a node.] |
---|
| 667 | |
---|
| 668 | Description [Processes the name of a node. If there is no node in network |
---|
| 669 | with name nameString, then the function writes a message in error_string, |
---|
| 670 | and returns FALSE. If the corresponding node is found, then the node is |
---|
| 671 | added to the end of nodeList; else, nothing is done. In either case, TRUE |
---|
| 672 | is returned.] |
---|
| 673 | |
---|
| 674 | SideEffects [] |
---|
| 675 | |
---|
| 676 | ******************************************************************************/ |
---|
| 677 | static boolean |
---|
| 678 | NameStringProcess( |
---|
| 679 | char * nameString, |
---|
| 680 | Ntk_Network_t * network, |
---|
| 681 | lsList nodeList, |
---|
| 682 | int verbose) |
---|
| 683 | { |
---|
| 684 | Ntk_Node_t *node = Ntk_NetworkFindNodeByActualName(network, nameString); |
---|
| 685 | |
---|
| 686 | if (node == NIL(Ntk_Node_t)) { |
---|
| 687 | error_append("Node not found for name: "); |
---|
| 688 | error_append(nameString); |
---|
| 689 | error_append("\n"); |
---|
| 690 | return FALSE; |
---|
| 691 | } |
---|
| 692 | |
---|
| 693 | if (verbose > 1) { |
---|
| 694 | (void) fprintf(vis_stdout, "Reading node: %s\n", Ntk_NodeReadName(node)); |
---|
| 695 | } |
---|
| 696 | |
---|
| 697 | (void) lsNewEnd(nodeList, (lsGeneric) node, LS_NH); |
---|
| 698 | return TRUE; |
---|
| 699 | } |
---|
| 700 | |
---|
| 701 | |
---|
| 702 | |
---|
| 703 | |
---|
| 704 | |
---|
| 705 | |
---|
| 706 | |
---|
| 707 | |
---|
| 708 | |
---|
| 709 | |
---|
| 710 | |
---|
| 711 | |
---|