Re: [sv-ac] coverage

Hi Dmitry:

In Clause 17, we have an intuitive description of multiplicity 
of matching.  For example, in 17.7.5 p. 251, the multiplicity of 
matching for "intersect" is described as follows:

   Matches of the first and second operands that are of the same
   length are paired.  Each such pair results in a match of the
   composite sequence, with length and endpoint equal to the 
   shared length and endpoint of the paired matches of the operand
   sequences.

In Annex E, we do not define multiplicity.  Instead, we have a
relation:

   w |== R

[Let's ignore local variables for simplicity.  Multiplicity is
related to local variables, though, because it is through distinct 
local variable values that you can witness multiplicity.]

We should be able to define a multiplicity function m such that 
m(w, R) is a non-negative integer and such that

   w |== R  iff  m(w, R) > 0

Then we should find 

   m(w, R intersect S) = m(w, R) * m(w, S)

   m(w, R or S) = m(w, R) + m(w, S)

   m(w, R ##1 S) = \sum_{u,v : uv = w} m(u, R) * m(v, S)

and so forth.  There should not be much (if any) guesswork
to writing down the definition.  Logical "or" and "exists"
should go into arithmetic sums, while logical "and" and "forall" 
should go into arithmetic products.

Regarding first_match, from 17.7.7 p. 255 we have:

   If there are multiple matches of seq with the same ending
   clock tick as the earliest one, then all those matches are
   matches of first_match(seq). 

This is why I say that first_match(a or b) has a multiplicity
two match at a clock tick if both a and b are satisfied there.

Whether or not the coverage hit definition should incorporate
multiplicity is not so clear.  My interpretation of "all matches 
per attempt" semantics in 17.13.3 has been that it includes 
multiplicity.  However, I think 17.13.3 needs to be rewritten,
and there is certainly the opportunity to relax the requirements
on the tools to collect coverage statistics.  

Best regards,

John H.

> X-IronPort-AV: i="4.03,136,1141632000"; 
>    d="scan'208"; a="15687499:sNHT36939273"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 28 Mar 2006 11:21:34 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] coverage
> thread-index: AcZOwAX4qgEumV4bT0u8gj6E/88RswDg06Rg
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <dbustan@freescale.com>, <sv-ac@eda.org>
> X-OriginalArrivalTime: 28 Mar 2006 09:21:53.0969 (UTC) FILETIME=[0D872A10:01C65249]
> 
> Hi John,
> 
> Apparently there is a problem with the hit definition for the coverage.
> I don't quite understand why first_match(a or b) should report two hits
> instead of one.
> 
> I see two options:
> 1) Significantly extend the language for coverage constructs introducing
> sets, skews (cross coverage items), etc which will define EXACTLY what
> is going to be checked (e.g., all possible combinations, one hit, etc).
> This implies merging two different coverage concepts (chapter 17 and
> chapter 18) into one. It might be a right thing to do, because at
> present there is absolutely no relation between the two coverage
> concepts, and SV coverage treatment is very eclectic; but it requires a
> deep revision of the entire language.
> 
> 2) Define minimal requirements for the tools - e.g., each tool should
> report all witness points (=3D all points defining the finite property
> witness plus one partial witness at the simulation end). It does not
> define exactly - how the tool actually does it: reports one hit point
> for each time moment, multiple hit points when several transactions
> terminated simultaneously etc.
> 
> Consider the following examples (using proposed followed_by construct):
> 
> cover property (@(posedge clk) a ##1 (b or c));
> 
> The tool should report all points when either consecutive a, b or a, c
> combinations happen. It should be up to the tool whether to distinguish
> between a, b and a, c or not. It also should be up to the tool to match
> between a transaction beginning (=3Dwhen a happened) and its end (=3D =
> when b
> or c happened)
> 
> cover property (@(posedge clk) en followed_by !b[*1:$] |-> a);
> 
> The tool should report all sequences triggered by en, started with a
> series of a terminating with b. It also should report the sequence when
> a was always asserted until the end of the simulation.
> 
> The second version seems much more feasible, since the first version
> will take years to define.
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
> Havlicek
> Sent: Thursday, March 23, 2006 11:20 PM
> To: krolnik@lsil.com
> Cc: dbustan@freescale.com; sv-ac@eda.org
> Subject: Re: [sv-ac] coverage
> 
> Hi Adam:
> 
> >=20
> > Is there consideration of a first match operator for choosing single
> instead of=20
> > multiple matches?
> >=20
> 
> I think that trying to use first_match is a reasonable thing,
> but there are some difficulties in getting this solution to
> work.
> 
> The two coverage semantics described currently in the LRM are
> really "all matches per attempt" and "at most one match per attempt".
> The main problem with the LRM is the way it defines when one or
> the other of these applies. =20
> 
> My opinion is that the criteria described in 17.13.3 are ambiguous and
> too "tricky".  Some accidents of the way the sequence expression is
> written are used to determine which semantics applies.  This is why
> I prefer some clear syntax for the distinction, like a different=20
> directive.
> 
> The use of first_match seems like a clear syntactic distinction,
> but I don't think it exactly solves the problem without creating
> some others. =20
> 
> While first_match usually results in "at most one match per
> attempt", this is not always the case.  For example, if both=20
> boolean conditions "a" and "b" occur at the clock event, then=20
> "first_match(a or b)" has a double hit at that event.  So if the=20
> "all matches per attempt" semantics is used, you will get 2 hits,
> while if the "at most one match per attempt" semantics is used,
> you will get only 1 hit. =20
> 
> Also, with the current wording of 17.13.3, the appliction of
> "first_match" does not itself clarify which semantics to use.
> Therefore, some modifications to 17.13.3 need to be made to
> explain how the use of "first_match" determines which semantics
> apply.  To me, this seems tricky and likely to result in more
> backward incompatibilities than the solution that adds a
> "cover sequence" directive that has "all matches per attempt"
> semantics and redefines "cover property" always to have=20
> "at most one match per attempt" semantics.
> 
> Best regards,
> 
> John H.