RE: [sv-ac] Ballot item 241 proposal

From: Kulshrestha, Manisha <Manisha_Kulshrestha_at_.....>
Date: Sun Apr 17 2005 - 23:03:52 PDT
Hi Ed,

Please see my inlined comments. I am not sure if we have time to include
some of your suggestions in this proposal.

 
Thanks.
Manisha

I wonder if the examples in Mantis #626 (issue 241) should also include
the following situation:

clocking ck @(posedge clk);
  input a;
endclocking

property p3;
  @ck ck.a;
endproperty

a5: assert property(p3);

This would be the case of possible double sampling too and it should
state again that the results is the same as in the other cases a1-a4. Or
is this illegal?

I think "a3" is exactly same example in the proposal. The proposal does
not include clocking event of this type (@ck) though. I am assuming that
you are asking about hierarchical reference to a signal which is
clocking block input. The example in the proposal is as follows:

clocking cb_with_input @(posedge clk);
  input a;
 
  property p1;
    a;
  endproperty

endclocking

property p2;
  @(posedge clk) cb_with_input.a;
endproperty

a3: assert property (p2);

And an example of the illegal case:

clocking ck @(posedge clk);
  input #1 a;
endclocking

property illegal_sampling;
  @ck ck.a;
endproperty

a5: assert property(illegal_sampling);
I am open to adding this example but I am not sure if we have time for
that as Monday is the last day for the ballot approval. I think the
first paragraph in the proposal clearly says that it is illegal.

-----------
And what about the following case? Is it legal? If we go by the timing
diagram in the proposal, this would mean resampling the sampled value by
posedge clk by the posedge of clk2:

clocking ck @(posedge clk);
  input a;
endclocking

property p4;
  @(posedge clk2) ck.a;
endproperty

a5: assert property(p4);

I think based on the statements in the proposal, it means that property
will read the value sampled by the clocking block and will not do double
sampling at clk2. I think this should be the case to avoid confusion
about which value is being used by the property in case (posedge clk)
and (posedge clk2) occur at the same time.

I am not sure how you are interpretting the timing diagrams to say that
this means double sampling. I created timing diagrams to show that there
is no double sampling. 

----------

ed



> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Surrendra Dudani
> Sent: Thursday, April 14, 2005 8:58 PM
> To: sv-ac@eda.org
> Subject: [sv-ac] Ballot item 241 proposal
>
>
> Please review ballot issue 241 with Manisha's proposal in mantis item
> #626.
> If I don't hear anything by tomorrow, I'll assume it's ok to change
> the status to resolve.
> Surrendra
> ****************************************
> Surrendra A. Dudani
> Synopsys, Inc.
> 377 Simarano Drive, Suite 300
> Marlboro, MA 01752
>
> Tel:   508-263-8072
> Fax:   508-263-8123
> email: Surrendra.Dudani@synopsys.com
> ****************************************
>
>
>
Received on Sun Apr 17 23:04:02 2005

This archive was generated by hypermail 2.1.8 : Sun Apr 17 2005 - 23:06:02 PDT