Synopsys, Inc.

Synopsis Incorporated

Alfred Koelbl

Carl Preston Pixley

Jerry R Burch

Per Mattias Bjesse

Sudipta Kundu

Arunava Saha

Sandeep Jana

Naiyong Jin

Pratik Mahajan

A security verification system performs security verification of a circuit design. The security verification system simplifies formal security verification of the circuit design by replacing circuit blocks of the circuit with black box circuit blocks. The security verification system instruments the circuit design so that black-boxing can be performed for security verification without changing the security decision over the data paths. The security verification system uses dependence information of the inputs and outputs of the black box to connect inputs of the circuit block with outputs of the circuit block. The black-box circuit block keeps the logic inside the cone of influence of clocks and resets. The system performs security verification of the circuit design by proving a non-interference property of the instrumented circuit design.

Scalable formal security verification of circuit designs

The fault analysis problem is modelled by automatically creating additional properties (fault properties) and constraints based on a plurality of injected faults and existing user assertions. These fault properties and constraints are sent to formal verification in a single run to qualify all of the faults together, rather than sequentially checking each fault in a separate formal verification run.

Efficient mechanism of fault qualification using formal verification

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

Some embodiments of the present invention provide techniques and systems for determining whether a high-level model (HLM) for a circuit design is equivalent to a register-transfer-level (RTL) model for the circuit design. During operation, a system can identify a set of checkpoints. Each checkpoint can be associated with a characteristic function defined over the states of a finite-state-machine (FSM) representation of the HLM, a characteristic function defined over the states of an FSM representation of the RTL model, and an invariant defined over a set of variables in the HLM and a set of registers in the RTL model. Next, the system can generate a set of invariant proof problems, wherein each invariant proof problem corresponds to a transition between two checkpoints in the set of checkpoints. The system can then determine whether the HLM is equivalent to the RTL model by solving the set of invariant proof problems.

Formal equivalence checking between two models of a circuit design using checkpoints

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.

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. The user specifies a location within the HLM where initialization is finished. The HLM is executed, with procedure calls related to memory allocation intercepted and allocation information collected. The initialization techniques can be used with any formal analysis tool operating on representations derived from an HLM.

Growing community of inventors

Dachau, Germany

Alfred Koelbl