Subject: System Verilog Assertion Requirements from 0-In
From: Richard Ho (rho@0-in.com)
Date: Wed Jul 31 2002 - 11:51:35 PDT
System Verilog Assertion Requirements:
R1. Assertions specified in the language must not alter design
behavior directly or by side-effects.
Discussion: An assertion should have no functional impact on
the design files. If a user simulates the design with
assertions disabled, the result must always be the same as
simulation with assertions enabled. All synthesis tools must
be able to fully ignore assertions.
R2. The language must support easy to specify assertions in a procedural
context with no side-effects (refer to R1).
Discussion: An example of a procedural assertion -
always @(posedge clk) begin
if (cond1) begin
if (cond2) begin
if (cond3) begin
...error_correction; // ASSERTION
The assertion would activate on (cond1 && cond2 && cond3).
Placing the assertion in the midst of the procedural code
simplifies writing the assertion. However, it must not
have a side-effect when placed "in-context".
R3. The language must support declarative assertions.
Discussion: Here, "declarative" means the assertion is checked
concurrently. There must be a mechanism that links the
assertion with the design code. Requirement R4 addresses
this mechanism.
R4. The language must support assertions to be linked to
a module declaration.
Discussion: For example, an assertion A could be linked to a module
foo, so that all variables used in assertion A refer to variables
in module foo. All instances of module foo get instantiated
with assertion A. Any reporting or state associated with
assertion A must be unique to the corresponding instance of foo.
R5. The language must support synchronous clocking of assertions,
with an implied, default, or explicitly specified clock
(including support for gated clocks).
Discussion: In mulitple clock designs, it must be possible to
specify the clocking of assertions to match the behavior being
checked.
R6. The language must support synchronous reset of assertions,
with an implied, default or explicitly specified reset.
Discussion: Assertions generally should not be active during
reset.
R7. The language must support dynamic disable of assertions.
Discussion: Often, designs must go through a long initialization
sequence after reset is de-asserted. During this time, assertions
must be disabled to prevent false error reporting.
R8. The language must support library element instantiation with
arguments. A "library element" is either a System Verilog
module or a named unit of the assertion language (e.g
named property of FVTC language).
Discussion: Library elements allow for re-use of verification code.
R9. The language must support compact specification of assertions,
using inference from context to provide implicit or default
values for variables.
Discussion: Assertion specification is simpler when inference
of simple arguments can be performed by tools. Default
values and explicit setting of arguments can override the
infered values.
R10. The language must support assignment of severity levels to
assertions.
Discussion: In practice, assertions have different levels of
error severity. These should be specified with the assertion.
R11. The language must support explicit verification directives.
Two examples of verification directives are: "assume" an
assertion is true in order to model an environmental
constraint; and "assert" an assertion is true in order to
check the functionality of the design.
Discussion: For complex assertions, environmental constraints
for verification cannot be automatically inferred from
context. Directives from users are required.
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 11:53:40 PDT