一个sv assertion的写法

zzczx · 发表于 2016-9-20 14:48:07

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

要求对以下场景做assertion:
如果a 脉冲后要来c脉冲，则中间必须有个b脉冲。
2016_0920_ 1449.png

自己写了一个，但是感觉不是很好。同时只能在vcs下编译通过，irun会有语法错误。想看看有没有更好的写法。谢谢大家。

module a ( ); reg a , b ,c; reg clk; initial begin init_var;
delay(1);
//success a=1; delay(2); a = 0; delay(10);
a=1; delay(2); a = 0; delay(10);
b=1; delay(2); b = 0; delay(10);
c=1; delay(2); c = 0; delay(10);
//failed a=1; delay(2); a = 0; delay(10);
a=1; delay(2); a = 0; delay(10);
c=1; delay(2); c = 0; delay(10);
$finish(); end
sequence seq_rd_to_wr(a,b); !a[*1:$] ##1 $rose(b); endsequence
sequence rose_wr(a,b,c); //@(posedge clk) $fell(a) ##1 !a[*1:$] ##1 $rose(b) ##[1:$] $rose(c); s_rd(a) intersect s_cs(b,c); endsequence
sequence s_rd(a); @(posedge clk) $fell(a) ##1 !a[*1:$]; endsequence
sequence s_cs(b,c); @(posedge clk) !b[*1:$]##1 b[*2] ##1 !b[*1:$] ##1 $rose(c); endsequence
property prop_check_rd_to_wr; @(posedge clk) $rose(c) |-> rose_wr(a,b,c).triggered; endproperty
A_check_rd_to_wr:assert property(prop_check_rd_to_wr);
parameter PERIOD = 20; always begin #(PERIOD/2) clk = ~clk; end
task init_var(); begin a <= 0 ; b <= 0 ; c <= 0 ; clk <= 0; end endtask
task delay(int clk_num=1); #(clk_num*PERIOD); endtask task automatic pulse(int clk_num=1,ref i); i = 1; repeat(clk_num) @(posedge clk); i = 0; endtask
initial begin:fsdb_block $fsdbAutoSwitchDumpfile(100,"a.fsdb",100); $fsdbDumpvars(0,"a","+all"); endendmodule

复制代码

AnswerLJ · 发表于 2016-9-20 19:13:01

module test;
reg a , b ,c;
reg clk;
initial begin
a = 0;
b = 0;
c = 0;
delay(1);
//success
a=1;
delay(2);
a = 0;
delay(10);
a=1;
delay(2);
a = 0;
delay(10);
b=1;
delay(2);
b = 0;
delay(10);
c=1;
delay(2);
c = 0;
delay(10);
//failed
a=1;
delay(2);
a = 0;
delay(10);
a=1;
delay(2);
a = 0;
delay(10);
c=1;
delay(2);
c = 0;
delay(10);
$finish();
end
initial begin
clk = 0;
forever begin
#5 clk = ~clk;
end
end
task delay(int clk_num=1);
repeat(clk_num) begin
@(posedge clk);
end
endtask
sequence boundary;
@(posedge clk) $rose(a) ##[2:$] $rose(c);
endsequence
sequence detect_b;
@(posedge clk) $rose(a) ##[1:$] $rose(b) ##[1:$] $rose(c);
endsequence
sequence detect_bn;
@(posedge clk) $rose(a) ##0 !b[*1:$] ##0 $rose(c);
endsequence
property rules_check_correct;
@(posedge clk) $rose(a) |->
boundary intersect detect_b;
endproperty
property rules_check_error;
@(posedge clk) $rose(a) |->
boundary intersect detect_bn;
endproperty
rules_check_ast:assert property(rules_check_error) $display("property fail detected!");
rules_check_cov:cover property(rules_check_correct) $display("property success detected!");
endmodule

复制代码

提供一个参考，没有剔除多重 $rose(a)的情况，可自己演进，另外不包含B,C同周期判定的情况，也可自行修改

zzczx · 发表于 2016-9-21 11:55:28

谢谢回复。
拓展下思路。

zzczx · 发表于 2016-9-21 14:28:42

这个assert我觉得难就难在多重$rose(a)的情况，因此由$rose触发不好写。所以后面我用了.triggered.
不知道还有哪位能给个好法子不需要用到.triggered的

AnswerLJ · 发表于 2016-9-21 16:34:48

sequence boundary;
@(posedge clk) $fell(a) ##0 !a[*2:$] ##0 $rose(c);
endsequence
sequence detect_b;
@(posedge clk) $fell(a) ##[1:$] $rose(b) ##[1:$] $rose(c);
endsequence
sequence detect_bn;
@(posedge clk) $fell(a) ##0 !b[*1:$] ##0 $rose(c);
endsequence
property rules_check_correct;
@(posedge clk) $fell(a) |->
detect_b within boundary;
endproperty
property rules_check_error;
@(posedge clk) $fell(a) |->
detect_bn within boundary;
endproperty

复制代码

AnswerLJ · 发表于 2016-9-21 16:36:15

sequence boundary;
@(posedge clk) $fell(a) ##[2:$] $rose(c);
endsequence
sequence detect_b;
@(posedge clk) $fell(a) ##[1:$] $rose(b) ##[1:$] $rose(c);
endsequence
sequence detect_bn;
@(posedge clk) $fell(a) ##0 !b[*1:$] ##0 $rose(c);
endsequence
property rules_check_correct;
@(posedge clk) $fell(a) |->
!a throughout
(boundary intersect detect_b);
endproperty
property rules_check_error;
@(posedge clk) $fell(a) |->
!a throughout
(boundary intersect detect_bn);
endproperty

复制代码

zzczx · 发表于 2016-9-22 10:01:59

@AnswerLJ 强。！a throughout写起来简洁多了。
不过还是没有解决之前说的：多个a pulse之间没有 bpulse或者c pulse应该是允许的。不应该failed。
所以我感觉用c pulse的triggered来触发会比较容易点。
不用triggered的法子还不知道怎么写。

AnswerLJ · 发表于 2016-9-22 10:50:02

sequence boundary;
@(posedge clk) !a throughout ($fell(a) ##[0:$] $rose(c));
endsequence
sequence detect_b;
@(posedge clk) !a throughout ($fell(a) ##[0:$] $rose(b) ##[0:$] $rose(c));
endsequence
sequence detect_bn;
@(posedge clk) !a throughout ($fell(a) ##0 !b[*1:$] ##0 $rose(c));
endsequence
property rules_check_correct;
@(posedge clk) detect_b.ended |->
boundary.ended;
endproperty
property rules_check_error;
@(posedge clk) detect_bn.ended |->
boundary.ended;
endproperty

复制代码

zzczx · 发表于 2016-9-22 16:46:49

本帖最后由 zzczx 于 2016-9-22 17:33 编辑

sequence detect_bn;
@(posedge clk) (!a throughout ($fell(a) ##0 !b[*1:$] ##0 $rose(c)));
endsequence
property rules_detect_error;
@(posedge clk) $rose(c) |-> !detect_bn.ended;
endproperty
rules_check_detect_error: assert property(rules_detect_error)$display("property successed detected! %t",$time);else
$display("property failed detected! %t",$time) ;

复制代码

这个是目前想到最简单的写法了。
还是需要.ended/.triggered.

AnswerLJ · 发表于 2016-9-22 19:21:31

very good

[讨论] 一个sv assertion的写法

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

相关帖子

站长推荐 /2