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

Hi Doron,
 
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 ?
 
 
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).
 
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.
 
 
Thanks,
Yaniv
 
 
________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Bustan, Doron
Sent: Sunday, September 23, 2007 11:05
To: Lisa Piper; sv-ac@eda-stds.org
Subject: RE: [sv-ac] 1757 accept_on/reject_on proposal



Hi Lisa,

I made some changes according to the notes below.

 

1.      in 16.12, there is discussion of several kinds of properties.  I
am trying to relate this to the F.2.1 list.  F.2.1 does not list the
if-else and it references the "and" and "or" forms instead of
"conjunction" and "disjunction".  I'm not sure what the instantiation
means unless it is the parenthesized form. Should we use the same
terminology?  

[DB] That is a good question and we probably do something about it. But
since it is more then the accept_on reject_on issue, I would put it in
another mantis item. I did change the form to reset in annex F.

Also note the extra space in the new text "reset,   and instantiation"

[DB] fixed.

2.      "In particular, when reject_on ..."   ->  suggest dropping the
"in particular" since the statement before is not the same concept.

[DB] I disagree, the general clause talks about termination of the sub
property inside the accept_on, and the particular clause talks about
termination of the sub property inside the accept_on which happen to be
a reject_on.

3.      The paragraph above Annex F.3.6.1 that starts with "the operator
reject_on has the dual semantics." Needs to be reworded. Are you trying
to say:  "A word w satisfies property "reject_on(b) P" if and only if w
satisfies P before b is asserted. 

 

[DB] I made reject_on a derived operator (not accept_on (b) not P) and
removed this paragraph.

Doron

 

 

 

 

 

 

 

 

 

Lisa

---------------------------------------------------------------------
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 <http://www.mailscanner.info/> , and is

believed to be clean. 
-- 
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.