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

Hi, Brad.

> -----Original Message-----
> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On
> Behalf Of Brad Pierce
> Sent: Monday, February 20, 2006 7:32 PM
> To: sv-bc@eda.org
> Subject: 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?

[Shalom] And in unique 'if'. I admit I don't understand all the
discussion about interleaving orderings in that I don't think it makes a
difference in any normal case. Is there any such case which is not
pathological? I would be happy with deleting all the discussion about
various orderings from the LRM and even be willing to have the LRM
specify evaluation in top-down order.

What is much more relevant than interleaving ordering, I think, is the
problem of input constraints. In many cases, uniqueness is a result of
constraints on the set of legal input combinations and sequences to the
module. The module is designed according to the assumptions on the input
constraints. When you give such a module to synthesis, for example, with
a parallel_case directive ("unique"), you are telling the tool, "You
cannot know that these combinations are mutually exclusive, but I know
they are, and I want you to assume that. It is my responsibility to
ensure that that assumption is fulfilled." How are tools going to react
to uniqueness assertions in such situations? 


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

[Shalom] No, that puts the responsibility on the tool to do an
exhaustive search. Closer to the intent would be something like "if an
implementation detects such an interleaving..."

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

[Shalom] Except for the use of the term "illegal", I agree. Did it sound
like I was implying otherwise?

I still say that even if a uniqueness assertion is false or potentially
false, that does not make the code illegal. It makes it code where the
uniqueness assertion fails.
 

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

[Shalom] Agreed. In fact, I would say that about any synthesized
if/case, regardless of the assertions.

Shalom