source: vis_dev/vis-2.3/src/eqv/eqv.h @ 82

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

vis2.3
File size: 5.8 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [eqv.h]
4
5  PackageName [eqv]
6
7  Synopsis    [Provides commands for doing combinational and sequential
8  verification on two networks.]
9
10  Description [The eqv package provides two commands - comb_verify and
11  seq_verify for doing combinational and sequential verification respectively.
12  Two networks along with options for partitioning and ordering form the input
13  to the commands.<p>
14
15  Combinational verification : Two sets of distinguished nodes, roots and
16  leaves, are specified for each network. The leaves should form a complete
17  support for the roots in both networks. The correspondence between the roots
18  and leaves of the two networks can be specified in an input file. The format
19  of the input file is as follows-<p>
20
21  .roots<p>
22  &lt;name1&gt; &lt;name2&gt;<p>
23  .<p>
24  .<p>
25  .leaves<p>
26  &lt;name1&gt; &lt;name2&gt;
27  .<p>
28  .<p>
29  Here, name1 is a node name in the first network and name2 a node name in the
30  second network.<p>
31
32  If no input file is given, the combinational outputs are assumed to be roots
33  and the combinational inputs are assumed to be leaves. comb_verify checks
34  for each pair of corresponding roots whether the two are equivalent as
35  logical functions of corresponding leaf variables. This is done by
36  constructing BDD's for the roots in terms of the leaf variables. For each
37  pair in which the two roots are not equivalent, a minterm where they are not
38  equal is written out. Note that pseudo inputs are treated no differently
39  from any other inputs.<p>
40
41  Sequential verification : Two inputs and an option for partitioning form the
42  input for this command. A set of distinguished nodes called roots is
43  specified for each network. The correspondence between the two sets can be
44  specified in an input file as described above. If no input file is given,
45  the primary outputs are assumed to be roots. seq_verify checks for each
46  pair of corresponding roots whether the two roots have different values in a
47  reachable state of the product machine of the networks for any input. For
48  each pair that this happens, an error trace is written out.<p>
49
50  The method used in sequential verification i.e. product machine cannot handle
51  non-determinism. Therefore, the two networks shouldn't have any pseudo
52  inputs.]
53
54  SeeAlso     [ntk.h]
55
56  Author      [Shaz Qadeer]
57
58  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
59  All rights reserved.
60
61  Permission is hereby granted, without written agreement and without license
62  or royalty fees, to use, copy, modify, and distribute this software and its
63  documentation for any purpose, provided that the above copyright notice and
64  the following two paragraphs appear in all copies of this software.
65
66  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
67  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
68  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
69  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
70
71  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
72  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
73  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
74  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
75  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
76
77  Revision    [$Id: eqv.h,v 1.6 2002/09/08 23:28:36 fabio Exp $]
78
79******************************************************************************/
80
81#ifndef _EQV
82#define _EQV
83
84#include "fsm.h"
85#include "ord.h"
86#include "io.h"
87
88/*---------------------------------------------------------------------------*/
89/* Constant declarations                                                     */
90/*---------------------------------------------------------------------------*/
91
92
93/*---------------------------------------------------------------------------*/
94/* Type declarations                                                         */
95/*---------------------------------------------------------------------------*/
96typedef void (*OFT) (Ntk_Network_t *, Ntk_Network_t *, st_table *);
97
98/*---------------------------------------------------------------------------*/
99/* Structure declarations                                                    */
100/*---------------------------------------------------------------------------*/
101
102
103/*---------------------------------------------------------------------------*/
104/* Variable declarations                                                     */
105/*---------------------------------------------------------------------------*/
106
107
108/*---------------------------------------------------------------------------*/
109/* Macro declarations                                                        */
110/*---------------------------------------------------------------------------*/
111
112
113/**AutomaticStart*************************************************************/
114
115/*---------------------------------------------------------------------------*/
116/* Function prototypes                                                       */
117/*---------------------------------------------------------------------------*/
118
119EXTERN void Eqv_Init(void);
120EXTERN void Eqv_End(void);
121EXTERN boolean Eqv_NetworkVerifyCombinationalEquivalence(Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *leavesMap, st_table *rootsMap, OFT AssignCommonOrder, Part_PartitionMethod method1, Part_PartitionMethod method2);
122EXTERN boolean Eqv_NetworkVerifySequentialEquivalence(Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *rootsTable, st_table *leavesTable, Part_PartitionMethod partMethod, boolean useBackwardReach, boolean reordering);
123
124/**AutomaticEnd***************************************************************/
125
126#endif /* _EQV */
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
Note: See TracBrowser for help on using the repository browser.