User guide

20-18
Using OpenVera Assertions
Try to rewrite event "e2" without the use of "matched". In the case of
our simple example, the solution is simple due to the one cycle delay
introduced by "matched":
clock posedge clk {
// event e1: c #1 d; -- do not use
event e2: if a then c #1 d;
}
assert c: check(e2);
In general the transformation may not be as simple as in the above
example. It may be preferable to approach the problem differently
right from the start rather than trying to rewrite the case later.
MR5: ERROR simulation time is used as the OVA clock.
The notion of simulation time is not available in Magellan. However,
you can create an explicit periodic clock that provides some notion
of time advancement.
MR6: ERROR case equality is used in expressions.
This is non-synthesizable.
MR7: ERROR comparisons with 'z' and 'x' values is
used. This is non-synthesizable.
MR8: WARNING an uninitialized OVA variable is used.
An uninitialized variable may cause a simulation - formal mismatch
due to differences in interpreting the initial unknown value "x".