|
Static checking of assertions is termed property checking. Property checking is a formal analysis of the state space
of the design that guarantees that a design property, specified as a set of assertions about design behavior, is not violated. If a property violation is found then a counter-example is generated that shows the
violation. The counter-example is typically in the form of a specific sequence of vectors that uncovers the property violation. However, property checking is a static technique and no test-bench or logic simulator is
required. Property checking essentially involves a complete search through the state space of the design to ensure that the design behavior is always as asserted. To reduce the amount of search, logic and state space
pruning techniques are used. However, for properties involving complex sequential behavior of wide cones of logic it may not be possible to completely prove that the property holds for all cases. Thus, property checking
is a complete technique that may not complete. Nevertheless, in many cases, property checking will uncover a design property violation if it exists and, by constraining the search, checking of even wide logic cones is
possible. Verity-Check Expert supports the static property checking of design properties specified using either the Accellera Property Specification Language (PSL) / Sugar or in-line Verilog assertion directives.
|
