Patent ID: 9032345
Filing Date: 2015-05-12
Classification: G06F

Abstract:
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 b) introducing a free variable (v c) replacing the second side (r d) making sure that for each model checking step each g e) adding a constraint one_hot(g f) checking for the existence of counter-examples (c g) indicating, by using said computer, that an assignment (s h) adding a constraint not (g i) iterating this process starting at f) until no more counter-examples exist, or a resource limit for model checking is reached.