International Business Machines Corporation

Peng Fei Gou

Heng Liu

Yang Fan Liu

Zhen Peng Zuo

Yang Liu

Dan Liu

Bodo Hoppe

Yan Lu

Chen Qian

Lei Zhang

Yufei Li

Jin Jiang

Yong Feng Pan

Hua Xin Yao

ZeQiang Xiao

The computer processor identifies a first shared set of input ports that are common to a first hardware model and a second hardware model and a second shared set of input ports that are common to a first reference model and a second reference model. The computer processor selects logic of the first hardware model and logic of the second hardware model that are each traceable to the first shared set of input ports and selects logic of the first reference model and logic of the second reference model that are each traceable to the second shared set of input ports. The computer processor determines that the logic of the second hardware model and the logic of the second reference model have verified logic by determining that the logic of the first hardware model is equivalent to the logic of the second hardware model and the logic of the first reference model is equivalent to the logic of the second reference model.

Hardware incremental model checking verification

A symmetrical multi-processing (SMP) node, a distributed SMP (DSMP) system comprising a plurality of SMP nodes, and a method implemented in the SMP node are disclosed. The SMP node comprises: a plurality of processors, a memory coupled to the plurality of processors, and a memory coherent proxy coupled to the plurality of processors through a coherent accelerator interface. The memory coherent proxy is configured to manage statuses of cache lines in the memory.

Symmetrical multi-processing node

An apparatus for verification includes a processing module, a data collection module, an engine selection module and an engine execution module. The processing module processes a netlist using a plurality of engines. The netlist includes components and nodes of an integrated circuit design. Each engine includes an algorithm for verification of the integrated circuit design. The data collection module stores, for each engine, execution results for the engine for a plurality of netlists, the results stored in a history buffer. The engine selection module, for a current netlist, calculates using execution results in the history buffer which engine of the plurality of engines has a highest predicted performance and selects the engine with the highest predicted performance. The engine execution module executes the current netlist using the selected engine to produce execution results, reports the execution results and stores the execution results in the history buffer.

Verification algorithm engine selection

An apparatus for model splitting includes an extraction module that extracts netlist parameters from a static netlist. The netlist parameters include node parameters of each node of the static netlist. The node parameters include node connection information and execution cycle information. The nodes of the static netlist include nodes of an integrated circuit design from an input to an output. A split node module analyzes, using the netlist parameters, each node in a cycle and determines if each node is a potential split node, which is a node with a projected sub-proof execution time less than a time limit. A split chain module determines if a split chain exists. The split chain includes a connection between potential split nodes from the input to the output at each execution cycle. A reporting module reports nodes of a split chain in response to determining that a split chain exists.

Integrated circuit design model splitting for formal verification

A method and apparatus for ranking combinations of mutants, test cases and random seeds in mutation testing, comprising obtaining, based on a signal of a test case target, logic gates related to the signal of the test case target and mutants on the related logic gates, for a compiled integrated circuit under test; calculating distances between the mutants and the signal of the test case target; performing a circuit simulation on the compiled integrated circuit under test to obtain activation cycle numbers corresponding to combinations of the mutants, test cases and random seeds; obtaining activation cycle number variances corresponding to combinations of the mutants and the test cases; and ranking the combinations of the mutants, the test cases and the random seeds based on the distances, the activation cycle numbers and the activation cycle number variances. The invention can reduce the probability that the mutation simulation selects equivalent mutants.

Ranking combinations of mutants, test cases and random seeds in mutation testing

An integrated circuit (IC) can dynamically manage memory communication paths between multiple processors and multiple memory modules. The IC can include upstream logic that performs data conversion and provides memory communication paths between each processor and a corresponding upstream port. An interconnect layer in the IC can be electrically coupled to the upstream ports to multiple downstream ports. An interconnect management processor electrically coupled to the interconnect layer can respond to received commands by executing an allocation program stored in a read-only memory (ROM) that dynamically establishes and terminates memory communication paths between the upstream ports and the downstream ports. A memory interface layer in the IC can be electrically coupled to the downstream ports and to the memory modules, and can provide, through corresponding memory physical interfaces, memory communication paths between the multiple downstream ports and corresponding memory modules.

Elastic memory expansion chip architecture

Determining a quality parameter for a verification environment for a register-transfer level hardware design language description of a hardware design. A netlist is generated from the hardware design language description. A list of hardware design outputs is generated, and logical paths in the netlist are generated based on the list of hardware design outputs. Furthermore, a modified netlist involving logical paths is generated by determining whether a gate is selected as an insertion point, and selecting a fault type, which is part of the efficiency vector for the selected gate in the netlist and inserting a mutant. Additionally, a fault simulation is performed and the quality parameter for the verification environment is determined from the fault simulation and the simulation result data.

Growing community of inventors

Shanghai, China

Peng Fei Gou