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 the progress and quality of a verification of a digital circuit with model checking by using a computer, wherein the method verifies that a plurality (M) of assignments (s i ) in a set (S) of assignments are observation covered by a proven property (p) for a representation (D) of the digital circuit, each assignment (s i ) having a first side (l i ) and a second side (r i ), the method comprising:
a) introducing a guard input (g i ) for each said assignment (s i );
b) introducing a free variable (v i ) for each said assignment (s i );
c) replacing the second side (r i ) of each assignment (s i ) with the expression g i ? r i : v i ;
d) making sure that for each model checking step each g i has the same value;
e) adding a constraint one_hot(g l , g n ) such that exactly one guard input (g i ) is true and all others are false in any potential counter-example;
f) checking for the existence of counter-examples (c j ) for property (p);
g) indicating, by using said computer, that an assignment (s i ) is covered when a counter-example (c j ) is found where (g i ) is true, that the assignment (s i ) is uncovered when no counter-example exists, and that the assignment (s i ) is uncovered for (k) model checking steps if the model checking result is inconclusive at (k) steps after hitting a resource limit;
h) adding a constraint not (g i ) if property (p) fails with a counter-example that makes guard input (g i ) true while all other guard inputs are false; and
i) iterating this process starting at f) until no more counter-examples exist, or a resource limit for model checking is reached.
2. A method for providing information relating to the progress and quality of a verification of a digital circuit with bounded model checking by using a computer according to claim 1 , further comprising:
j) making sure that for each model checking step each g i has the same value is implemented by unrolling said modified design description D M and in each unrolling step duplicating all inputs to D M except for the guard input (g i ), which remains the same in each step.
3. A method for providing information relating to the progress and quality of a verification of a digital circuit with bounded model checking by using a computer according to claim 1 , wherein property p is proven to a certain bound of model checking steps (r) comprising:
a) checking for the presence of a counter-example for (p) in each step until a bound (r) is reached; and
b) indicating, by using said computer, that an assignment (s i ) is covered when a counter-example (c j ) of length less than or equal to (r) is found where (g i ) is true.
4. A method for providing information relating to the progress and quality of a verification of a digital circuit with model checking by using a computer, wherein the verification comprises verifying that a plurality (M) of assignments (s i ) in a set (S) of assignments are observation covered by a proven property (p) for a representation (D) of the digital circuit, each assignment (s i ) having a first side (l i ) and a second side (r i ), the method comprising:
a) introducing a guard input (g i ) for each said assignment (s i );
b) introducing a free variable (v i ) for each said assignment (s i );
c) replacing the second side (r i ) of each assignment (s i ) with the expression g i ? r i : v i ;
d) making sure that for each model checking step each gi has the same value;
e) adding a constraint one —hot(g l , . . . , g n ) such that exactly one guard input (g i ) is true and all others are false in any potential counter-example;
f) checking for the existence of counter-examples (c j ) for property (p);
g) indicating, by using said computer, that an assignment (s i ) is covered when a counter-example (c j ) is found where (g i ) is false, that the assignment (s i ) is uncovered when no counter-example exists, and that the assignment (s i ) is uncovered for (k) model checking steps if the model checking result is inconclusive at (k) steps after hitting a resource limit;
h) adding a constraint not (g i ) if property (p) fails with a counter-example that makes guard input (g i ) false while all other guard inputs are true; and
i) iterating this process starting at f) until no more counter-examples exist, or a resource limit for model checking is reached.