source: vis_dev/vis-2.3/src/res/resInt.h @ 43

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

vis2.3
File size: 17.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [resInt.h]
4
5  PackageName [res]
6
7  Synopsis    [Internal declarations of the residue package.]
8
9  Author      [Kavita Ravi    <ravi@boulder.colorado.edu> and
10               Abelardo Pardo <abel@boulder.colorado.edu>]
11
12  Copyright [This file was created at the University of Colorado at Boulder.
13  The University of Colorado at Boulder makes no warranty about the suitability
14  of this software for any purpose.  It is presented on an AS IS basis.]
15
16  Revision    [$Id: resInt.h,v 1.31 2002/09/08 23:55:58 fabio Exp $]
17
18******************************************************************************/
19
20#ifndef _RESINT
21#define _RESINT
22
23/*---------------------------------------------------------------------------*/
24/* Nested includes                                                           */
25/*---------------------------------------------------------------------------*/
26
27#include <stdlib.h>
28#include <unistd.h>
29#include <string.h>
30#include "res.h"
31
32/*---------------------------------------------------------------------------*/
33/* Constant declarations                                                     */
34/*---------------------------------------------------------------------------*/
35
36#define RES_NOT_VERIFIED -1  /* constant to indicate verification not taken
37                              * place
38                              */
39#define RES_PASS 1           /* constant to indicate verification success */
40#define RES_FAIL 0           /* constant to indicate verification failure */
41#define ResDefaultComposeMethod_c ResVector_c
42#define ResDefaultScheduleLayerMethod_c ResLayerAlap_c
43
44#define IMMEDIATE_FANIN 1 /* Static flag to indicate that the BDD/MDD has to
45                           * be built in terms  of immediate fanin
46                           */
47
48
49#define PRIMARY_INPUTS 2  /* Static flag to indicate PIs
50                           * used to indicate that the BDD/MDD has to be
51                           * built in terms  of primary inputs
52                           * also used to flag the building of input
53                           * match tables
54                           */
55
56#define PRIMARY_OUTPUTS 3 /* Static flag to indicate PIs
57                           * also used to flag the building of input
58                           * match tables
59                           */
60
61/*---------------------------------------------------------------------------*/
62/* Structure declarations                                                    */
63/*---------------------------------------------------------------------------*/
64
65
66/*---------------------------------------------------------------------------*/
67/* Type declarations                                                         */
68/*---------------------------------------------------------------------------*/
69
70/**Enum************************************************************************
71
72  Synopsis [Different methods to compute the layers for functional
73  compositions.]
74
75  SeeAlso     [ResComputeCompositionLayers]
76
77******************************************************************************/
78typedef enum {
79  ResLayerAsap_c,
80  ResLayerAlap_c
81} ResLayerScheduleMethod;
82
83/**Enum************************************************************************
84
85  Synopsis    [Different composition methods.]
86
87  SeeAlso     [ComposeLayersIntoResidue]
88
89******************************************************************************/
90typedef enum { 
91  ResVector_c,    /* Compose when fanout gates have been composed */
92  ResOneGateAtATime_c, /* Compose one gate at a time */
93  ResPreimageComputation_c, /* Treat the compositions like
94                              * partitioned transition relation */
95  ResSuperG_c        /* new cudd vector compose that creates a super G */
96} ResCompositionMethod;
97
98
99/*---------------------------------------------------------------------------*/
100/* Variable declarations                                                     */
101/*---------------------------------------------------------------------------*/
102/* variables to measure times of different components of residue verification*/
103extern long Res_composeTime;
104extern long Res_shuffleTime;
105extern long Res_smartVarTime;
106extern long Res_orderTime;
107
108/*---------------------------------------------------------------------------*/
109/* Macro declarations                                                        */
110/*---------------------------------------------------------------------------*/
111
112/**Macro***********************************************************************
113
114  Synopsis     [Macro to fetch the i-th layer in the layer Array.]
115
116  SideEffects  []
117
118  SeeAlso      [Res_ResidueInfo]
119
120******************************************************************************/
121#define ResLayerFetchIthLayer(layerArray, i) \
122    array_fetch(array_t *, layerArray, i)
123
124/**Macro***********************************************************************
125
126  Synopsis     [Macro to determine number of nodes in current layer]
127
128  SideEffects  []
129
130  SeeAlso      [Res_ResidueInfo]
131
132******************************************************************************/
133#define ResLayerNumNodes(layer) \
134    array_n(layer)
135
136/**Macro***********************************************************************
137
138  Synopsis     [Iterate through each node in a layer.]
139
140  SideEffects  []
141
142  SeeAlso      [Res_ResidueInfo]
143
144******************************************************************************/
145#define LayerForEachNode(layer, i, nodePtr) \
146    arrayForEachItem(Ntk_Node_t *, layer, i, nodePtr)
147
148/**Macro***********************************************************************
149
150  Synopsis     [Add node in the i-th position in the layer.]
151
152  SideEffects  []
153
154  SeeAlso      [Res_ResidueInfo]
155
156******************************************************************************/
157#define LayerAddNodeAtIthPosition(layer, i, nodePtr) \
158   array_insert(Ntk_Node_t *, layer, i, nodePtr)
159
160/**Macro***********************************************************************
161
162  Synopsis     [Add node at the end of the layer.]
163
164  SideEffects  []
165
166  SeeAlso      [Res_ResidueInfo]
167
168******************************************************************************/
169#define LayerAddNodeAtEnd(layer, nodePtr) \
170    array_insert_last(Ntk_Node_t *, layer, nodePtr)
171
172/**Macro***********************************************************************
173
174  Synopsis     [Fetch the i-th node in the layer.]
175
176  SideEffects  []
177
178  SeeAlso      [Res_ResidueInfo]
179
180******************************************************************************/
181#define LayerFetchIthNode(layer, i) \
182    array_fetch(Ntk_Node_t *, layer, i)
183
184/**Macro***********************************************************************
185
186  Synopsis     [Sort the layer nodes according to the given function.]
187
188  SideEffects  []
189
190  SeeAlso      [Res_ResidueInfo]
191
192******************************************************************************/
193#define LayerSort(layer, func) \
194              array_sort(layer, func)
195
196/**Macro***********************************************************************
197
198  Synopsis     [Free current layer.]
199
200  SideEffects  []
201
202  SeeAlso      [Res_ResidueInfo]
203
204******************************************************************************/
205#define LayerFree(layer)  \
206              array_free(layer)
207
208/**Macro***********************************************************************
209
210  Synopsis     [Create an empty layer.]
211
212  SideEffects  []
213
214  SeeAlso      [Res_ResidueInfo]
215
216******************************************************************************/
217#define LayerCreateEmptyLayer() \
218            array_alloc(Ntk_Node_t *, 0)
219
220/**Macro***********************************************************************
221
222  Synopsis     [Macro to read the network name field of Res_ResidueInfo.]
223
224  SideEffects  []
225
226  SeeAlso      [Res_ResidueInfo]
227
228******************************************************************************/
229#define ResResidueInfoReadNetworkName(rPtr) \
230  (rPtr)->networkName
231
232/**Macro***********************************************************************
233
234  Synopsis     [Macro to read the name of the circuit that has been
235  verified against.]
236
237  SideEffects  []
238
239  SeeAlso      [Res_ResidueInfo]
240
241******************************************************************************/
242#define ResResidueInfoReadNameVerifiedAgainst(rPtr) \
243  (rPtr)->networkNameVerifiedAgainst
244
245/**Macro***********************************************************************
246
247  Synopsis     [Macro to set the name filed of Res_ResidueInfo]
248
249  SideEffects  []
250
251  SeeAlso      [Res_ResidueInfo]
252
253******************************************************************************/
254#define ResResidueInfoSetNetworkName(rPtr, value) \
255  (rPtr)->networkName = (value)
256
257/**Macro***********************************************************************
258
259  Synopsis     [Macro to set the name field of the circuit that this one
260  has been verified against.]
261
262  SideEffects  []
263
264  SeeAlso      [Res_ResidueInfo]
265
266******************************************************************************/
267#define ResResidueInfoSetNameVerifiedAgainst(rPtr, value) \
268  (rPtr)->networkNameVerifiedAgainst = (value)
269
270/**Macro***********************************************************************
271
272  Synopsis     [Macro to read the numInputs field of Res_ResidueInfo]
273
274  SideEffects  []
275
276  SeeAlso      [Res_ResidueInfo]
277
278******************************************************************************/
279#define ResResidueInfoReadNumInputs(rPtr) \
280  (rPtr)->numInputs
281
282/**Macro***********************************************************************
283
284  Synopsis     [Macro to set the numInputs field of Res_ResidueInfo]
285
286  SideEffects  []
287
288  SeeAlso      [Res_ResidueInfo]
289
290******************************************************************************/
291#define ResResidueInfoSetNumInputs(rPtr, value) \
292  (rPtr)->numInputs = (value)
293
294/**Macro***********************************************************************
295
296  Synopsis     [Macro to read the numOutputs field of Res_ResidueInfo.]
297
298  SideEffects  []
299
300  SeeAlso      [Res_ResidueInfo]
301
302******************************************************************************/
303#define ResResidueInfoReadNumOutputs(rPtr) \
304  (rPtr)->numOutputs
305
306/**Macro***********************************************************************
307
308  Synopsis     [Macro to set the numOutputs field of Res_ResidueInfo.]
309
310  SideEffects  []
311
312  SeeAlso      [Res_ResidueInfo]
313
314******************************************************************************/
315#define ResResidueInfoSetNumOutputs(rPtr, value) \
316  (rPtr)->numOutputs = (value)
317
318/**Macro***********************************************************************
319
320  Synopsis [Macro to read the numDirectVerifiedOutputs field of
321  Res_ResidueInfo.]
322
323  SideEffects  []
324
325  SeeAlso      [Res_ResidueInfo]
326
327******************************************************************************/
328#define ResResidueInfoReadNumDirectVerifiedOutputs(rPtr) \
329  (rPtr)->numDirectVerifiedOutputs
330
331/**Macro***********************************************************************
332
333  Synopsis [Macro to set the numDirectVerifiedOutputs field of
334  Res_ResidueInfo.]
335
336  SideEffects  []
337
338  SeeAlso      [Res_ResidueInfo]
339
340******************************************************************************/
341#define ResResidueInfoSetNumDirectVerifiedOutputs(rPtr, value) \
342  (rPtr)->numDirectVerifiedOutputs = (value)
343
344/**Macro***********************************************************************
345
346  Synopsis [Macro to read the cpuDirectVerif field of
347  Res_ResidueInfo.]
348
349  SideEffects  []
350
351  SeeAlso      [Res_ResidueInfo]
352
353******************************************************************************/
354#define ResResidueInfoReadCpuDirectVerif(rPtr) \
355  (rPtr)->cpuDirectVerif
356
357/**Macro***********************************************************************
358
359  Synopsis [Macro to set the cpuDirectVerif field of
360  Res_ResidueInfo.]
361
362  SideEffects  []
363
364  SeeAlso      [Res_ResidueInfo]
365
366******************************************************************************/
367#define ResResidueInfoSetCpuDirectVerif(rPtr, value) \
368  (rPtr)->cpuDirectVerif = (value)
369
370/**Macro***********************************************************************
371
372  Synopsis [Macro to read the numOfPrimes field of Res_ResidueInfo.]
373
374  SideEffects  []
375
376  SeeAlso      [Res_ResidueInfo]
377
378******************************************************************************/
379#define ResResidueInfoReadNumOfPrimes(rPtr) \
380  (rPtr)->numOfPrimes
381
382/**Macro***********************************************************************
383
384  Synopsis [Macro to set the numOfPrimes field of Res_ResidueInfo.]
385
386  SideEffects  []
387
388  SeeAlso      [Res_ResidueInfo]
389
390******************************************************************************/
391#define ResResidueInfoSetNumOfPrimes(rPtr, value) \
392  (rPtr)->numOfPrimes = (value)
393
394/**Macro***********************************************************************
395
396  Synopsis [Macro to read the success field of Res_ResidueInfo.]
397
398  SideEffects  []
399
400  SeeAlso      [Res_ResidueInfo]
401
402******************************************************************************/
403#define ResResidueInfoReadSuccess(rPtr) \
404  ((Res_ResidueInfo_t *)rPtr)->success
405
406/**Macro***********************************************************************
407
408  Synopsis [Macro to read the direct verification success field of
409  Res_ResidueInfo.]
410
411  SideEffects  []
412
413  SeeAlso      [Res_ResidueInfo]
414
415******************************************************************************/
416#define ResResidueInfoReadDirectVerificationSuccess(rPtr) \
417  (rPtr)->successDirectVerification
418
419/**Macro***********************************************************************
420
421  Synopsis [Macro to read the success field of Res_ResidueInfo.]
422
423  SideEffects  []
424
425  SeeAlso      [Res_ResidueInfo]
426
427******************************************************************************/
428#define ResNetworkReadResidueInfo(network) \
429  (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network,RES_NETWORK_APPL_KEY);
430
431/**Macro***********************************************************************
432
433  Synopsis [Macro to set the success field of Res_ResidueInfo.]
434
435  SideEffects  []
436
437  SeeAlso      [Res_ResidueInfo]
438
439******************************************************************************/
440#define ResResidueInfoSetSuccess(rPtr, value) \
441  ((Res_ResidueInfo_t *)rPtr)->success = (value)
442
443/**Macro***********************************************************************
444
445  Synopsis [Macro to set the direct verification success field of
446  Res_ResidueInfo.]
447
448  SideEffects  []
449
450  SeeAlso      [Res_ResidueInfo]
451
452******************************************************************************/
453#define ResResidueInfoSetDirectVerificationSuccess(rPtr, value) \
454  ((Res_ResidueInfo_t *)rPtr)->successDirectVerification = (value)
455
456
457/**Macro***********************************************************************
458
459  Synopsis [Macro to read one entry of the PerPrimeInfo array of
460  Res_ResidueInfo.]
461
462  SideEffects  []
463
464  SeeAlso      [Res_ResidueInfo]
465
466******************************************************************************/
467#define ResResidueInfoReadPerPrimeInfo(rPtr, i) \
468  (&((rPtr)->primeInfoArray[(i)]))
469
470/**Macro***********************************************************************
471
472  Synopsis [Macro to set one entry of the PerPrimeInfo array of
473  Res_ResidueInfo.]
474
475  SideEffects  []
476
477  SeeAlso      [Res_ResidueInfo]
478
479******************************************************************************/
480#define ResResidueInfoSetPerPrimeInfo(rPtr, idx, num, time, size, dd) \
481  ((rPtr)->primeInfoArray)[(idx)].primeNumber = (num); \
482  ((rPtr)->primeInfoArray)[(idx)].cpuTime = (time); \
483  ((rPtr)->primeInfoArray)[(idx)].bddSize = (size); \
484  ((rPtr)->primeInfoArray)[(idx)].residueDd = (dd)
485
486/**Macro***********************************************************************
487
488  Synopsis [Macro to set DdNodeof the  entry of the PerPrimeInfo array of
489  Res_ResidueInfo.]
490
491  SideEffects  []
492
493  SeeAlso      [Res_ResidueInfo]
494
495******************************************************************************/
496#define ResResidueInfoSetPerPrimeDd(rPtr, idx, dd) \
497  ((rPtr)->primeInfoArray)[(idx)].residueDd = (dd)
498
499/**AutomaticStart*************************************************************/
500
501/*---------------------------------------------------------------------------*/
502/* Function prototypes                                                       */
503/*---------------------------------------------------------------------------*/
504
505EXTERN bdd_node * BuildBDDforNode(Ntk_Network_t *network, Ntk_Node_t *nodePtr, int fanin);
506EXTERN bdd_node * ComposeLayersIntoResidue(Ntk_Network_t *network, array_t *layerArray, bdd_node *residueDd, array_t *outputArray);
507EXTERN array_t * ResComputeCompositionLayers(Ntk_Network_t *network, array_t *outputArray, array_t *ignoreArray);
508EXTERN void ResLayerPrintInfo(Ntk_Network_t *network, array_t *layerArray);
509EXTERN void ResLayerArrayFree(array_t *layerArray);
510EXTERN Res_ResidueInfo_t * ResNetworkResidueInfoReadOrCreate(Ntk_Network_t *network);
511EXTERN Res_ResidueInfo_t * ResResidueInfoAllocate(char *name);
512EXTERN void ResResidueInfoAllocatePrimeInfoArray(Res_ResidueInfo_t *residueInfo, int numOfPrimes, int *tableOfPrimes);
513EXTERN void MddCreateVariables(mdd_manager *mgr, int numVarsToBeAdded);
514EXTERN int * ResResidueVarAllocate(bdd_manager *ddManager, lsList orderList, array_t *newIdArray);
515EXTERN void ResResidueVarDeallocate(array_t *currentLayer);
516EXTERN void ResResidueFreeVariableManager(void);
517EXTERN void ResResidueInitializeVariableManager(int numOfVars);
518EXTERN int * ResResidueVarUseAllocate(int howManyVars, boolean recicleVarIds, int consecutive);
519EXTERN void ResResidueVarUseDeallocate(int *varPool, int size);
520EXTERN int ResResidueVarHighestIndex(void);
521
522/**AutomaticEnd***************************************************************/
523
524#endif /* _RESINT */
Note: See TracBrowser for help on using the repository browser.