Patent Document ID: 5491639
Application ID: 08133208
Patent Flag: 1

Claim One:
1. 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.