一个sv assertion的写法

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

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

1. module a (                  );  reg a , b ,c;  reg clk;  initial begin    init_var;
   
2.     delay(1);
   
3.     //success    a=1;    delay(2);    a = 0;    delay(10);
   
4.     a=1;    delay(2);    a = 0;    delay(10);
   
5.     b=1;    delay(2);    b = 0;    delay(10);
   
6.     c=1;    delay(2);    c = 0;    delay(10);
   
7.     //failed    a=1;    delay(2);    a = 0;    delay(10);
   
8.     a=1;    delay(2);    a = 0;    delay(10);
   
9.     c=1;    delay(2);    c = 0;    delay(10);
   
10.     $finish();  end
    
11.   sequence seq_rd_to_wr(a,b);    ！a[*1:$] ##1 $rose(b);  endsequence
    
12.   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
    
13.   sequence s_rd(a);    @(posedge clk) $fell(a) ##1 ！a[*1:$];  endsequence
    
14.   sequence s_cs(b,c);    @(posedge clk) ！b[*1:$]##1 b[*2] ##1 ！b[*1:$] ##1 $rose(c);  endsequence
    
15.   property prop_check_rd_to_wr;    @(posedge clk) $rose(c) |->  rose_wr(a,b,c).triggered;   endproperty
    
16.   A_check_rd_to_wr:assert property(prop_check_rd_to_wr);
    
17.   parameter PERIOD = 20;  always begin    #(PERIOD/2) clk =  ~clk;  end
    
18.   task init_var();  begin    a <= 0 ;    b <= 0 ;    c <= 0 ;    clk <= 0;  end  endtask
    
19.    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
    
20.   initial begin:fsdb_block    $fsdbAutoSwitchDumpfile(100,"a.fsdb",100);    $fsdbDumpvars(0,"a","+all");  endendmodule

复制代码

1. module test;
   
2.         reg a , b ,c;  
   
3.         reg clk;  
   
4.        
   
5.         initial begin   
   
6.                 a = 0;
   
7.                 b = 0;
   
8.                 c = 0;
   
9.                 delay(1);
   
10.                 //success   
    
11.                 a=1;   
    
12.                 delay(2);   
    
13.                 a = 0;   
    
14.                 delay(10);
    
15.                 a=1;   
    
16.                 delay(2);   
    
17.                 a = 0;   
    
18.                 delay(10);
    
19.                 b=1;   
    
20.                 delay(2);   
    
21.                 b = 0;   
    
22.                 delay(10);
    
23.                 c=1;   
    
24.                 delay(2);   
    
25.                 c = 0;   
    
26.                 delay(10);
    
27.                 //failed   
    
28.                 a=1;   
    
29.                 delay(2);   
    
30.                 a = 0;   
    
31.                 delay(10);
    
32.                 a=1;
    
33.                 delay(2);   
    
34.                 a = 0;   
    
35.                 delay(10);
    
36.                 c=1;   
    
37.                 delay(2);   
    
38.                 c = 0;   
    
39.                 delay(10);
    
40.                 $finish();
    
41.         end
    
42. 
    
43.         initial begin
    
44.                 clk = 0;
    
45.                 forever begin
    
46.                         #5 clk = ~clk;
    
47.                 end
    
48.         end
    
49.        
    
50.    task delay(int clk_num=1);   
    
51.         repeat(clk_num) begin
    
52.                 @(posedge clk);
    
53.         end
    
54.    endtask
    
55.    
    
56.         sequence boundary;
    
57.                 @(posedge clk) $rose(a) ##[2:$] $rose(c);
    
58.         endsequence
    
59. 
    
60.         sequence detect_b;
    
61.                 @(posedge clk) $rose(a) ##[1:$] $rose(b) ##[1:$] $rose(c);
    
62.         endsequence
    
63.        
    
64.         sequence detect_bn;
    
65.                 @(posedge clk) $rose(a) ##0 ！b[*1:$] ##0 $rose(c);
    
66.         endsequence
    
67. 
    
68.         property rules_check_correct;
    
69.                 @(posedge clk) $rose(a) |->
    
70.                         boundary intersect detect_b;
    
71.         endproperty
    
72.        
    
73.         property rules_check_error;
    
74.                 @(posedge clk) $rose(a) |->
    
75.                         boundary intersect detect_bn;
    
76.         endproperty
    
77.        
    
78.         rules_check_ast:assert property(rules_check_error) $display("property fail detected！");
    
79.         rules_check_cov:cover property(rules_check_correct) $display("property success detected！");
    
80.        
    
81. endmodule

复制代码

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

谢谢回复。
拓展下思路。

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

1.   
   
2.         sequence boundary;
   
3.                 @(posedge clk) $fell(a) ##0 ！a[*2:$] ##0 $rose(c);
   
4.         endsequence
   
5. 
   
6.         sequence detect_b;
   
7.                 @(posedge clk) $fell(a) ##[1:$] $rose(b) ##[1:$] $rose(c);
   
8.         endsequence
   
9.        
   
10.         sequence detect_bn;
    
11.                 @(posedge clk) $fell(a) ##0 ！b[*1:$] ##0 $rose(c);
    
12.         endsequence
    
13. 
    
14.         property rules_check_correct;
    
15.                 @(posedge clk) $fell(a) |->
    
16.                         detect_b within boundary;
    
17.         endproperty
    
18.        
    
19.         property rules_check_error;
    
20.                 @(posedge clk) $fell(a) |->
    
21.                         detect_bn within boundary;
    
22.         endproperty

复制代码

1.         sequence boundary;
   
2.                 @(posedge clk) $fell(a) ##[2:$] $rose(c);
   
3.         endsequence
   
4. 
   
5.         sequence detect_b;
   
6.                 @(posedge clk) $fell(a) ##[1:$] $rose(b) ##[1:$] $rose(c);
   
7.         endsequence
   
8.        
   
9.         sequence detect_bn;
   
10.                 @(posedge clk) $fell(a) ##0 ！b[*1:$] ##0 $rose(c);
    
11.         endsequence
    
12. 
    
13.         property rules_check_correct;
    
14.                 @(posedge clk) $fell(a) |->
    
15.                         ！a throughout
    
16.                         (boundary intersect detect_b);
    
17.         endproperty
    
18.        
    
19.         property rules_check_error;
    
20.                 @(posedge clk) $fell(a) |->
    
21.                         ！a throughout
    
22.                         (boundary intersect detect_bn);
    
23.         endproperty
    
24.        

复制代码

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

1.         sequence boundary;
   
2.                 @(posedge clk) ！a throughout ($fell(a) ##[0:$] $rose(c));
   
3.         endsequence
   
4. 
   
5.         sequence detect_b;
   
6.                 @(posedge clk) ！a throughout ($fell(a) ##[0:$] $rose(b) ##[0:$] $rose(c));
   
7.         endsequence
   
8.        
   
9.         sequence detect_bn;
   
10.                 @(posedge clk) ！a throughout ($fell(a) ##0 ！b[*1:$] ##0 $rose(c));
    
11.         endsequence
    
12. 
    
13.         property rules_check_correct;
    
14.                 @(posedge clk) detect_b.ended |->
    
15.                         boundary.ended;
    
16.         endproperty
    
17.        
    
18.         property rules_check_error;
    
19.                 @(posedge clk) detect_bn.ended |->
    
20.                         boundary.ended;
    
21.         endproperty

复制代码

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

复制代码

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

very good