Now a days we use to deal with modules of Verilog or VHDL or combination of both. Mostly verification engineers are not allowed to modified these modules. But still SVA addition to these modules is required and easy to verify lot of RTL functionality. How can you add SVA to these modules? Let’s find out !!
Here is where System Verilog ‘bind’ comes into the picture. Generally, you create an SVA bind file and instantiate sva module with the RTL module.SVA bind file requires assertions to be wrapped in a module that includes the port declaration, So now let’s understand this with a small example to understand basic things on how to use SVA bind
module DUT_dummy (output logic [7:0] out,
output logic x,
input logic wr, rd, clk, rst,
input logic [7:0] in);
//DUT Logic
...
...
...
endmodule : DUT_dummy
module SVA_dummy (input [7:0] out, in,
input x,
input wr, rd, clk, rst_n);
ASSERTION1_NAME:
`assert_async_rst(!rst_n |-> ...
ASSERTION2_NAME:
`assert_clk (x > 1 |-> out);
...
endmodule : SVA_dummy
module TB();
logic [7:0] out;
logic x;
logic wr, rd, clk, rst;
logic [7:0] in;
//Instantiation
DUT_dummy DUT_U1 (.*);
//Binding with SVA using implicit port connection
bind DUT_dummy : DUT_U1 SVA_dummy sva (.*);
...
...
endmodule : TB
Here, you can see that there is a DUT instantiation created DUT_u1 instance of DUT_dummy. Now the point of interest for us would be, how to bind the DUT instance to the SVA module.
To understand this take a look at an example where you could see the ‘bind’ keyword used with the DUT_dummy module and SVA_dummy. This is the place where we are binding the DUT module with the SVA module. Thus passing DUT signal information to the SVA module. With this, we could play around with the DUT signal and can check assertion properties using DUT signals available through this instantiation. If the assertion module uses the same signal names as the target module, the bind file port declarations are still required but the bind-instantiation can be done using the SystemVerilog (.*) implicit port connections that you can see in the example. If signal names are not exactly matching between target and bind file module then we need to expand the instantiation with respected port names.