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

Hi Daniel,

See my reply to Steven, where I sketched a potential alternative
approach based on shadow variables. It should cover the behavior you
suggest.

Dmitry

-----Original Message-----
From: danielm [mailto:danielm@aldec.com.pl] 
Sent: Friday, March 14, 2008 3:00 PM
To: Korchemny, Dmitry; 'Steven Sharp'; sv-bc@server.eda.org;
sv-ac@server.eda.org
Subject: RE: [sv-ac] RE: [sv-bc] concurrent assertions in procedural
code

Was anybody thinking about different approach to concurent assertion in
procedural code where assertion placed in procedural code  is triggered
only
at the moment when processing is flowing by the asertion. Each time
processing flow through line with assertion the assertion is scheduled
to be
checked (bit similar to expect statement). In this approach there is no
need
for restricting the place where assertion may be inserted. Such
assertion is
much easier to understand and more powerfull.

As for clock and reset condition maybe they should be give up - if there
is
no way to define it in sensible way. 

The only cons is that it won't be back compatybile.


DANiel

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Korchemny, Dmitry
Sent: Thursday, March 13, 2008 5:38 PM
To: Steven Sharp; sv-bc@server.eda.org; sv-ac@server.eda.org
Subject: [sv-ac] RE: [sv-bc] concurrent assertions in procedural code

Hi Steven,

The issues you mentioned are serious, but I think that there are still
big
advantages in placing concurrent assertions in procedural code. You
pointed
the following problems:

1. The clock inference rules from the always block are not intuitive.
2. Concurrent assertions don't follow intermediate (blocking)
assignments.
3. They show variable values one clock behind than it is natural to
expect.
4. Wrapping code fragments into subroutines cannot be straightforward in
presence of concurrent assertions in the procedural code.

I will try first to show the need in specifying concurrent assertions in
procedural code, and then to address your issues.

When using assertion-based validation (ABV) methodology writing
concurrent
assertions inside procedural code becomes absolutely critical. 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
if (en[i]) begin
  p: assert property (en[i] |-> c1[i] == $past(c2[i]));
  end
end

In the real life instead of en, c1, and c2 you will have something like

always @(posedge clk) begin
  for (int i = 0; i < 2; i++) begin
    if (ABCbus1Enabler[i]) begin
      NewValueOfSomeVector[i] <= OldValueOfSomeVector[i];
      p: assert property (NewValueOfSomeVector[i] ==
$past(OldValueOfSomeVector[i]));
    end
  end
end

and more complex conditional expressions, probably nested with different
assertions in different conditional clauses. If the people have to
manually
rewrite this code to specify standalone assertions, their life will
become
very difficult. Note that in the above example you cannot replace
concurrent
assertions with immediate/deferred ones.

I.e., the ability of writing concurrent assertions in procedural code is
crucial.

Unfortunately the problems you mentioned really exist, and I don't know
how
to provide immediate solutions, though in the long term satisfactory
solutions should be possible. It should be taken into account concurrent
assertions cannot be absolutely transparent to the user and they require
basic understanding of the underlying simulation mechanism.


Now I would like to address the specific problems:

1. The clock inference rules from the always block are not intuitive.

As far as I understand the rationale behind these rules is to infer the
clock and not the reset conditions from an always or always_ff
procedures.
E.g., in the following case:

always @(posedge clk or negedge rst) begin
	if (!rst) ...
	else ...
end

a clever synthesis tool would infer that the clock is clk and the reset
is
rst, and it will be able to do it even if the event list is written as

always @(negedge rst or posedge clk)

Unfortunately there is no clear way to define this rule for the clock
inference rules for assertions, unless there is a standard for SV
synthesis
that P1800 is trying to avoid. Therefore the clock inference rule for
assertion is defined just as taking the first event of this form in the
list. This definition is old, and it already exists in LRM'05. Several
clarifications have been made recently, but they still refer to the
first
event of a specific kind in the list.

2. Concurrent assertions don't follow intermediate (blocking)
assignments.

This is also a matter of definition, and this definition was accepted
long
time ago. The rationale is that if you deal with temporal assertions you
usually don't want to check states from the middle of one simulation
tick
until the middle of another simulation tick, but rather to sample the
simulation state either at the beginning of a simulation tick as defined
in
the LRM, or at the end of a simulation tick. Your example provides a use
case when the latter behavior is not intuitive.

I don't think that this issue may be addressed right now, the users just
need to know what they are doing, and I don't see how writing standalone
assertions can solve this problem: you still have to rewrite your
assertion
manually, in your case explicitly using {sel1, sel2} instead of a. You
will
just have to duplicate big parts of your code.

I can see two possible approaches to resolve the problem you pointed.
One of them would be introducing yet another kind of assertions, similar
to
concurrent assertions, but based on shadow variables. Your example may
be
conceptually rewritten as:

  logic a1_shadow, a2_shadow;
  always @(posedge mclk) begin
    a = {sel1, sel0};
    a1_shadow = a;
    case (a1_shadow)
      1:  begin q <= d1;
          r4_p: assert ??? (r4);
          end
      default: q1 <= d1;
    endcase
    a = something else;
    a2_shadow = a;
    case (a2_shadow)
    ...
  end

and the assertion of the new kind "assert ???" will produce the
intuitive
result (I am omitting here a discussion about shadow variable
initialization).

Another approach would be not to introduce a new kind of assertions, but
to
introduce a pseudo-function $shadow to be used in checker declaration,
that
would return a reference to an appropriate shadow variable. E.g., in
your
example when using checker a instead of the assertion, one could write:

checker r4(..., en = $shadow($inferred_enable));

This will be transparent to the user, and will produce the expected
result.

3. They show variable values one clock behind then it is natural to
expect.

I don't see any feasible solution here. This is common for all
concurrent
assertions, both standalone and embedded. The users will eventually get
used
to this situation.

4. Wrapping code fragments into subroutines cannot be straightforward in
presence of concurrent assertions in the procedural code.

I would prefer to be able to specify concurrent assertions in functions,
but
I don't see any immediate solution for this. But it should be noted that
the
immediate/deferred assertions should be sufficient in functions, while
the
concurrent assertions are temporal, and there is no compelling reason to
put
them into functions or in the middle of the code to be wrapped later
into a
function. If a concurrent assertion is extracted into a function then in
most cases it indicates that they were not written in an appropriate
place,
and the compilation error will only help to clean up the design.

To summarize: the problems you raised are tough, and some of them may be
addressed in the long term. However, IMO avoiding assertion embedding in
the
code now does not solve any problem, but only results in the code
duplication, which makes the code more error prone and less supportable.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-bc@server.eda.org [mailto:owner-sv-bc@server.eda.org] On
Behalf Of Steven Sharp
Sent: Saturday, March 08, 2008 4:41 AM
To: sv-bc@server.eda.org
Subject: [sv-bc] concurrent assertions in procedural code

My biggest concerns with checkers are their interactions with procedural
code.  These concerns do not apply just to checkers, but in general to
concurrent assertions in procedural code (and extending this further in
proposals such as Mantis 1995).

I have heard a number of members of this and other SV committees express
surprise when they heard that this was allowed, and the intended
semantics.
I was surprised and concerned when I heard about it.  I would like to
describe some of my concerns here.

The starting point of this was in IEEE Std 1800-2005 subclause 17.13.5
"Embedding concurrent assertions in procedural code".  It may look
rather
innocuous on first reading, but there are significant issues with it.

From the start it assumes that all procedural code is written in such a
way
that cycle semantics can be inferred from it, which is an invalid
assumption.  It talks about "the clock from the event control of an
always
block."  Note that it just assumes that there is exactly one event
control
in an always block.  There appears to be another assumption that this
event
control must appear at the start of the always block, though this is not
as
clear.

I understand that this is being clarified for the next revision of the
standard.  Rules are being created for when a clock should be inferred
and
what to do if it cannot (presumably an error if there is a concurrent
assertion in the always block).  From the viewpoint of the language in
general, such rules are arbitrary, and are a kludge.  Even from a
synthesis
view, these rules are unlikely to match those of any specific synthesis
tool.  Such rules would be more justifiable if they started by being
restricted to an always_ff construct, and the LRM defined restrictions
for
an always_ff that ensured a clock could always be inferred.

A more serious concern is that the concurrent assertion is embedded in
the
procedural code, but it does not execute when the flow of execution
reaches
it.  It can refer to the same variables as the procedural code around
it,
but it is not referencing the same values for those variables as the
procedural code.  Instead, it is executing in the Observed region and
referencing values sampled in the Preponed region.  This is inconsistent
with anything else in procedural code, and seems likely to lead to much
confusion and many mistakes.

As an example, the procedural code may assign a value to a variable, and
then have a concurrent assertion that appears to use that value.  But in
fact it will use a sampled value of that variable.  If the variable
value
changes again before it is next sampled, the assertion will never see
that
value.  Even if it doesn't, the assertion is using a value that is
running
one clock behind the rest of the procedural code it is in.

Assertion writers may take care to avoid referring to such intermediate
variables explicitly in assertions.  But what about inferred enabling
conditions?  One of the advantages of putting these assertions inside
procedural code seems to be that the enabling conditions will be
inferred
automatically from the procedural if and case conditions.  Just write
normal
procedural code, and the inferrence process will take care of the
enabling
conditions.  But what if those enabling conditions turn out to be
intermediate variables?  If you aren't explicitly specifying the
conditions,
but are trusting the implicit rules, you may not notice if this happens.

Take the case-statement example at the end of the subclause.  Suppose it
were written as

  always @(posedge mclk) begin
    a = {sel1, sel0};
    case (a)
      1:  begin q <= d1;
          r4_p: assert property (r4);
          end
      default: q1 <= d1;
    endcase
    a = something else;
    case (a)
    ...
  end
  
If I understand things correctly, this doesn't work as you would expect.
It works differently than if you had written "case ({sel1, sel0})".  The
assertion will sample the value of 'a' in the Preponed region, not at
the
point where execution reaches the concurrent assertion, where its value
has
actually been computed.  So the assertion will have a stale value,
unless of
course the value gets changed later in the procedural code, in which
case
the assertion doesn't even get a stale value.

This looks like a serious problem to me.  You may be able to spot it
fairly
easily in a simple case like this one.  But the advantages of embedding
assertions seem to be closeness to the related procedural code and not
having to explicitly specify the clock and enables.  For those
advantages to
be significant, the procedural code must be large and the enables
complex.
So this problem will not be easy to spot.
Even if you are careful when you insert the assertion, somebody may come
along later and modify some of the procedural code to insert an
intermediate
variable.

This all gets worse if Mantis 1995 is included.  My example of using an
intermediate variable and then re-using it for another value later may
have
seemed unusual.  But if you are writing code inside a loop, it is normal
to
have an intermediate variable that gets re-used each time around the
loop.

Another minor issue I have with this involves the use of tasks and
functions.  Normally you can take procedural code and modularize it,
moving
pieces into tasks and functions.  But if the procedural code contains
concurrent assertions, it cannot be moved into a subroutine.
There is no way to infer clocks and enables for a concurrent assertion
in a
subroutine.  So the use of concurrent assertions in procedural code will
prevent modularizing it.  To me, the fact that procedural code can
normally
be moved into tasks, but concurrent assertions cannot, is another
indication
that concurrent assertions do not belong in procedural code.

Steven Sharp
sharp@cadence.com


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

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


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