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

Hello Daniel;

There is a large history of trying to incorporate assertions into 
procedural code. My book
contains a chapter on a pli based assertion code from Harry Foster. That 
chapter describes
some problems that come up with an in line based approach. The problems 
are similar to
the problems discussed with the priority and unique keywords for case 
statements, but include
other issues related to clocks, resets, and time delays. Not accounting 
for these in an assertion
structure prevents one from reliably using assertions to report real 
problems in a design.

danielm wrote:
> 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.
>
>
>
>   

-- 
    Soli Deo Gloria
    Adam Krolnik
    Director of Design Verification
    VeriSilicon Inc.
    Plano TX. 75074
    Co-author "Assertion-Based Design", "Creating Assertion-Based IP"


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