Browse Prior Art Database

Using control flow analysis to improve the performance of rules in a model checker

IP.com Disclosure Number: IPCOM000016030D
Original Publication Date: 2002-Oct-29
Included in the Prior Art Database: 2003-Jun-21
Document File: 2 page(s) / 44K

Publishing Venue

IBM

Abstract

Problem

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 52% of the total text.

Page 1 of 2

  Using control flow analysis to improve the performance of rules in a model checker

Problem

    The main problem in running rules in a model checker is referred to as the state explosion problem. Execution time is usually exponentially related to the program size. For a certain class of rules, it is possible to use control flow analysis to reduce the program size on which the rule is performed.

Solution

    This invention represents a means for reducing the program size using control flow analysis, prior to executing the rule on the program with the model checker. We use the idea of dominating blocks to figure out which blocks are not relevant for our rules, and we remove these blocks from the program.

    The analysis currently done using cone of influence looks at the variables, and not at the control flow, and therefore is orthogonal to our invention.

Definitions

    Basic Block A pre dominate Basic Block B (Pre(A,B)), if before the control gets to B, it MUST go through A.

    Basic Block A is reachable from Basic Block B (Reach(B,A)), if there is a path from B to A. First optimization: If we want to check if basic block A is reachable, we can remove from the program:

{X : X in Pre(A,X)}

{X: X in !Reach(X,A)}

Then we can check if A is reachable on the modified program. Second optimization: If we want to check if basic block A is ALWAYS reachable, we can remove from the program:

{X: X in !Reach(X,A)}

Then we can check if A is always reachable on the modified program.

    This optimization can be used when we want to know if in the line Aux = (some condition), Aux always gets the value 1. This is an interesting case, because if we can allow the user to write annotations to the program in a language that he is familiar with, for example { / always y > x } or { / can happen y > x}, where (y>x) can be written in Verilog or VHDL and then we will automatically translate it to Aux = y>x and will apply on it the appropriate rule . The advantage is clear-the user does not have to learn Sugar or SMV or any other language he is not familiar with. When the user has such an option, the optimization above will be useful.

For { / first_time y > x } (first_time optimization), the first optimization above is

useful. Third optimization: Let's assume that we want to check if variable y can have the value 1, and there are n places in which the assignment happens (i.e., it can happen exactly in these places, and it can't h...