[$ieee-1850] PSL:suggestion for the next round

At the VerificationGuild there was a request to have the SV or Verilog 
"generate" statement see the psl verification directives, particulalry when 
they are embedded within an RTL code, as shown below. 

// psl default clock = (posedge clk); 
// psl sequence q_req_grant_5_10 (const i)= {req[i]; [*6:11]; grant[i]}; 
generate begin : gen_q_req_grant_5_10 
for (i=0; i<SIZE; i=i+1) begin : forloop
// psl cover q_req_grant_5_10(i); 
// psl assert (always {req[i]} |=> {grant[i]}); 
end : forloop
end : gen_q_req_grant_5_10 
endgenerate
See 
http://verificationguild.com/modules.php?name=Forums&file=viewtopic&p=3050#3050 
for the whole discussion (2 pages). 

It turns out that one vendor recognizes the generate for embedded 
directives, while another one does not. But the real issue is the fact that the 
visibility of genvar inside PSL domain is questionable. Specifically, PSL 
LRM doesn't talk about embedding PSL code into a HDL. So strictly speaking 
this use model is un-specified in LRM. 

I strongly suggest that in the next round we adopt a standard for the inline 
definition of embedded PSL within a VHDL'93, VHDL'87, Verilog, 
SystemVerilog, SystemC module. There is a de facto standard adopted by EDA 
vendors, but even there, there are some minor variations. And that brings 
interoperability issues. The reality is that users like the inline adoption 
of PSL, and then issues like the "generate" or even the common use of 
pragmas gets into play. 
Thanks, 
Ben 
 
--------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 
http://www.vhdlcohen.com/ ben_ f rom _abv-sva.org
* Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
* Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd 
Edition, 2004, ISBN 0-9705394-6-0 
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 
0-9705394-2-8 
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115 
---------------------------------------------------------------------------