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

Hi Steven,

Of course, my example can be rewritten, but this style is not intuitive
for the users. Also, the users will have to write complicated enable
conditions in case of generate loops. I think that a more feasible
approach would be to use a linting tool which will issue warning
messages when trying to use a result of a blocking assignment in always
@(posedge ...) in embedded concurrent assertions. It looks to me that
such a check should not be difficult to implement, and it may be
built-in into a simulation/formal verification tool front end.

Thanks,
Dmitry

-----Original Message-----
From: Steven Sharp [mailto:sharp@cadence.com] 
Sent: Friday, March 21, 2008 2:51 AM
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>

>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.

I don't think this one is all that tricky.  You just factor the loop
to the outside.  It shouldn't matter that it was inside a conditional.

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

However, I do see other situations that would be problematic.  This
works if all the loops in the block have the same bounds, in which
case you can factor that loop out and then make it a generate loop.
But if there are different loops in the block with different bounds,
then you cannot factor the loops out.  The block would have to be
broken up into separate blocks that each had only a single set of
loop bounds first.

How big of a problem this is depends on how common such code is.  If
it is rare to be iterating across different sized arrays in the same
block, then this is not a big problem.  At worst, you can fall back on
the inconvenient separate generate loop for the assertions in that rare
case.



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

So is checking that the automatically inferred enable condition does
not use any values computed within the procedural block, and therefore
will work correctly (or that all of the values are computed within the
procedural block, and therefore will work correctly but with a delay
of one clock that must be compensated for).

Any argument based on the complexity of manually inferring the enable
condition also applies to the complexity of manually checking that the
automatic inferrence will actually function as expected.  

But users won't do that anyway.  They will assume that automatic means
that it is always correct, and then be unable to figure out why it is
not working correctly.  At least with a mistake in manually inferring
the enable condition, they can debug their mistake.  With it hidden
inside the automatically inferred condition, that is going to be hard.


>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.

IMO this feature should wait until we have come up with the improved
version that actually works correctly, rather than having a version
that only works if you carefully follow certain coding rules (which
are not even explained in the LRM).  Not only is this current version
unsafe, but it might conflict with adding an improved version in the
future that is safe.


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.