SVA 再了解(十)

bind的使用

先看一下bind的語法

先寫一個給bind用的module
module mutex_chk(a, b, elk);
input logic a, b, elk;

property p_mutex;
©(posedge elk) not (a && b);
endproperty

a_mutex: assert property{p_mutex);
endmodule

假如有一個design如下
module t o p {. . ) ;
inline ul (elk, a, b, inl, in2, outl);
inline u2 (elk, c, d, in3, in4, out2);
endmodule

我們可以在design上加入下面的bind作check
bind top.ul mutex_ehk il(a, b, elk);
bind top.u2 mutex_ehk i2(c, d, elk);