ConcurrentAssertNewProposal < P1800

P1800 Web>SystemVerilogSpecialCommittee>ConcurrentAssertNewProposal (2008-05-05, ErikSeligman) (raw view)EditAttach
---+ New Proposal for Concurrent Assertions

The current definition of concurrent assertions in procedural code (from the 2005 standard) seems a bit shaky to many committee members, due to numerous special-case rules and behavior which does not follow the procedural code.  Thus this new proposal, summarized below by Gord.

---++ Procedural Triggering

Getting rid of the inferred enabling and rather to talk about "triggering"  an assertion.  I prefer to think of this as creating and dispatching an assertion process.  Let's consider a simple example.  The following is from 16.14.5 (P1800-Draft 5):

<verbatim>
     property r3;
         @(posedge mclk)(q != d);
     endproperty
     always @(posedge mclk) begin
         if (a) begin
             q <= d1;
             r3_p: assert property (r3);
         end
     end


     property r3;
         @(posedge mclk)a |-> (q != d);
     endproperty
     r3_p: assert property (r3);
</verbatim>

The key aspect here is the "r3" rewrite, so I'll focus on that.

The suggestion that was made was that the enable could be evaluated "in place".  In other words, one could create a new process to evaluate "r3" each time the sequential flow led to the concurrent assertions location.  This would be somewhat similar to conceptually doing:

<verbatim>
     property r3;
         @(posedge mclk)(q != d);
     endproperty
     always @(posedge mclk) begin
         if (a) begin
             q <= d1;
             fork
                  assert property (r3);
             join_none
         end
     end
</verbatim>

This isn't really any different from the perspective of the current LRM, but if you consider the "assert property (r3)"
is causing the initiation of a new assertion process, then I think we have an idea of what is being proposed.

This does make a difference in that the enabling conditions aren't subject to the same sampling as the current definitions.  That is what needs to be explicitly discusssed yet.


---++ Immediate vs Sampled Values

For the purposes of argument, I copied over one of Dmitry's examples from the [[http://www.eda-stds.org/sv-sc/hm/att-0049/EmbeddedConcurrentAssertions__080422dk.pdf][EmbeddedConcurrentAssertions__080422dk.pdf]] document on the Twiki site.

<verbatim>
     always @(posedge clk) begin
         for (int i = 0; i < 2; i++) begin
             if (en[i]) begin
                 if (a) begin
                 end
                 else begin
                     c1[i] <= c2[i] || b;

                     p: assert property (c2[i] |=> c1[i]);
                 end
             end
         end
     end
</verbatim>

Consider the assertion:

<verbatim>
     p: assert property (c2[i] |=> c1[i]);
</verbatim>

Assume that we allow an assert to have optional list of "const" (or immediate) names specified prior to the property.  For example:

<verbatim>
     p: assert const (i) property (c2[i] |=> c1[i]);
</verbatim>

The conceptual  intent here is that "i" adopts a constant value for the dispatch of a process that evaluates the property.  So "c2" and "c1" are normal sampled values and "i" is an "immediately captured" value that is captured at the time that the assertion process is initiated.

This approach is "owned" by the context, not the assertion.
So, for example, one could have:
<verbatim>
     p: assert const (i) some_prop(c2[i], c1[i]);
</verbatim>

and "i" would have the same "immediate capture" semantics.  This would also deal with situations that were raised with respect to intermediates:

<verbatim>
     int j;
     always @(posedge clk) begin
         for (int i = 0; i < 2; i++) begin
             if (en[i]) begin
                 if (a) begin
                 end
                 else begin
                     j = i;
                     c1[i] <= c2[j] || b;

                     p: assert const (i,j) property (c2[i] |=> c1[j]);
                 end
             end
         end
     end
</verbatim>

The nature of "j" as a static is immaterial since it was explicitly noted as a "const".





-- Main.ErikSeligman - 05 May 2008
Topic revision: r1 - 2008-05-05 - 14:26:05 - ErikSeligman
P1800