Subject: [sv-ac] cover requirements
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Thu Feb 20 2003 - 08:49:11 PST
Hi: I'm sending this for Surrendra who is on vacation today.
Proposal for "cover" requirements:
Cover directive syntax
cover_directive ::= [identifier : ] 'cover' prop_spec statement_or_null
prop_spec ::=
[ initial ] [ accept ( expression ) ] [ never ] clocked_expr
| identifier [ ( expression_list ) ] // identifier must be a property
clocked_expr ::=
[event_control] ( prop_expr )
prop_expr ::=
sequence_expr
| implication
| ( prop_expr )
implication ::=
sequence_expr => prop_expr
Requirements are divided into two:
1) coverage for properties,
2) coverage for sequences
For sequences, the expression appears as:
cover_directive ::= [identifier : ] 'cover' [event_control] '('
sequence_expr ')' statement_or_null
All other forms are considered to be properties.
Result of coverage directive for a property contains:
1) Number of times attempted
2) Number of times succeeded
3) Number of times failed
4) Number of times succeeded because of vacuity(limited)
5) Each attempt with attemptID and time
6) Each success/failure with attemptId and time
statement_or_null gets executed every time a property succeeds.
Vacuity rules are applied only when implication operator is used.
A property succeeds non-vacuously only if the last consequent of the
implication, if nested, contributes to success.
Result of coverage directive for a sequence is:
1) Number of times attempted
2) Number of times matched (each attempt can generate multiple matches)
statement_or_null gets executed for every match. If there are multiple
matches at the same time, the statement gets executed multiple times, one
for each match.
3) Each attempt with attemptId and time
4) Each match with clock step, attemptId and time
Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
This archive was generated by hypermail 2b28 : Thu Feb 20 2003 - 08:50:14 PST