| 摘要 |
A method for verifying at least one aspects of a digital circuit, the method comprising: providing a set of operations to be performed by the digital circuit, each one of the set of operations having at least one functional element; identifying a first subset of a plurality of the at least one functional element; describing in a description the plurality of the at least one functional element of the identified first subset in terms of properties, each one of the properties having an assumption component and a proof component; formally verifying each one of the properties; arranging the plurality of the at least one functional element of the identified first subset to be proven for the digital circuit in an arrangement with temporal relations satisfying at least said description; analysing completeness of the arrangement of the plurality of the at least one functional element to verify that the at least one aspects of the digital circuit are completely verified.
|
