User guide

20-17
Using OpenVera Assertions
This type of an assertion cannot be used effectively as an assumption
in Magellan because it requires constraining the signals driving the
OVA variable "tmp" in the past clock tick. This is not possible when
doing random simulation constrained by OVA assertions. The result
is that no constraint is imposed. Consider correcting the assertion as
follows:
logic [bw-1:0] tmp;
assign tmp = c1 ? reg_A :
c2 ? reg_B;
clock posedge clk {
event e: |tmp == 1'b1;
}
assert c: check(tmp);
The constraint is now applied in the current clock cycle rather than in
the past one.
MR3: WARNING the "matched" or "ended" operator
appears in the consequent sequence of a "check"
assertion or as part of the sequence in a "forbid"
assertion.
The problem is that this form of an assertion cannot be used
effectively in random simulation under OVA constraints / assumption
because it requires constraining inputs in past clock cycles.
Example:
clock posedge clk {
event e1: c #1 d;
event e2: if a then matched e1;
}
assert c: check(e2);