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 14:13:02 2004
This archive was generated by hypermail 2.1.8 : Fri Dec 03 2004 - 14:13:02 PST