Synopsys, Inc.

Carl Preston Pixley

Alfred Koelbl

Himanshu Jain

Jerry R Burch

Per Mattias Bjesse

James Herbert Kukula

Sudipta Kundu

Robert F Damiano

Brian Eugene Lockyear

Methods and apparatuses are described for sharing inductive invariants while performing formal verification of a circuit design. Specifically, some embodiments assume at least an inductive invariant for a property to be true while proving another property. According to one definition, an inductive invariant of a property is an inductive assertion such that all states that satisfy the inductive assertion also satisfy the property. According to one definition, an inductive assertion describes a set of states that includes all legal initial states of the circuit design and that is closed under a transition relation that models the circuit design.

Invariant sharing to speed up formal verification

Methods and apparatuses are described for proving equivalence between two or more circuit designs that include one or more division circuits and/or one or more square-root circuits. Some embodiments analyze the circuit designs to determine an input relationship between the inputs of two division (or square-root) circuits. Next, the embodiments determine an output relationship between the outputs of two division (or square-root) circuits based on the input relationship. The embodiments then prove equivalence between the circuit designs by using the input and output relationships.

Equivalence checking between two or more circuit designs that include square root circuits

A method for equivalence checking includes obtaining a first and a second representation for a semiconductor design and applying a set of inputs to both representations. The outputs of the first representation are compared to the outputs of the second representation. If a mismatch is found, the starting states for the first and second representations are evaluated using a model checker to see if they are reachable from a known legal state such as reset state for that representation. If both of the starting states are reachable, the mismatch is a real mismatch providing a counter-example of the equivalence of the two representations. If one or both of the starting states are unreachable, the mismatch is a spurious mismatch and the model checker can be used to generate an invariant to preclude those starting states in future iterations of the equivalence checker.

Elimination of illegal states within equivalence checking

Equivalence checking between two or more circuit designs that include division circuits

A design is verified by using equivalence checking to compare a word-level description of the design to a bit-level description of the design. A word-level data flow graph (DFG) based on the word-level description and a bit-level DFG is obtained. Structural analysis is used to reduce the graphs and partition them into smaller portions for the equivalence checking. The analysis includes searching the bit-level DFG to find partial-product encoding and removing redundancy from the bit-level DFG. A reference model with architectural information from the bit-level DFG is created based on the word-level DFG. The reference model is reduced and equivalence checked against the bit-level DFG to determine if the word-level description is equivalent to the bit-level description.

Equivalence checking using structural analysis on data flow graphs

Methods and apparatuses are described for formally verifying a bit-serial division circuit design or a bit-serial square-root circuit design. Some embodiments formally verify a bit-serial division circuit design using a set of properties that can be efficiently proven using a bit-level solver. In some embodiments, the set of properties that are used for verifying a bit-serial division circuit design does not include any terms that multiply a w-bit partial quotient with the divisor. Some embodiments formally verify a bit-serial square-root circuit design using a set of properties that can be efficiently proven using a bit-level solver. In some embodiments, the set of properties that are used for verifying a bit-serial square-root circuit design does not include any terms that compute a square of a w-bit partial square-root.

Formal verification of bit-serial division and bit-serial square-root circuit designs

An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLMand HLM. RTLMand HLMare then put into timestep form and are called RTLMand HLM. A test bench CSis selected that couples RTLMand HLM. The combination of RTLM[t], HLM[t] and CS[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[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.

Formally checking equivalence using equivalence relationships

Method and apparatus for performing formal verification using data-flow graphs

Method and apparatus for formally checking equivalence using equivalence relationships

One embodiment of the present invention provides a system that formally proves the functional equivalence of pipelined designs. First, the system receives a specification for a first pipelined design, which includes a first memory system, and a specification for a second pipelined design, which includes a second memory system. Next, the system determines a correspondence between operations on the first memory system and corresponding operations on the second memory system. This correspondence enables memory operations to be represented in a combinational form based on design inputs, thereby allowing both memory systems to be logically abstracted out of their respective designs. After the memory systems have been abstracted out, the system compares the combinational outputs of the first pipelined design and the combinational outputs of the second pipelined design to verify that the designs are functionally equivalent.

Formally proving the functional equivalence of pipelined designs containing memories

One embodiment of the present invention provides a system that produces a non-canonical data flow graph (DFG) structure by symbolic simulation of an input representation for a high-level model (HLM). This system considers all scenarios for flow-of-control for the HLM, and represents the flows-of-control under consideration with execution paths. Then, the system determines a set of next execution paths to be processed from a set of active execution paths, and determines a set of indication points, in the input representation, from the set of next execution paths. The system then determines a next symbolic simulation operation to be performed for producing the non-canonical DFG structure using the indication points, and performs the next symbolic simulation operation on the input representation to produce the non-canonical DFG structure. Symbolic simulation can be used with any application utilizing non-canonical representations of an HLM.

Method and apparatus for production of data-flow-graphs by symbolic simulation

An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLMand HLM. RTLMand HLMare then put into timestep form and are called RTLMand HLM. A test bench CSis selected that couples RTLMand HLM. The combination of RTLM[t], HLM[t] and CS[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. The theorem proving starts from initial conditions for HLM[t] determined by partial execution of the HLM. A CSfor proving stream-based equivalence is presented. The CSoperates by allowing one DFG to process data as soon as it can, while not guaranteeing the same for a second DFG. The stream-based combining structure can be used in with any formal analysis tool.

Method and apparatus for formally comparing stream-based designs

An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLMand HLM. RTLMand HLMare then put into timestep form and are called RTLMand HLM. A test bench CSis selected that couples RTLMand HLM. The combination of RTLM[t], HLM[t] and CS[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. The theorem proving starts from initial conditions for HLM[t] determined by partial execution of the HLM. CScan be selected depending upon a classification of RTLMand HLM. Techniques for classifying RTLMand HLM, and for selecting a suitable CS, are presented. The classifications can operate on non-DFG representations. The CSgeneration techniques can be used with any formal analysis technique.

Growing community of inventors

Beaverton, OR, United States of America

Carl Preston Pixley