有两种方法可以将sva断言与您的设计联系起来。
使用`include
将assertions放到单独的文件中，然后在设计module的最后 `include这个文件。
/* File name : bus_arbiter.sv */
// Design module
module bus_arbiter (
input logic clk,
input logic rst,
input logic [7:0] a,
input logic a_vld,
input logic [7:0] b,
input logic b_vld,
output logic [7:0] c);
logic [1:0] arb_sig;
logic [31:0] a_cnt;
logic [31:0] b_cnt;
logic [3:0] current_state;
// ... design code goes here
// place this at the end, right before endmodule
`include "bus_arb_assertions.svh"
endmodule: bus_arbiter/* File name : bus_arb_assertions.svh */
prop_a_cnt: assert property (
@(posedge clk) disable iff (rst)
a_vld |-> (a_cnt == $past(a_cnt) + 1));
property valid_state;
@(posedge clk) disable iff (rst)
$onehot0(current_state);
endproperty
prop_valid_state: assert property (valid_state);
// ... other assertions and cover props使用bind
但是，有一种更强大的方法可以将断言插入到您的设计中——使用SystemVerilog bind指令。
将assertions或者cover properties放到一个单独的module中, 然后使用 bind命令，将这个 assertions module 连接到某个instance 或者某个module的所有instances 。这是我最喜欢的连接方式。
bind语法的工作原理如下：
bind {design_module_name/design_instance_name} {sva_module_name} {bind_instance_name} (port_list);bind是在另一个模块中实例化模块的一种方式。用通俗易懂的英语说
bind的语句可以放在你的tb_top中。
bind tb_top.bus_arb_inst bus_arb_assertions bus_arb_sva_inst (
clk, rst, a, a_vld, b, b_vld, c, current_state, a_cnt );