Property generating method, verification method and verification apparatus
OwnerYasuyo Shimizuinventor
Life of this patent
Estimating the term…
Abstract
When a property for verifying a logic system is generated, a list of corresponding events is generated from specifications that the logic system should meet, an event of an undefined state in a first property is extracted from the list of events, and a property representing that the extracted event of the undefined state is improbable is generated as a second property that makes up for an event lacking in the first property.
Claims10
A property generating method of generating a property for verifying a logic system, comprising:
- a list generating step of generating a list of corresponding events from specifications that the logic system should meet;
- and
- a property generating step of generating a second property that makes up for an event lacking in a first property.
A verification method of verifying a logic system using a property, comprising:
- a list generating step of generating a list of corresponding events from specifications that the logic system should meet;
- a property generating step of generating a second property that makes up for an event lacking in a first property;
- and
- a verification implementing step of implementing static verification of the logic system using the second property.
A verification apparatus for verifying a logic system using a property, comprising:
- property generating means for generating a list of corresponding events from specifications that the logic system should meet, and generating a second property that makes up for an event lacking in a first property;
- and
- verification implementing means for implementing static verification of the logic system using the second property.
Dependencies are inferred from the claim text.