[sv-ac] More on vacuity of property implies

Hi Ben:

 

I changed the subject line to be more clear about the topic of discussion. See my comments below.

 

Thanks,

Scott

 

<snip>

Consider this variation:

property pComplex;

(req |-> ##2 rdy) implies
(master_mode |-> (t4 ##0 ack) and (##[5:8] done));
endproperty : pComplex

What is that saying?

1) If req is false, then we don't care about the value of rdy @t2. What about master_mode, ack, and done?

This is the case where the differences between the proposed definitions for implies1 and implies2 may become interesting. If req is false and master_mode is true then the antecedent of implies is vacuous and the consequent is nonvacuous. If we use implies1 the vacuity result for implies would be nonvacuous. If we use implies2 the vacuity result for implies would be vacuous. It seems to me that the result of implies2 is what I want. I would like to hear the opinions of others on this case and maybe other potentially problematic cases.

<snip>

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