Assertion checking is a simulation based technique that involves the addition of RTL statements in the hardware description language (HDL) representation of a design
specifically for verification purposes. The inserted RTL statements are said to be assertions about design behavior. They typically state that when specified events occur certain other events should occur or that
certain design conditions must be met. If the asserted design behavior does not occur then the assertion is said to be violated and this typically results in an error being flagged in the HDL. Assertion
checking is a dynamic technique that requires the use of a test-bench. Thus, assertion checks may also be performed using specialized test bench automation languages that run in conjunction with logic simulation. When
the assertions are written directly in the HDL, synthesis directives are typically used to prevent the assertion code being synthesized. However, this code may be exercised during simulation if the test-bench causes
activation of the code. The effectiveness of assertion checking is highly dependent on the quality of the test bench with respect to the targeted design behavior. If the test-bench does not exercise the design in such a
way that the design behavior being checked is exhibited then the assertion will never be violated even if the design behaves incorrectly. Assertion checking is a non-formal technique; it does not guarantee that
faulty design behavior will be detected. RTL assertions may also be statically checked without the use of a test-bench or logic simulator. Static checking of assertions is termed property checking. Verity-Check Expert supports the static checking of assertions specified using either the Accellera Property Specification Language (PSL) / Sugar or in-line Verilog assertion directives.
. |
