Re: PSL v1.1 draft A review // precedence

Hi Ben:

> You have not addressed why the necessity to put the "always" higher in
> precedence than the implication operators.

I don't see a real necessity behind this kind of choice, actually, but whilst writing an answer to Håkan I probably found a few further motivations in favor of your position:

1) (always p) -> q;

is unlikely to be a frequent needed property, surely (at least in my experience) much less frequent than always (p -> q); hence, in spite of my personal preference for parentheses abundance, I guess that v1.0.1 precedence scheme would generally produce slightly shorter PSL sentences than v1.1.

2) At a different level, there is a more serious issue that would, again, work in favor of your objection: having a tool interpreting "always p -> q" as "(always p) -> q" without reporting warnings could potentially expose the verification in a formal context to false *positives*, i.e.: a property would be reported as passing when it should fail [if interpreted as "always (p -> q)"]; again, parentheses would obviously prevent any misinterpretation, but having to choose between one of the two choices, in view of a widespread diffusion of PSL, I am now thinking that, unless some SVA compatibility I haven't gone through yet is recommending differently, v1.0.1 priority would be preferable to v1.1.

Cheers,

        Andrea.

-- 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
| Andrea Fedeli,  Functional Verification - Formal Methods |
|                              Technical Leader            |
|~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~|
| Email : andrea.fedeli@st.com | Central R&D - NVMDP       |
| Voice : +39 039 603 7147     | STMicroelectronics Srl    |
| FAX   : +39 039 603 5820     | 20041 Agrate Brianza (Mi) |
|                              | Via C. Olivetti, 2, Italy |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~