source: vis_dev/vis-2.3/src/res/res.c @ 93

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

vis2.3
File size: 79.3 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [res.c]
4
5  PackageName [res]
6
7  Synopsis    [ The main file that incorporates procedures for residue
8                verification.]
9
10  Author      [ Kavita Ravi    <ravi@boulder.colorado.edu>,
11                Abelardo Pardo <abel@boulder.colorado.edu>]
12
13  Copyright [This file was created at the University of Colorado at Boulder.
14  The University of Colorado at Boulder makes no warranty about the suitability
15  of this software for any purpose.  It is presented on an AS IS basis.]
16
17******************************************************************************/
18
19#include "resInt.h"
20
21static char rcsid[] UNUSED = "$Id: res.c,v 1.55 2009/04/11 21:31:29 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26#define RES_VERIFY_NOTHING 0
27#define RES_VERIFY_DONE 1
28#define RES_VERIFY_IGNORE_PREV_RESULTS 2
29#define LOG2_FIRST_PRIME 8
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Type declarations                                                         */
37/*---------------------------------------------------------------------------*/
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43
44static int PrimePool [] = { 5,   7,  9, 11, 13, 17,  19,  23,  29,
45                            31,  37,  41,  43,  47,  53,  59,  61,  67,  71,
46                            73,  79,  83,  89,  97, 101, 103, 107, 109, 113,
47                            127, 131, 137, 139, 149, 151, 157, 163, 167, 173,
48                            179, 181, 191, 193, 197, 199, 211, 223, 227, 229,
49                            233, 239, 241, 251, 257, 263, 269, 271, 277, 281,
50                            283, 293, 307, 311, 313, 317, 331, 337, 347, 349,
51                            353, 359, 367, 373, 379, 383, 389, 397, 401, 409,
52                            419, 421, 431, 433, 439, 443, 449, 457, 461, 463,
53                            467, 479, 487, 491, 499, 503, 509, 521, 523, 541,
54                            547};
55static int PrimePoolSize = 100;    /* Number of elements of the array above */
56
57/*---------------------------------------------------------------------------*/
58/* Macro declarations                                                        */
59/*---------------------------------------------------------------------------*/
60
61/**AutomaticStart*************************************************************/
62
63/*---------------------------------------------------------------------------*/
64/* Static function prototypes                                                */
65/*---------------------------------------------------------------------------*/
66
67static int ChoosePrimes(int numOutputs, int **pool, int numDirectVerify);
68static int ComputeMaxNumberOfOutputs(void);
69static void RestoreOldMddIds(Ntk_Network_t *network, st_table *table);
70static st_table * GeneratePointerMatchTableFromNameMatch(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *nameMatchTable);
71static st_table * GenerateDirectVerifyPointerTable(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *outputMatch, array_t *outputOrderArray, int numDirectVerify);
72static st_table * GenerateIdentityMatchTable(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int inputOrOutput);
73static bdd_manager * Initializebdd_manager(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int *initManagerHere);
74static int SetBasicResultInfo(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int numDirectVerify);
75static void Cleanup(int error, Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int initManagerHere, int done, st_table *outputMatch, st_table *inputMatch, st_table *directVerifyMatch, st_table *oldSpecMddIdTable, st_table *oldImplMddIdTable, array_t *specLayerArray, array_t *implLayerArray);
76static st_table * SaveOldMddIds(Ntk_Network_t *network);
77static int DirectVerification(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *directVerifyMatch, st_table *inputMatch, st_table *outputMatch, array_t *outputOrderArray);
78static bdd_reorder_type_t DecodeDynMethod(char *dynMethodString);
79static int ResidueVerification(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *outputMatch, st_table *inputMatch, int numDirectVerify, array_t *specLayerArray, array_t *implLayerArray, array_t *outputArray);
80static void ExtractACubeOfDifference(bdd_manager *mgr, Ntk_Network_t *specNetwork, bdd_node *fn1, bdd_node *fn2);
81
82/**AutomaticEnd***************************************************************/
83
84
85/*---------------------------------------------------------------------------*/
86/* Definition of exported functions                                          */
87/*---------------------------------------------------------------------------*/
88
89/**Function********************************************************************
90
91  Synopsis      [Performs direct and residue verification of a given network.]
92
93  Description   [ Performs direct and residue verification of a given network.
94  This function is the core routine for residue verification. The network
95  parameters are in a specific order: SPECIFICATION first, IMPLEMENTATION
96  second. The two networks are differentiated because the specification is the
97  only circuit which may store  previously computed results. Also all other
98  parameters are with reference to the specification. The next parameter is
99  the number  of outputs to directly verify.
100  The output order array gives the order of the outputs,
101  starting from the MSB. The output and input match table contain name matches
102  for the output and input. The key in this table belongs to the specification
103  and the value to the implementation. The procedure initializes  the manager,
104  computes maximum number of outputs that can be verified, sets basic result
105  information. It also sets up the match tables with pointers and saves the
106  old MDD Ids in a table. It then calls the direct verification procedure, if
107  there are any outputs to be verified. For residue verification, the procedure
108  calls the layering procedure on both networks and creates layers. It calls
109  the main residue verification procedure and updates the result structures.
110  Returns the value 0 on success. The procedure takes in as arguments the
111  specification network, the implementation network in that order, the number
112  of outputs that need to be directly verified, the order of all the outputs,
113  the table with outputs name matches of the spec. and the impl. and a similar
114  input name match table.]
115
116  SideEffects        [The residue Info structure gets updated.]
117
118******************************************************************************/
119int
120Res_NetworkResidueVerify(
121         Ntk_Network_t *specNetwork,
122         Ntk_Network_t *implNetwork,
123         int numDirectVerify,
124         array_t *outputOrderArray,
125         st_table *outputNameMatch,
126         st_table *inputNameMatch)
127{
128  Ntk_Node_t *nodePtr;           /* To iterate over nodes */
129  Ntk_Node_t *implNodePtr;       /* To iterate over nodes */
130  Res_ResidueInfo_t *resultSpec; /* Structure holding all the info */
131  Res_ResidueInfo_t *resultImpl; /* Structure holding all the info */
132  array_t *specLayerArray;       /* array containing the reverse
133                                  * topological layers of the spec.
134                                  */
135  array_t *implLayerArray;       /* array containing the reverse
136                                  * topological layers of the impl.
137                                  */
138  st_table *oldSpecMddIdTable;   /* Tables to store MDD IDs of the spec
139                                  * if already assigned
140                                  */
141  st_table *oldImplMddIdTable;   /* Tables to store MDD IDs of the impl.
142                                  * if already assigned
143                                  */
144
145  st_table *outputMatch;         /* Output match table with node
146                                  * pointers, spec node pointer is
147                                  * the key
148                                  */
149  st_table *inputMatch;          /* Input match table with node
150                                  * pointers, spec node pointer is
151                                  * the key
152                                  */
153
154  bdd_manager *ddManager;          /* Manager read from the network */
155  int initManagerHere;           /* Flag to indicate the network Mdd
156                                  * managers initialized here
157                                  */
158
159  lsGen listGen;                 /* To iterate over outputList */
160  long overallLap;               /* To measure overall execution time */
161  int maxNumberOfOutputs;        /* max number of outputs that can be
162                                  * verified here
163                                  * = product(100 primes)
164                                  */
165  int numOutputs;                /* Store the number of outputs in spec.,
166                                  * impl
167                                  */
168  int done;                      /* flag to determine the status of
169                                  * previous verification
170                                  */
171  int error;                     /* error flag, set for cleanup, 1 failed,
172                                  * 0 if successful
173                                  */
174  int status;                    /* error status of residue verification */
175  int directVerifyStatus;        /* direct verification status, 1 if failed,
176                                  * 0 if successful
177                                  */
178  st_table *directVerifyMatch;   /* match table with pointers for the
179                                  * directly verified outputs, spec pointer
180                                  * is key
181                                  */
182  char *name;                    /* variable to store name of node */
183  array_t *outputArray;          /* array to store output nodes */
184  array_t *ignoreOutputArray;    /* array to store outputs nodes to be
185                                  * ignored
186                                  */
187  int verbose;                   /* variable to read residue_verbosity value */
188  char *flagValue;               /* string to read flag values */
189  int i;                         /* Loop iterators */
190  int unassignedValue;           /* NTK_UNASSIGNED_MDD_ID value holder */
191
192  /* Initialize some variables to default values */
193
194  overallLap = 0;
195  initManagerHere = 0;
196  ddManager = NIL(bdd_manager);
197  done = RES_VERIFY_NOTHING;
198  error = 0;
199  status = 1;
200  verbose = 0;
201
202  unassignedValue =  NTK_UNASSIGNED_MDD_ID;
203  directVerifyStatus = 1;
204  directVerifyMatch = NIL(st_table);
205  specLayerArray = NIL(array_t);
206  implLayerArray = NIL(array_t);
207  outputArray = NIL(array_t);
208  ignoreOutputArray = NIL(array_t);
209  outputMatch = NIL(st_table);
210  inputMatch = NIL(st_table);
211  oldSpecMddIdTable = NIL(st_table);
212  oldImplMddIdTable = NIL(st_table);
213  resultSpec = NIL(Res_ResidueInfo_t);
214  resultImpl = NIL(Res_ResidueInfo_t);
215
216
217  /* Initialize global time values*/
218  Res_composeTime = 0;
219  Res_smartVarTime = 0;
220  Res_shuffleTime = 0;
221  Res_orderTime = 0;
222
223
224  /* Read verbosity value */
225  flagValue = Cmd_FlagReadByName("residue_verbosity");
226  if (flagValue != NIL(char)) {
227    verbose = atoi(flagValue);
228  }
229
230  /* Read the mdd Manager (or create it if necessary) */
231  ddManager = Initializebdd_manager(specNetwork, implNetwork, &initManagerHere);
232  if (ddManager == NIL(bdd_manager)) {
233    /* error, but nothing allocated, so no cleanup */
234    return 1;
235  }
236
237  /* Set up the correct maximum number of outputs */
238  maxNumberOfOutputs  = ComputeMaxNumberOfOutputs();
239  if (verbose >= 2) {
240    fprintf(vis_stdout, "The Maximum Number of outputs that can be");
241    fprintf(vis_stdout, " verified are %d.\n", maxNumberOfOutputs);
242  }
243
244  /* check number of outputs */
245  numOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
246  /* Check if the circuit has too many outputs */
247  if (numOutputs >= maxNumberOfOutputs) {
248    error_append("Circuit with too many outputs.\n");
249    /* Clean up before you leave */
250    error = 1;
251    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
252            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
253            oldImplMddIdTable, specLayerArray, implLayerArray);
254    return 1;
255  } /* End of if */
256
257  /* Create result data structure for both the spec and the implementation */
258  done = SetBasicResultInfo(specNetwork, implNetwork, numDirectVerify);
259  if (done ==  RES_VERIFY_DONE) {/* same verification as previous time */
260    /* Clean up before you leave */
261    fprintf(vis_stdout, "Verification has been previously performed\n");
262    error = 0;
263    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
264            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
265            oldImplMddIdTable, specLayerArray, implLayerArray);
266    return 0; /* success */
267  } /* end of case RES_VERIFY_DONE */
268
269  /* if output match table does not exist, create one with matching names
270   * in the two networks. Insert with spec network node pointer as key
271   * in the outputMatch table. If match table does exist, convert name table
272   * to pointer table.
273   */
274  if(outputNameMatch == NIL(st_table)) {
275    outputMatch = GenerateIdentityMatchTable(specNetwork, implNetwork, PRIMARY_OUTPUTS);
276  } else {
277    outputMatch = GeneratePointerMatchTableFromNameMatch(specNetwork,
278                                                         implNetwork,outputNameMatch);
279    if (outputMatch == NIL(st_table)) {
280      error_append("Output pointer table is NULL\n");
281      /* Clean up before you leave */
282      error = 1;
283      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
284              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
285              oldImplMddIdTable, specLayerArray, implLayerArray);
286      return 1; /* error return */
287    }
288  }
289
290  /* if input match table does not exist, create one with matching names
291   * in the two networks. Insert with spec network node pointer as key
292   * in the inputMatch table. If match table does exist, convert name table
293   * to pointer table.
294   */
295  if(inputNameMatch == NIL(st_table)) {
296    inputMatch = GenerateIdentityMatchTable(specNetwork, implNetwork, PRIMARY_INPUTS);
297  } else {
298    inputMatch = GeneratePointerMatchTableFromNameMatch(specNetwork,
299                                                        implNetwork,inputNameMatch);
300    if (inputMatch == NIL(st_table)) {
301      error_append("Input pointer table is NULL\n");
302      /* Clean up before you leave */
303      error = 1;
304      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
305              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
306              oldImplMddIdTable, specLayerArray, implLayerArray);
307      return 1; /* error return */
308    }
309  }
310
311  /* Save the old MDD IDs in a st_table */
312  oldSpecMddIdTable = SaveOldMddIds(specNetwork);
313  if (oldSpecMddIdTable == NIL(st_table)) {
314    error_append("Unable to save old Mdd Ids for spec\n");
315    /* Clean up before you leave */
316    error = 1;
317    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
318            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
319            oldImplMddIdTable, specLayerArray, implLayerArray);
320    return 1;
321  }
322
323  /* Save the old MDD IDs in a st_table */
324  oldImplMddIdTable = SaveOldMddIds(implNetwork);
325  if (oldImplMddIdTable == NIL(st_table)) {
326    error_append("Unable to save old Mdd Ids for impl\n");
327    /* Clean up before you leave */
328    error = 1;
329    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
330            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
331            oldImplMddIdTable, specLayerArray, implLayerArray);
332    return 1;
333  }
334
335  /* Initialize time to measure overall lap time */
336  overallLap = util_cpu_time();
337
338  /* Perform direct verification of the given outputs. */
339  if (numDirectVerify) {
340    /* generate output match table for outputs to be directly verified */
341    directVerifyMatch = GenerateDirectVerifyPointerTable(specNetwork,
342         implNetwork, outputMatch, outputOrderArray, numDirectVerify);
343    if (directVerifyMatch == NIL(st_table)) {
344      error_append("Directly verify  pointer table is NULL\n");
345      /* Clean up before you leave */
346      error = 1;
347      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
348              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
349              oldImplMddIdTable, specLayerArray, implLayerArray);
350      return 1; /* error return */
351    }
352
353    /* perform direct verification of the outputs in the match table */
354    directVerifyStatus = DirectVerification(specNetwork, implNetwork,
355                    directVerifyMatch, inputMatch, outputMatch, outputOrderArray);
356    /* Direct verification error */
357    if (directVerifyStatus == 1) {
358      error_append("Direct Verification error\n");
359      /* Clean up before you leave */
360      error = 1;
361      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
362      outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
363              oldImplMddIdTable, specLayerArray, implLayerArray);
364      return 1; /* error return */
365    }
366
367    resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
368                                            RES_NETWORK_APPL_KEY);
369    resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
370                                            RES_NETWORK_APPL_KEY);
371    /* Direct verification failed */
372    if ((ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_FAIL) &&
373        (ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_FAIL)) {
374      ResResidueInfoSetSuccess(resultSpec, RES_FAIL);
375      ResResidueInfoSetSuccess(resultImpl, RES_FAIL);
376      /*  Clean up before you leave */
377      error = 0;
378      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
379      outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
380              oldImplMddIdTable, specLayerArray, implLayerArray);
381      return 0;
382    } else if (numDirectVerify == numOutputs) {
383      if ((ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_PASS) &&
384          (ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_PASS)) {
385        /* if all outputs are directly verified */
386        ResResidueInfoSetSuccess(resultSpec, RES_PASS);
387        ResResidueInfoSetSuccess(resultImpl, RES_PASS);
388      }
389    } /* end of else */
390
391
392  } /* Direct Verification, done and successful */
393
394  (void) fprintf(vis_stdout, "Total Direct Verification Time = %.3f (secs).\n",
395                 (util_cpu_time() - overallLap)/1000.0);
396
397  if (verbose >= 1) {
398    util_print_cpu_stats(vis_stdout);
399  }
400
401
402  /* RESIDUE VERIFICATION starts here */
403
404  if (numOutputs - numDirectVerify) { /* if residue verification required */
405    /* reset all Ids after direct verification as residue verification
406     * assigns new Ids.
407     */
408    Ntk_NetworkForEachNode(specNetwork, listGen, nodePtr) {
409      Ntk_NodeSetMddId(nodePtr, unassignedValue);
410    }
411    Ntk_NetworkForEachNode(implNetwork, listGen, nodePtr) {
412      Ntk_NodeSetMddId(nodePtr, unassignedValue);
413    }
414
415    /* check if directly verified outputs are to be involved in residue
416     * verification
417     */
418    flagValue = Cmd_FlagReadByName("residue_ignore_direct_verified_outputs");
419    if (flagValue != NIL(char)) {
420      if ((strcmp(flagValue, "1") == 0) && (numDirectVerify)) {
421        ignoreOutputArray = array_alloc(Ntk_Node_t *, numDirectVerify);
422      }
423    }
424    if (ignoreOutputArray == NIL(array_t)) {
425      /* fill the output array with all output nodes */
426      outputArray = array_alloc(Ntk_Node_t *, array_n(outputOrderArray));
427      arrayForEachItem(char *, outputOrderArray, i, name) {
428        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
429        st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
430        array_insert(Ntk_Node_t *, outputArray, i, implNodePtr);
431      }
432    } else {
433      outputArray = array_alloc(Ntk_Node_t *, array_n(outputOrderArray)-numDirectVerify);
434      /* fill the output array with nodes not directly verified */
435      for (i = 0; i < (array_n(outputOrderArray) - numDirectVerify); i++) {
436        name = array_fetch(char *, outputOrderArray, i);
437        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
438        st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
439        array_insert(Ntk_Node_t *, outputArray, i, implNodePtr);
440      }
441      /* fill ignore array with outputs directly verified. */
442      for (i = (array_n(outputOrderArray) - numDirectVerify); i < array_n(outputOrderArray); i++) {
443        name = array_fetch(char *, outputOrderArray, i);
444        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
445        st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
446        array_insert(Ntk_Node_t *, ignoreOutputArray, (i-array_n(outputOrderArray)+numDirectVerify) , implNodePtr);
447      }
448    }
449
450
451    /* Compute the layers to be used for function composition */
452    implLayerArray = ResComputeCompositionLayers(implNetwork, outputArray, ignoreOutputArray);
453
454    /* create the output array for the spec. */
455    if (ignoreOutputArray == NIL(array_t)) {
456      /* fill the output array with all output nodes */
457      arrayForEachItem(char *, outputOrderArray, i, name) {
458        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
459        array_insert(Ntk_Node_t *, outputArray, i, nodePtr);
460      }
461    } else {
462      /* fill the output array with nodes not directly verified */
463      for (i = 0; i < (array_n(outputOrderArray) - numDirectVerify); i++) {
464        name = array_fetch(char *, outputOrderArray, i);
465        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
466        array_insert(Ntk_Node_t *, outputArray, i, nodePtr);
467      }
468      /* fill ignore array with outputs directly verified. */
469      for (i = (array_n(outputOrderArray) - numDirectVerify); i < array_n(outputOrderArray); i++) {
470        name = array_fetch(char *, outputOrderArray, i);
471        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
472        array_insert(Ntk_Node_t *, ignoreOutputArray, (i-array_n(outputOrderArray)+numDirectVerify), nodePtr);
473      }
474    }
475
476    /* Compute the layers to be used for function composition */
477    specLayerArray = ResComputeCompositionLayers(specNetwork, outputArray, ignoreOutputArray);
478
479    /* print the array */
480    if (verbose >=3) {
481      ResLayerPrintInfo(specNetwork, specLayerArray);
482      ResLayerPrintInfo(implNetwork, implLayerArray);
483    }
484
485    /* free the ignore array */
486    if (ignoreOutputArray != NIL(array_t)) {
487      array_free(ignoreOutputArray);
488    }
489
490    /* Perform residue verification on the spec. and impl. */
491    status = ResidueVerification(specNetwork, implNetwork, outputMatch, inputMatch, numDirectVerify, specLayerArray, implLayerArray, outputArray);
492
493    /* free output array */
494    array_free(outputArray);
495
496    if (status) {
497      error_append("Residue Verification error\n");
498      /* Clean up before you leave */
499      error = 1;
500      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
501              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
502              oldImplMddIdTable, specLayerArray, implLayerArray);
503      return 1; /* error return */
504    }
505
506
507    resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
508                                              RES_NETWORK_APPL_KEY);
509    resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
510                                            RES_NETWORK_APPL_KEY);
511    /* Print success message and info */
512    if ((ResResidueInfoReadSuccess(resultSpec) == RES_FAIL) &&
513        (ResResidueInfoReadSuccess(resultImpl) == RES_FAIL)) {
514      /* Clean up before you leave */
515      error = 0;
516            Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
517              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
518              oldImplMddIdTable, specLayerArray, implLayerArray);
519      return 0;
520    }
521
522    if(verbose >= 2) {
523      (void) fprintf(vis_stdout, "Total Compose Time = %3f(secs).\n",
524                     Res_composeTime/1000.0);
525      (void) fprintf(vis_stdout, "Total Order Time = %3f(secs).\n",
526                     Res_orderTime/1000.0);
527      (void) fprintf(vis_stdout, "Total Shuffle Time = %3f(secs).\n",
528                     Res_shuffleTime/1000.0);
529
530      (void) fprintf(vis_stdout, "Total Smart Var Time = %3f(secs).\n",
531                     Res_smartVarTime/1000.0);
532    }
533
534
535  } /* end of residue verification */
536
537  /* Print success message and info */
538  if ((ResResidueInfoReadSuccess(resultSpec) == RES_PASS) &&
539      (ResResidueInfoReadSuccess(resultImpl) == RES_PASS))
540    (void) fprintf(vis_stdout, "Verification of %s and %s successful.\n",
541                   Res_ResidueInfoReadName(resultSpec),
542                   Res_ResidueInfoReadName(resultImpl));
543
544
545  if (verbose >= 1) {
546    fprintf(vis_stdout, "Specification:\n");
547    (void) Res_ResidueInfoPrint(resultSpec);
548    fprintf(vis_stdout, "Implementation:\n");
549    (void) Res_ResidueInfoPrint(resultImpl);
550  }
551  if (verbose >= 1) {
552    util_print_cpu_stats(vis_stdout);
553  }
554
555  (void) fprintf(vis_stdout, "Total Time = %.3f (secs).\n",
556                 (util_cpu_time() - overallLap)/1000.0);
557
558  /* no error */
559  error = 0;
560  Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
561          outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
562          oldImplMddIdTable, specLayerArray, implLayerArray);
563
564  /* End of clean up */
565
566  return 0;
567} /* End of Res_NetworkResidueVerify */
568
569/*---------------------------------------------------------------------------*/
570/* Definition of internal functions                                          */
571/*---------------------------------------------------------------------------*/
572
573
574
575/*---------------------------------------------------------------------------*/
576/* Definition of static functions                                            */
577/*---------------------------------------------------------------------------*/
578
579/**Function********************************************************************
580
581  Synopsis [Chooses the primes to process a circuit with those many outputs.]
582
583  Description [Chooses the primes to process a circuit with those many
584  outputs. It returns an allocated array of primes selected from PrimePool. The
585  number of primes required should exceed the quotient from dividing 2^number
586  of outputs by 2^number of directly verified outputs. If there are no directly
587  verified outputs, the first prime chosen is 2^LOG2_FIRST_PRIME. The procedure
588  is passed the following parameters: number of outputs, the array of primes
589  (to be filled) and the number of directly verified outputs.]
590
591  SideEffects [Fills the primes array.]
592
593  See Also    [Res_NetworkResidueVerify]
594
595******************************************************************************/
596static int
597ChoosePrimes(int numOutputs,
598             int **pool,
599             int numDirectVerify)
600{
601  double accumulator = 0.0;
602  int i,max, index = 0;
603  double factor = log10((double)2.0);
604
605  assert(*pool == NIL(int));
606
607  if (numDirectVerify) {
608    accumulator = (double)numDirectVerify;
609  } else {
610    /* make first prime 2^LOG2_FIRST_PRIME */
611    if (numOutputs >= LOG2_FIRST_PRIME) {
612      accumulator = (double)LOG2_FIRST_PRIME;
613    } else {
614      accumulator = (double)numOutputs;
615    }
616  }
617
618  /* step through primes till their product exceeds the max value of outputs */
619  max = 0;
620  while (accumulator < ((double)numOutputs)) {
621    accumulator += log10((double)PrimePool[max])/factor;
622    max++;
623  }
624
625  index = 0;
626  /* if no direct verification, then set the first prime to be 2^LOG2_FIRST_PRIME */
627  if (!numDirectVerify) {
628    *pool = ALLOC(int, max+1);
629    if (numOutputs >= LOG2_FIRST_PRIME) {
630      (*pool)[index++] = (int)pow((double)2.0, (double)LOG2_FIRST_PRIME);
631    } else {
632      (*pool)[index++] = (int)pow((double)2.0, (double)numOutputs);
633    }
634  } else {
635    *pool = ALLOC(int, max);
636  }
637
638  /* fill the array with other primes */
639  for(i=0; i < max; i++) {
640   (*pool)[index++] = PrimePool[i];
641  }
642
643  return index;
644} /* End of ChoosePrimes */
645
646
647/**Function********************************************************************
648
649  Synopsis [Computes the maximum number of outputs a circuit may have in order
650  to be processed with the array PrimePool.]
651
652  Description [Computes the maximum number of outputs a circuit may have in
653  order to be processed with the array PrimePool. This is the product of all
654  the primes in the Prime Pool Table.]
655
656  SideEffects [Updates the static variable maxNumberOfOutputs.]
657
658  SeeAlso     [Res_NetworkResidueVerify]
659
660******************************************************************************/
661static int
662ComputeMaxNumberOfOutputs(void)
663{
664  int i;
665  double result = 0;
666  int maxNumberOfOutputs;
667
668  result = LOG2_FIRST_PRIME;
669  for(i = 0; i < PrimePoolSize; i++) {
670    result += log10((double)PrimePool[i]);
671  } /* End of for */
672
673  maxNumberOfOutputs = (int) (result/log10((double) 2.0)) - 1;
674
675  return (maxNumberOfOutputs);
676} /* End of ComputeMaxNumberOfOutputs */
677
678
679/**Function********************************************************************
680
681  Synopsis    [A procedure restore  MDD Ids from an st table.]
682
683  Description [A procedure restore MDD Ids from an st table. This is to leave
684  the network in the state it was in before residue verification was
685  called. The procedure's parameters are the network whose IDs need to be
686  restored and a table to restore from.]
687
688  SideEffects [The mdd Ids of the network change.]
689
690  SeeAlso     [Res_NetworkResidueVerify SaveOldMddIds]
691
692******************************************************************************/
693static void
694RestoreOldMddIds(Ntk_Network_t *network,
695                 st_table *table)
696{
697  lsGen listGen;
698  Ntk_Node_t *nodePtr;
699  int value;
700  if (table != NULL) {
701    Ntk_NetworkForEachNode(network, listGen, nodePtr) {
702      if(st_lookup_int(table, (char *)nodePtr, &value)) {
703        Ntk_NodeSetMddId(nodePtr, value);
704      } else {
705        error_append("Node");
706        error_append(Ntk_NetworkReadName(network));
707        error_append("should have been in the table.\n");
708        (void) lsFinish(listGen);
709      }
710    }
711  }
712} /* End of RestoreOldMddIds */
713
714
715/**Function********************************************************************
716
717  Synopsis [Procedure to generate a match Table with node pointers from a match
718  table with names.]
719
720  Description [Procedure to generate a match Table with node pointers from a
721  match table with names.The name match table will have pairs of names which
722  may be from the spec or the impl. So for each unique pair there are two
723  entries in the name match table. The pointer match table is constructed with
724  the spec. node pointer as the key. If the node pointer for a name isn't found
725  in either network, return NIL (error). The procedure takes in the parameters:
726  spec., impl and a name match table and returns a pointer match table
727  corresponding to the names.]
728
729  SideEffects   []
730
731  SeeAlso            [Res_NetworkResidueVerify]
732
733******************************************************************************/
734static st_table *
735GeneratePointerMatchTableFromNameMatch(
736                       Ntk_Network_t *specNetwork,
737                       Ntk_Network_t *implNetwork,
738                       st_table *nameMatchTable)
739{
740  st_table *pointerMatch;
741  Ntk_Node_t *nodePtr, *implNodePtr;
742  st_generator *stGen;
743  char *key, *value;
744
745  pointerMatch = st_init_table( st_ptrcmp, st_ptrhash);
746  st_foreach_item(nameMatchTable, stGen, &key, &value) {
747    /* find node in spec */
748    nodePtr = Ntk_NetworkFindNodeByName(specNetwork, key);
749    if (nodePtr == NIL(Ntk_Node_t)) {
750      /* if node not in spec, find in impl */
751      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork, key);
752      nodePtr = Ntk_NetworkFindNodeByName(specNetwork, value);
753    } else {
754      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork,value);
755    }
756    if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))) {
757      /* error */
758      error_append("Nodes not found by the keys in match table.\n");
759      st_free_gen(stGen);
760      return NIL(st_table);
761    }
762    st_insert(pointerMatch, (char *)nodePtr, (char *)implNodePtr);
763  } /* end of st_foreach_item */
764
765  return(pointerMatch);
766} /* End of GeneratePointerMatchTableFromNameMatch */
767
768
769/**Function********************************************************************
770
771  Synopsis [Generates a pointer match table for the directly verified outputs.]
772
773  Description [Generates a pointer match table for the directly verified
774  outputs. Returns NIL if a node isn't found, else returns the table.The
775  procedure takes as arguments the spec., the impl., the output match table
776  with pointers, the output order array and the number of directly verified
777  outputs.]
778
779  SideEffects   []
780
781  SeeAlso            [Res_NetworkResidueVerify]
782
783******************************************************************************/
784static st_table *
785GenerateDirectVerifyPointerTable(Ntk_Network_t *specNetwork,
786                                 Ntk_Network_t *implNetwork,
787                                 st_table *outputMatch,
788                                 array_t *outputOrderArray,
789                                 int numDirectVerify)
790
791{
792  char *specName;
793  int i;
794  Ntk_Node_t *nodePtr, *implNodePtr;
795  st_table *directVerifyMatch;
796
797  directVerifyMatch = st_init_table(st_ptrcmp, st_ptrhash);
798  for (i = 0; i < numDirectVerify; i++) {
799    specName = array_fetch(char *, outputOrderArray, array_n(outputOrderArray) - 1 - i);
800    nodePtr = Ntk_NetworkFindNodeByName(specNetwork, specName);
801    st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
802    if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))) {
803      error_append("Couldn't find nodes to directly verify\n");
804      st_free_table(directVerifyMatch);
805      return NIL(st_table);
806    }
807    st_insert(directVerifyMatch, (char *)nodePtr, (char *)implNodePtr);
808  }
809  return (directVerifyMatch);
810} /* End of GenerateDirectVerifyPointerTable */
811
812
813/**Function********************************************************************
814
815  Synopsis [ A procedure to generate a pointer Match table with from
816  nodes with identical names.]
817
818  Description [A procedure to generate a pointer Match table with from nodes
819  with identical names. This procedure does it for either the inputs or outputs
820  depending on the flag. Returns NULL if the impl. does not have a node
821  corresponding to the spec. The procedure takes as arguments the spec., the
822  impl. and the flag specifying whether the pointer match table is to be built
823  for the output or the input.]
824
825  SideEffects   []
826
827  SeeAlso            [Res_NetworkResidueVerify]
828
829******************************************************************************/
830static st_table *
831GenerateIdentityMatchTable(Ntk_Network_t *specNetwork,
832                           Ntk_Network_t *implNetwork,
833                           int inputOrOutput)
834{
835  Ntk_Node_t *nodePtr, *implNodePtr;
836  st_table *matchTable;
837  lsGen listGen;
838  char *name;
839
840  matchTable = st_init_table(st_ptrcmp, st_ptrhash);
841  if (matchTable == NULL) return(NIL(st_table));
842
843  if (inputOrOutput == PRIMARY_INPUTS) {
844    Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
845      name = Ntk_NodeReadName(nodePtr);
846      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork, name);
847      if (implNodePtr == NIL(Ntk_Node_t)) {
848        error_append(name);
849        error_append(" node does not have corresponding node in impl.");
850        st_free_table(matchTable);
851        return (NIL(st_table));
852      }
853      st_insert(matchTable, (char *)nodePtr, (char *)implNodePtr);
854    }
855  } else if (inputOrOutput == PRIMARY_OUTPUTS) {
856    Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
857      name = Ntk_NodeReadName(nodePtr);
858      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork,name);
859      if (implNodePtr == NIL(Ntk_Node_t)) {
860        error_append(name);
861        error_append(" node does not have corresponding node in impl.");
862        st_free_table(matchTable);
863        return (NIL(st_table));
864      }
865      st_insert(matchTable, (char *)nodePtr, (char *)implNodePtr);
866    }
867  }
868  return (matchTable);
869} /* End of GenerateIdentityMatchTable */
870
871/**Function********************************************************************
872
873  Synopsis    [Initialize bdd_managers for the networks.]
874
875  Description [Initialize bdd_managers for the networks. If both managers are
876  NIL , initialize a DD Manager here and set it in both networks. If the
877  manager is not NIL, then they have to be the same. If different, keep the
878  spec network manager. Return a flag if managers are initialized here. The
879  procedure takes as arguments the spec., the impl. and the flag specifying
880  whether the the manager was initialized here (to be filled).]
881
882  SideEffects [Network manager values might change.]
883
884  SeeAlso     [Res_NetworkResidueVerify]
885
886******************************************************************************/
887static bdd_manager *
888Initializebdd_manager(Ntk_Network_t *specNetwork,
889                    Ntk_Network_t *implNetwork,
890                    int *initManagerHere)
891{
892  bdd_manager *ddManager;
893
894  /* Read the mdd Manager (or create it if necessary) */
895  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
896
897  /* To set the spec manager the same as the impl. manager, either
898   * both are nil, or the impl manager is freed and set to the
899   * spec manager
900   */
901  if(ddManager != (bdd_manager *)Ntk_NetworkReadMddManager(implNetwork)) {
902    if ((bdd_manager *)Ntk_NetworkReadMddManager(implNetwork) != NIL(bdd_manager)) {
903      /* unacceptable if the impl. manager is different from NIl or
904       * from the spec manager
905       */
906      mdd_quit(Ntk_NetworkReadMddManager(implNetwork));
907    }
908    Ntk_NetworkSetMddManager(implNetwork, (mdd_manager *)ddManager);
909  }
910
911  /* if the spec. manager is NIL, then network initialize manager */
912  if (ddManager ==  NIL(bdd_manager)) {
913    /* flag to say that manager is verified here */
914    *initManagerHere = 1;
915    ddManager = (bdd_manager *)Ntk_NetworkInitializeMddManager(specNetwork);
916    Ntk_NetworkSetMddManager(implNetwork, (mdd_manager *)ddManager);
917  }
918  return (ddManager);
919} /* End of Initializebdd_manager */
920
921/**Function********************************************************************
922
923  Synopsis [Create the basic result structures for both the specification and
924  implementation.]
925
926  Description [Create the basic result structures for both the specification
927  and implementation. This procedure returns a flag that specifies if the
928  previous verification was a success. If previous information is to be used
929  only the condition that either the same spec and impl were verified before,
930  is allowed. If the previous verification had the same number of directly
931  verified outputs and the verification was a success, a success is returned.
932  The impl. result will be overwritten in any case. Returns a flag that
933  indicates if verification is to be done. The procedure records the number of
934  outputs, inputs, directly verified outputs, spec and impl name. Adds the
935  result structure as a hook to the network. The procedure takes as arguments
936  the spec., the impl. and the number of directly verified outputs.]
937
938  SideEffects [Changes the result structure in the 2 networks.]
939
940  SeeAlso [Res_NetworkResidueVerify]
941
942******************************************************************************/
943static int
944SetBasicResultInfo (Ntk_Network_t *specNetwork,
945                    Ntk_Network_t *implNetwork,
946                    int numDirectVerify)
947{
948  int numInputs;
949  int numOutputs;
950  char *specName;
951  char *implName;
952  Res_ResidueInfo_t *resultSpec;
953  Res_ResidueInfo_t *resultImpl;
954
955  /* if previous verification to be considered, make sure the
956   *  verification was with the same spec network and the number
957   *  of directly verified outputs are the same.
958   */
959  resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
960                                                    RES_NETWORK_APPL_KEY);
961
962  if (resultSpec != NIL(Res_ResidueInfo_t)) {
963    if ((strcmp(ResResidueInfoReadNameVerifiedAgainst(resultSpec),
964              Ntk_NetworkReadName(implNetwork)) == 0) &&
965        (ResResidueInfoReadNumDirectVerifiedOutputs(resultSpec) ==
966                                                 numDirectVerify) &&
967        (ResResidueInfoReadSuccess(resultSpec) == RES_PASS)) {
968      /* if already verified then done, return success (0) */
969      return RES_VERIFY_DONE;
970    }
971    /* if the above conditions are not satisfied, attempt
972     * verification again
973     */
974    Ntk_NetworkFreeApplInfo(specNetwork, RES_NETWORK_APPL_KEY );
975  }
976
977
978  /* create result structure */
979  resultSpec = (Res_ResidueInfo_t *)
980    ResNetworkResidueInfoReadOrCreate(specNetwork);
981  /* add hook to network */
982  Ntk_NetworkAddApplInfo(specNetwork, RES_NETWORK_APPL_KEY,
983                 (Ntk_ApplInfoFreeFn) Res_ResidueInfoFreeCallback,
984                 (void *)resultSpec);
985
986  /* number of outputs */
987  numOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
988  ResResidueInfoSetNumOutputs(resultSpec, numOutputs);
989  /* number of Inputs */
990  numInputs = Ntk_NetworkReadNumCombInputs(specNetwork);
991  ResResidueInfoSetNumInputs(resultSpec, numInputs);
992  /* impl name */
993  implName = util_strsav(Ntk_NetworkReadName(implNetwork));
994  ResResidueInfoSetNameVerifiedAgainst(resultSpec, implName);
995  /* number of directly verified outputs */
996  ResResidueInfoSetNumDirectVerifiedOutputs(resultSpec, numDirectVerify);
997
998  /*
999   * Assumption: The implementation residue information is invalid even
1000   * if it does exist and will be overwritten
1001   */
1002  resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
1003                                        RES_NETWORK_APPL_KEY);
1004  /* free existing structure */
1005  if (resultImpl != NIL(Res_ResidueInfo_t)) {
1006    Ntk_NetworkFreeApplInfo(implNetwork,RES_NETWORK_APPL_KEY);
1007  }
1008
1009  /* create a new structure for the implementation network */
1010  resultImpl = (Res_ResidueInfo_t *)
1011    ResNetworkResidueInfoReadOrCreate(implNetwork);
1012  Ntk_NetworkAddApplInfo(implNetwork, RES_NETWORK_APPL_KEY,
1013                (Ntk_ApplInfoFreeFn) Res_ResidueInfoFreeCallback,
1014                (void *)resultImpl);
1015
1016
1017  /*
1018   * Get some information about the network  and initialize the residue
1019   * information for the implementation network.
1020   */
1021
1022  /* number of outputs */
1023  assert (numOutputs == Ntk_NetworkReadNumCombOutputs(implNetwork));
1024  ResResidueInfoSetNumOutputs(resultImpl, numOutputs);
1025  /* number of Inputs */
1026  assert (numInputs == Ntk_NetworkReadNumCombInputs(implNetwork));
1027  ResResidueInfoSetNumInputs(resultImpl, numInputs);
1028  /* spec name */
1029  specName = util_strsav(Ntk_NetworkReadName(specNetwork));
1030  ResResidueInfoSetNameVerifiedAgainst(resultImpl, specName);
1031  /* number of directly verified outputs */
1032  ResResidueInfoSetNumDirectVerifiedOutputs(resultImpl, numDirectVerify);
1033
1034  return RES_VERIFY_IGNORE_PREV_RESULTS;
1035} /* End of SetBasicResultInfo */
1036
1037/**Function********************************************************************
1038
1039  Synopsis [Cleanup procedure to free all data structures allocated here.]
1040
1041  Description [Cleanup procedure to free all data structures allocated here.
1042  Quit manager if created here. Quit result data structures if created here.
1043  The check against RES_VERIFY_NOTHING is to check if the cleanup is called
1044  before the result structures were allocated. The arguments to this procedure
1045  are an error flag staying if this cleanup is under an error condition, the
1046  spec network, impl. network, a flag that says if the manager was initialized
1047  here, a flag that indicates if this verification has already been performed,
1048  an output pointer match table, an input pointer match table, a directly
1049  verified output pointer match table, a table that contains saved mdds for the
1050  spec. and the impl., and the layer structures for the spec. and the impl.]
1051
1052  SideEffects [All data structures allocated in the Res_NetworkResidueVerify
1053  procedure will be freed here.]
1054
1055  SeeAlso     [Res_NetworkResidueVerify]
1056
1057******************************************************************************/
1058static void
1059Cleanup(int error,
1060        Ntk_Network_t *specNetwork,
1061        Ntk_Network_t *implNetwork,
1062        int initManagerHere,
1063        int done,
1064        st_table *outputMatch,
1065        st_table *inputMatch,
1066        st_table *directVerifyMatch,
1067        st_table *oldSpecMddIdTable,
1068        st_table *oldImplMddIdTable,
1069        array_t *specLayerArray,
1070        array_t *implLayerArray)
1071{
1072  bdd_manager *ddManager;
1073
1074  if (initManagerHere) {
1075    ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
1076    if (ddManager != NIL(bdd_manager)) {
1077      mdd_quit(ddManager);
1078      Ntk_NetworkSetMddManager(specNetwork, NIL(mdd_manager));
1079      Ntk_NetworkSetMddManager(implNetwork, NIL(mdd_manager));
1080    }
1081  }
1082
1083  if (done != RES_VERIFY_NOTHING) {  /* if result structure allocated */
1084    if (error) { /* on error free results */
1085      if (done == RES_VERIFY_IGNORE_PREV_RESULTS) {
1086        /* if spec result was created here */
1087        Ntk_NetworkFreeApplInfo(specNetwork,RES_NETWORK_APPL_KEY);
1088      }
1089      Ntk_NetworkFreeApplInfo(implNetwork,RES_NETWORK_APPL_KEY);
1090    }
1091  }
1092  if (outputMatch != NIL(st_table)) {
1093    st_free_table(outputMatch);
1094  }
1095  if (inputMatch != NIL(st_table)) {
1096    st_free_table(inputMatch);
1097  }
1098  if (directVerifyMatch != NIL(st_table)) {
1099    st_free_table(directVerifyMatch);
1100  }
1101
1102  if (oldSpecMddIdTable != NIL(st_table)) {
1103    RestoreOldMddIds(specNetwork, oldSpecMddIdTable);
1104    st_free_table(oldSpecMddIdTable);
1105  }
1106  if (oldImplMddIdTable != NIL(st_table)) {
1107    RestoreOldMddIds(implNetwork, oldImplMddIdTable);
1108    st_free_table(oldImplMddIdTable);
1109  }
1110  if (specLayerArray != NULL) {
1111    ResLayerArrayFree(specLayerArray);
1112  }
1113  if (implLayerArray != NULL) {
1114    ResLayerArrayFree(implLayerArray);
1115  }
1116  return;
1117} /* End of Cleanup */
1118
1119
1120/**Function********************************************************************
1121
1122  Synopsis [Save mdd ids for each node.]
1123
1124  Description [Save old mdd ids for each node and returns a table with the
1125  nodes and the Ids.]
1126
1127  SideEffects   []
1128
1129  SeeAlso [Res_NetworkResidueVerify RestoreOldMddIds]
1130
1131******************************************************************************/
1132static st_table *
1133SaveOldMddIds(Ntk_Network_t *network)
1134{
1135  st_table *oldMddIdTable;
1136  Ntk_Node_t *nodePtr;
1137  lsGen listGen;             /* To iterate over outputList */
1138
1139  oldMddIdTable = st_init_table(st_ptrcmp, st_ptrhash);
1140  if (oldMddIdTable == NULL) return NIL(st_table);
1141
1142  Ntk_NetworkForEachNode(network, listGen, nodePtr) {
1143    st_insert(oldMddIdTable, (char *)nodePtr,
1144              (char *)(long)Ntk_NodeReadMddId(nodePtr));
1145  }
1146  return(oldMddIdTable);
1147}
1148
1149/**Function********************************************************************
1150
1151  Synopsis [Perform direct verification of the given outputs.]
1152
1153  Description [Perform direct verification of the given outputs. If error,
1154  returns 1, if successful returns 0. The directVerifyMatch table contains the
1155  node pointer matches for the outputs to be directly verified. The procedure
1156  first checks if the input variables are ordered.  If not ordered, it orders
1157  the variables. builds two array with corresponding nodes to be directly
1158  verified and a permutation array for the correspondence of the inputs.  The
1159  outputs arrays are ordered starting with the LSB. For each of these nodes in
1160  the array, the bdd is built and compared. Since the primary input variables
1161  in the spec and the impl may have different mdd ids, a step of bdd permute is
1162  performed on the impl bdd to represent it in terms of the spec PI
1163  variables. The resultant Bdds are checked to see if they are identical.  The
1164  result structure is updated. The parameters to this procedure are the spec.
1165  and the impl. network, the match table of the pointers of the directly
1166  verified outputs, the tables with the input and output pointer matches and
1167  the order array of the outputs.]
1168
1169  SideEffects   [Result Structure is updated.]
1170
1171  SeeAlso     [Res_NetworkResidueVerify]
1172
1173******************************************************************************/
1174static int
1175DirectVerification(Ntk_Network_t *specNetwork,
1176                   Ntk_Network_t *implNetwork,
1177                   st_table *directVerifyMatch,
1178                   st_table *inputMatch,
1179                   st_table *outputMatch,
1180                   array_t *outputOrderArray)
1181{
1182
1183    Ntk_Node_t *nodePtr, *implNodePtr;         /* node variables */
1184    long startTime, endTime, directVerifyTime; /* to measure elapsed time */
1185    long lapTimeSpec, lapTimeImpl;             /* to measure elapsed time */
1186    bdd_node *specBDD, *implBDD, *permutedBDD;   /* bdds of direct verified outputs */
1187    lsGen listGen;                             /* To iterate over outputList */
1188    int *permut;                              /* permutation array to store
1189                                               * correspondence of inputs
1190                                               */
1191    int specMddId, implMddId;
1192    Ntk_Node_t **specArray, **implArray;      /* arrays to store the
1193                                               * corresponding nodes of the
1194                                               * spec. and the impl.
1195                                               */
1196    st_generator *stGen;
1197    lsList dummy;                               /* dummy list fed to the ord
1198                                                 * package.
1199                                                 */
1200    char *key, *value;                          /* variables to read values
1201                                                 * from the st_table
1202                                                 */
1203    int index, i;                               /* iterators */
1204    char *name;                                 /* variable to read node name */
1205    int numOutputs;                             /* total number of outputs of
1206                                                 * the spec.(impl).
1207                                                 */
1208    bdd_manager *ddManager;                     /* the bdd manager */
1209    bdd_reorder_type_t oldDynMethod, dynMethod = BDD_REORDER_SAME;
1210                                                /* dynamic reordering methods */
1211    int dynStatus = 0;                          /* original status of the manager
1212                                                 * w. r. t. dynamic reordering
1213                                                 */
1214    boolean dyn;                                /* current dynamic reordering
1215                                                 * status
1216                                                 */
1217    int verbose;                                /* verbosity level */
1218    char  *flagValue;                           /* string to hold "Set" variable
1219                                                 * value
1220                                                 */
1221    Res_ResidueInfo_t *resultSpec;              /* result structure for the
1222                                                 * spec.
1223                                                 */
1224    Res_ResidueInfo_t *resultImpl;              /* result structure for the
1225                                                 * impl.
1226                                                 */
1227    int specSize, implSize;                     /* sizes of bdds */
1228    mdd_t *fnMddT;                              /* mdd_t structure to calculate sizes */
1229
1230
1231    /* Initializations */
1232    dummy = (lsList)0;
1233    lapTimeSpec = 0;
1234    lapTimeImpl = 0;
1235    dyn = FALSE;
1236    verbose = 0;
1237
1238    /* read verbosity value */
1239    flagValue = Cmd_FlagReadByName("residue_verbosity");
1240    if (flagValue != NIL(char)) {
1241      verbose = atoi(flagValue);
1242    }
1243
1244    /* read if dynamic ordering is required */
1245    flagValue = Cmd_FlagReadByName("residue_autodyn_direct_verif");
1246    if (flagValue != NIL(char)) {
1247      dyn = (strcmp(flagValue, "1") == 0) ? TRUE : FALSE;
1248    }
1249    /* read method for dynamic reordering */
1250    if (dyn == TRUE) {
1251      flagValue = Cmd_FlagReadByName("residue_direct_dyn_method");
1252      if (flagValue != NULL) {
1253        dynMethod = DecodeDynMethod(flagValue);
1254      } else {
1255        dynMethod = BDD_REORDER_SAME;
1256      }
1257    }
1258
1259    /* read manager from network */
1260    ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
1261    /* save old values for dynamic reordering */
1262    if (dyn == TRUE) {
1263      dynStatus = bdd_reordering_status(ddManager, &oldDynMethod);
1264      bdd_dynamic_reordering(ddManager, dynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
1265    }
1266
1267    /* find total time elapsed */
1268    directVerifyTime = util_cpu_time();
1269
1270    /* find number of outputs to be directly verified */
1271    numOutputs = st_count(directVerifyMatch);
1272
1273    /*
1274     * Order primary input variables in the network to build the BDDs for
1275     * outputs to be directly verified.
1276     */
1277    if (Ord_NetworkTestAreVariablesOrdered(specNetwork,
1278                                           Ord_InputAndLatch_c) == FALSE) {
1279      /* order the variables in the network since not done */
1280      startTime = util_cpu_time();
1281      Ord_NetworkOrderVariables(specNetwork, Ord_RootsByDefault_c,
1282                      Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
1283                      Ord_Unassigned_c, dummy, 0);
1284
1285      endTime = util_cpu_time();
1286      lapTimeSpec += endTime - startTime;
1287
1288      startTime = endTime;
1289      Ord_NetworkOrderVariables(implNetwork, Ord_RootsByDefault_c,
1290                      Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
1291                      Ord_Unassigned_c, dummy, 0);
1292      lapTimeImpl += endTime - startTime;
1293
1294    } else {
1295      /* if order is not specified, assume the same order for spec.
1296       * and implementation
1297       */
1298      Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
1299        assert(Ntk_NodeReadMddId(nodePtr) != NTK_UNASSIGNED_MDD_ID);
1300        st_lookup(inputMatch, (char *)nodePtr, &implNodePtr);
1301        Ntk_NodeSetMddId(implNodePtr, Ntk_NodeReadMddId(nodePtr));
1302      }
1303    }
1304
1305    if (verbose >= 5) {
1306      Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
1307        specMddId = Ntk_NodeReadMddId(nodePtr);
1308        if (specMddId != NTK_UNASSIGNED_MDD_ID) {
1309          fprintf(vis_stdout, "%s ", Ntk_NodeReadName(nodePtr));
1310        }
1311      }
1312      fprintf(vis_stdout, "\n");
1313      Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
1314        specMddId = Ntk_NodeReadMddId(nodePtr);
1315        if (specMddId != NTK_UNASSIGNED_MDD_ID) {
1316          fprintf(vis_stdout, "%d ", specMddId);
1317        }
1318      }
1319      fprintf(vis_stdout, "\n");
1320    }
1321
1322    /* build arrays of corresponding nodes to be directly verified */
1323    specArray = ALLOC(Ntk_Node_t *, numOutputs);
1324    implArray = ALLOC(Ntk_Node_t *, numOutputs);
1325    index = 0;
1326    /* Order array starting from the LSB, so direct verification is performed
1327     * starting from the inputs.
1328     */
1329    for (i = 0; i < array_n(outputOrderArray); i++) {
1330      name = array_fetch(char *, outputOrderArray, array_n(outputOrderArray)-1-i);
1331      nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
1332      /* find node in direct verify match table */
1333      if (st_lookup(directVerifyMatch, (char *)nodePtr, (char **)&value)) {
1334        specArray[index] = (Ntk_Node_t *)nodePtr;
1335        implArray[index] = (Ntk_Node_t *)value;
1336        index++;
1337      }
1338    }
1339    /* number of outputs in the arrays should be as many entries as the match
1340     * table.
1341     */
1342    assert(numOutputs == index);
1343
1344    /* Create a permutation array for the specMddId and implMddId input nodes */
1345    permut = ALLOC(int, bdd_num_vars(ddManager));
1346    for (i= 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
1347      permut[i] = i;
1348    }
1349    st_foreach_item(inputMatch, stGen, &key, &value) {
1350      nodePtr = (Ntk_Node_t *)key;
1351      implNodePtr = (Ntk_Node_t *)value;
1352      if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))){
1353        error_append("Input match values do not return");
1354        error_append("valid node pointers.\n");
1355        /* Clean up */
1356        FREE(permut);
1357        FREE(specArray);
1358        FREE(implArray);
1359        st_free_gen(stGen);
1360        return 1;
1361      }
1362      /* create the array with the impl. vars to be composed with spec. vars. */
1363      specMddId = Ntk_NodeReadMddId(nodePtr);
1364      implMddId = Ntk_NodeReadMddId(implNodePtr);
1365      /* there should be no node with NTK_UNASSIGNED_MDD_ID due to the
1366       * ordering above
1367       */
1368      assert(specMddId != NTK_UNASSIGNED_MDD_ID);
1369      assert(implMddId != NTK_UNASSIGNED_MDD_ID);
1370      permut[implMddId] = specMddId;
1371
1372    } /* end of input match */
1373
1374    /*
1375     * Build BDDs for each output to be directly verified and check
1376     * for identical BDDs in spec. and impl.
1377     */
1378    for (i = 0; i < numOutputs; i++) {
1379      /* build the spec BDD */
1380      startTime = util_cpu_time();
1381      specBDD = BuildBDDforNode(specNetwork, specArray[i], PRIMARY_INPUTS);
1382      if (specBDD == NIL(bdd_node)) {
1383        error_append("Unable to build spec. BDD for the direct verification output");
1384        error_append(Ntk_NodeReadName(specArray[i]));
1385        error_append(".\n");
1386        /* Clean up */
1387        FREE(permut);
1388        FREE(specArray);
1389        FREE(implArray);
1390        return 1; /* error status */
1391      } /* end of if spec BDD is NIL */
1392      endTime = util_cpu_time();
1393      lapTimeSpec += endTime - startTime;
1394
1395      /* build the impl BDD */
1396      startTime = endTime;
1397      implBDD = BuildBDDforNode(implNetwork, implArray[i], PRIMARY_INPUTS);
1398      if (implBDD == NIL(bdd_node)) {
1399        error_append("Unable to build spec. BDD for the direct verification output");
1400        error_append(Ntk_NodeReadName(implArray[i]));
1401        error_append(".\n");
1402        /* Clean up */
1403        bdd_recursive_deref(ddManager, specBDD);
1404        FREE(permut);
1405        FREE(specArray);
1406        FREE(implArray);
1407        return 1; /* error status */
1408      } /* end of if spec BDD is NIL */
1409      endTime = util_cpu_time();
1410      lapTimeImpl += endTime - startTime;
1411
1412      /* call bdd permute to compose the impl variables with the spec
1413       * variables.
1414       */
1415      startTime = endTime;
1416      bdd_ref(permutedBDD = bdd_bdd_permute(ddManager, implBDD, permut));
1417      bdd_recursive_deref(ddManager, implBDD);
1418      endTime = util_cpu_time();
1419      lapTimeSpec += (endTime - startTime)/2;
1420      lapTimeImpl += (endTime - startTime)/2;
1421      implBDD = permutedBDD;
1422      if (implBDD == NIL(bdd_node)) {
1423        error_append("Permuting the impl bdd in terms of spec bdd vars failed\n");
1424        /* Clean up */
1425        bdd_recursive_deref(ddManager, specBDD);
1426        FREE(permut);
1427        FREE(specArray);
1428        FREE(implArray);
1429        return 1; /* error status */
1430      }
1431
1432      /* compare the bdds */
1433      if(specBDD != implBDD)  {
1434        /* error since spec and impl are not the same */
1435        /* update result structure */
1436        if (verbose >= 2) {
1437          (void)fprintf(vis_stdout, "Vector where the two networks differ :\n");
1438          (void)fprintf(vis_stdout, "Specification Input Names :\n");
1439          ExtractACubeOfDifference(ddManager, specNetwork, specBDD, implBDD);
1440        }
1441        resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
1442                                          RES_NETWORK_APPL_KEY);
1443        resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
1444                                          RES_NETWORK_APPL_KEY);
1445        ResResidueInfoSetDirectVerificationSuccess(resultSpec, RES_FAIL);
1446        ResResidueInfoSetDirectVerificationSuccess(resultImpl, RES_FAIL);
1447        (void) fprintf(vis_stdout, "%.2f (secs) spent in failed direct verification.\n",
1448                       (util_cpu_time() - directVerifyTime)/1000.0);
1449        fprintf(vis_stdout, "Residue Direct Verification failed at output node ");
1450        fprintf(vis_stdout, "%s", Ntk_NodeReadName(specArray[i]));
1451        fprintf(vis_stdout, " of the spec.\n");
1452        fprintf(vis_stdout, "Spec. did not match Impl.\n");
1453        /* Clean up */
1454        /* free the bdds just created */
1455        bdd_recursive_deref(ddManager, specBDD);
1456        bdd_recursive_deref(ddManager, implBDD);
1457        FREE(permut);
1458        FREE(specArray);
1459        FREE(implArray);
1460        return 0;
1461      } /* end if spec BDD != impl BDD */
1462
1463      /* if the bdds are equal, print some information */
1464      if (verbose >= 2) {
1465        fprintf(vis_stdout, "%d out of %d ", i + 1 ,numOutputs);
1466        fprintf(vis_stdout, "direct verification outputs done.\n");
1467      }
1468      if (verbose >= 3) {
1469        fprintf(vis_stdout, "%s(spec)/%s(impl) output verified. \n",
1470                Ntk_NodeReadName(specArray[i]), Ntk_NodeReadName(implArray[i]));
1471        bdd_ref(specBDD);
1472        fnMddT = bdd_construct_bdd_t(ddManager, specBDD);
1473        specSize = bdd_size(fnMddT);
1474        bdd_free(fnMddT);
1475        bdd_ref(implBDD);
1476        fnMddT = bdd_construct_bdd_t(ddManager, implBDD);
1477        implSize = bdd_size(fnMddT);
1478        bdd_free(fnMddT);
1479        fprintf(vis_stdout, "Size of %s(spec) = %d, Size of %s(impl) = %d\n",
1480         Ntk_NodeReadName(specArray[i]) ,specSize, Ntk_NodeReadName(implArray[i]), implSize);
1481        fprintf(vis_stdout, "%.3f spec time elapsed, %.3f impl. time elapsed.\n", lapTimeSpec/1000.0,
1482                lapTimeImpl/1000.0);
1483      }
1484      /* free the bdds just created */
1485      bdd_recursive_deref(ddManager, specBDD);
1486      bdd_recursive_deref(ddManager, implBDD);
1487
1488    } /* end of for-loop that iterates through the nodes to be directly
1489       * verified.
1490       */
1491
1492    FREE(permut);
1493    FREE(specArray);
1494    FREE(implArray);
1495
1496    /* set direct verification success info */
1497    /* update result structure */
1498    resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
1499                                                        RES_NETWORK_APPL_KEY);
1500    resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
1501                                                        RES_NETWORK_APPL_KEY);
1502    ResResidueInfoSetDirectVerificationSuccess(resultSpec, RES_PASS);
1503    ResResidueInfoSetCpuDirectVerif(resultSpec, (float) lapTimeSpec);
1504    ResResidueInfoSetDirectVerificationSuccess(resultImpl, RES_PASS);
1505    ResResidueInfoSetCpuDirectVerif(resultImpl, (float) lapTimeImpl);
1506
1507    /* Print success message */
1508    fprintf(vis_stdout, "Residue Direct Verification successful.\n");
1509
1510    /* Print Time taken for direct verification */
1511    if (verbose >= 1) {
1512      (void) fprintf(vis_stdout, "%.2f (secs) spent in Direct verification.\n",
1513                       (util_cpu_time() - directVerifyTime)/1000.0);
1514    }
1515
1516    /* Print which outputs were directly verified and time spent for
1517     * the spec and the impl
1518     */
1519    if (verbose >= 2) {
1520      fprintf(vis_stdout, "Time taken to build spec. BDD = %.3f\n",
1521              ResResidueInfoReadCpuDirectVerif(resultSpec)/1000.0);
1522      fprintf(vis_stdout, "Time taken to build impl. BDD = %.3f\n",
1523              ResResidueInfoReadCpuDirectVerif(resultImpl)/1000.0);
1524      st_foreach_item(directVerifyMatch, stGen, &key, &value) {
1525        fprintf(vis_stdout, "%s ", Ntk_NodeReadName((Ntk_Node_t *)key));
1526      }
1527      fprintf(vis_stdout, "verified successfully.\n");
1528    }
1529
1530    /* Print order of variables of this verification */
1531    if (verbose >= 3) {
1532      Ord_NetworkPrintVariableOrder(vis_stdout, specNetwork,
1533      Ord_InputAndLatch_c);
1534      Ord_NetworkPrintVariableOrder(vis_stdout, implNetwork,
1535      Ord_InputAndLatch_c);
1536    }
1537
1538    /* restore the old values for dynamic reordering */
1539    if(dyn == TRUE) {
1540      bdd_dynamic_reordering(ddManager, oldDynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
1541      if (!dynStatus) {
1542        bdd_dynamic_reordering_disable(ddManager);
1543      }
1544    }
1545
1546    return 0; /* direct verification success */
1547} /* End of Direct Verification */
1548
1549
1550/**Function********************************************************************
1551
1552  Synopsis [Decode the option of reordering.]
1553
1554  Description [Decode the option of reordering. Returns the dynMethod value.]
1555
1556  SideEffects   []
1557
1558******************************************************************************/
1559static bdd_reorder_type_t
1560DecodeDynMethod(char *dynMethodString)
1561{
1562  bdd_reorder_type_t dynMethod;
1563
1564  /* Translate reordering string to specifying method */
1565  if (dynMethodString == NIL(char)) {
1566    dynMethod = BDD_REORDER_SIFT;
1567  } else if (strcmp(dynMethodString, "same") == 0) {
1568    dynMethod = BDD_REORDER_SAME;
1569  } else if (strcmp(dynMethodString, "none") == 0) {
1570    dynMethod = BDD_REORDER_NONE;
1571  } else if (strcmp(dynMethodString, "random") == 0) {
1572    dynMethod = BDD_REORDER_RANDOM;
1573  } else if (strcmp(dynMethodString, "randompivot") == 0) {
1574    dynMethod = BDD_REORDER_RANDOM_PIVOT;
1575  } else if (strcmp(dynMethodString, "sift") == 0) {
1576    dynMethod = BDD_REORDER_SIFT;
1577  } else if (strcmp(dynMethodString, "siftconverge") == 0) {
1578    dynMethod = BDD_REORDER_SIFT_CONVERGE;
1579  } else if (strcmp(dynMethodString, "symmsift") == 0) {
1580    dynMethod = BDD_REORDER_SYMM_SIFT;
1581  } else if (strcmp(dynMethodString, "symmsiftconverge") == 0) {
1582    dynMethod = BDD_REORDER_SYMM_SIFT_CONV;
1583  } else if (strcmp(dynMethodString, "window2") == 0) {
1584    dynMethod = BDD_REORDER_WINDOW2;
1585  } else if (strcmp(dynMethodString, "window3") == 0) {
1586    dynMethod = BDD_REORDER_WINDOW3;
1587  } else if (strcmp(dynMethodString, "window4") == 0) {
1588    dynMethod = BDD_REORDER_WINDOW4;
1589  } else if (strcmp(dynMethodString, "window2converge") == 0) {
1590    dynMethod = BDD_REORDER_WINDOW2_CONV;
1591  } else if (strcmp(dynMethodString, "window3converge") == 0) {
1592    dynMethod = BDD_REORDER_WINDOW3_CONV;
1593  } else if (strcmp(dynMethodString, "window4converge") == 0) {
1594    dynMethod = BDD_REORDER_WINDOW4_CONV;
1595  } else if (strcmp(dynMethodString, "groupsift") == 0) {
1596    dynMethod = BDD_REORDER_GROUP_SIFT;
1597  } else if (strcmp(dynMethodString, "groupsiftconverge") == 0) {
1598    dynMethod = BDD_REORDER_GROUP_SIFT_CONV;
1599  } else if (strcmp(dynMethodString, "anneal") == 0) {
1600    dynMethod = BDD_REORDER_ANNEALING;
1601  } else if (strcmp(dynMethodString, "genetic") == 0) {
1602    dynMethod = BDD_REORDER_GENETIC;
1603  } else if (strcmp(dynMethodString, "linear") == 0) {
1604    dynMethod = BDD_REORDER_LINEAR;
1605  } else if (strcmp(dynMethodString, "linearconverge") == 0) {
1606    dynMethod = BDD_REORDER_LINEAR_CONVERGE;
1607  } else if (strcmp(dynMethodString, "exact") == 0) {
1608    dynMethod = BDD_REORDER_EXACT;
1609  } else {
1610    dynMethod = BDD_REORDER_SIFT;
1611  }
1612  return dynMethod;
1613} /* End of DecodeDynMethod */
1614
1615
1616
1617/**Function********************************************************************
1618
1619  Synopsis  [Main Function to perform residue verification.]
1620
1621  Description [Main Function to perform residue verification.  The network
1622  parameters are in a specific order: SPECIFICATION first, IMPLEMENTATION
1623  second.  All other parameters store values of the specification. The
1624  procedure first turns off dynamic reordering unless specified otherwise. The
1625  array of required primes are computed and the cudd manager is
1626  initialized. The main loop iterates over the primes. The residue ADD is
1627  constructed for as many variables as POs with respect to each prime.  Then
1628  calls a procedure which composes the networks (in layers) into the residue
1629  ADD. The final ADD is compared for both the spec and the impl.  A sub-routine
1630  composes the network into the residue ADD depending on the composition
1631  method.  The final ADDs for the specification and the implementation are
1632  checked against each other. The procedure returns 0 if it were unable to
1633  complete for some reason, like memory failure, incomplete networks, etc.  The
1634  procedure returns 0 if successful in building the BDDs of the two
1635  circuits. The parameters to this procedure are spec. network, impl. network,
1636  output pointer match table, input pointer match table, number of directly
1637  verified outputs, layer structure of the spec. and the impl. and an array of
1638  nodes with outputs for residue verification.]
1639
1640  SideEffects   []
1641
1642******************************************************************************/
1643static int
1644ResidueVerification(Ntk_Network_t *specNetwork,
1645                    Ntk_Network_t *implNetwork,
1646                    st_table *outputMatch,
1647                    st_table *inputMatch,
1648                    int numDirectVerify,
1649                    array_t *specLayerArray,
1650                    array_t *implLayerArray,
1651                    array_t *outputArray)
1652{
1653  int numOutputs;                 /* number of outputs in the networks */
1654  int actualOutputs;                 /* number of outputs in the networks */
1655  int msbId;                      /* stores the top Id available */
1656  int msbLsb;                     /* 1 means Msb on top */
1657
1658  Ntk_Node_t *nodePtr, *implNodePtr; /* variables to store nodes in networks */
1659
1660  Res_ResidueInfo_t *resultSpec;   /* spec. result structure */
1661  Res_ResidueInfo_t *resultImpl;   /* impl. result structure */
1662
1663  int verbose;                     /* verbosity value */
1664  char *flagValue;                 /* string to store flag values */
1665  int i;                           /* iterating index */
1666
1667  lsGen listGen;                   /* list generator for looping over nodes
1668                                    * in a network.
1669                                    */
1670  st_generator *stGen;     /* generator to step through st_table */
1671  char *key, *value;               /* variables to read in st-table values */
1672  long overallLap;      /* to measure elapsed time */
1673  long lap;     /* to measure elapsed time */
1674  int primeIndex;       /* index to iterate over prime array */
1675  bdd_manager *ddManager;      /* Manager read from the network */
1676  bdd_node *implADD, *specADD, *tmpDd; /* final ADDs after composition */
1677  int specSize, implSize;               /* sizes of bdds */
1678  int specMddId, implMddId;  /* id variables for nodes */
1679  bdd_node *residueDd;  /* residue ADD (n x m) */
1680  int *permut;  /* array to permute impl ADD variables to spec.
1681                                 * ADD variables.
1682                                 */
1683  int numOfPrimes;      /* Number of primes needed for verification */
1684  int *primeTable;      /* array to store primes needed for current
1685                                 * verification
1686                                 */
1687  bdd_reorder_type_t oldDynMethod, dynMethod; /* dynamic reordering
1688                                               * methods
1689                                               */
1690  int dynStatus;                /* Status of manager w.r.t. original
1691                                 * reordering
1692                                 */
1693  boolean dyn;          /* flag to indicate dynamic reordering
1694                                 * is turned on.
1695                                 */
1696  mdd_t *fnMddT;                /* mdd_t structure to calculate sizes */
1697  int unassignedValue;          /* NTK_UNASSIGNED_MDD_ID value holder */
1698  array_t *implOutputArray;     /* array of output nodes of the impl.in consideration
1699                                 * for composition
1700                                 */
1701
1702  /* Initialization */
1703  verbose = 0;
1704  unassignedValue =  NTK_UNASSIGNED_MDD_ID;
1705  numOfPrimes = 0;
1706  msbLsb = 1; /* default value msb is on top */
1707  primeTable = NULL;
1708  overallLap = util_cpu_time();
1709  dyn = FALSE; /* default dynamic reordering disabled */
1710  permut = NULL;
1711
1712  /* specify if the top var of the residue ADD is the MSB/LSB */
1713  flagValue = Cmd_FlagReadByName("residue_top_var");
1714  if (flagValue != NIL(char) && strcmp(flagValue,"lsb") == 0) {
1715    msbLsb = 0;
1716  } else {
1717    msbLsb = 1;
1718  }
1719
1720  /* initialize number of outputs */
1721  actualOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
1722
1723  /* Read the mdd Manager (or create it if necessary) */
1724  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
1725    /* save old dynamic reordering values */
1726  dynStatus = bdd_reordering_status(ddManager, &oldDynMethod);
1727
1728  /* read verbosity value */
1729  flagValue = Cmd_FlagReadByName("residue_verbosity");
1730  if (flagValue != NIL(char)) {
1731    verbose = atoi(flagValue);
1732  }
1733
1734  /* read if dynamic ordering is required */
1735  flagValue = Cmd_FlagReadByName("residue_autodyn_residue_verif");
1736  if (flagValue != NIL(char)) {
1737    dyn = (strcmp(flagValue,"1")==0) ? TRUE : FALSE;
1738  }
1739  /* read method of dynamic reordering */
1740  if (dyn == TRUE) {
1741    flagValue = Cmd_FlagReadByName("residue_residue_dyn_method");
1742    if ( flagValue != NULL) {
1743      dynMethod = DecodeDynMethod(flagValue);
1744    } else {
1745      dynMethod = BDD_REORDER_SAME;
1746    }
1747    /* update manager with dynamic reordering and the method */
1748    bdd_dynamic_reordering(ddManager, dynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
1749  } else {
1750    /* unless specified, TURN REORDERING OFF for residue verification */
1751    bdd_dynamic_reordering_disable(ddManager);
1752  }
1753
1754  /*
1755   * Choose the set of primes that will be used, primeTable is allocated
1756   * here.
1757   */
1758  numOfPrimes = ChoosePrimes(actualOutputs,  &primeTable, numDirectVerify);
1759
1760  /* get result structures */
1761  resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
1762                                                    RES_NETWORK_APPL_KEY);
1763  resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
1764                                                    RES_NETWORK_APPL_KEY);
1765
1766  /* update result with primes info */
1767  if ((resultSpec  != NIL(Res_ResidueInfo_t)) && (resultImpl != NIL(Res_ResidueInfo_t))) {
1768    ResResidueInfoAllocatePrimeInfoArray(resultSpec, numOfPrimes, primeTable);
1769    ResResidueInfoAllocatePrimeInfoArray(resultImpl, numOfPrimes, primeTable);
1770    ResResidueInfoSetNumOfPrimes(resultSpec, numOfPrimes);
1771    ResResidueInfoSetNumOfPrimes(resultImpl, numOfPrimes);
1772  } else {
1773    /* error - the result structure should be there */
1774    error_append("Result structures are missing\n");
1775    FREE(primeTable);
1776    return 1;
1777  }
1778
1779  /* Print the list of primes depending on the verbosity level*/
1780  if (verbose >= 0) {
1781    (void) fprintf(vis_stdout, "List of Primes used: ");
1782    for(i=0; i<numOfPrimes; i++) {
1783      (void) fprintf(vis_stdout, "%d ", primeTable[i]);
1784    }
1785    (void) fprintf(vis_stdout, "\n");
1786  } /* End of if */
1787
1788  /* form impl Output Array */
1789  implOutputArray = array_alloc(Ntk_Node_t *, array_n(outputArray));
1790  arrayForEachItem(Ntk_Node_t *, outputArray, i, nodePtr) {
1791    st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
1792    array_insert(Ntk_Node_t *, implOutputArray, i, implNodePtr);
1793  }
1794
1795  /* number of outputs in consideration */
1796  numOutputs = array_n(outputArray);
1797
1798
1799  /* Main Loop in which the verification is done for each prime. */
1800  for(primeIndex = 0; primeIndex < numOfPrimes; primeIndex++) {
1801    int currentPrime;
1802
1803    /* Read current prime from table */
1804    currentPrime = primeTable[primeIndex];
1805    if (verbose >=2)
1806      (void) fprintf(vis_stdout, "Processing prime %d:\n", currentPrime);
1807
1808    /* update the mdd manager with the first set of output variables */
1809    MddCreateVariables((mdd_manager *)ddManager, numOutputs-bdd_num_vars(ddManager));
1810
1811
1812    /* Obtain the residue bdd for the given prime, assume top id is
1813     * always 0i.e. msbId = 0;
1814     */
1815    msbId = 0;
1816    bdd_ref(residueDd = bdd_add_residue(ddManager, numOutputs, currentPrime,
1817                                         msbLsb, msbId));
1818
1819    /*  Set the output Id. Needs to be set each time because it gets
1820     * cleared each time.
1821     */
1822    arrayForEachItem(Ntk_Node_t *, outputArray, i , nodePtr) {
1823      st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
1824      if (msbLsb == 1) {
1825        Ntk_NodeSetMddId(nodePtr, i);
1826        Ntk_NodeSetMddId(implNodePtr, i);
1827      } else {
1828        Ntk_NodeSetMddId(nodePtr, numOutputs - i);
1829        Ntk_NodeSetMddId(implNodePtr, numOutputs - i);
1830      }
1831    }
1832
1833
1834    /* Set the cpu usage lap */
1835    lap = util_cpu_time();
1836
1837    if (verbose >= 1) {
1838      fprintf(vis_stdout, "Specification being built\n");
1839    }
1840    /* the actual composition of the spec. network into the residue ADD
1841     * is done here. The composed ADD return is referenced
1842     */
1843    specADD = ComposeLayersIntoResidue(specNetwork, specLayerArray, residueDd, outputArray);
1844    if (specADD == NIL(bdd_node)) {
1845      error_append("Composition of spec. failed.\n");
1846      /* Clean up before you leave */
1847      array_free(implOutputArray);
1848      FREE(primeTable);
1849      bdd_recursive_deref(ddManager, residueDd);
1850      return 1; /* error return */
1851    }
1852
1853    /* Store the information in the result structure of the spec.*/
1854    bdd_ref(specADD);
1855    fnMddT = bdd_construct_bdd_t(ddManager, specADD);
1856    specSize = bdd_size(fnMddT);
1857    bdd_free(fnMddT);
1858    ResResidueInfoSetPerPrimeInfo(resultSpec, primeIndex, currentPrime,
1859                                  (util_cpu_time() - lap)/1000.0, specSize, specADD);
1860    /* Print info regarding this prime if pertinent */
1861    if (verbose >=3) {
1862      (void) fprintf(vis_stdout, "%.2f (secs) spent in composing prime\n",
1863                     ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->cpuTime);
1864      (void) fprintf(vis_stdout, "Composed Dd with %d nodes\n", specSize);
1865    }
1866
1867    /* Set the cpu usage lap */
1868    lap = util_cpu_time();
1869
1870    /*
1871     * the actual composition of the impl. network into the residue ADD
1872     * is done here. The composed ADD return is referenced
1873     */
1874    if (verbose >= 1) {
1875      fprintf(vis_stdout, "Implementation being built\n");
1876    }
1877    implADD = ComposeLayersIntoResidue(implNetwork, implLayerArray, residueDd, implOutputArray);
1878
1879    bdd_recursive_deref(ddManager, residueDd);
1880    if (implADD == NIL(bdd_node)) {
1881      error_append("Composition of spec. failed.\n");
1882      /* Clean up before you leave */
1883      bdd_recursive_deref(ddManager, specADD);
1884      array_free(implOutputArray);
1885      FREE(primeTable);
1886      return 1; /* error return */
1887    }
1888
1889    /* Create a permutation array for the specMddId and implMddId input nodes */
1890    permut = ALLOC(int, bdd_num_vars(ddManager));
1891    for (i= 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
1892      permut[i] = i;
1893    }
1894    st_foreach_item(inputMatch, stGen, &key, &value) {
1895      nodePtr = (Ntk_Node_t *)key;
1896      implNodePtr = (Ntk_Node_t *)value;
1897      if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))){
1898        error_append("Input match values do not return");
1899        error_append("valid node pointers.\n");
1900        /* Clean up */
1901        FREE(permut);
1902        FREE(primeTable);
1903        array_free(implOutputArray);
1904        bdd_recursive_deref(ddManager, specADD);
1905        bdd_recursive_deref(ddManager, implADD);
1906        st_free_gen(stGen);
1907        return 1;
1908      }
1909      /* create the array with the impl. vars to be composed with spec. vars. */
1910      specMddId = Ntk_NodeReadMddId(nodePtr);
1911      implMddId = Ntk_NodeReadMddId(implNodePtr);
1912
1913      /* there should be no node with NTK_UNASSIGNED_MDD_ID due to the
1914       * ordering above
1915       */
1916
1917#if 0
1918      if (Ntk_NodeReadNumFanouts(nodePtr) != 0) {
1919        assert(specMddId != NTK_UNASSIGNED_MDD_ID);
1920      }
1921      if (Ntk_NodeReadNumFanouts(implNodePtr) != 0) {
1922        assert(implMddId != NTK_UNASSIGNED_MDD_ID);
1923      }
1924#endif
1925
1926      if ((specMddId != NTK_UNASSIGNED_MDD_ID) &&
1927          (implMddId != NTK_UNASSIGNED_MDD_ID)) {
1928        permut[implMddId] = specMddId;
1929      } else {
1930        assert(specMddId == implMddId);
1931      }
1932
1933    } /* end of st_foreach_item */
1934
1935    /* permute the variables so that the impl variables are replaced by
1936     * spec. variables
1937     */
1938    bdd_ref(tmpDd = bdd_add_permute(ddManager, implADD, permut));
1939    bdd_recursive_deref(ddManager, implADD);
1940    FREE(permut);
1941    implADD = tmpDd;
1942    if(implADD == NIL(bdd_node)) { /* error */
1943      error_append("Last composition failed,");
1944      error_append("Cannot compose spec. ADD PI vars into Impl. ADD.\n");
1945      FREE(primeTable);
1946      array_free(implOutputArray);
1947      return 1; /* error return */
1948    }
1949
1950    if (verbose > 0) {
1951      (void) fprintf(vis_stdout, "%.2f (secs) spent in residue verification.\n",
1952                     (util_cpu_time() - overallLap)/1000.0);
1953    }
1954
1955    /* Store the information in the result structure of the impl.*/
1956    bdd_ref(implADD);
1957    fnMddT = bdd_construct_bdd_t(ddManager, implADD);
1958    implSize = bdd_size(fnMddT);
1959    bdd_free(fnMddT);
1960    ResResidueInfoSetPerPrimeInfo(resultImpl, primeIndex, currentPrime,
1961         (util_cpu_time() - lap)/1000.0, implSize, implADD);
1962    /* Print info regarding this prime if pertinent */
1963    if (verbose >=3) {
1964      (void) fprintf(vis_stdout, "%.2f (secs) spent in composing prime\n",
1965                     ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->cpuTime);
1966      (void) fprintf(vis_stdout, "Composed Dd with %d nodes\n", implSize);
1967    }
1968
1969
1970    /* Compare the Spec and the Impl composed Dds */
1971    if (ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd !=
1972        ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd) {
1973      ResResidueInfoSetSuccess(resultSpec, RES_FAIL);
1974      ResResidueInfoSetSuccess(resultImpl, RES_FAIL);
1975      (void) fprintf(vis_stdout, "Verification of %s and %s failed.\n",
1976                     Res_ResidueInfoReadName(resultSpec),
1977                     Res_ResidueInfoReadName(resultImpl));
1978      (void)fprintf(vis_stdout,"The composed ADDs with residue are not the same.\n");
1979      (void)fprintf(vis_stdout,"Verification failed at prime %d.\n", currentPrime);
1980      if (verbose >= 2) {
1981        (void)fprintf(vis_stdout, "Vector where the two networks differ :\n");
1982        (void)fprintf(vis_stdout, "Specification Input Names :\n");
1983        ExtractACubeOfDifference(ddManager, specNetwork, specADD, implADD);
1984      }
1985
1986      /* Clean up before you leave */
1987      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd);
1988      ResResidueInfoSetPerPrimeDd(resultSpec, primeIndex, NIL(bdd_node));
1989
1990      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd);
1991      ResResidueInfoSetPerPrimeDd(resultImpl, primeIndex, NIL(bdd_node));
1992      array_free(implOutputArray);
1993      FREE(primeTable);
1994      return 0;
1995    } else {
1996
1997      /* free the result Dd*/
1998      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd);
1999      ResResidueInfoSetPerPrimeDd(resultSpec, primeIndex, NIL(bdd_node));
2000
2001      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd);
2002      ResResidueInfoSetPerPrimeDd(resultImpl, primeIndex, NIL(bdd_node));
2003    }
2004
2005
2006    /* reset node Ids of primary inputs */
2007    Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
2008      Ntk_NodeSetMddId(nodePtr, unassignedValue);
2009    }
2010    Ntk_NetworkForEachCombInput(implNetwork, listGen, nodePtr) {
2011      Ntk_NodeSetMddId(nodePtr, unassignedValue);
2012    }
2013
2014
2015  } /* End of the main for-loop */
2016  FREE(primeTable);
2017  array_free(implOutputArray);
2018
2019  /* restore old dynamic reordering values */
2020  bdd_dynamic_reordering(ddManager, oldDynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
2021  if (!dynStatus) {
2022    bdd_dynamic_reordering_disable(ddManager);
2023  }
2024
2025  /* set pass flag if residue verification success and direct verification
2026   * success.
2027   */
2028  if (((numDirectVerify) &&
2029       (ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_PASS)) ||
2030       (ResResidueInfoReadDirectVerificationSuccess(resultSpec) != RES_FAIL)) {
2031    ResResidueInfoSetSuccess(resultSpec, RES_PASS);
2032  }
2033  if (((numDirectVerify) &&
2034       (ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_PASS)) ||
2035      (ResResidueInfoReadDirectVerificationSuccess(resultImpl) != RES_FAIL)) {
2036    ResResidueInfoSetSuccess(resultImpl, RES_PASS);
2037  }
2038  return 0;
2039} /* End of ResidueVerification */
2040
2041/**Function********************************************************************
2042
2043  Synopsis [ Prints out a cube in the XOR of the 2 Bdds]
2044
2045  Description [ ]
2046  value]
2047
2048  SideEffects   [.]
2049
2050  SeeAlso            []
2051
2052******************************************************************************/
2053static void
2054ExtractACubeOfDifference(bdd_manager *mgr,
2055                         Ntk_Network_t *specNetwork,
2056                         bdd_node *fn1,
2057                         bdd_node *fn2)
2058{
2059  bdd_t *fnMddT, *fnMddT1;      /* mdd_t structure to calculate sizes */
2060  bdd_t *fnMddT2, *fnMddT3;     /* mdd_t structure to calculate sizes */
2061  bdd_gen *gen;
2062  array_t *cube, *namesArray;
2063  lsGen listGen;
2064  int i, literal;
2065  Ntk_Node_t *nodePtr;
2066
2067  /* make bdd_ts of the two functions */
2068  bdd_ref(fn2);
2069  fnMddT = bdd_construct_bdd_t(mgr, fn2);
2070  bdd_ref(fn1);
2071  fnMddT1 = bdd_construct_bdd_t(mgr, fn1);
2072  fnMddT2 = bdd_not(fnMddT1);
2073  /* extracts some cubes in the intersection of fn1' and fn2 */
2074  fnMddT3 = bdd_intersects(fnMddT, fnMddT2);
2075  /* check not zero */
2076  if (bdd_is_tautology(fnMddT3, 0)) {
2077    bdd_free(fnMddT3);
2078    bdd_free(fnMddT2);
2079    /* extracts some cubes in the intersection of fn2' and fn1 */
2080    fnMddT2 = bdd_not(fnMddT);
2081    fnMddT3 = bdd_intersects(fnMddT1, fnMddT2);
2082  }
2083  assert(!bdd_is_tautology(fnMddT3, 0));
2084  bdd_free(fnMddT);
2085  bdd_free(fnMddT1);
2086  bdd_free(fnMddT2);
2087
2088  /* pick a cube from the xor of fn1 and fn2 */
2089  gen = bdd_first_cube(fnMddT3, &cube);
2090  bdd_free(fnMddT3);
2091
2092  /* store the names to be printed out later */
2093  namesArray = array_alloc(char *, array_n(cube));
2094  Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
2095    array_insert(char *, namesArray , Ntk_NodeReadMddId(nodePtr),  Ntk_NodeReadName(nodePtr));
2096  }
2097
2098  /* print out the cube */
2099  arrayForEachItem(int, cube, i, literal) {
2100    if (literal != 2) {
2101      (void) fprintf(vis_stdout, "%s ", array_fetch(char *, namesArray, i));
2102    }
2103  }
2104  fprintf(vis_stdout, "\n");
2105  arrayForEachItem(int, cube, i, literal) {
2106    if (literal != 2) {
2107      (void) fprintf(vis_stdout, "%1d", literal);
2108    }
2109  }
2110  fprintf(vis_stdout, "\n");
2111  array_free(namesArray);
2112  bdd_gen_free(gen);
2113  return;
2114}
Note: See TracBrowser for help on using the repository browser.