source: vis_dev/vis-2.3/src/eqv/eqvMisc.c @ 30

Last change on this file since 30 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 35.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [eqvMisc.c]
4
5  PackageName [eqv]
6
7  Synopsis    [This file provides some miscellaneous functions for the eqv
8               package.]
9
10  Description []
11
12  SeeAlso     []
13
14  Author      [Shaz Qadeer]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35******************************************************************************/
36
37#include "eqvInt.h"
38
39static char rcsid[] UNUSED = "$Id: eqvMisc.c,v 1.10 2009/04/11 01:40:06 fabio Exp $";
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45
46/*---------------------------------------------------------------------------*/
47/* Type declarations                                                         */
48/*---------------------------------------------------------------------------*/
49
50
51/*---------------------------------------------------------------------------*/
52/* Structure declarations                                                    */
53/*---------------------------------------------------------------------------*/
54
55
56/*---------------------------------------------------------------------------*/
57/* Variable declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60
61/*---------------------------------------------------------------------------*/
62/* Macro declarations                                                        */
63/*---------------------------------------------------------------------------*/
64
65
66/**AutomaticStart*************************************************************/
67
68/*---------------------------------------------------------------------------*/
69/* Static function prototypes                                                */
70/*---------------------------------------------------------------------------*/
71
72static boolean NodesMatchUp(Ntk_Node_t *node1, Ntk_Node_t *node2);
73
74/**AutomaticEnd***************************************************************/
75
76
77/*---------------------------------------------------------------------------*/
78/* Definition of exported functions                                          */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Definition of internal functions                                          */
84/*---------------------------------------------------------------------------*/
85/**Function********************************************************************
86
87  Synopsis    [This function returns a hash table of corresponding primary input
88               nodes in network1 and network2.]
89
90  Description [The hash table returned by the function contains corresponding
91               primary input nodes in network1 and network2. The correspondence
92               is based on the names of the nodes. The following conditions
93               constitute an error:
94               1) the number of primary inputs in the two networks is different.
95               2) there is no primary input in network2 by the same name as
96               one occurring in network1.
97               3) the two primary inputs in network1 and network2 having the
98               same names have different variable types. 
99               If an error occurs, NULL is returned.]
100
101  SideEffects []
102
103  SeeAlso     []
104
105******************************************************************************/
106st_table *
107MapPrimaryInputsByName(
108  Ntk_Network_t *network1,
109  Ntk_Network_t *network2)
110{
111  lsGen gen1, gen2;
112  Ntk_Node_t *node1, *node2;
113  Var_Variable_t *var1, *var2;
114  char *name1, *name2;
115  boolean flag = FALSE;
116  boolean equivalent = TRUE;
117  boolean causeOfError = TRUE;
118  st_table *inputMap;
119  int numValues;
120  int i;
121 
122  if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
123           Ntk_NetworkReadNumPrimaryInputs(network2)) {
124    error_append("Different number of primary inputs in the two networks\n");
125    return NIL(st_table);
126  }
127  inputMap = st_init_table(st_ptrcmp, st_ptrhash);
128  Ntk_NetworkForEachPrimaryInput(network1, gen1, node1) {
129    name1 = Ntk_NodeReadName(node1);
130    Ntk_NetworkForEachPrimaryInput(network2, gen2, node2) {
131      name2 = Ntk_NodeReadName(node2);
132      if (strcmp(name1, name2) == 0) {
133        boolean a, b;
134       
135        var1 = Ntk_NodeReadVariable(node1);
136        var2 = Ntk_NodeReadVariable(node2);
137        a = Var_VariableTestIsEnumerative(var1);
138        b = Var_VariableTestIsEnumerative(var2);
139        if((a && !b) || (!a && b)) {
140          error_append("Input ");
141          error_append(name1);
142          error_append(" and ");
143          error_append(name2);
144          error_append(" have different variable types\n");
145          causeOfError = FALSE;
146        }
147        else {
148          numValues = Var_VariableReadNumValues(var1);
149          if(a && b) {
150            if(numValues == Var_VariableReadNumValues(var2)) {
151              st_insert(inputMap, (char *) node1, (char *) node2);
152              flag = TRUE;
153            }   
154            else {
155              error_append("Input ");
156              error_append(name1);
157              error_append(" and ");
158              error_append(name2);
159              error_append(" have different range of values\n");
160              causeOfError = FALSE;
161            }
162          }
163          else {/* both are symbolic */
164            boolean flag2 = TRUE;
165            for(i=0; i<numValues; i++) {
166              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
167                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
168                {
169                  flag2 = FALSE;
170                  error_append("Input ");
171                  error_append(name1);
172                  error_append(" and ");
173                  error_append(name2);
174                  error_append(" have different symbolic values\n");
175                  causeOfError = FALSE;
176                }
177            }
178            if(flag2) {
179              st_insert(inputMap, (char *) node1, (char *) node2);
180              flag = TRUE;
181            }
182          }
183        }
184      }
185    }
186
187    if(!flag) {
188      equivalent = FALSE;    /* name1 did not find a match in network2 */
189      if(causeOfError) {
190        error_append("Input ");
191        error_append(name1);
192        error_append(" does not have a match\n");
193      }
194      else {
195        causeOfError = TRUE;
196      }
197    }
198    else {
199      flag = FALSE;
200    }   
201  }
202 
203 
204  if(!equivalent) {
205    st_free_table(inputMap);
206    return NIL(st_table);
207  }
208  else {
209    return inputMap;
210  }
211}
212
213/**Function********************************************************************
214
215  Synopsis     [The function returns a hash table of corresponding
216  combinational input nodes in network1 and network2.]
217
218  Description  [The hash table returned by the function contains corresponding
219               combinational input nodes in network1 and network2. The
220               correspondence is based on the names of the nodes. The
221               following conditions constitute an error:
222               1) the number of combinational inputs in the two networks is
223               different.
224               2) there is no combinational input in network2 by the same name as
225               one occurring in network1.
226               3) the two combinational inputs in network1 and network2 having
227               same names have different variable types. 
228               If an error occurs, NULL is returned.]
229
230  SideEffects  []
231
232  SeeAlso      []
233
234******************************************************************************/
235st_table *
236MapCombInputsByName(
237  Ntk_Network_t *network1,
238  Ntk_Network_t *network2)
239{
240  lsGen gen1, gen2;
241  Ntk_Node_t *node1, *node2;
242  Var_Variable_t *var1, *var2;
243  char *name1, *name2;
244  boolean flag = FALSE;
245  boolean equivalent = TRUE;
246  boolean causeOfError = TRUE;
247  st_table *inputMap;
248  int numValues;
249  int i;
250 
251  if(Ntk_NetworkReadNumCombInputs(network1) !=
252           Ntk_NetworkReadNumCombInputs(network2)) {
253    error_append("Different number of combinational inputs in the two networks\n");
254    return NIL(st_table);
255  }
256  inputMap = st_init_table(st_ptrcmp, st_ptrhash);
257  Ntk_NetworkForEachCombInput(network1, gen1, node1) {
258    name1 = Ntk_NodeReadName(node1);
259    Ntk_NetworkForEachCombInput(network2, gen2, node2) {
260      name2 = Ntk_NodeReadName(node2);
261      if (strcmp(name1, name2) == 0) {
262        boolean a, b;
263       
264        var1 = Ntk_NodeReadVariable(node1);
265        var2 = Ntk_NodeReadVariable(node2);
266        a = Var_VariableTestIsEnumerative(var1);
267        b = Var_VariableTestIsEnumerative(var2);
268        if((a && !b) || (!a && b)) {
269          error_append("Input ");
270          error_append(name1);
271          error_append(" and ");
272          error_append(name2);
273          error_append(" have different variable types\n");
274          causeOfError = FALSE;
275        }
276        else {
277          numValues = Var_VariableReadNumValues(var1);
278          if(a && b) {
279            if(numValues == Var_VariableReadNumValues(var2)) {
280              st_insert(inputMap, (char *) node1, (char *) node2);
281              flag = TRUE;
282            }   
283            else {
284              error_append("Input ");
285              error_append(name1);
286              error_append(" and ");
287              error_append(name2);
288              error_append(" have different range of values\n");
289              causeOfError = FALSE;
290            }
291          }
292          else {/* both are symbolic */
293            boolean flag2 = TRUE;
294            for(i=0; i<numValues; i++) {
295              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
296                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
297                {
298                  flag2 = FALSE;
299                  error_append("Input ");
300                  error_append(name1);
301                  error_append(" and ");
302                  error_append(name2);
303                  error_append(" have different symbolic values\n");
304                  causeOfError = FALSE;
305                }
306            }
307            if(flag2) {
308              st_insert(inputMap, (char *) node1, (char *) node2);
309              flag = TRUE;
310            }
311          }
312        }
313      }
314    }
315
316    if(!flag) {
317      equivalent = FALSE;    /* name1 did not find a match in network2 */
318      if(causeOfError) {
319        error_append("Input ");
320        error_append(name1);
321        error_append(" does not have a match\n");
322      }
323      else {
324        causeOfError = TRUE;
325      }
326    }
327    else {
328      flag = FALSE;
329    }   
330  }
331 
332 
333  if(!equivalent) {
334    st_free_table(inputMap);
335    return NIL(st_table);
336  }
337  else {
338    return inputMap;
339  }
340}
341 
342/**Function********************************************************************
343
344  Synopsis    [This function returns a hash table of corresponding primary
345  output nodes in network1 and network2.]
346
347  Description [The hash table returned by the function contains corresponding
348               primary output nodes in network1 and network2. The correspondence
349               is based on the names of the nodes. The following conditions
350               constitute an error:
351               1) the number of primary outputs in the two networks is different.
352               2) there is no primary output in network2 by the same name as
353               one occurring in network1.
354               3) the two primary outputs in network1 and network2 having the
355               same names have different variable types. 
356               If an error occurs, NULL is returned.]
357               
358  SideEffects []
359
360  SeeAlso     []
361
362******************************************************************************/
363st_table *
364MapPrimaryOutputsByName(
365  Ntk_Network_t *network1,
366  Ntk_Network_t *network2)
367{
368  lsGen gen1, gen2;
369  Ntk_Node_t *node1, *node2;
370  Var_Variable_t *var1, *var2;
371  char *name1, *name2;
372  boolean flag = FALSE;
373  boolean equivalent = TRUE;
374  boolean causeOfError = TRUE;
375  st_table *outputMap;
376  int numValues;
377  int i;
378 
379  if(Ntk_NetworkReadNumPrimaryOutputs(network1) !=
380           Ntk_NetworkReadNumPrimaryOutputs(network2)) {
381    error_append("Different number of primary outputs in the two networks\n");
382    return NIL(st_table);
383  }
384  outputMap = st_init_table(st_ptrcmp, st_ptrhash);
385  Ntk_NetworkForEachPrimaryOutput(network1, gen1, node1) {
386    name1 = Ntk_NodeReadName(node1);
387    Ntk_NetworkForEachPrimaryOutput(network2, gen2, node2) {
388      name2 = Ntk_NodeReadName(node2);
389      if (strcmp(name1, name2) == 0) {
390        boolean a, b;
391       
392        var1 = Ntk_NodeReadVariable(node1);
393        var2 = Ntk_NodeReadVariable(node2);
394        a = Var_VariableTestIsEnumerative(var1);
395        b = Var_VariableTestIsEnumerative(var2);
396        if((a && !b) || (!a && b)) {
397          error_append("Output ");
398          error_append(name1);
399          error_append(" and ");
400          error_append(name2);
401          error_append(" have different variable types\n");
402          causeOfError = FALSE;
403        }
404        else {
405          numValues = Var_VariableReadNumValues(var1);
406          if(a && b) {
407            if(numValues == Var_VariableReadNumValues(var2)) {
408              st_insert(outputMap, (char *) node1, (char *) node2);
409              flag = TRUE;
410            }   
411            else {
412              error_append("Output ");
413              error_append(name1);
414              error_append(" and ");
415              error_append(name2);
416              error_append(" have different range of values\n");
417              causeOfError = FALSE;
418            }
419          }
420          else {/* both are symbolic */
421            boolean flag2 = TRUE;
422            for(i=0; i<numValues; i++) {
423              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
424                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
425                {
426                  flag2 = FALSE;
427                  error_append("Output ");
428                  error_append(name1);
429                  error_append(" and ");
430                  error_append(name2);
431                  error_append(" have different symbolic values\n");
432                  causeOfError = FALSE;
433                }
434            }
435            if(flag2) {
436              st_insert(outputMap, (char *) node1, (char *) node2);
437              flag = TRUE;
438            }
439          }
440        }
441       
442      }
443    }
444
445    if(!flag) {
446      equivalent = FALSE;    /* name1 did not find a match in network2 */
447      if(causeOfError) {
448        error_append("Output ");
449        error_append(name1);
450        error_append(" does not have a match\n");
451      }
452      else {
453        causeOfError = TRUE;
454      }
455    }
456    else {
457      flag = FALSE;
458    }   
459  }
460 
461 
462  if(!equivalent) {
463    st_free_table(outputMap);
464    return NIL(st_table);
465  }
466  else {
467    return outputMap;
468  }
469}
470
471/**Function********************************************************************
472
473  Synopsis    [This function returns a hash table of corresponding
474  combinational output nodes in network1 and network2.]
475
476  Description [The hash table returned by the function contains corresponding
477               combinational output nodes in network1 and network2. The
478               correspondence is based on the names of the nodes. The
479               following conditions constitute an error:
480               1) the number of combinational outputs in the two networks is
481               different.
482               2) there is no combinational output in network2 by the same
483               name as one occurring in network1.
484               3) the two combinational outputs in network1 and network2 having
485               same names have different variable types. 
486               If an error occurs, NULL is returned.]
487
488  SideEffects []
489
490  SeeAlso     []
491
492******************************************************************************/
493st_table *
494MapCombOutputsByName(
495  Ntk_Network_t *network1,
496  Ntk_Network_t *network2)
497{
498  lsGen gen1, gen2;
499  Ntk_Node_t *node1, *node2;
500  Var_Variable_t *var1, *var2;
501  char *name1, *name2;
502  boolean flag = FALSE;
503  boolean equivalent = TRUE;
504  boolean causeOfError = TRUE;
505  st_table *outputMap;
506  int numValues;
507  int i;
508 
509  if(Ntk_NetworkReadNumCombOutputs(network1) !=
510     Ntk_NetworkReadNumCombOutputs(network2)) {
511    error_append("Different number of combinational outputs in the two networks\n");
512    return NIL(st_table);
513  }
514  outputMap = st_init_table(st_ptrcmp, st_ptrhash);
515  Ntk_NetworkForEachCombOutput(network1, gen1, node1) {
516    name1 = Ntk_NodeReadName(node1);
517    Ntk_NetworkForEachCombOutput(network2, gen2, node2) {
518      name2 = Ntk_NodeReadName(node2);
519      if (NodesMatchUp(node1, node2)) {
520        boolean a, b;
521
522        var1 = Ntk_NodeReadVariable(node1);
523        var2 = Ntk_NodeReadVariable(node2);
524        a = Var_VariableTestIsEnumerative(var1);
525        b = Var_VariableTestIsEnumerative(var2);
526        if((a && !b) || (!a && b)) {
527          error_append("Output ");
528          error_append(name1);
529          error_append(" and ");
530          error_append(name2);
531          error_append(" have different variable types\n");
532          causeOfError = FALSE;
533        }
534        else {
535          numValues = Var_VariableReadNumValues(var1);
536          if(a && b) {
537            if(numValues == Var_VariableReadNumValues(var2)) {
538              st_insert(outputMap, (char *) node1, (char *) node2);
539              flag = TRUE;
540            }
541            else {
542              error_append("Output ");
543              error_append(name1);
544              error_append(" and ");
545              error_append(name2);
546              error_append(" have different range of values\n");
547              causeOfError = FALSE;
548            }
549          }
550          else {/* both are symbolic */
551            boolean flag2 = TRUE;
552            for(i=0; i<numValues; i++) {
553              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
554                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
555                {
556                  flag2 = FALSE;
557                  error_append("Output ");
558                  error_append(name1);
559                  error_append(" and ");
560                  error_append(name2);
561                  error_append(" have different symbolic values\n");
562                  causeOfError = FALSE;
563                }
564            }
565            if(flag2) {
566              st_insert(outputMap, (char *) node1, (char *) node2);
567              flag = TRUE;
568              break;
569            }
570          }
571        }
572      }
573    }
574
575    if(!flag) {
576      equivalent = FALSE;    /* name1 did not find a match in network2 */
577      if(causeOfError) {
578        error_append("Output ");
579        error_append(name1);
580        error_append(" does not have a match\n");
581      }
582      else {
583        causeOfError = TRUE;
584      }
585    }
586    else {
587      flag = FALSE;
588    }   
589  }
590 
591 
592  if(!equivalent) {
593    st_free_table(outputMap);
594    return NIL(st_table);
595  }
596  else {
597    return outputMap;
598  }
599}
600
601/**Function********************************************************************
602
603  Synopsis    [This function returns the ordering method to be used.]
604
605  SideEffects []
606 
607  SeeAlso     []
608
609******************************************************************************/
610OFT
611FindOrderingMethod(void)
612{
613  return (OFT) NULL;
614}
615
616/**Function********************************************************************
617
618  Synopsis    [The function checks whether inputMap and outputMap form valid
619               roots and leaves for network1 and network2.]
620
621  Description [inputMap is a hash table of the corresponding leaves in
622  network1 and network2. outputMap is a hash table of the corresponding roots
623  in network1 and network2. The function checks whether the leaves of each
624  network form a complete support of its roots. If this turns out to be false
625  for any network, FALSE is returned otherwise TRUE is returned.]
626
627  SideEffects []
628
629  SeeAlso     []
630
631******************************************************************************/
632boolean
633TestRootsAndLeavesAreValid(
634  Ntk_Network_t *network1,
635  Ntk_Network_t *network2,
636  st_table *inputMap,
637  st_table *outputMap)
638{
639 
640  st_generator *gen;
641  array_t *roots1, *roots2;
642  st_table *leaves1, *leaves2;
643  Ntk_Node_t *node1, *node2;
644  boolean test = TRUE;
645 
646  roots1 = array_alloc(Ntk_Node_t *, 0);
647  roots2 = array_alloc(Ntk_Node_t *, 0);
648  st_foreach_item(outputMap, gen, &node1, &node2) {
649    array_insert_last(Ntk_Node_t *, roots1, node1);
650    array_insert_last(Ntk_Node_t *, roots2, node2);
651  }
652  leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
653  leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
654  st_foreach_item(inputMap, gen, &node1, &node2) {
655    st_insert(leaves1, node1, NULL);
656    st_insert(leaves2, node2, NULL);
657  }
658  if(!Ntk_NetworkTestLeavesCoverSupportOfRoots(network1, roots1,
659                                             leaves1)) {
660    error_append("Leaves do not form a complete support for roots in network1.\n");
661    test = FALSE;
662  }
663  if(!Ntk_NetworkTestLeavesCoverSupportOfRoots(network2, roots2,
664                                             leaves2)) {
665    error_append("Leaves do not form a complete support for roots in network2.\n");
666    test = FALSE;
667  }
668  array_free(roots1);
669  array_free(roots2);
670  st_free_table(leaves1);
671  st_free_table(leaves2);
672  return test;
673}
674
675/**Function********************************************************************
676
677  Synopsis    [This function takes a hash table of names and generates a
678               hash table of nodes.]
679
680  Description [The input to the function is a hash table of names of nodes.
681               It returns a hash table of nodes corresponding to the names.
682               In the hash table names, key is a name in network1 and value
683               is a name in network2. Similarly, in the table which is
684               returned, key is a node in network1 and value a node in
685               network2. If no node by a certain name is found in a network,
686               NULL is returned.]
687
688  SideEffects []
689
690  SeeAlso     []
691
692******************************************************************************/
693st_table *
694MapNamesToNodes(
695  Ntk_Network_t *network1,
696  Ntk_Network_t *network2,
697  st_table *names)
698{
699  st_table *nodes = st_init_table(st_ptrcmp, st_ptrhash);
700  char *name1, *name2;
701  Ntk_Node_t *node1, *node2;
702  boolean error = FALSE;
703  st_generator *gen;
704 
705 
706  st_foreach_item(names, gen, &name1, &name2) {
707    if((node1 = Ntk_NetworkFindNodeByName(network1, name1)) ==
708       NIL(Ntk_Node_t)) {
709      error = TRUE;
710      error_append(name1);
711      error_append(" not present in network1.\n");
712    }
713   
714    if((node2 = Ntk_NetworkFindNodeByName(network2, name2)) ==
715       NIL(Ntk_Node_t)) {
716      error = TRUE;
717      error_append(name2);
718      error_append(" not present in network2.\n");
719    }
720    st_insert(nodes, (char *) node1, (char *) node2);
721  }
722  if(error) {
723    st_free_table(nodes);
724    return NIL(st_table);
725  }
726  else {
727    return nodes;
728  }
729}
730
731   
732/**Function********************************************************************
733
734  Synopsis    [This function reads an input file containing names of roots and
735  leaves, and stores the corresponding names in the two hash tables-
736  rootsTable and leavesTable.]
737 
738  Description [The function returns 0 if there are no roots or leaves in the
739               file. It is an error not to have either roots or leaves in the
740               file. It returns 1 if there are roots but no leaves, 2 if there
741               are leaves but no roots, and 3 if there are both roots and
742               leaves.]
743
744  SideEffects []
745
746  SeeAlso     []
747
748******************************************************************************/
749int
750ReadRootLeafMap(
751  FILE *inputFile,
752  st_table *rootsTable,
753  st_table *leavesTable)
754{
755  char *name;
756  char *rootName1, *rootName2;
757  char *leafName1, *leafName2;
758  char c;
759  boolean rootsFlag= 0;
760  boolean leavesFlag = 0;
761  st_generator *gen;
762 
763  while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
764  ungetc(c, inputFile);
765  name = ALLOC(char, 20);
766 
767  if(fscanf(inputFile, "%s", name) == EOF) {
768    FREE(name);
769    return 0;
770    /* both roots and leaves absent */
771  }
772  if(!strcmp(name, ".roots")) {
773    rootsFlag = 1;
774    while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
775    ungetc(c, inputFile);
776    while((fscanf(inputFile, "%s", name) != EOF) && strcmp(name, ".leaves")) {
777      rootName1 = ALLOC(char, strlen(name) + 1);
778      strcpy(rootName1, name);
779      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
780      ungetc(c, inputFile);
781      if((fscanf(inputFile, "%s", name) == EOF) || (!strcmp(name, ".leaves"))) {
782        FREE(name);
783        FREE(rootName1);
784        st_foreach_item(rootsTable, gen, &rootName1, &rootName2) {
785          FREE(rootName1);
786          FREE(rootName2);
787          return 0;
788        }
789      }
790      rootName2 = ALLOC(char, strlen(name) + 1);
791      strcpy(rootName2, name);
792      st_insert(rootsTable, rootName1, rootName2);
793      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
794      ungetc(c, inputFile);
795      name[0] = '\0'; /* this is to insure that whenever the while loop
796                         is terminated, only one of the conditions is false */
797    }
798  }
799  if(!strcmp(name, ".leaves")) {
800    leavesFlag = 1;
801    while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
802    ungetc(c, inputFile);
803    while(fscanf(inputFile, "%s", name) != EOF) {
804      leafName1 = ALLOC(char, strlen(name) + 1);
805      strcpy(leafName1, name);
806      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
807      ungetc(c, inputFile);
808      if(fscanf(inputFile, "%s", name) == EOF) {
809        FREE(name);
810        FREE(leafName1);
811        st_foreach_item(leavesTable, gen, &leafName1, &leafName2) {
812          FREE(leafName1);
813          FREE(leafName2);
814          return 0;
815        }
816      }
817      leafName2 = ALLOC(char, strlen(name) + 1);
818      strcpy(leafName2, name);
819      st_insert(leavesTable, leafName1, leafName2);
820      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
821      ungetc(c, inputFile);
822    }
823  }
824  FREE(name);
825  if(rootsFlag == 1) {
826    if(leavesFlag == 1) {
827      return 3; /* both leaves and roots present */
828    }
829    else {
830      return 2; /* roots present but leaves absent */
831    }
832  }
833  else {
834    if(leavesFlag == 1) {
835      return 1; /* roots absent but leaves present */
836    }
837    else {
838      return 0;
839    }
840  }
841}
842 
843/**Function********************************************************************
844
845  Synopsis    [This function generates the default ordering of leaf nodes.]
846
847  Description [The function checks if network1 has a partition registered with
848  it. If there is no partition, The function orders the variables of network1,
849  using the option Ord_All_c i.e. orders all the nodes. If a partition exists,
850  the existing ordering is left undisturbed. It then copies the mddIds
851  of those nodes of network1 which are present in inputMap into
852  the corresponding nodes of network2.]
853
854  SideEffects []
855
856  SeeAlso     []
857
858******************************************************************************/
859void
860DefaultCommonOrder(
861  Ntk_Network_t *network1, 
862  Ntk_Network_t *network2,
863  st_table *inputMap)
864{
865  st_generator *gen;
866  Ntk_Node_t *node1, *node2;
867  int id;
868  lsList dummy = (lsList) 0;
869 
870  if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) == NIL(void)) {
871    Ord_NetworkOrderVariables(network1, Ord_RootsByDefault_c,
872                              Ord_NodesByDefault_c, FALSE, Ord_All_c,
873                              Ord_Unassigned_c, dummy, 0);
874  }
875 
876  st_foreach_item(inputMap, gen, &node1, &node2) {
877    id = Ntk_NodeReadMddId(node1);
878    Ntk_NodeSetMddId(node2, id);
879  }
880}
881 
882     
883
884/**Function********************************************************************
885
886  Synopsis    [This function checks whether the leaves present in leavesTable
887  constitute the full set of primary inputs of network1 and network2.]
888
889  Description [leavesTable contains names of corresponding leaves in network1
890  and network2. The function returns TRUE if the leaves present in leavesTable
891  constitute the full set of primary inputs of network1 and network2. The
892  following  conditions result in a return value of FALSE:
893  a) there is no node by a name present in leavesTable.
894  b) the node with a particular name is not a primary input
895  c) the number of leaves is different from the number of primary inputs in
896  either network.]
897
898  SideEffects []
899
900  SeeAlso     []
901
902******************************************************************************/
903boolean
904TestLeavesAreValid(
905  Ntk_Network_t *network1,
906  Ntk_Network_t *network2,
907  st_table *leavesTable)
908
909{
910  st_generator *gen;
911  Ntk_Node_t *node1, *node2;
912  char *name1, *name2;
913  boolean valid = TRUE;
914  int count = 0;
915 
916  st_foreach_item(leavesTable, gen, &name1, &name2) {
917    node1 = Ntk_NetworkFindNodeByName(network1, name1);
918    node2 = Ntk_NetworkFindNodeByName(network2, name2);
919    if(node1 == NIL(Ntk_Node_t)) {
920      error_append(name1);
921      error_append(" not found in network1.\n");
922      valid = FALSE;
923    }
924    else {
925      if(!Ntk_NodeTestIsPrimaryInput(node1)) {
926        error_append(name1);
927        error_append(" is not a primary input node\n");
928        valid = FALSE;
929      }
930    }
931   
932    if(node2 == NIL(Ntk_Node_t)) {
933      error_append(name2);
934      error_append(" not found in network2.\n");
935      valid = FALSE;
936    }
937    else {
938      if(!Ntk_NodeTestIsPrimaryInput(node2)) {
939        error_append(name2);
940        error_append(" is not a primary input node\n");
941        valid = FALSE;
942      }
943    }
944   
945    count ++;
946  }
947  if(valid) {
948    if(!((Ntk_NetworkReadNumPrimaryInputs(network1) == count) && (Ntk_NetworkReadNumPrimaryInputs(network2) == count))) {
949      error_append("All primary inputs not specified in the input file\n");
950      valid = FALSE;
951    }
952  }
953  return valid;
954}
955
956/**Function********************************************************************
957
958  Synopsis       [The function checks whether the names present in rootsTable
959  have nodes corresponding to them present in network1 and network2.]
960
961  Description    [rootsTable contains names of corresponding roots in network1
962  and network2. The function returns TRUE if the roots present in rootsTable
963  have nodes corresponding to them in the network1 and network2. Otherwise,
964  FALSE is returned.]
965
966  SideEffects    []
967
968  SeeAlso        []
969
970******************************************************************************/
971boolean
972TestRootsAreValid(
973  Ntk_Network_t *network1,
974  Ntk_Network_t *network2,
975  st_table *rootsTable)
976
977{
978  st_generator *gen;
979  char *name1, *name2;
980  boolean valid = TRUE;
981 
982  st_foreach_item(rootsTable, gen, &name1, &name2) {
983    if(Ntk_NetworkFindNodeByName(network1, name1) == NIL(Ntk_Node_t)) {
984      valid = FALSE;
985      error_append(name1);
986      error_append(" not present in network1.\n");
987    }
988   
989    if(Ntk_NetworkFindNodeByName(network2, name2) == NIL(Ntk_Node_t)) {
990      valid = FALSE;
991      error_append(name2);
992      error_append(" not present in network2.\n");
993    }
994  }
995  return valid;
996}
997
998/**Function********************************************************************
999
1000  Synopsis           [The function checks whether the partition registered
1001  with network has vertices corresponding to nodes stored as keys in roots and
1002  leaves.]
1003
1004  Description        [The function returns TRUE if all the nodes stored as
1005                      keys in roots and leaves have corresponding vertices in
1006                      the partition of network. It returns FALSE otherwise. It
1007                      is assumed that network has a partition associated with
1008                      it.]
1009
1010  SideEffects        []
1011
1012  SeeAlso            []
1013
1014******************************************************************************/
1015boolean
1016TestPartitionIsValid(
1017  Ntk_Network_t *network,
1018  st_table *roots,
1019  st_table *leaves)
1020{
1021  graph_t *partition = Part_NetworkReadPartition(network);
1022  st_generator *gen;
1023  char *name;
1024  Ntk_Node_t *node1, *node2;
1025  boolean flag = TRUE;
1026 
1027  st_foreach_item(roots, gen, &node1, &node2) {
1028    name = Ntk_NodeReadName(node1);
1029    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
1030      flag = FALSE;
1031    }
1032  }
1033  st_foreach_item(leaves, gen, &node1, &node2) {
1034    name = Ntk_NodeReadName(node1);
1035    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
1036      flag = FALSE;
1037    }
1038  }
1039  return flag;
1040}
1041
1042/*---------------------------------------------------------------------------*/
1043/* Definition of static functions                                            */
1044/*---------------------------------------------------------------------------*/
1045
1046/**Function********************************************************************
1047
1048  Synopsis    [Check whether two nodes may be matched by name.]
1049
1050  Description [Check whether two nodes from different networks may be
1051  matched by name in equivalence verification.  If the two nodes have
1052  the same names, then they match.  Moreover, if the two nodes are
1053  latch inputs and the corresponding latches match by name, they also
1054  match.  This last clause makes comb_verify a lot more useful because
1055  small changes in Verilog source or in its translation to blif-mv
1056  usually leave the latch names unchanged, but alter the names of
1057  the next state variables.]
1058
1059  SideEffects [none]
1060
1061  SeeAlso     [MapCombOutputsByName]
1062
1063******************************************************************************/
1064static boolean
1065NodesMatchUp(
1066  Ntk_Node_t *node1 /* node from network1 */,
1067  Ntk_Node_t *node2 /* node from network2 */
1068  )
1069{
1070  char *name1, *name2;
1071
1072  name1 = Ntk_NodeReadName(node1);
1073  name2 = Ntk_NodeReadName(node2);
1074
1075  if (strcmp(name1, name2) == 0)
1076    return TRUE;
1077
1078  /* Try to match through the state variables. */
1079  if ((Ntk_NodeTestIsLatchDataInput(node1) &&
1080      Ntk_NodeTestIsLatchDataInput(node2)) ||
1081      (Ntk_NodeTestIsLatchInitialInput(node1) &&
1082       Ntk_NodeTestIsLatchInitialInput(node2))) {
1083    Ntk_Node_t *latch1, *latch2;
1084    char *nameLatch1, *nameLatch2;
1085    array_t *fanout1, *fanout2;
1086
1087    fanout1 = Ntk_NodeReadFanouts(node1);
1088    if (array_n(fanout1) != 1) return FALSE;
1089    fanout2 = Ntk_NodeReadFanouts(node2);
1090    if (array_n(fanout2) != 1) return FALSE;
1091
1092    latch1 = array_fetch(Ntk_Node_t *, fanout1, 0);
1093    assert(Ntk_NodeTestIsLatch(latch1));
1094    latch2 = array_fetch(Ntk_Node_t *, fanout2, 0);
1095    assert(Ntk_NodeTestIsLatch(latch2));
1096
1097    nameLatch1 = Ntk_NodeReadName(latch1);
1098    nameLatch2 = Ntk_NodeReadName(latch2);
1099
1100    return (strcmp(nameLatch1, nameLatch2) == 0);
1101  }
1102
1103  return FALSE;
1104
1105} /* NodesMatchUp */
Note: See TracBrowser for help on using the repository browser.