SystemVerilog Assertions应用指南 Chapter1.39将SVA与设计连接

编程入门 行业动态 更新时间:2024-10-14 14:16:37

SystemVerilog Assertions应用<a href=https://www.elefans.com/category/jswz/34/1769915.html style=指南 Chapter1.39将SVA与设计连接"/>

SystemVerilog Assertions应用指南 Chapter1.39将SVA与设计连接

        有两种方法可以将SVA检验器连接到设计中。
        (1)在模块( module)定义中内建或者内联检验器。
        (2)将检验器与模块、模块的实例或者一个模块的多个实例绑定。
        有的工程师不喜欢在设计中加任何验证代码。在这种情况下,在外部绑定SVA检验器是很好的选择。SVA代码可以内建在模块定义中的任何地方。下面的例子显示了内联在模块中的SVA。

module inline(clk, a, b, d1, d2, d);input logic clk, a, b;
input logic [7:0] d1, d2;
output logic [7:0] d;always@(posedge clk)
beginif(a)d <= d1;if(b)d <= d2;
endendmodulemodule top(clk, a, b, c, d, in1, in2, in3, in4, out1, out2);input logic clk, a, b, c, d;
input logic [7:0] in1, in2, in3, in4;
output logic [7:0] out1, out2;inline u1 (clk, a, b, in1, in2, out1);
inline u2 (clk, c, d, in3, in4, out2);endmodulemodule mutex_chk(a, b, clk);input logic a, b, clk;property p_mutex;@(posedge clk) not (a && b);
endpropertya_mutex: assert property(p_mutex);
c_mutex: cover property(p_mutex);endmodule// bind inline mutex_chk i2 (a, b, clk);
bind top mutex_chk i3 (a, b, clk);
bind top mutex_chk i4 (c, d, clk);module tb;logic clk, a, b, c, d;
// logic [7:0] d1, d2;
// logic [7:0] d;logic [7:0] in1, in2, in3, in4;
logic [7:0] out1, out2;// inline i1 (clk, a, b, d1, d2, d);top top1 (clk, a, b, c, d, in1, in2, in3, in4, out1, out2);initial $vcdpluson();initial
begin
clk=1'b0; a=1'b0; b=1'b0;
// #100 d1 = 8'd10; d2 = 8'd25;
#100 in1 = 8'd10; in2 = 8'd25;
#100 a=1'b1;
#100 b=1'b1; a=1'b0;
#100 a=1'b1;
#100 a=1'b0; b=1'b0;
#100
$finish;
endinitial forever clk = #25 ~clk;endmodule// c_mutex, 12 attempts, 12 match, 0 vacuous match

        如果用户决定将SVA检验器与设计代码分离,那么就需要建立一个独立的检验器模块。定义独立的检验器模块,增强了检验器的可重用性。下面所示的是一个检验器模块的代码实例。

module mutex_chk(a, b, clk);input logic a, b, clk;property p_mutex;@(posedge clk) not (a && b);
endpropertya_mutex: assert property(p_mutex);
c_mutex: cover property(p_mutex);endmodule

        注意,定义检验器模块时,它是一个独立的实体。检验器用来检验一组通用的信号,检验器可以与设计中任何的模块( module或者实例( instance)绑定,绑定的语法如下所示。

bind <module_name or instance_name ><checker_name > <checker_instance_name><design_signals>;

在上面的检验器例子中,绑定可以用下面的方式实现。

bind inline mutex_chk i2 (a,b,clk);
module top(...);inline u1 (clk,a,b,in1,in2,out1);inline u2 (clk,c,d,in3,in4,out2);endmodule

        检验器 mutex_chk可以用下面的方式与顶层模块中内联( inline)的两个模块实例绑定。

bind top.u1 mutex_chk i1 (a,b,clk);
bind top.u2 mutex_chk i2(c,d,clk);

        与检验器绑定的设计信号可以包含绑定实例中的任何信号的跨模块引用(cross module reference)。
 

更多推荐

SystemVerilog Assertions应用指南 Chapter1.39将SVA与设计连接

本文发布于:2023-12-05 01:50:06,感谢您对本站的认可!
本文链接:https://www.elefans.com/category/jswz/34/1662705.html
版权声明:本站内容均来自互联网,仅供演示用,请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系,我们将在24小时内删除。
本文标签:指南   Assertions   SystemVerilog   SVA

发布评论

评论列表 (有 0 条评论)
草根站长

>www.elefans.com

编程频道|电子爱好者 - 技术资讯及电子产品介绍!