RE: [sv-ac] 1757 accept_on/reject_on proposal

Hi Yaniv,

 

See my answers below

 

 

This proposal states that those constructs (accept_on/reject_on) are
checked asynchrounously, this is different from all other constructs
(except disable which is non nestable and only top-level) which are
synchronous to a clock, is there a reason and need for that ? wouldn't
this possibly slow-up simulation time ?

 

[DB] I must admit that I am not familiar with the practical need for
these operators (I know it exists but not the details).

But a few years ago when there was a debate about these operators in PSL
(there I believe that it is nestable and a synchronous) 

the motivation was a system with a few components each with its own
clock that  may reset one another. In this case a property that describe


one or more components may need to disable a sub property when the
component it describes is being reset (possibly by a component that is
not described by the property).

 

Dmitry do you wan to elaborate on that?

 

I think that any asynchronous modeling adds some complexity, but I am
not sure that the combination of nesting and asynchronous itself adds to
the complexity.

 

 

Your proposal also alows accept_on/reject_on for recursive properties, I
didn't find your examples however very motivating since the code you
wrote can be simply written without the accept_on/reject_on inside the
recursion.

 

instead of:

property p1(p, bit b, abort);

  accept_on(b) (p and (1'b1 |=> reject_on(abort) p1(p,b,abort)));

endproperty 

 

property s2(s,p,bit b, abort);

  s |-> p1(p,b,abort);

endproperty

 

write:

 

property p1(p, bit b);

  (p and (1'b1 |=> p1(p,b)));

endproperty 

 

property s2(s,p,bit b, abort);

  s |-> accept_on(b) (p and (1'b1 |=> reject_on(abort) p1(p,b);

endproperty

so the accept_on/reject_on are not inside the recursion.

 

instead of your the 2'nd example:

property p3(p,bit b, abort);

  (p and (1'b1 |=> p4(p,b,abort));

endproperty

 

property p4(p, bit b, abort);

  accept_on(b) reject_on(abort) p3(p,b,abort);  

endproperty

 

here if p4 is called first then the "accept_on(b) reject_on(abort)" can
be inside "p" (if that is a named property, if not then written next to
it), if p3 is called first then the same trick as the first example
(sepearing the first iteration from all the rest).

 

[DB] I agree that these are not very motivating examples. Our motivation
to put them was to demonstrate legal syntax.

I guess that the two examples are a little redundant I don't mind
removing one of them, what do people think?

 

 

 

This is since your examples are not changing the "reset conditions" of
every iteration of the recursive call therefore the usage of both
accept_on/reject_on inside recursion doesn't give much benefit.

 

since you allow nesting of accept_on/reject_on inside recursive
properties then I guess this kind of example is also allowed:

 

property p_rec(logic [SIZE-1:0] rjct_cond);

  reject_on(rjct_cond)

    ( cond_until 

      and

    ( cond_next |=> p_rec(dut_sig ^ rjct_cond));

endproperty

 

In the above example the reject_on condition is changing from each
recursive call to another making each iteration slightly different, this
is in contrast to the "return to the same state" meaning of the
recursive property call today, this could possibly make a bounded
automaton representation of this impossible.

 

[DB] this is not legal because of restriction:

 

RESTRICTION 4: For every recursive instance of q in the declaration of
p, each actual argument

expression e of the instance satisfies one of the following conditions:

- e is itself a formal argument of p.

- No formal argument of p appears in e.

 

 

I think that this means that only finite number of reset conditions
(linear in the property size) can be used. I guess

that this means that every recursive property with accept_on/reject_on
can be linearly translated to an equivalent one 

where the accept_on/reject_on operators are not in any cycle of the
dependency graph of the property. I don't think that

this decrease the motivation, which may simply be convenient and
readability 

 

Doron

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