source: vis_dev/vis-2.3/src/res/res.h

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

vis2.3
File size: 6.4 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [res.h]
4
5  PackageName [res]
6
7  Synopsis    [Combinational verification by residue arithmetic.]
8
9  Description [This package implements residue verification between two
10  networks. The method used is based on residue arithmetic and the
11  Chinese Remainder theorem. Verification is performed by interpreting
12  the outputs of the circuits as integers and verifying the residues
13  of the outputs with respect to a set of moduli. The choice of moduli
14  is directed by the Chinese Remainder Theorem in order to prove
15  equivalence of the two circuits. This method works well with
16  multipliers and possibly other arithmetic circuits (due to its
17  dependence on residue arithmetic).  Discretion should be exercised
18  in applying this method to general combinational circuits. Residue
19  verification is provided with vis-cu ONLY. It reads both blif and
20  blif-mv files. However, it does NOT support multi-valued
21  variables. Residue verification is primarily for combinational
22  verification, but may be applied to sequential circuits with the
23  same state encoding. The latch outputs are then considered to be
24  combinational inputs of the circuits and the latch inputs and reset
25  are considered to be combinational outputs of the circuits. This
26  package provides some combinational verification also. Some/all of
27  the outputs of the circuit may be verified directly (without using
28  residues). In using both direct and residue verification,
29  verification of arithmetic circuits may become easier. ]
30
31  Author      [Kavita Ravi    <ravi@boulder.colorado.edu> and
32               Abelardo Pardo <abel@boulder.colorado.edu>]
33
34  Copyright   [This file was created at the University of Colorado at Boulder.
35  The University of Colorado at Boulder makes no warranty about the suitability
36  of this software for any purpose.  It is presented on an AS IS basis.]
37
38  Revision    [$Id: res.h,v 1.22 2002/09/08 23:53:32 fabio Exp $]
39
40******************************************************************************/
41
42#ifndef _RES
43#define _RES
44
45/*---------------------------------------------------------------------------*/
46/* Nested includes                                                           */
47/*---------------------------------------------------------------------------*/
48#include "io.h"
49#include "ord.h"
50#include "ntm.h"
51#include "cmd.h"
52
53/*---------------------------------------------------------------------------*/
54/* Constant declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57#define RES_NETWORK_APPL_KEY "Res_NetworkApplKey"
58
59/*---------------------------------------------------------------------------*/
60/* Structure declarations                                                    */
61/*---------------------------------------------------------------------------*/
62
63/**Struct**********************************************************************
64
65  Synopsis    [Information for every prime used in the verification.]
66
67******************************************************************************/
68typedef struct PerPrimeInfo {
69  int primeNumber;
70  float cpuTime;
71  int bddSize;
72  bdd_node *residueDd;
73}PerPrimeInfo_t;
74
75
76/**Struct**********************************************************************
77
78  Synopsis [Structure holding the information related to the residual
79  verification.]
80
81******************************************************************************/
82typedef struct Res_ResidueInfo {
83  char  *networkName;                /* Name of the circuit verified */
84  char  *networkNameVerifiedAgainst; /* Name of the circuit verified Against*/
85  int   numInputs;                   /* Number of inputs*/
86  int   numOutputs;                  /* Number of outputs */
87  int   numDirectVerifiedOutputs;
88  float cpuDirectVerif;              /* Cpu time spent in direct
89                                      * verification */ 
90  int   numOfPrimes;                 /* Number of Primes needed for the
91                                      * verification */
92  PerPrimeInfo_t *primeInfoArray;    /* Information stored per prime */
93  int successDirectVerification;     /* Outcome of the direct verification */
94  int success;                       /* Outcome of the verification */
95  bdd_manager *ddManager;                    /* Manager required to free the residue BDDs */
96}Res_ResidueInfo_t;
97
98/*---------------------------------------------------------------------------*/
99/* Type declarations                                                         */
100/*---------------------------------------------------------------------------*/
101
102/*---------------------------------------------------------------------------*/
103/* Variable declarations                                                     */
104/*---------------------------------------------------------------------------*/
105
106
107/*---------------------------------------------------------------------------*/
108/* Macro declarations                                                        */
109/*---------------------------------------------------------------------------*/
110
111
112/**AutomaticStart*************************************************************/
113
114/*---------------------------------------------------------------------------*/
115/* Function prototypes                                                       */
116/*---------------------------------------------------------------------------*/
117
118EXTERN int Res_NetworkResidueVerify(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int numDirectVerify, array_t *outputOrderArray, st_table *outputNameMatch, st_table *inputNameMatch);
119EXTERN void Res_Init(void);
120EXTERN void Res_End(void);
121EXTERN void Res_ResidueInfoFree(Res_ResidueInfo_t *residue);
122EXTERN void Res_ResidueInfoFreeCallback(void *data);
123EXTERN Res_ResidueInfo_t * Res_NetworkReadResidueInfo(Ntk_Network_t *network);
124EXTERN char * Res_ResidueInfoReadName(Res_ResidueInfo_t *residuePtr);
125EXTERN int Res_ResidueInfoReadNumInputs(Res_ResidueInfo_t *residuePtr);
126EXTERN int Res_ResidueInfoReadNumOutputs(Res_ResidueInfo_t *residuePtr);
127EXTERN int Res_ResidueInfoReadNumDirectVerifiedOutputs(Res_ResidueInfo_t *residuePtr);
128EXTERN int Res_ResidueInfoReadCpuDirectVerif(Res_ResidueInfo_t *residuePtr);
129EXTERN int Res_ResidueInfoReadNumOfPrimes(Res_ResidueInfo_t *residuePtr);
130EXTERN int Res_ResidueInfoReadSuccess(Res_ResidueInfo_t *residuePtr);
131EXTERN void Res_ResidueInfoPrint(Res_ResidueInfo_t *result);
132
133/**AutomaticEnd***************************************************************/
134
135#endif /* _RES */
Note: See TracBrowser for help on using the repository browser.