Scalable dependent state element identification
View Patent ↗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.
1. A method of partitioning a model of a circuit diagram representing an electrical circuit comprising a plurality of variables representing state elements in said electrical circuit, the method comprising:
select a variable from the plurality of variables;
identify a first set of variables among the plurality of variables that each support said selected variable;
identify a second set of variables among the plurality of variables that each have support overlapping said first set of variables; and
storing said second set of variables on a machine readable medium;
wherein said second set of variables is a partition of state elements suitable for use in determining an overapproximation of reachable states of said selected variable.
2. The method of claim 1 ,
wherein said plurality of variables represent a plurality of registers.
3. The method of claim 1 ,
wherein an output of each of the first set of variables affects an output of the selected variable; and
wherein an output of each of the second set of variables is affected by the output of each of the first set of variables.
4. The method of claim 1 , wherein an output of each of the second set of variables is affected by a set of outputs of the first set of variables that serve as inputs to the selected variable.
5. The method of claim 1 , further comprising:
perform a reachability analysis on said second set of variables;
wherein the reachability analysis is performed using a binary decision diagram.
6. The method of claim 1 , further comprising:
conduct a size evaluation to determine whether said second set of variables is within an acceptable size; and
perform preprocessing to adjust a size of said second set of variables to within said acceptable size.
7. The method of claim 6 , wherein said acceptable size is based upon one of a group consisting of a predetermined maximum number of the second set of variables, a predetermined minimum number of the second set of variables, and a maximum amount of computing resources associated with reachability computations for the second set of variables.
8. The method of claim 1 , wherein said method comprises steps performed by a computer or processor.
9. A software product comprising a machine readable medium including a program of instructions for partitioning a model comprising a plurality of variables representing state elements, wherein the program of instructions upon being executed on a computer causes the computer to perform activities comprising:
select a variable from the plurality of variables;
identify a first set of variables among the plurality of variables that each support said selected variable; and
identify a second set of variables among the plurality of variables that each have support overlapping said first set of variables;
wherein said second set of variables is a partition of state elements suitable for use in determining an overapproximation of reachable states of said selected variable.
10. The software product of claim 9 , further comprising:
perform a reachability analysis on said second set of variables using a binary decision diagram;
conduct a size evaluation to determine whether said second set of variables is within an acceptable size; and
perform preprocessing to adjust a size of said second set of variables to within said acceptable size.
11. The software product of claim 10 , wherein said acceptable size is based upon one of a group consisting of a predetermined maximum number of the second set of variables, a predetermined minimum number of the second set of variables, and a maximum amount of computing resources associated with reachability computations for the second set of variables.
12. The software product of claim 9 ,
wherein said model is a circuit diagram representing an electrical circuit; and
wherein said plurality of variables represent a plurality of registers.
13. The software product of claim 9 ,
wherein an output of each of the first set of variables affects an output of the selected variable; and
wherein an output of each of the second set of variables is affected by the output of each of the first set of variables.
14. The software product of claim 9 , wherein an output of each of the second set of variables is affected by a set of outputs of the first set of variables that serve as inputs to the selected variable.
15. A system for partitioning a model comprising a plurality of variables representing state elements, the system comprising:
a display device configured to display a variable selected from the plurality of variables;
a processor configured to identify a first set of variables among the plurality of variables that each support said selected variable, wherein said processor is further configured to identify a second set of variables among the plurality of variables that each have support overlapping said first set of variables; and
a memory configured to store said second set of variables on a machine readable medium;
wherein said second set of variables is a partition of state elements suitable for use in determining an overapproximation of reachable states of said selected variable.
16. The system of claim 15 , wherein said processor is further configured to perform a reachability analysis on said second set of variables using a binary decision diagram, conduct a size evaluation to determine whether said second set of variables is within an acceptable size, and perform preprocessing to adjust a size of said second set of variables to within said acceptable size.
17. The system of claim 15 ,
wherein said model is a circuit diagram representing an electrical circuit; and
wherein said plurality of variables represent a plurality of registers.
18. The system of claim 15 ,
wherein an output of each of the first set of variables affects an output of the selected variable; and
wherein an output of each of the second set of variables is affected by the output of each of the first set of variables.
19. The system of claim 15 , wherein an output of each of the second set of variables is affected by a set of outputs of the first set of variables that serve as inputs to the selected variable.
20. The system of claim 15 , wherein said acceptable size is based upon one of a group consisting of a predetermined maximum number of the second set of variables, a predetermined minimum number of the second set of variables, and a maximum amount of computing resources associated with reachability computations for the second set of variables.