User guide

20-13
Using OpenVera Assertions
GR17: RECOMMENDATION for loop over events /
assertions with large (>20) ranges with loop index
appearing in delay or repetition operators.
Consider using variables and / or compacting into a single event. For
an example see the OVA standard checker "ova_req_ack_unique".
It contains two versions of a checker, version 0 that is suitable for
small ranges of parameters, and version 1 that uses a time stamp
and a queue when the loop ranges become large (thus creating too
many events / assertions).
GR19: WARNING the "past" operator is over a long
time interval (> 1000).
Consider if the same property can be expressed differently without
the use of a deep look into the past (or in the future using # delay,
which would have a similar problem.)
GR25: WARNING a conditional check assertion that
involves open-ended delay interval in the consequent
(unbounded eventuality).
Example:
event e: if c then some_sequence1 #[1..] some_sequence2;
This assertion cannot fail in a simulation because of the failure of
"some_sequence2" because "some_sequence2" could occur after
the simulation ends.
Consider placing an upper bound on the delay interval as follows:
event e: if c then some_sequence1 #[1..20] some_sequence2;
GR26: WARNING OVA variable not initialized to a
known value.
Consider initializing the variable to 0. For example:
logic v = 1'b0;
This may be needed if the OVA checker is to be used with formal tools.