Access internal reg and local param of the RTL from the sva file

Hi there,

I have a design module which I need to verify using system verilog assertions and formal verification. The requirement is that I do not change / alter the RTL block. So I have created a sva file and a bind file that binds the rtl and the sva file. Now the issue is that I am not able to test the rtl completely as the RTL logic has lots of internal reg/wire and localparam . I am not able to access this in the sva file. Can someone please guide me on how to proceed with this.

Thanks

https://www.perplexity.ai/search/in-secret-Am.OYBNZQmSy_V9NJzJwvQ#0

To access internal signals, lets say read_en and write_en from your RTL, in your SystemVerilog Assertions (SVA) file and bind them with your RTL module, follow the steps outlined below, making use of hierarchical access:

module sva;

// Property to check signal conditions using hierarchical access

property check_en;
disable iff(rst)
@(posedge clk)


// Using hierarchical access to check internal signals in the RTL module
rtl_module_name.read_en == 1’b1 && rtl_module_name.write_en == 1’b0


;endproperty

// Instantiate the property with an assertion
assert property(check_en);

endmodule

bind rtl_name sva_name instance_name(.*);