Subject: [sv-ac] more advanced sampling
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Feb 13 2003 - 19:51:38 PST
All:
I have been thinking about the relationship between CBV local
variables, the "forall" construct in PSL, and dynamic variables in
OVA/ForSpec and SVA. I am trying to understand if and how the
following sort of check can be written in these languages. I believe
thinking about writing this check is useful because it helps to show
how well the languages facilitate the dataflow and use of sampled data
in a temporal check.
I want to write a parameterized check, sum_check, with the following
parameters:
n, a 4-bit signal parameter;
x,y, 8-bit signal parameters;
b, a 1-bit signal parameter.
I want to be able to have multiple instances of sum_check active at
the same time, and I want to be able write such instances in a way
that an instance of sum_check can be triggered on match of a sequence.
In a full temporal language like PSL or OVA/ForSpec, I want to
be able to write an instance of sum_check anywhere a formula can be
written.
Here is the specification of sum_check:
Let n_0 be the value of n at the time the check is triggered.
If n_0 == 4'h0, pass.
If n_0 == 4'h1, then at the first occurrence of b from the
time the check is triggered, assert that y == 8'h0. If there
is no such occurrence of b, then pass.
Otherwise, at the (n_0)th occurrence of b from the time the
check is triggered, assert that the value of y is equal to the
sum mod 2^8 of the values taken by x at the previous (n_0)-1
occurrences of b. If there is no such (n_0)th occurrence of b,
then pass.
Notice that this check requires sampling the value of n at
the start to get n_0. I think such sampling can be accomplished
in all the langauges.
The more interesting part of the check is that x must be
sampled at various points and accumulated in order to make
the assertion on y. The number of these samplings depends
on the value sampled initially from n and on the parameter b,
which determines the event for the sample points.
Can this kind of parameterized check be written in PSL, OVA/ForSpec,
and/or SVA? If so, how? If not, can the check be written if each
instance of the check binds n to a compile-time constant?
The check can be written in fairly straightforward CBV as
shown in the code below.
Best regards,
John Havlicek
---------------------------------------------------------------------
m_task next_high(s[0:0]);
begin
if (s)
match;
else
if +(0 to *) : (!s)
if +(1) : (s)
match;
end
endtask
task sum_check_recur(const n[0:3], x[0:7], y[0:7], b[0:0], const sum[0:7]);
begin
if (next_high(b))
if (n == 4'h1)
y == sum;
else
begin
local temp_sum[0:7] = sum + x;
+(1) : sum_check(n-1, x, y, b, temp_sum);
end
end
endtask
task sum_check(const n[0:3], x[0:7], y[0:7], b[0:0]);
begin
if (n == 4'h0)
1;
else
sum_check_recur(n, x, y, b, 8'h0);
end
endtask
This archive was generated by hypermail 2b28 : Thu Feb 13 2003 - 19:56:57 PST