RE: [sv-ac] AC 196:

John,

Thanks for the better explanation on sequence/property activation.

I think the proposal of using input/output for local variables, should be
part of a different proposal. I would like to focus on data types in this
proposal.

Many Thanks
Hillel

-----Original Message-----
From: Havlicek John-r8aaau
Sent: Wednesday, November 17, 2004 7:22 AM
To: Miller Hillel-R53776
Cc: Eduard.Cerny@synopsys.com; sv-ac@eda.org; Miller Hillel-R53776
Subject: Re: [sv-ac] AC 196:

Hillel:

I have just a couple of comments on remarks that have been made.

> - if passed by value, e.g., int x, what is the value? Is the one at the
> first clock tick of every eval. attempt, the value at time 0, other?
>
> HM: The value is the value of the evaluated "actual expression" at the clock tick that sequence/property are activated.

I think it is important to explain a little more what "activated"
means. You are talking about activation of property instances,
not property declarations.

If I write

   assert property (@(posedge clk) foo(a,b,c))

then the instance foo(a,b,c) gets activated at each posedge of clk.
If I write

   assert property (@(posedge clk) seqA |-> goo(a,b,c))

then, assuming that seqA is singly clocked, the instance goo(a,b,c)
gets activated at each posedge of clk that is an endpoint of seqA.

Etc., etc.

>
> - if passed by reference, e.g., ref int x, I would suppose that if used in
> expressions it will be the value sampled at each clock tick or the immediate
> value if used in disable iff? It can be read and written.
>
> HM: The formal parameter recieves that value of the respective evaluated "actual expression" at the clock tick that
> the formal parameter is observed. With disable iff, it is the same, the "actual expression" continues to be evaluated throughout the property evaluation.
> That is the immeadiate value is not the one used.
> The initial proposal will not include writing to parameters that have data types on them.
> - if specified as const ref, it should only allow reading.

I think there is some problem in not addressing the writing to
formal arguments. We do need this in the case that the actual
argument passed in is a local variable. This is because the
current mechanism for getting local variables out of sequence
instances is to declare the local variables in the instantiating
context, pass them in as actual arguments, and allow them to
be assigned in the instantiated sequence.

I think it would be a lot nicer if we could use an "output" or
"inout" modifier to the formal argument when a sequence will
export local variables.

For example, currently we write something like

   sequence collect_data (a, b);
      (s, a = e) ##1 (t, b = f);
   endsequence

   property check;
      int A, B;
      collect_data(A,B) |-> A == B;
   endproperty

Wouldn't it make more sense to write the following?

   sequence collect_data (output int a, output int b);
      (s, a = e) ##1 (t, b = f);
   endsequence

   property check;
      int A, B;
      collect_data(A,B) |-> A == B;
   endproperty

We could use "input" and inout" to mean that a local variable
passed into a sequence instance is guaranteed already to have been
assigned when passed in and therefore can be referenced before
assigned in the sequence instance.

Then we could say that "output" means that a local variable
passed in is not guaranteed to be assigned before being passed
in and therefore cannot be referenced in the instantiated sequence
before it has been assigned.

We could use "input" to mean that a local variable does not flow
out of the sequence instance.

Local variables do not flow out of property instances, so
formal arguments of properties would be only "input" or unmodified.

Best regards,

John H.
Received on Wed Nov 17 05:26:42 2004