Freescale Semiconductor,inc.

Advanced Micro Devices Corporation

Freescale Semiconductors Inc.

Xiushan Feng

Jayanta Bhadra

Xiao Sun

Ashish Goel

Yinfang Lin

Jayanta Bahadra

Scott R Little

Ross L Patterson

An approach is provided in which an equivalence class generator selects a configurable module that includes control points and configuration parameters. The configuration parameters define a parameter state space of the configurable module. The equivalence class generator utilizes the control points to generate equivalence classes, which include class representatives that indicate values for the configuration parameters. Next, one of the class representatives are selected and verified from each of the equivalence classes. In turn, the verification of the class representatives verifies the parameter state space of the configurable module.

Equivalence classes over parameter state space

A technique for determining whether an integrated circuit design is susceptible to glitches includes identifying storage elements in an original register-transfer level (RTL) file of the integrated circuit design and identifying clock signals for each of the storage elements in the original RTL file. The technique also includes generating respective assertions for each of the identified clock signals and identifying potential glitchy logic in respective clock paths for each of the identified clock signals. Finally, the technique includes inserting, at the potential glitchy logic, glitches in each of the respective clock paths of the original RTL file to provide a modified RTL file and executing an RTL simulation using the modified RTL file and the respective assertions.

Integrated circuit design verification through forced clock glitches

An approach is provided in which a power design verification system retrieves a power intent data corresponding to a power design, which identifies the power design's power modes and power mode transition conditions. The power design verification system selects one of the power mode transition conditions, which identifies input signals that invoke a transition from a first power mode to a second power mode. In turn, the power design verification system generates simulation stimuli based upon the identified input signals and simulates the power design utilizing the generated simulation stimuli accordingly.

Verification of design derived from power intent

An approach is provided in which a computing system retrieves a design description that corresponds to an electronic circuit design. The computing system selects an assertion corresponding to the electronic circuit design, which includes one or more assertion signal identifiers corresponding to one or more description signal points included in the design description. Next, the computing system creates a partitioned region from the design description based upon the description signal points. The computing system compiles and verifies the partitioned region that, in turn, verifies the electronic circuit design.

Assertion-based design partitioning

An approach is provided in which a formal verification tool sends a condition signal to a first circuit instance and to a second circuit instance, which are both instances of an electric circuit design. The formal verification tool selects a common input port and sends a first input value to the common input port of the first circuit instance and sends a second input value, which is different than the first input value, to the common input port of the second circuit instance. In turn, the first circuit instance generates a first output value and the second circuit instance generates a second instance value, which are utilized to verify dependencies between the electronic circuit's input ports and output ports.

Automatic verification of dependency

One set of illegal vector sequences is manually generated for a circuit design and a symbolic simulator is used to automatically generate another set of illegal vector sequences for the circuit design. For verification purposes, the relationship between the manually generated set and the automatically generated set is determined. Prior to determining this relationship, one or both of the sets are simplified. One simplification technique includes replacing pairs of illegal vector sequences that are the same except at one bit position with a more general illegal vector sequence representative of both illegal vector sequences of the pair. Another simplification technique includes sorting the illegal vector sequences in a list having a sort order from most general to most specific and then identifying illegal vector sequences that are redundant in view of one or more other illegal vector sequences prior in the sort order based on a binary decision diagram (BDD)-based analysis that sequences through the sorted list in its sort order.

Growing community of inventors

Austin, TX, United States of America

Xiushan Feng