International Business Machines Corporation

Eli Arbel

Oleg Rokhlenko

Cynthia Rae Eisner

Karen Frida Yorav

Shiri Moran

Alexander Itskovich

Bodo Hoppe

Oded Fuhrmann

Erez Barak

Ziv Nevo

Udo Krautz

Shaked Flur

David J Levitt

Michael Shamis

Maja Vukovic

Pradip Bose

Giora Biran

Ruchir Puri

K Paul Muller

Haoxing Ren

Prabhakar Nandavar Kudva

Saurabh Sinha

Rachel Tzoref-Brill

Nicolas Maeding

Ilan Beer

Victor N Kravets

David John Geiger

Smita Krishnaswamy

Cindy Eisner

Oshri Adler

Sergey Novimov

A system, computer program product, and method are presented for executing a validation test on at least a portion of a refactored application. The refactored application is resident within a partitioned computing architecture including a plurality of partitions and communication between the partitions uses one or more boundary methods. The refactored application is at least partially similar to a transformed monolithic application. The method includes automatically generating one or more test sequences for exercising one or more functional behaviors for each boundary method of the one or more boundary methods.

Validating inter-partition communication in microservice decomposition

An unobservable cycle for at least one latch in a circuit design is detected. The unobservable cycle indicates that the at least one latch is not observable to downstream logic in the circuit design. A coverage event is generated to identify the unobservable cycle for the at least one latch. The coverage event is tracked to detect a state associated with the unobservable cycle and a state change cycle. The state change cycle is determined based on a simulation technique. A redundant switching of the at least one latch based on the state associated with the unobservable cycle and the state change cycle is determined. Furthermore, manufacturing of a circuit based on the circuit design is at least initiated. The circuit design is modified to prevent the redundant switching of the at least one latch.

Modifying circuits to prevent redundant switching

A computer-implemented method may include retrieving a design netlist with a processor, identifying, via the processor, a logic structure in the design netlist, generating, via the processor, a driver based on the logic structure, applying, via the processor, a simulation and a formal model based on the driver, and testing, via the processor, an output of the simulation and the formal model.

Assuring chip reliability with automatic generation of drivers and assertions

A mechanism is provided for validating overall resilience and security characteristics of a sub-component chip design. For each instance of a resiliency template identified as appearing in a design netlist of the sub-component chip design thereby forming one or more identified resiliency sections, a determination is made as to whether an output of the design netlist where an error signal is output interconnects to the one or more identified resiliency sections of the design netlist. Responsive to the one or more identified resiliency sections interconnecting to the output of the design netlist where the error signal is output, one or more identified resiliency sections are marked as being protected by the error signal. An identification of the one or more identified resiliency sections and an identification of the error signal protecting the one or more identified resiliency sections are output to a design team.

Template matching for resilience and security characteristics of sub-component chip designs

A method, apparatus and product for detecting corresponding paths in combinationally equivalent circuit designs. The method comprising: obtaining a first circuit design and a second circuit design, the first and second circuit designs have corresponding sets of input and output elements; obtaining a path in the first circuit design, the path commencing in an input element and ending in an output element, wherein the input element and the output element are connected by combinational logic elements; automatically extracting, by a computer, a sensitization function of the path in the first circuit design; and automatically determining, by the computer, one or more paths in the second circuit design which are sensitized by the sensitization function of the path.

Detecting corresponding paths in combinationally equivalent circuit designs

A circuit design, responsive the input signals, may be obtained and processed. The circuit design may define connections between combinational elements, memory elements, and input signals. Identification of cut-off points may be performed with respect to predetermined combinational logic input signals. The cut-off points may be connections whose values are not dependant on the value of the predetermined combinational logic input signals. An approximated circuit design may be synthesized by relaxing the logic associated with the cut-off points. Based on the approximated circuit design, processing may be performed. In some exemplary embodiments, a clock gating function of a memory element may be determined by approximating the circuit design with respect to the output signal of the memory element. The clock gating function may be determined based on the approximated circuit design and introduced to the circuit design, with or without additional refinement.

Circuit design approximation

A method, apparatus and computer program product for automatic parity check identification. The method comprising: automatically identifying a parity signal in a circuit design, wherein the parity signal is defined as a parity function of a set of support signals, wherein the automatic identification comprises: obtaining a candidate parity signal and a corresponding set of candidate support signals; and verifying that a bit flip in exactly one of any of the corresponding candidate set of support signals induces a bit flip on a value of the candidate parity signal; wherein said method further comprises reporting the automatically identified parity signal.

Automatic parity checking identification

A method, apparatus and computer program product for modifying a circuit design. The method comprising: obtaining a design of a circuit, the design comprising at least a first memory element and a second memory element. The method further comprising selecting the second memory element to be a dominant memory element over the first memory element. The method further comprising modifying the design of the circuit by replacing usage of an output signal of the first memory element with usage of an output signal of the dominant memory element in one or more cycles in which values of the output signals of the first memory element and the dominant memory element are equal. Whereby a reduction in observabiltiy of the first memory element in the design is achieved.

Reducing observability of memory elements in circuits

Formal verification of models using concurrent model-reduction and model-checking. For example, a system for formal verification of models includes: one or more model reducers to reduce a model; one or more model checkers to check the model, wherein at least one of the model reducers is to run concurrently with at least one of the model checkers; and a model synchronizer to synchronize information between at least one of the model reducers and at least one of the model checkers.

Formal verification of models using concurrent model-reduction and model-checking

Two circuits, an original and a modified, are being recognized, with the original circuit having a first logic and the modified circuit having a second logic. The second logic contains at least one desired logic change relative to the first logic. An equivalence line is detected in the original circuit such that the first and second logic are equivalent from the circuit inputs to the equivalence line. At least one point of change is located amongst the logic gates that are neighboring the equivalence line. The points of change are accepted as verified if an observability condition is fulfilled. The observability condition is checked within a Boolean Satisfiability (SAT) formulation. Substitute logic for the verified points of change is derived using SAT and Boolean equation solving techniques, in such manner that the first logic becomes equivalent to the second logic.

Logic modification synthesis

Clock gating circuit is determined by transforming a clock gating opportunity function to a non-Boolean function and constraining inputs of the non-Boolean function. The non-Boolean function may be a ternary function. Constraining the inputs may be achieved by introducing control variables and a cardinality constraint associated with their values. The non-Boolean function may be utilized to approximate universal quantification of an input assigned with a non-Boolean value, such as 'don't care' value. The non-Boolean function may be utilized to provide an ALL SAT solution of a Boolean function using a SAT solver.

SAT-based synthesis of a clock gating function

A method for reducing a depth of binary decision diagram includes identifying, with a processing device, one or more less probable positive paths within the binary decision diagram, the less probable positive paths within the binary decision diagram include a number of decision nodes from a starting variable to a positive, binary logic '1' terminal node within the binary decision diagram, and the identified less probable positive paths are eliminated. Identifying the less probable positive paths within the binary decision diagram includes: assigning &#x192; to the binary decision diagram, assigning K to a depth threshold of the binary decision diagram, and constructing a second binary decision diagram g by logically ORing together positive paths in &#x192; that have a length above K. Eliminating the identified less probable positive paths in &#x192; comprises obtaining an approximated function &#x192;', by conjuncting &#x192; and the negation of g, such that &#x192;&#x2032;&#x2261;&#x192;^.

Growing community of inventors

Nesher, Israel

Eli Arbel