International Business Machines Corporation

Geert Janssen

Viresh Paruthi

Jason Raymond Baumgartner

Hari Mony

Christian Jacobi

Kai Oliver Weber

Robert Lowell Kanzelman

Michael L Case

Jiazhao Xu

Andreas Kuehlmann

Jayant R Kalagnanam

Jinjun Xiong

Yada Zhu

Louise Helen Trevillyan

Florian Karl Krohm

Malay Kumar Ganai

A method for predicting and managing an occurrence of a power outage resulting from human activity, the method comprising the steps of: obtaining at least one short-term notification of a planned human activity event; generating a corrected human activity notification as a function of the short-term notification and data corresponding to power grid information, geographical information relating to the power grid and customers utilizing the power grid, power grid customer information, and/or historical information corresponding to prior power outages resulting from human activity events; generating an outage probability as a function of the corrected human activity notification and trained predictive modeling data; generating an optimization model as a function of the outage probability; and initiating at least one action for mitigating the occurrence of the power outage resulting from human activity as a function of the optimization model.

System and method to reduce human activity damage-induced power outage

Leveraging existing Binary Decision Diagrams (BDDs) to enhance circuit reductions in a system model representing a state machine as a netlist. The netlist is evaluated to determine the regions with the greatest potential reductions. BDD sweeping is performed to identify redundancies in the netlist. BDD rewriting implements the circuit reductions by replacing gates of the original netlist with more efficient equivalent logic.

Optimizing a netlist circuit representation by leveraging binary decision diagrams to perform rewriting

Methods and systems are provided for reducing an original circuit design into a simplified circuit design by merging gates that may not be equivalent but can be demonstrated to preserve target assertability with respect to the original circuitry design. A composite netlist is created from the simplified netlist and the original netlist. The composite netlist includes a number of targets that imply the existence of a target in the simplified netlist and a corresponding target in the original netlist. The implications are verified and then validated to ensure the simplified circuit design is a suitable replacement for the original circuit design.

Method and system for design simplification through implication-based analysis

A method, system and computer program product for integrating implication-based analysis and equivalent gate analysis to maintain transitive reduction in an implication graph over a sequence of graph operations. One or more gates of a design are identified that are equivalent in all reachable states. Equivalent gates are assigned to an equivalence class when all gates within the equivalence class are equal. During the implication-based analysis the system determines when one or more implication paths are associated with the one or more equivalence classes, and an implication is generated at the implication path associated with the equivalence classes. A transitively reduced graph is received depicting the implications and equivalence classes of the design. When one or more operations are assigned to the transitively reduced graph, the graph is automatically adjusted to maintain transitive reduction.

Method for scalable derivation of an implication-based reachable state set overapproximation

A method, system and computer program product for X-Saturated ternary simulation based reduction. An X-Saturated ternary simulation (XSTS) utility, which executes on a computer system, receives design information, where the design information includes a netlist. The XSTS utility initializes one or more data structures and/or variables and simulates, in a ternary fashion, the netlist at a time value by applying logical X values to all RANDOM gates of the netlist and to registers marked X_SATURATED. For each register of the netlist XSTS utility: determines whether or not the register departs from its expected prefix behavior, and if the register departs from its expected prefix behavior, the register is marked as X_SATURATED and the current state is updated with an X value upon the register. XSTS utility can store the current state in a data structure and can use the information from the data structure to simplify the design.

Automated convergence of ternary simulation by saturation of deep gates

A method, system and computer program product for reversing effects of reparameterization is disclosed. The method comprises receiving an original design, an abstracted design, and a first trace over the abstracted design. One or more conditional values are populated into the first trace over the abstracted design, and a k-step satisfiability check is cast to obtain a second trace. One or more calculated values are concatenated to an initial gate set in the second trace with one or more established values to a generated subset of the initial design in the abstracted trace to form a new trace, and one or more effects of a reparameterization are reversed by returning the new trace over the initial design.

Reversing the effects of sequential reparameterization on traces

Method and system for reversing the effects of sequential reparameterization on traces

A method, system, and computer program product for preserving critical inputs. According to an embodiments of the present invention, an initial design including one or more primary inputs which cannot be eliminated, one or more primary inputs which can be eliminated, one or more targets, and one or more state elements are received. A cut of said initial design including one or more cut gates is identified, and a relation of one or more values producible to said one or more cut gates in terms of said one or more primary inputs which cannot be eliminated, said one or more primary inputs which can be eliminated and said one or more state elements is computed. Said relation is synthesized to form a gate set, and an abstracted design is formed from said gate set. Verification is performed on said abstracted design to generate verification results.

Method for heuristic preservation of critical inputs during sequential reparameterization

A method, system and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit using a dynamic resource constrained and interleaved depth-first-search and modified breadth-first-search schedule is disclosed. The method includes setting a first size limit for a first set of one or more m-ary decision representations describing a logic function and setting a second size limit for a second set of one or more m-ary decision representations describing a logic function. The first set of m-ary decision representations of the logic function is then built with one of the set of a depth-first technique or a breadth-first technique until the first size limit is reached, and a second set of m-ary decision representations of the logic function is built with the other technique until the second size limit is reached. In response to determining that a union of first set and the second set of m-ary decision representations do not describe the logic function, the first and second size limits are increased, and the steps of building the first and second set are repeated. In response to determining that the union of the first set of m-ary decision representations and the second set of m-ary decision representations describe the logic function, the union is reported.

System for building binary decision diagrams efficiently in a structural network representation of a digital circuit

Building binary decision diagrams efficiently in a structural network representation of a digital circuit

Methods, systems and software products are provided to enhance the scalability of dependent state analysis element identification. In a method of partitioning a model representing a state machine, a variable is selected from the variables of the model, and a first set of variables are identified that support the selected variable. Then a second set of variables is identified that have overlapping support of the first set of variables. The second set of variables is a partition suitable for use in determining an overapproximation of the reachable states of the selected variable.

Scalable dependent state element identification

A method, system and computer program product for performing synthesis of representations is disclosed. The method comprises receiving a representation of a relation and building a gate representing an OR function of one or more selected parent paths into a node of said representation of said relation. A synthesized gate for said gate representing said OR function and synthesis of a set of representations of relations by iterating said building step and said creating step over one or more variables in said representation of said relation is performed to accumulate a synthesized gate set, which synthesized gate set is returned.

Method for improved synthesis of binary decision diagrams with inverted edges and quantifiable as well as nonquantifiable variables

A method, system and computer program product for performing parametric reduction of sequential designs is disclosed. The method comprises receiving an initial design including one or more primary inputs, one or more targets, and one or more state elements. A cut of the initial design including one or more cut gates is identified, and a relation of one or more values producible to the one or more cut gates in terms of the one or more primary inputs and the one or more state elements is computed. The relation is synthesized to form a gate set, and an abstracted design is formed from the gate set. Verification is performed on the abstracted design to generate verification results.

Parametric reduction of sequential design

A method for performing verification includes receiving a design and building for the design an intermediate binary decision diagram set containing one or more nodes representing one or more variables. A first case-splitting is performed upon a first fattest variable from among the one or more variables represented by the one or more nodes by setting the first fattest variable to a primary value, and a first cofactoring is performed upon the intermediate binary decision diagram set with respect to the one or more nodes using an inverse of the primary value to generate a first cofactored binary decision diagram set. A second cofactoring is performed upon the intermediate binary decision diagram set with respect to the one or more nodes using the primary value to generate a second cofactored binary decision diagram set, and verification of the design is performed by evaluating a property of the second cofactored binary decision diagram set.

Growing community of inventors

Putnam Valley, NY, United States of America

Geert Janssen