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
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(.*);