Re: [sv-bc] Semantics of PSL statement inside SV module

Shalom is correct.
Having dealt for many years with similar language-extension-by-commentary, I'd like to add one thought.
When an embedded sublanguage declares or otherwise introduces new identifiers,
a choice needs to be made and documented as to whether these occur within the HDL namespace(s),
or outside of them. Note that (with wildcard package import) even references within the sublanguage
to names in the HDL namespaces may have semantic consequences. Since the original query concerned
name collisions (albeit between names entirely within the sublanguage), this seems like a good thread
in which to ask sublanguage designers to take some care with how references from annotation affect
the HDL namespace. The illusion that the commentary can be simply ignored often breaks down when
the namespaces interact.

Greg Jaxon

On 6/28/2012 8:05 AM, Bresticker, Shalom wrote:
> Hi, Parul.
>
> From the point of view of the SV language standard, these "PSL statements" are just comments and have no meaning and no semantics.
>
> Any meaning would be either tool-specific or possibly defined by the PSL standard.
>
> Regards,
> Shalom
>
>> -----Original Message-----
>> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On Behalf Of
>> Parul Goel
>> Sent: Thursday, June 28, 2012 15:31
>> To: sv-bc@eda.org
>> Subject: [sv-bc] Semantics of PSL statement inside SV module
>>
>>
>> Hi
>>
>> We are using multiple PSL statements (with same name) within a module,
>> though the scope of each PSL statement is different. As can be seen
>> from
>> the following test case, PSLs are defined within For block, Generate
>> Block and Module block.
>>
>> =======================
>> module top(input bit clk);
>> bit [3:0] counter = 4'b0000;
>>
>> always @(posedge clk)
>> counter = counter +1;
>>
>> generate
>> genvar i;
>> begin : B1
>> for (i = 0; i < 2; i++)
>> begin : B2
>> // psl psl_test: assert always ( counter[0] ) @(posedge clk);
>> end
>> // psl psl_test: assert always ( counter[0] ) @(posedge clk);
>> end
>> endgenerate
>> // psl psl_test: assert always ( counter[0] ) @(posedge clk);
>> endmodule
>> ========================
>>
>> Questions:
>> 1. Are there any scope properties for PSL statements inside modules?
>> 2. Can the PSL statements, present within a module but in different
>> scopes, as in our case, have same name?
>> 3. From simulation perspective, the assertion data in PSL statements
>> belong to the module or to respective scopes.
>>
>> Regards,
>> Parul
>>
>>
>>
>>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
>
>
Received on Fri Jun 29 09:50:36 2012