Re: [sv-ac] assertion of vacuous_prop_at_t0 or nonvacuous_prop_at_t5 // what results??

 //An open question (c.f. Mantis 0921) is what do you want the tool
// to do with something like
    1 |=> (0 |-> 1) or (##5 (1, $fatal(“go away!”)))
    1 |=> (1 |-> 1) or (##5 (1, $fatal(“go away!”)))

Also, addressing http://www.eda-stds.org/svdb/view.php?id=0921

I think that a tool should terminate an assertion upon one of the following
conditions:
a) In the cycle in which the property fails (nonvacuous fail or vacuous
fail)
b) In the cycle in which the property evaluates to nonvacuous true
c) In the cycle in which there are no more threads to evaluate and the
property evaluates to vacuous true
Thus, consider the following assertions (format simplified for discussion):
*case 1)*   1 |=> (0 |-> 1) or (##5 (1, $fatal(“go away!”)))
The property should proceed through to the $fatal("go away!")
 *case *2)   1 |=> (1 |-> 1) or (##5 (1, $fatal(“go away!”)))
The property should end in the cycle following the antecedent, $fatal would
be be processed.
*Note*: We could have a simulator switch that requires that all threads be
evaluated, but that would be combersome, particularly for sometime with an
infinite potential threads.  If the user wants the $fatal then he can split
the assertion into separate assertions.
 *case 3)*  ((a ##1 a) or(b ##1 b)) ##1 (c, $display("c")); *// assume
a==b==c==1 at all cycles*
The $display should be executed once because the sequence ((a ##1 a) or(b
##1 b)) consists
of 2 threads and one success occurs in cycle 2, thus ending that
subsequence  Now consider the following variation:

*case 4)*  ((a ##2 a) or(b ##1 b)) ##1 (c, $display("c")); *// assume
a==b==c==1 at all cycles*
The $display should be executed once because the subsequence ((a ##2 a)
or(b ##1 b)) consists of 2 threads and terminates in cycle 2 with the (b
##1 b).  The ##1 (c, $display("c") is evaluated once.

*case 5)*  ((a[*2] , $display("aa")) ##1 a) intersect b[*3];
The $display should be executed once because at the conclusion of a[*2],
the $display is executed.
 *case 6)*  (a , $display("aa")[*2]  ##1 a) intersect b[*3];
The $display should be executed twice because at the concluse of each a,
the $display is executed.

Ben Cohen

On Tue, Dec 18, 2012 at 6:33 AM, John Havlicek <johnh@cadence.com> wrote:

> Hi Erik:****
>
> ** **
>
> The LRM does not state rules for deciding to terminate assertion
> evaluation early.  See Mantis 0921.  The hole has been known for a long
> time and there has been considerable technical work, but interest in what
> seems an esoteric question has been low and consensus on a solution has not
> been reached.  In my opinion, it remains important to resolve this Mantis
> to provide semantics for subroutines attached to sequences.****
>
> ** **
>
> The LRM does specify semantics for non-vacuous evaluation in F.5.3.3.  If
> you follow that definition in Ben’s example****
>
> ** **
>
> (*)   a |=> (0 |-> 1) or (##5 1)****
>
> ** **
>
> it says that for non-vacuity you must****
>
> ** **
>
> **1.       **match the antecedent “a ##1 1” (the ##1 from translation of
> |=>)****
>
> **2.       **follow that either with non-vacuous evaluation of “0 |-> 1”
> or with non-vacuous evaluation of “##5 1”****
>
> ** **
>
> You can’t have non-vacuous evaluation of “0 |-> 1” because the antecedent
> “0” doesn’t match.  Therefore you have to get a non-vacuous evaluation of
> “##5 1”.  The “##5 1” is a weak sequential property, so any evaluation of
> it is considered non-vacuous.****
>
> ** **
>
> The net result is that evaluation of (*) is non-vacuous provided “a ##1 1”
> matches, and a tool could stop there.****
>
> ** **
>
> An open question (c.f. Mantis 0921) is what do you want the tool to do
> with something like****
>
> ** **
>
> (+) a |=> (0 |-> 1) or (##5 (1, $fatal(“go away!”)))****
>
> ** **
>
> Best regards,****
>
> ** **
>
> John Havlicek****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Seligman,
> Erik
> *Sent:* Tuesday, December 11, 2012 11:21 AM
> *To:* hdlcohen@gmail.com; sv-ac@eda-stds.org; Korchemny, Dmitry;
> Bresticker, Shalom
> *Subject:* RE: [sv-ac] assertion of vacuous_prop_at_t0 or
> nonvacuous_prop_at_t5 // what results??****
>
> ** **
>
> Does the LRM state any rules for deciding to terminate an assertion
> evaluation early, due to concluding that it’s true, false, or vacuous?  At
> a quick glance, I didn’t see such a rule.   If there are no explicit rules
> for early termination, your answer (c) would look right to me.****
>
> ** **
>
> Is this something that should be prescribed by the language, or is it
> intentionally left up to EDA tool implementers to decide when to optimize
> in this area?****
>
> ** **
>
> ** **
>
> *From:* Ben Cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Tuesday, December 11, 2012 8:31 AM
> *To:* sv-ac@eda-stds.org; Korchemny, Dmitry; Bresticker, Shalom;
> Seligman, Erik
> *Subject:* [sv-ac] assertion of vacuous_prop_at_t0 or
> nonvacuous_prop_at_t5 // what results??****
>
> ** **
>
> Consider the example below that breaks down to: ****
>
>   ap_or: assert property(a |=> (0 |-> 1)  or (##5 1) ); // assume a==1 at
> cycle t****
>
> What results should a simulator provide, per LRM? ****
>
> a) true vacuously, and quit evaluating at cycle t+1? ****
>
> b) true nonvacuously, and quit evaluating at cycle t+1?  *// Definitely
> not becuase of LRM 16.14.8h*****
>
> c) Since at cycle t+1 the evaluation is vacuous and there could be a
> nonvacuous evaluation in the other term of the or operator, ****
>
>    then the simulator should evaluate the other term in search of a
> potential nonvacuous result.****
>
> ** **
>
> The LRM is ambiguous on this point. If a tool yield answer****
>
>  "a", would that be acceptable? ****
>
> "b" would be an error, ****
>
> "c" might be better. ****
>
> ** **
>
> We need to clarify (another mantis) what result should be expected. ****
>
> ** **
>
> 16.12.3 Disjunction property****
>
> A property is a disjunction if it has the following form:****
>
> *property_expr or property_expr*****
>
> The property evaluates to true if, and only if, at least one of
> property_expr1 and property_expr2 evaluates to true.****
>
> ** **
>
> 16.14.8 Nonvacuous evaluations****
>
> e) An evaluation attempt of a property of the form *property_expr1 or property_expr2
> *is nonvacuous****
>
> if, and only if, either the underlying evaluation attempt of
> property_expr1 is nonvacuous or the****
>
> underlying evaluation attempt of property_expr2 is nonvacuous.****
>
> ** **
>
> h) An evaluation attempt of a property of the form sequence_expression |=>
> property_expr is****
>
> nonvacuous if, and only if, there is a successful match of the antecedent
> sequence_expression and****
>
> the evaluation attempt of property_expr that starts at the clock event
> following the end point of the****
>
> match is nonvacuous.****
>
> ** **
>
> module test_or;****
>
>             bit clk, a=1'b0, b, c; ****
>
>             initial forever #10 clk=!clk; ****
>
>             default clocking cb_ck1 @ (posedge(clk));  endclocking ****
>
>             property p_vac;****
>
>                         0 |-> 1;        ****
>
>             endproperty****
>
> ** **
>
>             property p_t_at5;****
>
>                         ##5 1'b1;       ****
>
>             endproperty****
>
>             ap_or: assert property(a |=> p_vac or p_t_at5);****
>
>             cp_or: cover property(p_vac or p_t_at5);****
>
> ** **
>
>             initial begin****
>
>                         repeat(2) @ (posedge clk); ****
>
>                         a <= 1'b1; ****
>
>                         @ (posedge clk) a <= 1'b0;  ****
>
>             end         ****
>
> endmodule****
>
> ** **
>
> Ben Cohen ****
>
> ** **
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>

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