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

Hi there,

I've appreciated the fact that in Draft 1.1 the precedence strength of logical implications (->, <->) has been distinguished from that of sequence implications, as they act at quite different levels; furthermore, whilst logical operators associativity had to be made explicit, sequence operators associativity is defined syntactically, as, like you wrote, there can be nothing but a sequence as LHS of a |->, hence it has to be right associative.

As a long time Sugar user I've been acquainted to isolate the main expression following the usual heading AG inside a couple of parentheses; possibly for this reason, even though I find quite natural to write

always SERE |=> SERE;

with no surrounding parentheses, I would not deprecate

always (SERE |=> SERE);

About "legacy" code, I cannot state how much PSL assertions have already been spread around the world, but I'm quite confident that the PSL LRM compliance level is not that high yet to give legacy code support a major impact; furthermore a two-lines sed script could give you the necessary aid to adapt the code, assuming it was already lexically and syntactically correct, as should be for "legacy" code.

For what pertains parentheses usage, I do agree with you that "{" is slightly more readable than "({", but a good editor would easily compensate this issue giving you the advantage to be able to move back and forth from the beginning to the end of property with a single key stroke ;)

If I had to choose I would give sequence implication operators a stronger precedence than occurrence operator, and I would leave boolean implication operators at a weaker level than occurrence ones, but I guess this sort of apparent asymmetry could would look odd to more than one mind.

Cheers,

        Andrea Fedeli.

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