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

Thanks to all for your inputs.

Regards,
Parul

On 6/28/2012 6:39 PM, Dhiraj Kumar Prasad wrote:
> Hello Parul,
>
> Please see my comment(s) for each of your query.
>
> Regards,
> dhiRAj
>
>
> -----Original Message-----
> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On Behalf Of Parul Goel
> Sent: Thursday, June 28, 2012 6:01 PM
> 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?
> [dhiRAj] : It evaluation is similar like concurrent assertion in SV
> 2. Can the PSL statements, present within a module but in different
> scopes, as in our case, have same name?
> [dhiRAj] : The label attached to PSL statement is local to scope and a tool report the message w.r.t scope So it can have.
> 3. From simulation perspective, the assertion data in PSL statements
> belong to the module or to respective scopes.
> [dhiRAj] : Did you mean the data used in assertion reporting ?? If Yes, then it's belong to respective scope.
>
> Regards,
> Parul
>
>
>
>
>
>
>
>
Received on Fri Jun 29 00:20:44 2012