| 主权项 |
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 (si) in a set (S) of assignments are observation covered by a proven property (p) for a representation (D) of the digital circuit, each assignment (si) having a first side (li) and a second side (ri), the method comprising:
a) introducing a guard input (gi) for each said assignment (si); b) introducing a free variable (vi) for each said assignment (si); c) replacing the second side (ri) of each assignment (si) with the expression gi ? ri: vi; d) making sure that for each model checking step each gi has the same value; e) adding a constraint one_hot(gl, gn) such that exactly one guard input (gi) is true and all others are false in any potential counter-example; f) checking for the existence of counter-examples (cj) for property (p); g) indicating, by using said computer, that an assignment (si) is covered when a counter-example (cj) is found where (gi) is true, that the assignment (si) is uncovered when no counter-example exists, and that the assignment (si) 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 (gi) if property (p) fails with a counter-example that makes guard input (gi) 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. |
