Method and apparatus for formally checking equivalence using equivalence relationships Number:7,386,820 from the United States Patent and Trademark Office (PTO) owispatent An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLM.sub.DFG and HLM.sub.DFG. RTLM.sub.DFG and HLM.sub.DFG are then put into timestep form and are called RTLM.sub.ts and HLM.sub.ts. A test bench CS.sub.ts is selected that couples RTLM.sub.ts and HLM.sub.ts. The combination of RTLM.sub.ts[t], HLM.sub.ts[t] and CS.sub.ts[t] can have parts designated as datapath. Parts designated as datapath can be subject to a form of equivalence checking that seeks to prove equivalence by a form of inductive theorem proving that propagates symbolic values indicative of whether a node carries the same data content as another node. The theorem proving starts from initial conditions for HLM.sub.ts[t] determined by partial execution of the HLM. Propagation to a combinational function output can be determined from equivalence relationships between it and another combinational function. Propagation through a multiplexer can produce a conditional symbolic value.<H relationships, equivalence, Method, and, appa, 7386820.html, Patent, pto, 7386820

Title: Method and apparatus for formally checking equivalence using equivalence relationships

Abstract: An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLM.sub.DFG and HLM.sub.DFG. RTLM.sub.DFG and HLM.sub.DFG are then put into timestep form and are called RTLM.sub.ts and HLM.sub.ts. A test bench CS.sub.ts is selected that couples RTLM.sub.ts and HLM.sub.ts. The combination of RTLM.sub.ts[t], HLM.sub.ts[t] and CS.sub.ts[t] can have parts designated as datapath. Parts designated as datapath can be subject to a form of equivalence checking that seeks to prove equivalence by a form of inductive theorem proving that propagates symbolic values indicative of whether a node carries the same data content as another node. The theorem proving starts from initial conditions for HLM.sub.ts[t] determined by partial execution of the HLM. Propagation to a combinational function output can be determined from equivalence relationships between it and another combinational function. Propagation through a multiplexer can produce a conditional symbolic value.

Patent Number: 7,386,820 Issued on 06/10/2008 to Koelbl, et al.

Inventors: Koelbl; Alfred (Dachau, DE), Pixley; Carl Preston (Beaverton, OR)
Assignee: Synopsys, Inc. (Mountain View, CA)

Appl. No.: 11/149,751

Filed: June 10, 2005

Related U.S. Patent Documents


Application Number	Filing Date	Patent Number	Issue Date
60635152	Dec., 2004

Current U.S. Class: 716/6 ; 716/18; 716/4; 716/5

Field of Search: 716/1,3-6,18

References Cited [Referenced By]

U.S. Patent Documents


2003/0115562	June 2003	Martin et al.

Primary Examiner: Do; Thuan
Attorney, Agent or Firm: Park, Vaughan & Fleming LLP

Parent Case Text

As provided for under 35 U.S.C. .sctn. 119(e), this patent claims benefit of the filing date for U.S. Provisional Application "Method and Apparatus For Production Of Data-Flow-Graphs By Symbolic Simulation," Application No. 60/635,152, filed Dec. 10, 2004. Application No. 60/635,152 is herein incorporated by reference.

Claims

What is claimed is:

1. A method of propagating values in a data-flow graph, comprising: marking each node, of an initial set of nodes which represents a set of input variables to a data-flow graph, with a symbolic value indicative of whether a node carries the same data content as another node; forming a symbolic value at an output of a multiplexer, that conditionally evaluates to a symbolic value, chosen from a set of symbolic values input to the multiplexer, dependent upon a value at a selector input of the multiplexer; organizing the data-flow graph into timesteps; and organizing each timestep into a first section representative of a first model, a second section representative of a second model and a third section representative of a test bench between the first and second models.

2. The method of claim 1, wherein the symbolic values, for the initial set of nodes, represent integers.

3. The method of claim 2, wherein the symbolic values, for the initial set of nodes, are represented by binary decision diagrams.

4. The method of claim 1, wherein the symbolic value, for the output of the multiplexer, is represented by a multi-terminal binary decision diagram.

5. The method of claim 1, wherein the symbolic value, for the output of the multiplexer, represents if-then-else functionality.

6. The method of claim 1, wherein the value at the selector input, is a symbolic Boolean expression.

7. The method of claim 6, wherein the symbolic Boolean expression is a Boolean expression.

8. The method of claim 6, wherein the symbolic Boolean expression includes an indication of a timestep.

9. The method of claim 6, wherein the symbolic Boolean expression is comprised of a plurality of symbolic Boolean variables connected by Boolean operators.

10. The method of claim 1, further comprising: determining whether, from a first timestep to a second timestep, each timestep is fully populated with symbolic values.

11. The method of claim 1, further comprising: determining whether, from a first timestep to a second timestep, each timestep is fully populated with symbolic values.

12. The method of claim 1, further comprising: initializing a section of an initial timestep of the data-flow graph by partial execution of a high-level model corresponding to the section.

13. The method of claim 1, further comprising: organizing the third section, when the first and second sections are equivalent, to produce an equivalence indicator.

14. The method of claim 13, further comprising: determining whether, from a first timestep to a second timestep, each timestep is sufficiently populated with symbolic values such that equivalency indicator, for each of the first timestep to the second timestep, can be tested.

15. The method of claim 14, further comprising: reencoding, a set of symbolic values for a third timestep, one timestep later than the second timestep, if each equivalency indicator, for each of the first timestep to the second timestep, indicates equivalency between the first section and the second section.

16. The method of claim 14, further comprising: adding a third timestep, one timestep later than the second timestep, if at least one equivalency indicator, for each of the first timestep to the second timestep, does not indicate equivalence between the first section and the second section.

17. The method of claim 14, further comprising: producing a counter-example, if at least a first equivalency indicator, for each of the first timestep to the second timestep, does not indicate equivalence between the first section and the second section.

18. The method of claim 17, wherein the step of producing a counter-example further comprises: determining a conditional equivalence relation for which the first equivalency indicator indicates equivalence.

19. A data-processing system for propagating values in a data-flow graph, comprising the following sub-systems: a sub-system configured to mark each node, of an initial set of nodes which represents a set of input variables to a data-flow graph, with a symbolic value indicative of whether a node carries the same data content as another node; a sub-system configured to form a symbolic value at an output of a multiplexer, that conditionally evaluates to a symbolic value, chosen from a set of symbolic values input to the multiplexer, dependent upon a value at a selector input of the multiplexer; and a sub-system configured to: organize the data-flow graph into timesteps; and organize each timestep into a first section representative of a first model, a second section representative of a second model and a third section representative of a test bench between the first and second models.

20. A computer program on a computer readable medium, having computer-readable code devices embodied therein, for propagating values in a data-flow graph, the computer program comprising: computer readable program code devices configured to mark each node, of an initial set of nodes which represents a set of input variables to a data-flow graph, with a symbolic value indicative of whether a node carries the same data content as another node; computer readable program code devices configured to form a symbolic value at an output of a multiplexer, that conditionally evaluates to a symbolic value, chosen from a set of symbolic values input to the multiplexer, dependent upon a value at a selector input of the multiplexer; computer readable program code devices configured to organize the data-flow graph into timestep; and computer readable program code devices configured to organize each timestep into a first section representative of a first model a second section representative of a second model and a third section representative of a test bench between the first and second models.

Description

CROSS REFERENCE TO RELATED APPLICATIONS

This application is related to the following four U.S. patent applications, all of which are herein incorporated by reference in their entirety:

"Method and Apparatus For Formally Comparing Stream-Based Designs," filed on Jun. 10, 2005, having inventors Alfred Koelbl and Carl Preston Pixley, having Ser. No. 11/149,852.

"Method and Apparatus For Automatic Test Bench Generation," filed on Jun. 10, 2005, having inventors Alfred Koelbl and Carl Preston Pixley, having Ser. No. 11/150,685.

"Method and Apparatus For Production Of Data-Flow-Graphs By Symbolic Simulation," filed on Jun. 10, 2005, having inventors Alfred Koelbl and Carl Preston Pixley, having Ser. No. 11/149,756.

"Method and Apparatus For Initial State Extraction," filed on Jun. 10, 2005, having inventors Alfred Koelbl and Carl Preston Pixley, having Ser. No. 11/149,827.

FIELD OF THE INVENTION

The present invention relates generally to the comparison of models prepared at differing levels of abstraction, and more particularly to the comparison of a high-level model to a register transfer level model.

BACKGROUND OF THE INVENTION

To cope with the high complexity of modern hardware design, designers can adopt a methodology that starts with a very high-level design specification. Such high-level specification can also be referred to as a high-level model (HLM). An HLM captures basic functionality of the design, but can leave out implementation details. The focus can therefore be on algorithm design and design exploration, since even extensive changes in the HLM's architecture can be easily made. Furthermore, a methodology using HLMs enables validation of the architecture during the early stages of design. HLMs can be written in a high-level programming language, such as C or C++.

Once the HLM has been validated, and sufficient decisions have been made regarding implementation of the design, the HLM can be refined to an RTL model (RTLM), that can then be processed by more "back-end" tools that perform synthesis and placement. The process of producing the RTLM from the HLM, however, is often performed in a mainly manual fashion that is error prone. A need therefore exists for EDA tools to assist the designer in verifying that the RTLM adheres to (or is equivalent to) the HLM.

A known approach for determining equivalence between an RTLM and HLM is the running of extensive simulations on both models. The results of such simulations are compared. Such simulations can be very time consuming and can miss subtle discrepancies between the two models.

Therefore, there exists a need for better methods of determining equivalence between RTLMs and HLMs. A formal approach to determining such equivalency is desirable since such approaches have the possibility of actually proving that, according to some standard of equivalency, the two models are equivalent.

However, conventional approaches to formal analysis are often too inefficient when applied to anything but small scale designs. What is needed, therefore, are more efficient approaches to formal analysis that have a good expectation of proving equivalency between large-scale designs.

In addition to the formal analysis itself, issues that can also be addressed, for improving the efficiency of formal approaches to equivalence determination, include the following: producing an appropriate common representation of the RTLM and HLM; producing an appropriate test bench for combining the RTLM and HLM; and determining appropriate initial conditions from which to start a formal analysis.

SUMMARY OF THE INVENTION

Please refer to the Glossary of Selected Terms, included at the end of the Detailed Description, for the definition of selected terms used in the below Summary. Section numbers in the below Summary correspond to section numbers in the Detailed Description.

1. Summary of an Equivalency Testing System

A novel equivalency testing system is presented. As a framework for discussing the various components of the equivalency testing system, a pseudo-coded procedure called "test_for_equivalency" is also presented.

Both an RTLM and HLM to be compared for equivalence are converted into DFGs, called RTLM.sub.DFG and HLM.sub.DFG. The HLM can be specified as a function written in a high-level programming language, such as C++. HLM.sub.DFG can be determined by a new technique, of symbolic simulation of the HLM, presented herein.

RTLM.sub.DFG and HLM.sub.DFG are put into a timestep form, referred to as RTLM.sub.ts and HLM.sub.ts. An arbitrary timestep "t," of RTLM.sub.ts and HLM.sub.ts, can be referred to as RTLM.sub.ts[t] and HLM.sub.ts[t].

A combining structure CS.sub.ts can be selected that couples RTLM.sub.ts and HLM.sub.ts. A combining structure can also be referred to as a "test bench." The combining structure has the following property: if, for a timestep t, RTLM.sub.ts[t] and HLM.sub.ts[t] are equivalent according to a given (or automatically determined) notion of equivalence, then CS.sub.ts[t] will detect this. Different types of combining structures can be selected depending upon the type of circuit represented by RTLM.sub.ts and HLM.sub.ts. Novel techniques, for classifying each of RTLM.sub.ts and HLM.sub.ts, and for selecting a suitable CS.sub.ts, are presented. In addition, novel forms of combining structure, suitable in general for formal verification, are presented. For example, a novel combining structure, for showing that RTLM.sub.ts and HLM.sub.ts are stream-equivalent, is presented.

The complete system, comprised of RTLM.sub.ts[t], HLM.sub.ts[t] and CS.sub.ts[t], is referred to as a "miter." The miter can have certain parts designated as representing control logic and other parts designated as representing datapath logic. Parts of the miter designated as control can be subject to a known form of bit-level equivalence checking. Parts of the miter designated as datapath are subject to a new form of equivalence checking that works above the bit level, using a node value indicator referred to herein as a "symbolic data value" or SDV, and that seeks to prove equivalence by a form of inductive theorem proving.

In the datapath portions of the miter, equivalence checking can be conducted at a higher level of abstraction if one is not interested in actual data values, but only in whether RTLM.sub.ts and HLM.sub.ts produce the same data (given that they receive the same input data). In this case, integers can be used as an abstraction for datapath data values: if two signals have the same integer number, this signifies that their actual data values are the same; if two signals have the different integer numbers, this signifies their actual data values are different. To refer to such integer values, the term "integer SDV" can be used.

If it can be proven that RTLM.sub.ts and HLM.sub.ts both produce the same SDVs on all of their primary outputs, and for all times, it is proven that both designs are equivalent. In order to determine the SDVs of the primary outputs of RTLM.sub.ts and HLM.sub.ts, input SDVs must be propagated through the miter.

A novel form of inductive theorem proving starts from initial conditions for the first timestep for the miter (i.e., for timestep RTLM.sub.ts[0], HLM.sub.ts[0] and CS.sub.ts[0]). The initial state for RTLM.sub.ts[0] can be determined by any suitable known means, but the initial state for HLM.sub.ts[0] can be determined by a new technique, of partial execution of the HLM, presented herein.

A first "phase" of SDV propagation is performed. In SDV propagation, SDVs of the first timestep are sought to be propagated forward to the outputs of the first timestep. If a path of propagation cannot be fully pursued to the outputs of a timestep, additional timesteps can be added. The first phase of SDV propagation ends when the miter is completely "populated" with SDVs up to a timestep called t_ready-1. The full population of SDVs means that if RTLM and HLM can be equivalent during those timesteps (i.e., the timesteps from the first timestep up to t_ready-1), this equivalence will be detected by the combining structure of each of those timesteps.

In propagating SDVs through a timestep, a complication arises with multiplexers. Consider the case of a two-input multiplexer where an integer SDV is present at each of the multiplexer's inputs. If the two SDVs are to be propagated through the multiplexer, the resulting SDV on the multiplexer output cannot be represented as an integer, since the multiplexer's selector input determines which SDV is routed to the output. To model the conditional dependency of the multiplexer output, on the selector condition, a second type of SDV, referred to herein as an ITE (If-Then-Else) SDV, is introduced.

The SDVs chosen and formed, as part of the first phase of SDV propagation, are guided by labels that are assigned to the nodes of the miter in a particular order as timesteps are added.

The timestep at t_ready is reencoded and the symbolic values of its datapath signals, relative to their timestep-invariant node names, are recorded as a potential first "fixed-point" of the SDV propagation process.

As part of the reencode, the order of label assignment, that guided the selection and formation of SDVs during the first phase of SDV propagation, is repeated from the beginning.

Starting with the potential first fixed-point as the initial condition, a second phase of SDV propagation is performed. Like the first phase, the ending of the second phase of SDV propagation is marked by the miter being completely "populated" with SDVs up to a later timestep, also called t_ready-1.

Because the second phase of SDV propagation is guided by a repetition of the same labeling process that guided the first phase of SDV propagation, if the potential first fixed-point is a real fixed-point, the exact same form of SDV propagation will occur during the second phase as occurred during the first phase.

This repetition of propagation phases can be detected as follows. The timestep of the later t_ready is reencoded. The symbolic values of the next-state and primary inputs of the later t_ready, relative to their timestep-invariant node names, are recorded as a potential second "fixed-point."

If the first and second, potential fixed-points, are identical, then it has been inductively proven that the process of SDV propagation can be repeated, indefinitely, for all timesteps. If each timestep "t," from the initial timestep of the first phase up to the timestep t_ready-1 of the second phase, indicates HLM.sub.ts[t] and RTLM.sub.ts[t] are equivalent (as indicated by CS.sub.ts[t]), then it is known that HLM and RTLM are equivalent for all timesteps.

The proving of equivalence between HLM and RTLM can produce an "equivalence indicator" for a user of the system. If equivalence determination process cannot prove equivalence, a "counter example" can be produced to aid the user in locating where behavior of the HLM diverges from that of the RTLM.

1.1 Summary of Conversion of HLM and RTLM to DFGs

Within test_for_equivalency, a procedure "RTLM.sub.--2_DFG" can be invoked for conversion of an RTLM into an RTLM.sub.DFG. RTLM.sub.DFG is referred to in the pseudo-code as "RTLM_dfg." Also within test_for_equivalency, procedure "HLM.sub.--2_DFG" can be invoked for conversion of an HLM into an HLM.sub.DFG.

1.2 Summary of Conversion into Timestep Form

Within test_for_equivalency, a procedure "generate_timestep" can be invoked twice: once for generation of RTLM.sub.ts from RTLM.sub.DFG and a second time for generation of HLM.sub.ts from HLM.sub.DFG. RTLM.sub.ts is referred to in the pseudo-code as "RTLM_ts." HLM.sub.ts is referred to in the pseudo-code as "HLM_ts."

1.3 Summary of Combining Structure Generation

A process for producing a CS.sub.ts can be summarized as follows. RTLM.sub.ts and HLM.sub.ts can each be classified. Based upon the classification of each DFG, a CS.sub.ts can be selected.

A CS.sub.ts can be designed to produce an output "q" that has the following property: "q" for a timestep t, is TRUE if and only if RTLM.sub.ts[t] and HLM.sub.ts[t] are equivalent according to a given notion of equivalence.

One of the combining structures presented is for the comparison of stream-based designs. This stream-based combining structure, on its own and without a prior step of classification of the designs to be coupled, is novel. Other applications, of this stream-based combining structure, are discussed.

Production of the miter can include identification of control and datapath nodes. Each datapath node can be assigned a value referred to herein as an "SDV." Each control node can be assigned a value referred to herein as a "symbolic Boolean expression."

An SDV is not intended to represent a particular piece of data, or a particular value. Rather, an SDV is intended to represent whether one node of the datapath has been assigned the same value (or data structure) as another node of the datapath. An SDV can be of two types: integer and ITE.

An integer SDV is just an integer value. The actual data represented by the integer SDV can be arbitrarily complex.

An ITE SDV takes three arguments: a symbolic Boolean expression, a first SDV and a second SDV. If the symbolic Boolean expression is satisfied, then the value of the first SDV is returned by the ITE SDV, else the value of the second SDV is returned by the ITE SDV. The first and second SDVs can either be an integer SDV, or a nested ITE SDV.

An ITE SDV can be used to indicate whether or not datapath nodes are outputting the same data, at a particular time, depending upon which conditions of the control nodes are met.

A symbolic Boolean expression is the same as an ordinary Boolean expression, except that rather than being comprised of Boolean variables (e.g., "x" or "-x") and/or Boolean values (e.g., "1" or "0"), it is comprised of, respectively, symbolic Boolean variables and/or symbolic Boolean values. A symbolic Boolean expression can be a single symbolic Boolean variable or a single symbolic Boolean value. A symbolic Boolean expression can also be comprised of symbolic Boolean variables and/or symbolic Boolean values connected by Boolean operators.

A symbolic Boolean variable can differ from an ordinary Boolean variable as follows: it can indicate the timestep from which it arose. A symbolic Boolean value can differ from an ordinary Boolean value as follows: it can indicate the timestep from which it arose.

A CER is a symbolic Boolean expression that describes the conditions under which a node "n1" at a timestep "t1" has the same integer SDV as a node "n2" at a timestep "t2."

If "n1" and "n2" are both assigned integer SDVs, the CER between them can be as follows. The CER can be a logic 1 if both "n1" and "n2" have the same integer SDV. The CER can be a logic 0 if "n1" and "n2" have different integer SDVs.

If "n1" is assigned an integer SDV and "n2" is assigned an ITE SDV, then the CER between them can be as follows. The CER can be logic 0 if there is no setting of the variables of the ITE SDV for which it evaluates to the same integer SDV assigned to "n1." The CER can be a symbolic Boolean expression that specifies a setting of the variables of the ITE SDV for which it evaluates to the same integer SDV assigned to "n1."

If "n1" is assigned an ITE SDV "iteSDV1" and "n2" is assigned an ITE SDV "iteSDV2," then the CER between them can be as follows. Let us call the collection of all variables of iteSDV1 and iteSDV2 the "support" for any CER between them. The CER can be logic 0 if there is no setting of the support variables that causes iteSDV1 and iteSDV2 to evaluate to the same integer SDV. The CER can be a symbolic Boolean expression that specifies a setting of the variables of the support that causes iteSDV1 and iteSDV2 to evaluate to the same integer SDV.

Any appropriate heuristic or procedure can be used to identify a node of a miter as part of control or part of the datapath. Also, the division between control and datapath nodes can be guided by user input.

Within test_for_equivalency, a procedure "generate_test_bench" can be invoked for generation of CS.sub.ts from RTLM.sub.ts and HLM.sub.ts. CS.sub.ts is referred to in the pseudo-code as "CS_ts."

1.4 Summary of Initializations

An "Active Timestep Range" (ATR) is the range of timesteps, of a miter, currently being processed with the objective of further propagating SDVs. An ATR begins at a timestep t=ATR_begin and continues to a timestep at t=ATR_end.

Prior to starting an equivalence-determining process, the following initializations can be done.

The ATR of the miter can be defined by setting values for ATR_begin and ATR_end. The miter can be initialized to begin as a single timestep at t=0. In this case, for example, ATR_begin and ATR_end can both be initialized to zero.

For each timestep of the ATR, each datapath node can be assigned a "label identifier." A label identifier is a globally unique identifier for each datapath node of a miter. Label identifiers can be used, as described below, for insuring that equivalence classes of nodes, that have been determined by an equivalence-determining process, are combined according to a predictable ordering.

In order to "prime" an SDV propagation process, whereby equivalences between nodes can be determined, the following initializations can be accomplished.

Initial SDVs, for the present-state nodes of the ATR, can be assigned. In order to determine such initial SDVs, initial states for RTLM and for HLM can be determined. A novel technique is described herein for determining an initial state of an HLM by partial execution of it.

SDVs can be assigned to datapath primary inputs of the ATR. Symbolic Boolean expressions can be assigned to control primary inputs of the ATR.

Propagation of SDVs through TFs can be assisted by the determination of CERs. Specifically, propagation of SDVs through a TF "TF1" and a TF "TF2" can be assisted by the determination of CERs between the inputs of TF1 and TF2. Such CERs, combined with a CEC of TF1 and TF2, can allow for CERs between the outputs of TF1 and TF2 to be determined.

Within test_for_equivalency, the present-state inputs of the initial timestep of the initial ATR (e.g., RTLM.sub.ts[0] and HLM.sub.ts[0]), can be set by a procedure called "initialize_initial_timestep." initialize_initial_timestep can work by first finding initial states for RTLM and HLM. The initial state for HLM can be found by a novel technique that utilizes partial execution of the HLM. Results of the partial execution can be saved, using further novel techniques, such that initialization of the initial timestep can be accomplished.

1.5 Summary of Equivalence Checking with CERs

A flowchart, with an overview of a core equivalence-determining process, is presented.

The first step of the process is to produce and initialize a miter.

An SDV propagation process is applied to the ATR.

The ATR is tested for whether it has a timestep at t=t_ready that is ready for reencoding.

If there is a timestep t_ready, the following actions can be taken: t_ready is reencoded; a first fixed-point target (FPT) is extracted from t_ready and recorded in an array element FPT[0]; and the ATR is updated to begin at t_ready (i.e., ATR_begin=t_ready). In preparation for trying to find a second FPT, timesteps are also added to the ATR and they are initialized (or "primed") for more SDV propagation.

If a timestep ready for reencoding has not yet been found, the miter is tested for whether a maximum number of timesteps have already been tried. If a maximum number of timesteps have already been tried, the equivalence-determining process fails and a counter-example can be generated for the user. If a maximum number of timesteps have not been tried, a timestep (or timesteps) are added to the ATR. Once timesteps have been added to the ATR, the process repeats from the above step of applying an SDV propagation process to the ATR.

Assuming the search for a first FPT is successful, the above-described process is repeated in order to find a second FPT at a later timestep of the miter.

If a second FPT is found, the two FPTs can be compared. If the two FPTs are identical, then it is proven that HLM.sub.ts is equivalent to RTLM.sub.ts for all timesteps.

The equivalence-determining process presented herein is described mostly with respect to the analysis of a DFG that has been derived from an RTLM and HLM. However, the equivalence-determining process presented can be used for comparing two RTLMs to each other, or for comparing two HLMs to each other. Furthermore, the DFG, to which the equivalence-determining process presented herein is applied, can be derived from any type of initial source description.

Within test_for_equivalency, the procedure "equivalence_checking_with_CERs" can be called that performs the core equivalence determining process.

2. Summary of HLM to DFG Conversion by Symbolic Simulation

The term "symbolic simulation," as utilized herein, refers to a simulated execution of an input representation such that all possible scenarios, for flow-of-control, are considered. The result is a non-canonical data structure that explicitly represents the flows-of-control considered.

As an example, the input representation, to be symbolically simulated, can be a CFG. The CFG can be produced from an HLM, where the HLM is expressed in a high-level programming language, such as C or C++. The particular form of non-canonical data structure, produced by symbolic simulation of the CFG, can be a DFG.

Each possible flow-of-control through the CFG can be represented by a marker referred to herein as an "execution path." An execution path can serve as a bridge, between the CFG and the DFG being produced, as follows. In addition to marking a location with the CFG, an execution path can include an expression referred to herein as a "path condition." A path condition of an execution path "x" can express, in terms of variables set by nodes of the DFG being produced, the condition under which the CFG location (indicated by execution path "x") can be reached.

The initial value, of each variable of the CFG, can be represented as an input to the DFG to be produced. Once symbolic simulation is completed, these initial values can "flow through" the DFG and be transformed, by operators of the DFG, to produce output values for HLM variables.

Each possible flow of control through the CFG is encompassed within the DFG produced by symbolic simulation. Depending upon the initial values input to the DFG, data can flow through particular paths of the DFG in order to produce the correct result.

An example CFG, that can be symbolically simulated, is presented. An example symbolic simulation of the example CFG, to produce a DFG, is presented.

A key operation of any symbolic simulation is "splitting" an existing execution path "x," into two execution paths "x_true" and "x_false," when a conditional node "y" of a CFG is reached. Execution path x_true handles the case where the conditional expression, of conditional node "y," is satisfied. Execution path x_false handles the case where the conditional expression, of conditional node "y," is not satisfied. Symbolic execution fully explores both x_true and x_false so that the resulting DFG can handle both cases. Another key operation of symbolic simulation is "merging" two execution paths, "x_true" and "x_false," into a re-combined execution path "x."

The symbolic simulation techniques presented herein are discussed primarily with respect to their application to the equivalence-determining process presented herein. However, the symbolic simulation techniques presented herein can be used in conjunction with any application utilizing a non-canonical representation of an HLM. By way of example only, and without limiting the range of potential applications, non-canonical representations of an HLM can be useful with other types of design analysis tools and with synthesis tools.

Techniques for handling loops with efficient "decision procedures," during symbolic simulation, are presented.

The order in which execution paths are pushed-on or popped-off the queue of execution paths, during symbolic simulation, can have a significant impact on the efficiency of symbolic simulation and on the quality of the constructed DFG. In general, execution paths which are split should be merged again as soon as possible. This goal can be achieved by appropriately sorting the queue of execution paths.

As a preprocessing step, to applying symbolic simulation to a CFG, the nodes of the CFG can each be given a priority that determines when they are traversed during symbolic simulation. Execution paths that point to nodes with a higher priority can be traversed before execution paths pointing to lower priority nodes.

An example CFG, and an example application of a prioritization process to such CFG, is presented. The prioritization process, used for the example, is presented in pseudo-code form.

3. Summary of the Timestep Form

As discussed above, prior to applying an SDV-propagation process, the miter can be converted into timestep form.

An example DFG, for conversion into the timestep form, is presented.

An example conversion into timestep form, of the example DFG, is presented.

Production of the timestep form used herein is well-known in the art, and any suitable technique for production of the timestep form can be used in conjunction with the inventive techniques described herein.

4. Summary of Test Bench Generation

As discussed above, test bench generation relates to producing a DFG in timestep form, referred to herein as a "combining structure" (or CS.sub.ts), for combining RTLM.sub.ts and HLM.sub.ts in a way that permits the resulting timestep, referred to herein as a "miter" timestep, to be tested for equivalence. A timestep "t" of a miter (MT.sub.ts[t]) can be comprised of the following DFGs: RTLM.sub.ts[t], HLM.sub.ts[t] and CS.sub.ts[t].

A process for accomplishing the combination of DFGs can be summarized as follows. Each RTLM.sub.ts and HLM.sub.ts can each be classified, individually, based on structural criteria. The classification assigned is referred to herein as a "DFG class." Based upon the DFG class of RTLM.sub.ts and HLM.sub.ts, a structure CS.sub.ts for combining the two DFGs can be selected. Such selection of a combining structure can be viewed as applying the DFG class of RTLM.sub.ts and the DFG class of HLM.sub.ts to a two-dimensional decision matrix. The selected combining structure can be constructed by drawing upon a library of DFG building blocks.

As discussed above, the CS.sub.ts produced can be designed to have a "q" output with the following property: "q," for a timestep t, is TRUE if and only if RTLM.sub.ts[t] and HLM.sub.ts[t] are equivalent. Once the CS.sub.ts has been produced, the miter timestep can be processed, for identification of control and datapath nodes, prior to application of an equivalence-determining procedure.

While the above-described process, for the selection of CS.sub.ts, assumes RTLM.sub.ts and HLM.sub.ts each belong to only one. DFG class, this is not necessarily the case. To address this situation, for each pair of corresponding primary outputs, from RTLM.sub.ts and HLM.sub.ts, each primary output can be put into a DFG class to form a DFG class pair. This can be accomplished by applying the below-described classification techniques, to RTLM.sub.ts and HLM.sub.ts, on a primary-output-by-primary-output basis. If all such pairs, of a DFG class for an output of RTLM.sub.ts with a DFG class for a corresponding output of HLM.sub.ts, are the same, one type of miter can be generated for which equivalence determination is applied once.

However, if more than one type of pairing of DFG classes is identified, an appropriate miter can be generated for each different type of DFG class pair found. An equivalence-determining procedure can be applied to each miter. RTLM.sub.ts and HLM.sub.ts have been proven to be equivalent only if all such equivalence-determining tests are successful.

4.1 Summary of Classifying RTLM.sub.ts and HLM.sub.ts

Each DFG can be classified based upon a structural analysis. The types of DFG classes can include: combinational, pipelined, handshaking and unknown. Methods for testing a DFG, as to whether it belongs to each of the DFG classes, are presented. The classification methods share the common goal of trying to determine how many prior cycles of input data can affect the result of a computation.

4.2 Summary of Combining Structure Selection

Based on the DFG class for RTLM.sub.ts and the DFG class for HLM.sub.ts, an appropriate structure, for combining the two DFGs to produce MT.sub.ts, can be selected. A decision matrix can be used. An example decision matrix is presented. The output of the example decision matrix is one of five categories of combining structure: combinational, cycle-accurate, pipelined, stream-based and error.

Each of the five categories of combining structure is presented.

4.2.1 Summary of Combinational

The combinational combining structure can be applied when both DFGs are classified as combinational.

4.2.2 Summary of Cycle-Accurate

The cycle-accurate combining structure can be applied when either DFG is classified as unknown. The cycle-accurate combining structure can be preferred under these circumstances since it produces a "strong" form of equivalence testing that will not produce a false positive. On the other hand, because the cycle-accurate combining structure produces a MT.sub.ts that is so restrictive as to the conditions under which equivalence between HLM.sub.ts and RTLM.sub.ts can be found, it can produce a false negative where a "weaker" equivalence test might be able to show the DFGs are equivalent. Therefore, while the cycle-accurate combining structure is a suitable default, it can also be desirable to allow the user to select another combining structure that produces a weaker test for equivalence.

The cycle-accurate combining structure produces an equivalence test where both DFGs must produce exactly the same output on every clock cycle in order for equivalence to be found.

4.2.3 Summary of Pipelined

The pipelined combining structure can be applied under the following circumstances: both DFGs are classified as pipelined, one DFG is classified as combinational and the other is classified as pipelined. If one of the DFGs is classified as combinational, it can be converted into a one-stage pipeline.

The approach of a pipelined combining structure is to effectively modify one or both of the DFGs such that a cycle-accurate equivalence test can be performed.

Techniques are presented for using a pipelined combining structure to couple DFGs that use memories. The technique employs determination of a memory mapping between the memories of both designs.

4.2.4 Summary of Stream-Based

The stream-based combining structure is applicable when both RTLM.sub.ts and HLM.sub.ts have been put into the DFG class "handshaking."

Stream-based equivalence, if proven, can be characterized as follows. First, both RTLM.sub.ts and HLM.sub.ts receive the same stream of input data, but not necessarily at the same time. Second, both RTLM.sub.ts and HLM.sub.ts generate the same output data, but not necessarily at the same time. Phrased another way, stream-based equivalence means there are no constraints on the relative timing of the inputs or outputs of RTLM.sub.ts and HLM.sub.ts, however, data packets produced by the two DFGs should be produced in the same order.

An overall method, by which a stream-based combining structure can be used, is as follows. First, create two sub-miters. Each sub-miter is comprised of an instance of RTLM.sub.ts, HLM.sub.ts and the stream-based combining structure CS_STREAM.sub.ts. Second, if both sub-miters find equivalency, on a cycle-accurate basis, then RTLM.sub.ts and HLM.sub.ts are equivalent on a stream-accurate basis.

Each sub-miter is constructed as follows.

For a first sub-miter, RTLM.sub.ts is tested for equivalence with HLM.sub.ts under conditions that correspond to RTLM.sub.ts operating at "full speed." Put differently, every time RTLM.sub.ts can accept a set of data inputs, it is able to do so. HLM.sub.ts is tested for equivalence with RTLM.sub.ts under conditions that constrain its inputs to be the same as whatever RTLM.sub.ts indicates it is able to accept. Thus the first sub-miter determines equivalence between a fully exercised RTLM.sub.ts and a HLM.sub.ts limited to those inputs that exercise RTLM.sub.ts.

If the result of comparing RTLM.sub.ts to HLM.sub.ts is successful, then it is known that for any inputs acceptable by RTLM.sub.ts, HLM.sub.ts will produce stream-equivalent output. However, it is still not known whether, for the "full" range of inputs acceptable to HLM.sub.ts, if RTLM.sub.ts can produce stream-equivalent outputs. This is accomplished by reversing the roles of RTLM.sub.ts and HLM.sub.ts in the second sub-miter.

Put more symbolically, it is first shown by the first sub-miter that the set of outputs (or SOO) of RTLM.sub.ts (or SOO(RTLM.sub.ts)) is a subset of the SOO of HLM.sub.ts (or SOO(HLM.sub.ts)). Put in mathematical relation form: SOO(RTLM.sub.ts).OR right.SOO(HLM.sub.ts)

By reversing the roles of RTLM.sub.ts and HLM.sub.ts, the second sub-miter can show that: SOO(HLM.sub.ts).OR right.SOO(RTLM.sub.ts)

The only way both relations can be true is if the following is true: SOO(HLM.sub.ts)=SOO(RTLM.sub.ts)

An example stream-based combining structure, suitable for constructing the first and second sub-miters, is presented.

Since the first and second sub-miters can be constructed in an identical way, except for the roles of RTLM.sub.DFG and HLM.sub.DFG being reversed, just the construction of the first sub-miter is addressed.

The first sub-miter is constructed to allow DFG 2623 to process data as soon as it is able to, while not guaranteeing the same for DFG 2624.

DFGs 2623 and 2624, of a sub-miter, can produce their output packets at different times. A FIFO can be used to store outputs such that they can be compared. An example operation for such FIFO is presented.

The stream-based combining structure, presented herein, can be used in conjunction with any formal analysis tool. The stream-based combining structure, presented herein, can be used without the step of classifying the first and second designs that it couples.

When the stream-based combining structure is used without the step of classification, any appropriate representation can be used for the stream-based combining structure and for the first and second designs to be coupled. For the first and second designs to be coupled, each can be treated as a "black box," with just information on its inputs and outputs provided.

4.2.5 Summary of Error

The error combining structure can be applied if it is not known, for the classifications of the two DFGs, what combining structure, if any, should be applied.

4.3 Summary of Generating the Test Bench

Once a combining structure has been selected, MT.sub.ts can be generated.

4.4 Summary of Other Applications

The techniques of test bench generation presented herein are discussed primarily with respect to combining DFGs of an RTLM and HLM, for purposes of applying the equivalence determination process described herein. However, the test bench generation techniques presented herein can be used for combining any first DFG and second DFG, regardless of the source from which the first and second DFGs are derived. The resulting combination, of first DFG, second DFG and combining structure, can be used in conjunction with any formal analysis technique.

Furthermore, the test bench generation techniques presented herein can be used for combining a first and second design, where the first and second designs are not specified as DFGs. The step of classifying each of the first and second designs, in order to determine the applicable combining structure, only requires that the first and second designs be expressed in a representation that provides the necessary structural information. By way of example, a netlist representation could be used instead of a DFG representation.

5. Summary of Initialization of the Miter Timestep

As discussed above, in order to compare RTLM.sub.ts and HLM.sub.ts for potential equivalency, they may need to be set to equivalent initial states.

Suitable initial states of RTLM and HLM, for initializing RTLM.sub.ts and HLM.sub.ts, can be determined.

Whenever both RTLM and HLM are ready, the initial states for RTLM and HLM can be translated into appropriate initial values for RTLM.sub.ts and HLM.sub.ts.

For an HLM that is compiled, its initial state can be determined by the following process.

Before partially executing the HLM, the user can provide information on the location within the HLM where the initialization phase is finished, and a breakpoint can be set at the location.

An HLM written in a compiled language (such as C or C++) can be compiled such that debugging information is available. Debugging information, in a compiled executable, can be used to extract the values of program variables of the HLM when it stopped at the breakpoint.

An operating system process, under which the HLM runs, can be created.

For an HLM that is run with a dynamic (or run-time) linker, operating system libraries used by the HLM can be linked-to at run-time. At the time of such library linking, rather than linking the HLM's typical run-time library, a special "Interceptor Library" can be linked to.

An Interceptor Library is so-called because it can intercept operating system calls the HLM might make, such as those related to memory allocation, memory reallocation or memory deallocation.

The Interceptor Library functions can call the actual functions of the applicable operating system. Before returning, the Interceptor Library functions can record, for post run-time use, information about the currently allocated memory blocks.

The HLM can be run until the breakpoint is reached, at which point it is in an appropriate initial state to be used for setting the initial states of RTLM.sub.ts and HLM.sub.ts. Because the HLM was executed with debugging information enabled, and with the Interceptor Library substituted for certain operating system procedures, the necessary information is available for the process of setting RTLM.sub.ts and HLM.sub.ts to initial states.

Once initial states for RTLM and HLM are available, a process is presented for translating their values into appropriate initial values for the initial timesteps of RTLM.sub.ts and HLM.sub.ts.

An example initialization, for the control and datapath present-state inputs of an initial timestep, is presented.

The techniques of partial HLM execution, and of accessing the values of the partially executed HLM, are presented herein primarily with respect to initializing a DFG representation of the HLM. Furthermore, the discussion presented herein focuses primarily on applying the initialized DFGs to the equivalence determining process presented herein.

However, the techniques of partial HLM execution, and of accessing the values of the partially executed HLM, can be used in conjunction with initializing any formal analysis tool (including those that do not use DFGs), where the representation subject to formal analysis is derived from an HLM.

6. Summary of Verification with CERs

Pseudo-code, for a core equivalence-determining process, is presented. Before presenting the pseudo-code, an example application of a core equivalence-determining process is presented in overview form.

A core equivalence-determining process can be performed by invoking a pseudo-code procedure called "equivalence_checking_with_CERs." The hierarchical manner, in which procedures are invoked by equivalence_checking_with_CERs, is diagrammed.

7. Summary of Example

To illustrate the operation of the pseudo-code an example simulation is presented.

BRIEF DESCRIPTION OF THE DRAWINGS

The accompanying drawings, that are incorporated in and constitute a part of this specification, illustrate several embodiments of the invention and, together with the description, serve to explain the principles of the invention:

FIG. 1 presents a high-level overview of an equivalency testing system, where novel sub-systems are drawn with dashed lines.

FIG. 2A defines certain global variables and symbolic constants that are used throughout the pseudo-code of FIGS. 24 to 30.

FIG. 2B depicts a pseudo-coded procedure called "test_for_equivalency" that represents an example equivalency testing system that operates in accordance with teachings of the present inventions.

FIG. 3A presents an example of C or C++ code from which a CFG can be produced.

FIG. 3B presents an example CFG that can be symbolically simulated to produce a DFG.

FIGS. 4A-4G depict steps in the creation of a DFG by symbolic simulation.

FIGS. 5A-5F depict intermediate data structures, that can be used during DFG production by symbolic simulation, referred to herein as "output-lists."

FIGS. 6A-6H depict different states of a queue, referred to herein as an "execution path queue," that can be used to perform a breadth-first traversal of an HLM.sub.CFG.

FIGS. 7A-7F depict pseudo-code for symbolic simulation.

FIGS. 8A-8N and 8P-8Q (there is no FIG. 8O) depict an example of how the prioritization procedure, of FIGS. 9A-9B, can be applied.

FIGS. 9A-9B show pseudo-code for assigning priorities as part of a preprocessing step to symbolic simulation.

FIG. 10A depicts an example DFG for conversion into the timestep form.

FIG. 10B shows a conversion of the DFG of FIG. 10A into the timestep form.

FIG. 11 shows a pseudo-code implementation for use in determining whether a DFG primary output is of DFG class "combinational."

FIG. 12 shows a pseudo-code implementation for use in determining whether a DFG primary output is of DFG class "pipelined."

FIG. 13 depicts a combinational combining structure.

FIG. 14 depicts a cycle-accurate combining structure.

FIG. 15 depicts a pipelined combining structure.

FIG. 16A depicts a stream-based combining structure.

FIG. 16B depicts a process to allow DFG 2623 to process data as soon as it is able to, while not guaranteeing the same for DFG 2624.

FIG. 16C depicts a more detailed view of an example operation of a FIFO controller.

FIG. 17 depicts an example decision matrix for selecting an appropriate combining structure.

FIG. 18A depicts a flowchart for initialization of an initial timestep.

FIG. 18B presents an example initialization of the control and datapath present-state inputs for an initial timestep.

FIG. 19 presents an overview of an equivalence-determining process.

FIG. 20A presents, for an example application of an equivalence-determining process, an HLM.sub.DFG and RTLM.sub.DFG.

FIG. 20B presents, for an example application of an equivalence-determining process, DFGs 4200 and 4201 in timestep form.

FIGS. 21A-21N and 21P-21Q (there is no FIG. 21O) present an example application of a core equivalence-determining process.

FIGS. 22A-22K depict detailed actions in a first and second call to Add_CER.

FIG. 23 depicts the hierarchical manner in which procedures are invoked by equivalence_checking_with_CERs.

FIG. 24 depicts pseudo-code for a core equivalence-determining process called equivalence_checking_with_CERs.

FIGS. 25A-25B depict pseudo-code for find_FPT.

FIG. 26 depicts pseudo-code for propagate_SDVs.

FIG. 27 depicts pseudo-code for TF_prop.

FIGS. 28A-28B depict pseudo-code for Add_CER.

FIGS. 29A-29E depict detailed actions in a first and second call to Add_CER.

FIG. 30 depicts example procedures for determining a CER transitive closure and for labeling.

FIG. 31 depicts a data processing system for executing the equivalence determining architecture of the present invention, or for executing each of its component sub-systems individually.

DETAILED DESCRIPTION OF PREFERRED EMBODIMENTS

Reference will now be made in detail to preferred embodiments of the invention, examples of which are illustrated in the accompanying drawings. Wherever possible, the same reference numbers will be used throughout the drawings to refer to the same or like parts.

TABLE-US-00001 Table of Contents to Detailed Description 1. Equivalency Testing System 1.1. Conversion of HLM and RTLM to DFGs 1.1.1. Overview 1.1.2. Within test_for_equivalency 1.2. Conversion Into Timestep Form 1.2.1. Overview 1.2.2. Within test_for_equivalency 1.3. Combining Structure Generation 1.3.1. Overview 1.3.2. Symbolic Data Values (SDVs) and Conditional Equivalence Relations (CERs) 1.3.2.1. Integer SDV 1.3.2.2. ITE SDV 1.3.2.3. Symbolic Boolean Expression 1.3.2.4. CERs 1.3.2.5. MTBDDs 1.3.3. Identification Of Nodes As Control or Datapath 1.3.4. Within test_for_equivalency 1.4. Initializations 1.4.1. Overview 1.4.2. Active Timestep Range 1.4.3. SDV Propagation Processes 1.4.4. Within test_for_equivalency 1.5. Equivalence Checking With CERs 1.5.1. Overview 1.5.2. Other Applications 1.5.3. Ready For Reencoding 1.5.4. Fixed-Point Target (FPT) 1.5.5. Counter-Example Generation 1.5.6. Within test_for_equivalency 2. HLM to DFG Conversion By Symbolic Simulation 2.1. Overview 2.2. Other Applications 2.3. For HLM and RTLM Comparison 2.4. Initialization For CFG Traversal 2.5. Loop For Breadth-First Traversal Of CFG 2.5.1. Two EPs Point To Same CFG Node 2.5.2. Top EP Points To Conditional CFG Node 2.5.3. Top EP Points To Assignment CFG Node 2.5.4. Top EP Points To END CFG Node 2.6. Post-CFG-Traversal Processing 2.7. Handling Loops During Symbolic Simulation 2.8. Optimization: Global Priority Scheduling 2.8.1. Overview 2.8.2. Prioritization Pseudo-code 2.8.2.1. computePriorities 2.8.2.2. adjustPredecessors 2.8.3. Example Prioritization 2.8.3.1. First Iteration 2.8.3.2. Second Iteration 2.8.3.3. Third Iteration 2.8.3.4. Fourth Iteration 2.8.3.5. Fifth Iteration 2.8.3.6. Sixth Iteration 2.8.3.7. Seventh Iteration 2.8.3.8. Eighth Iteration 2.8.3.9. Ninth Iteration 2.8.3.10. Tenth Iteration 2.8.3.11. Eleventh Iteration 2.8.3.12. Twelfth Iteration 2.9. Other Optimizations 3. The Timestep Form 4. Test Bench Generation 4.1. Classifying RTLM.sub.ts and HLM.sub.ts 4.1.1. Combinational 4.1.2. Pipelined 4.1.3. Handshaking 4.1.4. Unknown 4.2. Combining Structure Selection 4.2.1. Combinational 4.2.2. Cycle-accurate 4.2.3. Pipelined 4.2.4. Stream-Based 4.2.4.1. Overview 4.2.4.2. Input of Data to RTLM.sub.ts and HLM.sub.ts DFGs 4.2.4.3. Output of Data from RTLM and HLM DFGs 4.2.4.4. Other Applications 4.2.5. Error 4.3. Generating The Test Bench 4.3.1. Overview 4.3.2. Reset Logic 4.3.3. Clocking Logic 4.3.4. Use of Libraries 4.4. Other Applications 5. Initialization Of The Miter Timestep 5.1. Initializing RTLM 5.2. Initializing HLM 5.3. Translation To Initial Timestep 5.4. Example 5.5. Other Applications 6. Verification With CERs 6.1.1. Overview 6.1.2. equivalence_checking_with_CERs 6.1.3. label_datapath_nodes 6.1.4. initialize_timestep_state 6.1.5. initialize_timestep_inputs 6.1.6. find_FPT 6.1.6.1. Overview 6.1.6.2. Further Details 6.1.7. eval_control_exps 6.1.8. propagate_SDVs 6.1.9. reencode 6.1.10. mux_prop 6.1.11. TF_prop 6.1.12. Add_CER 6.1.12.1. Overview 6.1.12.2. Pseudo-Code 7. Example 7.1. test_for_equivalency 7.2. equivalence_checking_with_CERs 7.3. find_FPT 7.3.1. Application of find_FPT to FIG. 21B 7.3.2. Application of find_FPT to FIG. 21L 7.4. eval_control_exps 7.5. propagate_SDVs 7.5.1. Applied to FIG. 21C 7.5.2. Applied to FIG. 21G 7.5.3. Applied to FIG. 21L 7.6. TF_prop 7.6.1. Applied to FIG. 21D 7.6.2. Applied to FIG. 21H 7.6.2.1. Pair (TF 4300, TF 4302) 7.6.2.2. Pair (TF 4301, TF 4302) 7.6.3. Applied to FIG. 21M 7.7. Add_CER 7.7.1. Applied to FIG. 22A 7.7.2. Applied to FIG. 22E 8. Hardware Environment 9. Glossary of Selected Terms

1. Equivalency Testing System

This section begins by presenting a high-level overview of an equivalency testing system (see FIG. 1, where novel sub-systems are drawn with dashed lines). Then, each of sub-sections 1.1 to 1.5 addresses, in further detail, a major component of such a system. To provide an example overall framework for presenting sub-sections 1.1 to 1.5, each of these sub-sections relates the component it discusses to a pseudo-coded procedure called "test_for_equivalency" (shown in FIG. 2B). test_for_equivalency presents an example equivalency testing system that operates in accordance with teachings of the present inventions. Each of sections 2-6, that follow this section 1, addresses a major component, of an equivalency testing system, in much greater detail. FIG. 2A defines certain global variables and symbolic constants that are used throughout the pseudo-code of FIGS. 24 to 30.

Both the RTLM and HLM, that are to be compared for equivalence, are converted into DFGs, called RTLM.sub.DFG and HLM.sub.DFG. RTLM.sub.DFG can be determined by any suitable known means, but HLM.sub.DFG can be determined by a new technique, of symbolic simulation of the HLM, presented herein. FIG. 1 presents an input RTLM 1020 and HLM 1010. A novel HLM to DFG conversion process 1011 is used to produce HLM.sub.DFG 1012. An RTLM to DFG conversion process 1021 is used to produce RTLM.sub.DFG 1022.

RTLM.sub.DFG and HLM.sub.DFG are put into a timestep form, referred to as RTLM.sub.ts and HLM.sub.ts. An arbitrary timestep "t," of RTLM.sub.ts and HLM.sub.ts, can be referred to as RTLM.sub.ts[t] and HLM.sub.ts[t]. FIG. 1 presents an HLM.sub.DFG to timestep conversion process 1013 that produces HLM.sub.ts 1014. FIG. 1 presents an RTLM.sub.DFG to timestep conversion process 1023 that produces RTLM.sub.ts 1024.

A combining structure CS.sub.ts can be selected, that couples to RTLM.sub.ts and HLM.sub.ts. The combining structure has the following property: if, for a timestep t, RTLM.sub.ts[t] and HLM.sub.ts[t] are equivalent according to a given (or automatically determined) notion of equivalence, then CS.sub.ts[t] will detect this. Different types of combining structures can be selected depending upon the type of circuit represented by RTLM.sub.ts and HLM.sub.ts. Novel techniques, for classifying each of RTLM.sub.ts and HLM.sub.ts, and for selecting a suitable CS.sub.ts, are presented. In addition, novel forms of combining structure, suitable in general for formal verification, are presented. For example, a novel combining structure, for showing that RTLM.sub.ts and HLM.sub.ts are stream-equivalent, is presented.

FIG. 1 presents a combining structure generation process 1031 that receives, as input, HLM.sub.ts 1014 and RTLM.sub.ts 1024. Process 1031 produces CS.sub.ts 1032.

The complete system, comprised of RTLM.sub.ts[t], HLM.sub.ts[t] and CS.sub.ts[t], will be referred to herein as "miter." The miter can have certain parts designated as representing control logic and other parts designated as representing datapath logic. Parts of the miter designated as control can be subject to a known form of bit-level equivalence checking. Parts of the miter designated as datapath are subject to a new form of equivalence checking that works above the bit level, using a node value indicator referred to herein as a "symbolic data value" or SDV, and that seeks to prove equivalence by a form of inductive theorem proving. Formation of the miter, and its processing for equivalence checking, is represented in FIG. 1 by HLM.sub.ts 1014, CS.sub.ts 1032 and RTLM.sub.ts 1024 feeding into equivalence determination process 1033.

In the datapath portions of the miter, equivalence checking can be conducted at a higher level of abstraction if one is not interested in actual data values, but only in whether RTLM.sub.ts and HLM.sub.ts produce the same data (given that they receive the same input data). In this case, integers can be used as an abstraction for datapath data values: if two signals have the same integer number, this signifies that their actual data values are the same; if two signals have the different integer numbers, this signifies their actual data values are different. To refer to such integer values, the term "integer SDV" can be used.

If it can be proven that RTLM.sub.ts and HLM.sub.ts both produce the same SDVs on all of their primary outputs, and for all times, it is proven that both designs are equivalent. In order to determine the SDVs of the primary outputs of RTLM.sub.ts and HLM.sub.ts, input SDVs must be propagated through the miter.

A novel form of inductive theorem proving starts from initial conditions for the first timestep for the miter (i.e., for timestep RTLM.sub.ts[0], HLM.sub.ts[0] and CS.sub.ts[0]). The initial state for RTLM.sub.ts[0] can be determined by any suitable known means, but the initial state for HLM.sub.ts[0] can be determined by a new technique, of partial execution of the HLM, presented herein. FIG. 1 represents the initialization of HLM.sub.ts 1014 and RTLM.sub.ts 1024 as follows. HLM 1010, RTLM 1020, HLM.sub.ts 1014 and RTLM.sub.ts 1024 all serve as inputs to an initial state determination process 1030. Initial state determination process 1030 sets HLM.sub.