Hi Bassam,
If I understand your point correctly, I agree that coverage computations can be done in the underlying HDL. However, the main challenge is capturing the data to cover, especially when it is somewhere in the middle of a transaction. The point of issues 42 and 43 is to make it possible for data captured in PSL to flow into coverage computations in the HDL.
Many users seem to want something like local variables in sequences, so they can capture data during recognition of the sequence and do something with it later. In this email I was trying to show two things:
1. A very specific, focused application for capturing data to use later, namely for data coverage and transaction coverage.
2. That the notion of forall (or 'for some') parameters would be sufficient for applications such as this.
Yes, as I've shown, you can write a cover directive for each value or each range of values that you are interested in - but if you can capture actual data (using PSL sequences as the vehicle for 'parsing' the behavior in which those values are embedded) and pass the data on to HDL code, you can do much more interesting analyses.
Regarding cross coverage, I'm not sure how you separate the language from the tools - after all, the simulator is one of the tools we use. In any case, cross coverage is just another function that requires data, and the basic issue is to find a way to leverage PSL specifications to extract data from the design's behavior.
Regards,
Erich
| -----Original Message-----
| From: Bassam Tabbara [mailto:bassam@novas.com]
| Sent: Friday, December 03, 2004 7:02 PM
| To: Erich Marschner; ieee-1850-extensions@eda.org
| Cc: ieee-1850-issues@eda.org
| Subject: RE: Examples of Data Coverage, Transaction Coverage
|
| Erich,
|
| Thanks for the detailed email explaining these issues. Here's
| an explanation for the 0 priority assignment I had made to
| both of these. I do not subscribe to the notion of needing
| "data coverage" because data expressions should be (and
| are...) part of the underlying "flavor", the "cover" at the
| PSL layer (so-called "control" cover (a misnomer really)) is
| just the top level shell giving the 0/1 (yes/no) response.
| For example I can always write "cover (0 < v < 4096)", if v
| is of the right data type ... And then cover
| (...) at the very top, no matter how complex the underlying
| expression (may be I need functions to do what I need, but
| that would still be in the underlying flavor...).
|
| So basically PSL should only be looking at the validity of
| the "characteristic function" of the data portion. If there
| is any expression of binning and the like it is the
| underlying model's role to do so (as in covergroups, ADTs,
| and the like in SV).
|
| Same goes for transactions, and you all but say this below for "3"
| (packages).
|
| As far as cross coverage and the like, isn't that in the
| realm of tools:
| statistics gathering/presentation/analysis/manipulation ?
|
| ** On a related side note: I also gave a low priority and OOS
| to the access APIs (e.g. cover) because that too is better
| addressed (defining what/how to
| access) in the underlying language.
|
| Thx.
| -Bassam.
|
|
| --
| Dr. Bassam Tabbara
| Architect, R&D
| Novas Software, Inc.
| (408) 467-7893
|
| -----Original Message-----
| From: owner-ieee-1850-issues@eda.org
| [mailto:owner-ieee-1850-issues@eda.org]
| On Behalf Of Erich Marschner
| Sent: Friday, December 03, 2004 2:13 PM
| To: ieee-1850-extensions@eda.org
| Cc: ieee-1850-issues@eda.org
| Subject: Examples of Data Coverage, Transaction Coverage
|
|
| All,
|
| During the Extensions Subcommittee meeting this week, I was
| asked to provide examples of what was intended by issues 42
| and 43, which address
| data-oriented and transaction-oriented coverage respectively. The
| following attempts to explain what I meant by these issues,
| and considers some ways of implementing the capability.
|
| For those of you in the Issues SC who needed more information
| in order to prioritize these two issues, please send me an
| updated priority list.
|
| If there are any questions, please contact me.
|
| Regards,
|
| Erich
|
| =======================================================
|
| Explanation of Issues 42 and 43 (Data and Transaction Coverage)
|
| 1. Data-oriented coverage (Issue 42)
|
| PSL cover directives are fine for monitoring for
| control-oriented coverage points, i.e., coverage of control
| conditions and sequences. It is easy to write cover
| directives such as
|
| CP1: cover {queue_full};
| CP2: cover {req[*]; (req && ack)[*]; (!req && ack); !ack};
|
| However, it is more difficult to monitor for data-oriented
| coverage, in which we are interested in the values that
| variables take on during verification. For example, if we
| have a variable V that stores an integer in the range 0:4095,
| we might want to know
| - whether the variable had each value in the range
| - whether the variable had values in representative
| subranges (e.g., 0:1023, 1024:2047, 2048:3071, 3072:4095)
| (this is called "binning")
| - how many times each of the above occurred
| (i.e, counting occurrences rather than returning a
| boolean result)
| - whether/how many times V had a value (in some range) when
| another variable had another value (in some range)
| (this is called "crossing", or computing a
| cross-product between two sets of coverage points)
|
| The first case, which is simplest, could be addressed by
| writing 4096 cover directives - e.g.,
|
| V_0: cover {v==0};
| V_1: cover {V==1};
| ...
| V_4094: cover {V==4094};
| V_4095: cover {V==4095};
|
| Since this is tedious to write, one might prefer to use the
| %for construct to generate them:
|
| %for i in 0:4095 do
| cover {V==i};
| %end
|
| Note, however, that it may be difficult to generate
| individual cover directive labels this way. Also, as
| mentioned in the meeting on Tuesday, since %for is a
| compile-time loop, the range must be compile-time static, so
| it cannot be dependent upon a VHDL generic or a Verilog
| parameter, which doesn't have a value until elaboration time.
|
| Another alternative would be to use forall, if forall were
| allowed to be used with directives. In this case, we might write
|
| forall i in {0:4095}: cover {V==i};
|
| the result of which would be a list of 4096 cover directives,
| and each would indicate whether the corresponding value of i
| was the value of V at some
| point in time. Although this approach avoids the requirement for
| compile-time static ranges, it still appears that it would be
| difficult to generate a unique label for each cover directive.
|
| Even if we support forall applied to cover directives, we
| would still have to address the need for binning, counting,
| and crossing. So it is not clear that either forall or %for
| by itself will be sufficient to enable data coverage in PSL.
|
| One possiblity might be to use the 'for some' concept we've
| been discussing to define an endpoint, and then allow the
| matching value of the 'for some'
| variable to be exported into modeling layer code. For
| example, we might write something like the following. (I've
| switched to VHDL here because it is easier for me; I believe
| that the same sort of thing can be done in Verilog, or at
| least in SystemVerilog).
|
| endpoint V_value is for some i in {0:4095} :
| {V=i}@rose(clk); -- note
| that '=' in VHDL is equality, not assignment
|
| Assume that this would match any sequence in which the value
| of V is in the range 0:4095. Furthermore, assume that
| whenever endpoint V_value holds, the expression (V_value.i)
| would return the value of i for which V_value holds.
|
|
| With this capability, one could write the following modeling
| layer code to track coverage of V:
|
| process (V_Value)
| constant Bins: Coverage.bin_array(1 to 5) := ((0,255),
| (256,511), (512,1023), (1024,2047), (2048,4095));
| variable Counts: Coverage.counter_array(1 to 5) := (0,0,0,0,0);
| begin
| if V_value then
| Coverage.count(V_Value.i, Bins, Counts);
| end if;
| end process;
|
| where 'Coverage' is the name of a package that defines types
| such as bin_array and counter_array used to specify bins and
| create coverage counters, as well as the 'count' procedure
| that increments the appropriate counter in an array of
| counters, based on a set of bin definitions and the current
| value of the covered variable. A definition of such a
| package appears below, in section 3.
|
| 2. Transaction-oriented coverage
|
| Transaction-oriented coverage is intended here to mean
| data-oriented coverage applied to transient data communicated
| over a bus rather than to data stored in a variable. A
| transaction can be thought of as a sequence of signal
| values/changes that accomplish such communication over a bus.
| For example, a simple bus protocol might define (say) 5
| transaction types, one of which is a Write transaction (i.e.,
| send some data to some address). The protocol might require
| something like the following sequence of events in order to
| accomplish a Write transaction:
|
| - Sender requests bus control
| - Arbiter grants bus control
| - Sender says "Write operation" and specifies the target address
| - Sender says "Write operation" and specifies data to be written
| - Memory acknowledges successful completion of Write operation
| - Sender releases bus control
| - Arbiter releases bus grant
|
| If we want to do data-oriented coverage analysis on the data
| written during such a Write transaction, we have two
| challenges: first, we have to recognize that a Write
| transaction is taking place on the bus; second, we have to
| sample the data lines of the bus in the appropriate cycle in
| order to capture the data value being transferred in the
| transaction. Once that is done, the problem reduces to the
| previous one - how to do data-oriented coverage on the values
| of a (in this case, virtual) variable.
|
| We can use the existing cover directive to recognize when a
| transaction is occurring. For example, we might write the
| following cover directive to recognize a Write transaction
| that conforms to the above simple protocol:
|
| cover {request; grant; op=WRITE; op=WRITE; memack; not
| request; not grant};
|
| But this only deals with the control signals involved in the
| transaction - in effect, with the 'envelope' that
| encapsulates the data being transferred.
| To look at the data, we need to save the value on the data
| lines of the bus during the 4th cycle of the transaction (in
| which the Sender says "Write operation" and specifies the
| data to be written).
|
| Forall applied to cover directives might enable us to detect
| each unique data value being transferred by a Write
| transaction. For example, we might write the following:
|
| forall d in {0:255}:
| cover {request; grant; op=WRITE; op=WRITE and
| to_int(dbus(7 downto 0))=d; memack; not request; not grant};
|
| However, as the range of values gets larger, this involves
| more and more copies of the directive, which would be
| inefficient. Also, as mentioned above, it does not provide a
| way to uniquely label each directive, nor does it support
| binning, counting, and crossing.
|
| We could apply the 'for some' mechanism suggested above to do
| transaction coverage also. For example, we might write
|
| endpoint WriteT is
| for some {d in 0:255} :
| {request;
| grant;
| op=WRITE;
| op=WRITE and to_int(dbus(7 downto 0))=d;
| memack;
| not request;
| not grant};
|
| and reference the endpoint in modeling layer code as follows:
|
| process (WriteT)
| constant Bins: Coverage.bin_array(1 to 3) := ((0,15),
| (16,31), (128,255));
| variable Counts: Coverage.counter_array(1 to 3) := (0,0,0);
| begin
| if WriteT then
| Coverage.count(WriteT.d, Bins, Counts);
| end if;
| end process;
|
| Note that there is no requirement that the bins fully cover
| the possible range of values of the variable. Similarly, one
| might want to define the 'count' procedure so that it can
| increment multiple bins, therefore allowing overlapping bins.
|
| This same approach could be used to cover multiple values
| within the sequence and do cross-product coverage as well.
| For example, we might want to capture the address value as
| well as the data value in a Write transaction, and then
| analyze how well we covered both the address range and the
| data range, as well as the combination of the two. This
| might be done as follows:
|
| endpoint WriteT is
| for some {d in 0:255} :
| for some {a in 0:2**16-1} :
| {request;
| grant;
| op=WRITE and to_int(abus(15 downto 0))=a;
| op=WRITE and to_int(dbus(7 downto 0))=d;
| memack;
| not request;
| not grant};
|
| process (WriteT)
| constant ABins: Coverage.bin_array(1 to 5) := ((0,0),
| (1,4095), (4096,2**10-1), (2**10,2**13-1), (2**13,2**16-1));
| constant DBins: Coverage.bin_array(1 to 4) := ((0,15),
| (16,31), (32,127), (128,255));
| variable Acounts: Coverage.counter_array(1 to 5) := (0,0,0,0,0);
| variable Dcounts: Coverage.counter_array(1 to 4) := (0,0,0,0);
| variable AxDcounts: Coverage.counter_array(1 to 20) :=
| (others => 0);
| begin
| if WriteT then
| Coverage.count(WriteT.a, ABins, Acounts);
| Coverage.count(WriteT.d, DBins, Dcounts);
| Coverage.cross(WriteT.a, WriteT.d, ABins, DBins, AxDcounts);
| end if;
| end process;
|
| This would produce 5 counts for address value a (one for each
| of the 5 specified subranges), 4 counts for data value d (one
| for each of the 4 specified subranges), and 20 counts for the
| cross-product of the counts of d and a.
|
|
| 3. Definition of a Coverage package
|
| The following definition is given in VHDL. I believe a
| similar definition could be provided in Verilog (or at least
| in SystemVerilog).
|
| The package declaration defines types bin (representing a
| range of integer values), bin_array (an array of any number
| of bins), counter, and counter_array (an array of any number
| of counters). The package declaration also declares the
| interface for the procedure 'count', which takes a value, an
| array of bin definitions, and an array of counters, as well
| as the interface for procedure 'cross', which takes two
| values, two bin arrays, and a counter array. The package
| body declaration contains the bodies of both procedures,
| which basically loop through the bin definitions and
| increment the appropriate counter.
|
| package Coverage is
|
| type bin is record
| low, high: integer;
| end record;
| type bin_array is array (natural range <>) of bin;
|
| type counter is integer range 0 to integer'high;
| type counter_array is array (natural range <>) of counter;
|
| procedure count (Value: in integer; Bins: in bin_array;
| Counters: inout counter_array);
| procedure cross (Value1, Value2: in integer; Bins1, Bins2:
| in bin_array;
| Counters: inout counter_array);
|
| end;
|
| package body Coverage is
|
| procedure count (Value: in integer; Bins: in bin_array;
| Counters: inout
| counter_array) is
| begin
| for i in Bins'range loop
| if Value >= Bins(i).low and Value <= Bins(i).high then
| Counters(i) := Counters(i) + 1;
| exit;
| end if;
| end loop;
| end;
|
| procedure cross (Value1, Value2: in integer; Bins1, Bins2:
| in bin_array;
| Counters: inout counter_array) is
| variable i1, i2, j: integer := 0;
| begin
| assert Counters'high = Bins1'high * Bins2'high; --
| check that the
| cross-product array is the right size
| for i in Bins1'range loop
| if (Value1 >= Bins1(i).low and Value1 <= Bins1(i).high) then
| i1 := i; exit;
| end if;
| end loop;
| for i in Bins2'range loop
| if (Value2 >= Bins2(i).low and Value2 <= Bins2(i).high) then
| i2 := i; exit;
| end if;
| end loop;
| j := i1*i2;
| if j > 0 then
| Counters(j) := Counters(j) + 1;
| end if;
| end;
|
| end;
|
|
|
|
|
|
|
Received on Fri Dec 3 17:01:34 2004
This archive was generated by hypermail 2.1.8 : Fri Dec 03 2004 - 17:01:34 PST