Procedure for verifying data-processing systems
AssigneeSiemens Aktiengesellschaft
InventorThomas Filkorn
Life of this patent
Estimating the term…
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.
Claims8
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.
Dependencies are inferred from the claim text.