Digital circuit verification monitor
A method, a system and a computer readable medium for providing information relating to a verification of a digital circuit. The verification may be formal verification and comprise formally verifying that a plurality of formal properties is valid for a representation of the digital circuit. The method comprises replacing at least a first input value relating to the representation of the digital circuit by a first free variable, determining if at least one of the plurality of formal properties is valid or invalid after replacing the first input value by the first variable and indicating if the at least one of the plurality of formal property is valid or invalid. The use of a free or open variable that has not determined value can be directly in the description or representation of the digital circuit. It is not necessary to insert errors or to apply an error model.
1. A method for providing information relating to a verification of a digital circuit by using a computer, wherein the formal verification comprises verifying that a plurality of properties (P) is valid for a representation (D) of the digital circuit, the method comprising:
a) replacing, at least a first input value (s) relating to the representation of the digital circuit by a first free variable (v);
b) determining, by using said computer, when at least one of the plurality of properties is valid or invalid after replacing the first input value by the first variable (v); and
c) indicating when the at least one of the plurality of properties is valid or invalid wherein the determining when at least one of the plurality of properties is valid or invalid comprises determining when at least one of the plurality of properties is disproved with the first free variable, and wherein the indicating when the at least one of the plurality of properties is valid or invalid comprises indicating that the first input value (s) is covered if at least one of the plurality of properties is disproved.
2. The method for providing information relating to a verification of a digital circuit according to claim 1 , wherein the indicating when the at least one of the plurality of properties is valid or invalid comprises indicating that a coverage of the first input value (s) is not determined when none of the plurality of properties is disproved and at least one of the plurality of properties (P) cannot be proven.
3. The method for providing information relating to a verification of a digital circuit according to any one of claims 1 , wherein the indicating when the at least one of the plurality of properties is valid or invalid comprises indicating that a coverage of the first input value (s) is determined to a lower limit when none of the plurality of properties is disproved and one or more of the plurality of properties (P) cannot be proven.
4. The method for providing information relating to a verification of a digital circuit according to claim 1 , wherein the verification is a formal verification and the set of properties is a set of formal properties.
5. The method for providing information relating to a verification of a digital circuit according to claim 1 , wherein the first input value is a first signal assignment.
6. The method for providing information relating to a verification of a digital circuit according to claim 1 , further comprising repeating the method steps with at least a second signal assignment.
7. The method for providing information relating to a verification of a digital circuit according to claim 1 , further comprising excluding one or more signal assignments from the representation of the digital circuit.
8. The method for providing information relating to a verification of a digital circuit according to claim 1 , further comprising excluding at least one portion of the description of the digital circuit from the method that has no influence on the functionality of the digital circuit.
9. The method for providing information relating to a verification of a digital circuit according to claim 1 , wherein the representation of the digital circuit comprises a plurality of statements relating to the functional behaviour of the digital circuit, and wherein the method further comprises indicating when one or more statements of the plurality of statements are covered, uncovered, not determined or a combination thereof.
10. The method for providing information relating to a verification of a digital circuit according to claim 1 , wherein the representation of the digital circuit comprises a Register Transfer List (RTL) code with a plurality of statements.
11. The method for providing information relating to a verification of a digital circuit according to claim 1 , further comprising indicating all input variables as undefined prior to the replacing of at least one first input value (s i ) assigned to the representation of the digital circuit by a free variable (v).
12. The method for providing information relating to a verification of a digital circuit according to claim 1 , further comprising at least one constraint relating to one or more properties.
13. A computer program product stored in a memory for providing information relating to a verification of a digital circuit, the computer program product executing the method according to method of claim 1 .
14. A method for providing information relating to a verification of a digital circuit by using a computer, wherein the formal verification comprises verifying that a plurality of properties (P) is valid for a representation (D) of the digital circuit, the method comprising:
a) replacing, at least a first input value (s) relating to the representation of the digital circuit by a first free variable (v);
b) determining, by using said computer, when at least one of the plurality of properties is valid or invalid after replacing the first input value by the first variable (v); and
c) indicating when the at least one of the plurality of properties is valid or invalid; wherein the determining when at least one of the plurality of properties is valid or invalid comprises determining when each one of the plurality of properties (P) is proved with the first free variable and wherein the indicating when the at least one of the plurality of properties is valid or invalid comprises indicating that the first input value (s) is uncovered if each one of the plurality of properties (P) is proved.
15. A system for providing information relating to a verification of a digital circuit, wherein the verification comprises verifying that a plurality of properties (P) is valid for a representation (D) of the digital circuit, the system comprising an assignment module for replacing at least a first input value (s) relating to the representation of the digital circuit by a first free variable (v), a verifying module for determining when at least one of the plurality of properties is valid or invalid after replacing the first input value by the first free variable (v), and an indication module for indicating when the at least one of the plurality of properties is valid or invalid wherein the indicating when the at least one of the plurality of properties is valid or invalid comprises indicating that a coverage of the first input value (s) is not determined when none of the plurality of properties is disproved and at least one of the plurality of properties (P) cannot be proven.