RE: [sv-ac] Ballot item 241 proposal

Additional comments inlined...
 
ed
 


  _____  

From: Prabhakar, Anupam [mailto:anupam_prabhakar@mentor.com] 
Sent: Saturday, April 16, 2005 7:07 PM
To: Eduard Cerny; Surrendra.Dudani@synopsys.COM; sv-ac@eda.org
Subject: RE: [sv-ac] Ballot item 241 proposal



Some comments below .. 

Thanks 
Anupam 

-----Original Message----- 
From: owner-sv-ac@eda.org [ <mailto:owner-sv-ac@eda.org>
mailto:owner-sv-ac@eda.org] On Behalf Of Eduard Cerny 
Sent: Saturday, April 16, 2005 3:11 PM 
To: Surrendra.Dudani@synopsys.com; sv-ac@eda.org 
Subject: RE: [sv-ac] Ballot item 241 proposal 

Hi, 

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); 

AP : This is equivalent to case a3.  As per P1800-D4 LRM Sec 16.9 
                clocking dram @(posedge phi1); 
                        inout data; 
                        output negedge #1 address; 
                endclocking 
        The clocking event of the dram clocking block can be used to wait
for that particular event: 
                @( dram ); 
        The above statement is equivalent to @(posedge phi1).  

 

The issue is not the sampling clock itself, that is correct, but the use of
ck.a as the boolean. ck.a refers to the sampled value of a in ck. 

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? 

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); 

AP : Given the above comment, is this still invalid ?  

 

See above. 

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

AP : Not sure if this can be written as 
        @(posedge clk2) ck.a ==> @(posedge clk2) (@(posedge clk)(a)) ==>
@(posedge clk)(a) 

a5: assert property(p4);  

 

No, =this does not follow, because ck.a refers to a sampled value, and does
not refere to a sequence (@(posedge clk)(a))  which the rewrite would do. 

---------- 

ed 



> -----Original Message----- 
> From: owner-sv-ac@eda.org [ <mailto: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  
> **************************************** 
> 
> 
>