Re: [sv-bc] Mantis 1345: 10.4: "illegal" unique if/case issues

Shalom,

Would it cut this Gordian knot to disallow side-effecting case items in
unique case?

>1. In each quote, the first sentence contains the phrase "for any such
>interleaving". This is ambiguous. It can be interpreted as "there
exists >some such interleaving" or as "for all such interleavings" (as
in >mathematical expressions, "for any x", which means "for all x"). In
fact, >the email discussion showed that the intent was closer to the
first >interpretation, but more precisely something like "the tools
detects such >an interleaving", which is subtly different from the first
interpretation >also.

Yes, "if there exists an interleaving such that" would be clearer.

I don't agree though that the illegality of the code has anything to do
with whether or not the tool can detect the illegality.  The LRM is
requiring simulators to make some modest efforts to help the user notice
illegality as soon as possible, but the responsibility for making true
assertions about the case statement is ultimately up to the user.
Because these assertions are checked at simulation time, they are a
safer way than pragmas or attributes for the user to communicate higher
knowledge to a synthesis tool.

The checks may fail to detect illegality in pathological test cases
where the user is attempting to synthesize and make assertions about
side-effecting case items.  My advice?  Don't do that.

-- Brad