RE: [sv-bc] concurrent assertions in procedural code

Hi Steven,

Unfortunately, it is not always easy to apply your approach. Consider a
slightly modified example:

always @(posedge clk) begin
 if (cond) begin
  for (int i = 0; i < 2; i++) begin
    if (en[i]) begin
      c1[i] <= c2[i];
      p: assert property (c1[i] == $past(c2[i]));
    end
  end
 end
end

Here the rewriting becomes much trickier.

Also, if you have a nested conditional statement, infer the enable
condition manually is really painful.

I think that the issues you pointed can be solved now on the
methodological level, in the future one can think how to improve
concurrent assertions in order to take the computation flow into
account. This should be feasible, but it is a major feature.

Thanks,
Dmitry

-----Original Message-----
From: Steven Sharp [mailto:sharp@cadence.com] 
Sent: Monday, March 17, 2008 5:49 PM
To: sharp@cadence.com; sv-bc@eda.org; sv-ac@eda.org; Korchemny, Dmitry
Subject: RE: [sv-bc] concurrent assertions in procedural code


>From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>

>Consider the following simplified example:
>
>always @(posedge clk) begin
>  for (int i = 0; i < 2; i++) begin
>    if (en[i]) begin
>      c1[i] <= c2[i];
>      p: assert property (c1[i] == $past(c2[i]));
>    end
>  end
>end
>
>If you want to rewrite it without embedding concurrent assertions into
>procedural code, you will have to write something like:
>
>always @(posedge clk) begin
>  for (int i = 0; i < 2; i++) begin
>    if (en[i]) begin
>      c1[i] <= c2[i];
>    end
>  end
>end
>
>genvar i;
>for (int i = 0; i < 2; i++) begin
>  p: assert property (en[i] |-> c1[i] == $past(c2[i]));
>  end
>end

One goal of having concurrent assertions inside procedural loops seems
to be sharing the loop structure and keeping them in sync between the
procedural code and the concurrent assertions.  As I have pointed out,
there are serious problems with trying to put the concurrent assertions
inside the procedural loops.  However, there is no reason you cannot
put both the procedural code and the concurrent assertions inside a
generate loop:

for (genvar i = 0; i < 2; i++) begin
  always @(posedge clk)
    if (en[i]) begin
      c1[i] <= c2[i];
    end
    p: assert property (en[i] |-> c1[i] == $past(c2[i]));
end

Here is an example of the problems caused by concurrent assertions
inside
procedural loops, illustrated with another version of the same example:

always @(posedge clk) begin
  for (int i = 0; i < 2; i++) begin
    int j = i + 1;
    if (en[j]) begin
      c1[j] <= c2[j];
      p: assert property (c1[j] == $past(c2[j]));
    end
  end
end

This looks fine to the reader, but the assertion completely fails to
work correctly.  Since j is not the loop index, this only generates
one check, and with a value for j that is different from any of the
values used in the assignments.

The closest equivalent using a generate loop would work:

for (genvar i = 0; i < 2; i++) begin
  localparam j = i + 1;
  always @(posedge clk)
    if (en[j]) begin
      c1[j] <= c2[j];
    end
    p: assert property (en[j] |-> c1[j] == $past(c2[j]));
end

A more likely example would have a variable offset instead of 1.
That would be just as easy to write in the procedural version, and
just as wrong.  It would take a little more thought to write it in
the generate version, because it doesn't allow you to write it in
the easy but wrong way.

I don't know how well this approach would work in general.  But a
procedural loop is a very bad match to the semantics of concurrent
assertions, while a generate loop works fine for both procedural
initial/always blocks and concurrent assertions.

Steven Sharp
sharp@cadence.com

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.