US5491639A
Expired / Lapsed
US
⏱️ 0.0 years remaining
Procedure for verifying data-processing systems
Assignee: Siemens AG
•
Filing: 1992-04-07
•
Granted: 1996-02-13
•
Expires: 2012-04-07
Abstract
Abstract Implementation and specification of synchronous sequential circuits and other data-processing systems can be modeled by finite state machines. The verification, that is to say the comparison between the implementation and the specification of such systems can then be reduced to the comparison between two finite state machines. On the basis of a symbolic representation of finite state machines with the aid of binary decision diagrams, a method for comparing finite state machines has been developed which can be automatically run on computer systems and thus provides the possibility of automatically verifying such circuits without simulation.
Inventors
- 👤 Thomas Filkorn
Bibliographic Details
Application Number
—
Jurisdiction
US
Data Source
google_patents
Last Synchronized
2026-11-07 20:32
CPC Classifications
G; G06; G06F; G06F30/00; G06F30/30; G06F30/32; G06F30/33; G06F30/3323
Claims Analysis
Total Claims: 9
Claim 1
Independent Claim
184 words
A method for verifying data-processing systems, comprising the steps of: a) representing two descriptions, generated independently of one another, of a system to be verified as Mealy automata and comparing the two descriptions to one another; b) carrying out the comparison with a fixed-point iteration procedure which initially generates a first set of all state pairs which generate at least one different output value for at least one set of input values, and which iteratively extends said first set by a second set of all state pairs which, in a finite number of steps of the two Mealy automata, lead to a state pair which belongs to the first set, until a fixed-point set of all non-equivalent state pairs is generated, the two Mealy automata being equivalent when their initial states or the state pairs formed from these states do not belong to the fixed-point set; c) representing equivalence relations between states, output and transition functions of the two Mealy automata by binary decision diagrams; and d) applying in each step of the fixed-point iteration, only boolean operations and substitutions to binary decision diagrams.
Claim 2
Independent Claim
184 words
A method for verifying data-processing systems, comprising the steps of: a) representing two descriptions, generated independently of one another, of a system to be verified as Mealy automata and comparing the two descriptions to one another; b) carrying out the comparison with a fixed-point iteration procedure which initially generates a first set of all state pairs which generate at least one different output value for at least one set of input values, and which iteratively extends said first set by a second set of all state pairs which, in a finite number of steps of the two Mealy automata, lead to a state pair which belongs to the first set, until a fixed-point set of all non-equivalent state pairs is generated, the two Mealy automata being equivalent when their initial states or the state pairs formed from these states do not belong to the fixed-point set; c) representing equivalence relations between states, output and transition functions of the two Mealy automata by binary decision diagrams; and d) applying in each step of the fixed-point iteration, only boolean operations and substitutions to binary decision diagrams.
Claim 3
Dependent Claim
14 words
The method as claimed in claim 1, wherein the data-processing systems are digital circuits.
Claim 4
Dependent Claim
23 words
The method as claimed in claim 2, wherein a digital circuit to be verified is described in the form of two network lists.
Claim 5
Dependent Claim
31 words
The method as claimed in claim 2, wherein a digital circuit to be verified is described in the form of a network list with the aid of a hardware description language.
Claim 6
Dependent Claim
14 words
The method as claimed in claim 1, wherein the data-processing systems are communication protocols.
Claim 7
Dependent Claim
14 words
The method as claimed in claim 1, wherein the data-processing systems are computer programs.
Claim 8
Dependent Claim
13 words
The method as claimed in claim 1, wherein the data-processing systems are microprograms.
Claim 9
Dependent Claim
75 words
The method as claimed in claim 1, wherein in the step of carrying out the comparison: the first set of all state pairs generate at least one different output value for at least one set of input values; and the first set is extended by a set of all state pairs which, in a finite number of steps of the two Mealy automata, lead to a state pair of which belongs to the first set.
References Cited (Backward Citations)
US3943350A
Cited
US4876640A
Cited
US4933897A
Cited
US4799141A
Cited
US5001479A
Cited
US5243538A
Cited
US5243538B1
Cited
US5231590A
Cited
US5287289A
Cited
US5258919A
Cited
US5331568A
Cited
USPTO Annuity & Maintenance Windows
| Annuity Stage | Window Opens | Payment Deadline | Surcharge Period Until | Estimated Fee | Status |
|---|---|---|---|---|---|
| 3.5 Years (Year 4) | 1999-02-12 | 1999-08-14 | 2000-02-13 | $2000.00 | Window Closed / Lapsed |
| 7.5 Years (Year 8) | 2003-02-12 | 2003-08-14 | 2004-02-13 | $3760.00 | Window Closed / Lapsed |
| 11.5 Years (Year 12) | 2007-02-12 | 2007-08-14 | 2008-02-13 | $7700.00 | Window Closed / Lapsed |