[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
Received on Thu Jun 28 05:31:42 2012