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


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