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

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

vis2.3
File size: 12.5 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [resRes.c]
4
5  PackageName [res]
6
7  Synopsis    [Data manipulation routines of the Res_ResidueInfo structure.]
8
9  SeeAlso     [Res_ResidueInfo]
10
11  Author      [Kavita Ravi    <ravi@boulder.colorado.edu> and
12               Abelardo Pardo <abel@boulder.colorado.edu>]
13               
14  Copyright [This file was created at the University of Colorado at Boulder.
15  The University of Colorado at Boulder makes no warranty about the suitability
16  of this software for any purpose.  It is presented on an AS IS basis.]
17
18******************************************************************************/
19
20#include "resInt.h"
21
22static char rcsid[] UNUSED = "$Id: resRes.c,v 1.18 2002/08/26 05:53:31 fabio Exp $";
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Structure declarations                                                    */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43
44/*---------------------------------------------------------------------------*/
45/* Macro declarations                                                        */
46/*---------------------------------------------------------------------------*/
47
48
49/**AutomaticStart*************************************************************/
50
51/*---------------------------------------------------------------------------*/
52/* Static function prototypes                                                */
53/*---------------------------------------------------------------------------*/
54
55
56/**AutomaticEnd***************************************************************/
57
58
59/*---------------------------------------------------------------------------*/
60/* Definition of exported functions                                          */
61/*---------------------------------------------------------------------------*/
62
63/**Function********************************************************************
64
65  Synopsis [Frees the structure storing the information related to the
66  residual verification.]
67
68  SideEffects []
69
70  SeeAlso [Res_ResidualInfo]
71
72******************************************************************************/
73void
74Res_ResidueInfoFree(Res_ResidueInfo_t *residue)
75{
76  int i;
77  /* Deallocate the information in the primeInfoArray, if any */
78  if (residue->primeInfoArray != NIL(PerPrimeInfo_t)) {
79
80   
81    for (i = 0; i < residue->numOfPrimes; i++) {
82      if ((residue->primeInfoArray[i]).residueDd != NIL(bdd_node)) {
83        bdd_recursive_deref(residue->ddManager, (residue->primeInfoArray[i]).residueDd);
84      }
85    }
86    FREE(residue->primeInfoArray);
87  } /* End of if */
88
89  FREE(residue->networkName);
90  FREE(residue->networkNameVerifiedAgainst);
91  FREE(residue);
92  return;
93} /* End of Res_ResidueInfoFree */
94
95/**Function********************************************************************
96
97  Synopsis  [Call-back function to free the residue information.]
98
99  Description [A pointer to this function will be stored in the network
100  together with the pointer to the structure. Whenever the network needs to
101  deallocate the residue information this function is called.]
102
103  SideEffects  []
104
105  SeeAlso  [Ntk_NetworkAddApplInfo]
106
107******************************************************************************/
108void
109Res_ResidueInfoFreeCallback(void *data)
110{
111  Res_ResidueInfoFree((Res_ResidueInfo_t *) data);
112  ResResidueFreeVariableManager();
113} /* End of Res_ResidueInfoFreeCallback */
114
115/**Function********************************************************************
116
117  Synopsis           [Reads the residue information  attached to a network.]
118
119  SideEffects        []
120
121  SeeAlso            [CommandResVerify]
122
123******************************************************************************/
124Res_ResidueInfo_t *
125Res_NetworkReadResidueInfo(Ntk_Network_t *network)
126{
127  return (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, RES_NETWORK_APPL_KEY);
128} /* End of Res_NetworkReadResidueInfo */
129
130/**Function********************************************************************
131
132  Synopsis [External function to read the name field of Res_ResidueInfo.]
133
134  SideEffects        []
135
136  SeeAlso            [CommandResVerify]
137
138******************************************************************************/
139char *
140Res_ResidueInfoReadName(Res_ResidueInfo_t *residuePtr)
141{
142  return (char *)(ResResidueInfoReadNetworkName(residuePtr));
143} /* End of Res_ResidueInfoReadName */
144
145/**Function********************************************************************
146
147  Synopsis [External function to read the number of inputs in Res_ResidueInfo.]
148
149  SideEffects        []
150
151  SeeAlso            [CommandResVerify]
152 
153
154******************************************************************************/
155int
156Res_ResidueInfoReadNumInputs(Res_ResidueInfo_t *residuePtr)
157{
158  return ResResidueInfoReadNumInputs(residuePtr);
159} /* End of Res_ResidueInfoReadNumInputs */
160
161/**Function********************************************************************
162
163  Synopsis [External function to read the number of outputs in
164  Res_ResidueInfo.]
165
166  SideEffects        []
167
168  SeeAlso            [CommandResVerify]
169 
170******************************************************************************/
171int
172Res_ResidueInfoReadNumOutputs(Res_ResidueInfo_t *residuePtr)
173{
174  return ResResidueInfoReadNumOutputs(residuePtr);
175} /* End of Res_ResidueInfoReadNumOutputs */
176
177/**Function********************************************************************
178
179  Synopsis [External function to read the number of directly verified outputs in
180  Res_ResidueInfo.]
181
182  SideEffects        []
183
184  SeeAlso            [CommandResVerify]
185
186******************************************************************************/
187int
188Res_ResidueInfoReadNumDirectVerifiedOutputs(Res_ResidueInfo_t *residuePtr)
189{
190  return ResResidueInfoReadNumDirectVerifiedOutputs(residuePtr);
191} /* End of Res_ResidueInfoReadNumDirectVerifiedOutputs */
192
193/**Function********************************************************************
194
195  Synopsis [External function to read the cpu seconds spent in directly
196  verifying outputs in Res_ResidueInfo.]
197
198  SideEffects        []
199
200  SeeAlso            [CommandResVerify]
201
202******************************************************************************/
203int
204Res_ResidueInfoReadCpuDirectVerif(Res_ResidueInfo_t *residuePtr)
205{
206  return (int) ResResidueInfoReadCpuDirectVerif(residuePtr);
207} /* End of Res_ResidueInfoReadCpuDirectVerif */
208
209/**Function********************************************************************
210
211  Synopsis [External function to read the number of primes in Res_ResidueInfo.]
212
213  SideEffects        []
214
215  SeeAlso            [CommandResVerify]
216
217******************************************************************************/
218int
219Res_ResidueInfoReadNumOfPrimes(Res_ResidueInfo_t *residuePtr)
220{
221  return ResResidueInfoReadNumOfPrimes(residuePtr);
222} /* End of Res_ResidueInfoReadNumOfPrimes */
223
224/**Function********************************************************************
225
226  Synopsis [External function to read the success field in Res_ResidueInfo.]
227
228  SideEffects        []
229
230  SeeAlso            [CommandResVerify]
231
232******************************************************************************/
233int
234Res_ResidueInfoReadSuccess(Res_ResidueInfo_t *residuePtr)
235{
236  return ResResidueInfoReadSuccess(residuePtr);
237} /* End of Res_ResidueInfoReadNumOfPrimes */
238
239/*---------------------------------------------------------------------------*/
240/* Definition of internal functions                                          */
241/*---------------------------------------------------------------------------*/
242
243/**Function********************************************************************
244
245  Synopsis           [Wrapper procedure to create a result data structure.]
246
247  SideEffects        []
248
249******************************************************************************/
250Res_ResidueInfo_t *
251ResNetworkResidueInfoReadOrCreate(Ntk_Network_t *network)
252{
253  Res_ResidueInfo_t *result;
254
255  assert(network != NIL(Ntk_Network_t));
256
257  result = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network,
258                                                        RES_NETWORK_APPL_KEY);
259  if (result == NIL(Res_ResidueInfo_t)) {
260    result = ResResidueInfoAllocate(Ntk_NetworkReadName(network));
261    result->ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
262  } /* End of if */
263
264  return result;
265} /* End of ResNetworkResidueInfoReadOrCreate*/
266
267
268/**Function********************************************************************
269
270  Synopsis           [Function that allocates the Res_ResidueInfo_t.]
271
272  Description [Only the name field is initialized. The field primeInfoArray it
273  is initialized to NIL. In a later phase, that field may be initialized with
274  the array of the correct size by means of Res_ResidueAllocatePrimeInfo.]
275
276  SideEffects        []
277
278  SeeAlso            [ResResidueAllocatePrimeInfo]
279
280******************************************************************************/
281Res_ResidueInfo_t *
282ResResidueInfoAllocate(char *name)
283{
284  Res_ResidueInfo_t *result = ALLOC(Res_ResidueInfo_t, 1);
285
286  result->networkName = util_strsav(name);
287  result->networkNameVerifiedAgainst = NULL;
288  result->numInputs = 0;
289  result->numOutputs = 0;
290  result->numDirectVerifiedOutputs = 0;
291  result->cpuDirectVerif = 0.0;
292  result->numOfPrimes = 0;
293  result->primeInfoArray = NIL(PerPrimeInfo_t);
294  result->success = RES_NOT_VERIFIED;
295  result->successDirectVerification = RES_NOT_VERIFIED;
296  result->ddManager = NIL(bdd_manager);
297  return result;
298} /* End of ResResidueInfoAllocate */
299
300/**Function********************************************************************
301
302  Synopsis [Allocates the array primeInfoArray inside the Res_ResidueInfo_t.]
303
304  SideEffects  []
305
306  SeeAlso  [Res_ResidueAllocate]
307
308******************************************************************************/
309void
310ResResidueInfoAllocatePrimeInfoArray(Res_ResidueInfo_t *residueInfo,
311                                     int numOfPrimes,
312                                     int *tableOfPrimes)
313{
314  int i;
315
316  residueInfo->primeInfoArray = ALLOC(PerPrimeInfo_t, numOfPrimes);
317
318  for (i = 0; i < numOfPrimes; i++) {
319    ResResidueInfoSetPerPrimeInfo(residueInfo, i, tableOfPrimes[i], 0, 0, 
320                                  NIL(bdd_node));
321  }
322
323  return;
324} /* End of ResResidualAllocatePrimeInfoArray */
325
326/**Function********************************************************************
327
328  Synopsis [Prints the residue and primeInfoArray information.]
329
330  SideEffects  []
331
332  SeeAlso  [Res_ResidueAllocate]
333
334******************************************************************************/
335void
336Res_ResidueInfoPrint(Res_ResidueInfo_t *result)
337{
338
339  int i;
340
341  if (result->success) { 
342    fprintf(vis_stdout, "The circuit %s was successfully verified against %s.\n", 
343            (char *)result->networkName, (char *)result->networkNameVerifiedAgainst);
344    fprintf(vis_stdout, "The circuit has %d inputs and %d outputs ", result->numInputs,
345           result->numOutputs);
346    fprintf(vis_stdout, "of which %d were directly verified.\n", 
347                                           result->numDirectVerifiedOutputs);
348   
349    if (result->numDirectVerifiedOutputs) {
350      fprintf(vis_stdout, "Direct verification took %.3f seconds\n", 
351                                                 result->cpuDirectVerif/1000.0);
352    }
353   
354    if (result->numOfPrimes) {
355      fprintf(vis_stdout, "In residue verification using %d primes, \n", 
356                                             result->numOfPrimes);
357      fprintf(vis_stdout, "Primes: ");
358      for (i = 0; i < result->numOfPrimes; i++) {
359       
360        fprintf(vis_stdout, "%d ", result->primeInfoArray[i].primeNumber);
361      }
362      fprintf(vis_stdout, "\n");
363      fprintf(vis_stdout, "Times: ");
364      for (i = 0; i < result->numOfPrimes; i++) {
365       
366        fprintf(vis_stdout, "%.2f ", result->primeInfoArray[i].cpuTime);
367      }
368      fprintf(vis_stdout, "\n");
369    }
370  }
371
372}
373
374/*---------------------------------------------------------------------------*/
375/* Definition of static functions                                            */
376/*---------------------------------------------------------------------------*/
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
Note: See TracBrowser for help on using the repository browser.