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 | |
---|