Back to results
US 8,554,522 B2Granted
Detection of design redundancy
AssigneeInternational Business Machines Corporation
InventorsShaked Flur, Ziv Nevo
Life of this patent
Estimating the term…
Abstract
Augmented-domain simulation, such as ternary-based simulation may be utilized to approximate a reachability analysis of a model being model checked. The approximated reachability analysis may be utilized to detect design redundancies and modify the model to remove such redundancies. Design redundancies may include unobservable variables, mergeable variables and utilization of surplus domains.
Claims14
A computerized apparatus having a processor, the computerized apparatus comprising:
- an input module configured to receive a model comprising at least one variable, the at least one variable is associated with a domain;
- an augmented-domain simulator configured to utilize the processor to simulate an execution of the model using an augmented-domain, the augmented-domain comprising the domain and an unknown value, said augmented-domain simulator comprising:
- a state repository for retaining states of the model determined by said augmented-domain simulator;
- and
- a fix-point determinator configured to identify convergence to a fix-point by said augmented-domain simulator based on said state repository;
- and
- design redundancy detector configured to determine a design redundancy in accordance with the states retained in said state repository, wherein the design redundancy detector comprises an unobservable variables detector, wherein said design redundancy detector comprises a mergeable variables detector configured to identify a first variable having a first value that is represented by a mapping from a second value of a second variable.
4 more elements
A computerized apparatus having a processor, the processor comprising:
- an input module configured to receive a model comprising at least one variable, the at least one variable is associated with a domain;
- an augmented-domain simulator configured to simulate an execution of the model using an augmented-domain, the augmented-domain comprising the domain and an unknown value, said augmented-domain simulator comprising:
- a state repository for retaining states of the model determined by said augmented-domain simulator;
- and
- a fix-point determinator configured to identify convergence to a fix-point by said augmented-domain simulator based on said state repository;
- and
- design redundancy detector configured to determine a design redundancy in accordance with the states retained in said state repository, wherein said design redundancy detector comprises a mergeable variables detector configured to identify a first variable having a first value that is represented by a mapping from a second value of a second variable.
4 more elements
A computerized apparatus having a processor, the processor comprising:
- an input module configured to receive a model comprising at least one variable, the at least one variable is associated with a domain;
- an augmented-domain simulator configured to utilize the processor to simulate an execution of the model using an augmented-domain, the augmented-domain comprising the domain and an unknown value, said augmented-domain simulator comprising:
- a state repository for retaining states of the model determined by said augmented-domain simulator;
- and
- a fix-point determinator configured to identify convergence to a fix-point by said augmented-domain simulator based on said state repository;
- and
- design redundancy detector configured to determine a design redundancy in accordance with the states retained in said state repository,
- wherein the fix-point determinator is an early fix-point determination module configured to identify convergence to a fix-point in respect to a portion of a state, wherein said early fix-point determination module comprises:
- a strongly connected component identification module configured to partition state variables into a plurality of strongly connected components;
- a dependency module configured to determine a portion of the plurality of strongly connected components determined by said strongly connected component identification module, the portion of the plurality of strongly connected components is characterized in influencing a value of a strongly connected component selected from the plurality of strongly connected components;
- wherein said early fix-point determination module is configured to identify a fix-point in respect to a first portion of the state associated with the strongly connected component based upon a fix-point of a second portion of the state associated with the portion of the plurality of strongly connected components.
8 more elements
A method for removing a design redundancy in a model, said method is performed in a computerized environment, said method comprising:
- receiving the model, the model comprising at least one variable, the at least one variable is associated with a domain;
- using a computer to perform augmented-domain simulation of an execution of the model using an augmented-domain, the augmented-domain comprising the domain and an unknown value, said performing augmented-domain simulation comprises:
- retaining simulated states;
- and
- identifying convergence to a fix-point;
- identifying the design redundancy based on the retained simulated states;
- and
- modifying the model to a modified model excluding the design redundancy, whereby the model is transformed to the modified model such that a model checker traverses the modified model in a different manner than the model checker traverses the model, wherein the identifying a design redundancy comprises identifing an unobservable variable;
- whereby the modified model comprises a reduced number of variables than the model;
- and
- wherein at least one of said receiving, performing, identifying and modifying is performed by a computer;
- wherein said identifying a design redundancy comprises determining a limited domain associated with the at least one variable, the limited domain is a subset of the domain;
- whereby the modified model comprises a reduced number of states than the model.
10 more elements
Dependencies are inferred from the claim text.