[sv-bc] inferred enabling conditions

Hi Steven:

A long time ago in SV-AC, I raised this issue of the inconsistency of
the semantics of an inferred enabling condition for a concurrent
assertion in procedural code with the semantics of the procedural
conditions executing as procedural code.

At that time the committee did not see a solution and/or chose not
to address the issue.

I was not previously aware of the issue involving tasks and functions.

J.H.

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

...

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

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