Coded data generation or conversion – Digital code to digital code converters – Coding by table look-up techniques
Reexamination Certificate
1998-12-11
2001-06-12
Young, Brian (Department: 2819)
Coded data generation or conversion
Digital code to digital code converters
Coding by table look-up techniques
C341S051000
Reexamination Certificate
active
06246349
ABSTRACT:
FIELD OF THE INVENTION
The present invention relates to computer systems and more particularly to a method and system for compressing state transition data which provides the ability to use the compressed state transition data without completely decompressing the compressed state transition data.
BACKGROUND OF THE INVENTION
Model checking provides a mechanism for evaluating digital logic and protocols. Model checking determines the states that a system may reach from different sets of inputs. The model can determine whether the states that the system can reach violate a condition, such as a design parameter. Typically, the states are checked using either implicit or explicit checking. Implicit checking allows a large number of states to be checked, but is time consuming. Consequently, explicit checking may be used.
Explicit checking is relatively fast. Explicit checking explicitly determines the valid states that a system being tested can reach. In order to determine the states a system under test can reach, state transition data is generated. State transition data is usually in the form of a state transition table. A state transition table is a table of state transitions. A state transition is an ordered pair of states, (S
1
, S
2
), where state S
2
succeeds state S
1
in the design/protocol under test. The state transition table may also be used to generate a state transition graph. The entries of the table can be evaluated to determine if the state violates a condition or design parameter. Similarly, a state transition graph can be used to plot the data in the state transition table. Thus, using the entries of the state transition table or using the state transition graph, it can be determined whether the system operates as designed.
For example, two types of conditions may be checked using explicit model checking: safety properties and liveness properties. Safety properties are of the form “it is/is not possible for the system to enter state X,” or “if X is true, then Y must be true Z cycles later.” Thus, safety properties are always true or bounded in time. Liveness properties are not bounded in time. An example of a liveness property is “if X is true, Y must eventually be true.” When all the states have been generated in a state transition table, a safety property may be checked by determining whether the safety property is true in any of the states generated. A liveness property may be checked using a state transition graph and determining the connection between particular states (nodes in the state transition graph) and the possible transitions to states which can be reached from the particular states.
Model checking rapidly consumes memory. The entries in the state transition table or nodes in the state transition graph should be capable of being accessed randomly to allow a user to adequately evaluate the system being checked. However, typical logic systems have an extremely large number of possible states. A system may be represented by n bits. The possible states that can be reached by that system are on the order of 2
n
. For example, a processor may be represented by a thousand bits. Consequently, the number of reachable states for such a processor is extremely large. Each of these possible states is stored in memory. Memory is, therefore, rapidly consumed by explicit model checking. Typically, the number of possible states is large enough to be incapable of being stored in memory for use.
To reduce the number of states that are generated, explicit model checking typically generates only valid states. Furthermore, explicit model checking is used for systems that can be represented by a smaller number of bits. However, memory is still rapidly consumed. For example, a system may be represented by only one hundred bits. Furthermore, only half of the possible states may be valid. However, 2
99
is still a large number of states. Thus, memory may still be rapidly consumed. As a result, the state transition data may still not be able to be accessed randomly to allow the system to be checked.
Conventional data compression would allow the state transition data to be stored using a smaller amount of memory. As the state transition data is read, unique patterns of bits are searched for and a dictionary generated. The dictionary associates a unique pattern of bits with a code word. If the current bits being read do not match a pattern, then the bits are resaved in the order of the source data file. However, if a pattern recurs, then a code word replaces the pattern. Typically, the code word may point to a previous occurrence of the pattern. However, the code word could also point to the entry in the dictionary corresponding to the code word. Thus, a conventional compressed state transition file is generated.
However, conventional data compression allows the conventional compressed state transition file to occupy less memory than the state transition data only while the conventional compressed state transition data is stored. The different states stored in the state transition data, or the entries of the state transition table, must be able to be accessed randomly. Using conventional data compression, random access of portions of the compressed data is not possible without uncompressing the entire conventional file. The uncompressed state transition file occupies the same amount of space as the state transition data. Thus, conventional data compression may not allow the state transition data to be used without exhausting memory.
In order to allow explicit model checking to be used, lossy checking schemes have been developed. Lossy checking schemes typically utilize only a portion of the states that may be generated. Thus, because the schemes are lossy, only a portion of the possible states is checked. For example, one popular scheme is known as the Murphi scheme. The Murphi scheme is described more fully in “New Scheme for Memory-Efficient Probabilistic Verification” by David Dill and Stem in IFIP Conference on Formal Description Techniques for Distributed Systems and Communications Protocol (1996). The Murphi scheme uses a hash table to represent the states that are generated. In the Murphi scheme, two unique states generated may be hashed to the same value and, therefore, treated as the same state. In other words, this scheme maps similar states to a single state. Only the states to which similar states have been mapped are explicitly checked. Thus, only a portion of the possible states is checked and only a portion of the possible transition data is saved.
Although lossy checking schemes allow systems to be checked, one of ordinary skill in the art will readily realize that important information may be lost. Checking only the states to which a number of similar states are mapped may allow a developer to check some severe conditions. However, other fault conditions may be missed because some information is lost. Thus, lossy checking schemes may result in false positives, which incorrectly indicate that a system is operating properly because of information lost due to the checking scheme chosen. For similar reasons, lossy checking schemes may also result in false negatives, which incorrectly indicate that the system is not operating properly. Consequently, lossy checking schemes may not adequately check a system of interest. Moreover, a lossy checking scheme such as the Murphi scheme does not compute the state transition graph or save each state generated. Instead, some information relating to the transitions between states is stored. When a state transition graph is to be generated, this data must be used to generate the state transition graph. This results in a larger file size, which consumes more memory, and input/output limitations. In addition, if a user wishes to check the states taken to reach a state that violated a condition, the states are regenerated. This is because lossy checking schemes typically do not include information relating to the transitions between states. Recalculation of the path taken to a state which violates a condition requires additional ti
Baumgartner Jason Raymond
Malik Nadeem
Roberts Steven Leonard
International Business Machines - Corporation
Leeuwen Leslie A. Van
Sawyer Law Group LLP
Young Brian
LandOfFree
Method and system for compressing a state table that allows... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and system for compressing a state table that allows..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for compressing a state table that allows... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2535925