SVA 快速参考手册

注意:该 SVA 快速参考手册目前支持 IEEE 1800-2005 标准。

0. 绑定(Binding)#

bind target bind_obj [ (params)] bind_inst (ports) ;

将 SystemVerilog 模块或接口附加到 Verilog 模块或接口实例,或 VHDL 实体/架构。支持多个目标。示例:

bind fifo fifo_full v1(clk,empty,full); 
bind top.dut.fifo1 fifo_full v2(clk,empty,full); 
bind fifo:fifo1,fifo2 fifo_full v3(clk,empty,full);

1. 立即断言(Immediate Assertions)#

[ label : ] assert (boolean_expr) [ action_block ] ;

在执行过程性代码时测试表达式。示例:

enable_set_during_read_op_only : assert (state >= `start_read && state <= `finish_read); 
    else $warning("Enable set when state => %b", state);

2. 声明(Declarations)#

2.1 序列(Sequence)#

sequence identifier [ argument_list ] ;
    sequence_expr [ seq_op sequence_expr ] ... ; 
endsequence [ : identifier ] 

声明一个可以在属性声明中使用的序列表达式。允许使用局部变量。示例:

sequence BusReq (bit REQ=0, bit ACK=0); 
    REQ ##[1:3] ACK; 
endsequence

2.2 属性(Property)#

property identifier [ argument_list ] ;
    [ clock_expr ] [ disable_clause ] property_expr ; 
endproperty [ : identifier ] 

声明在仿真过程中要验证的 condition 或 sequence。允许使用局部变量。示例:

property P6 (bit AA, BB=`true, EN=1); 
    @(negedge clk) 
    EN -> (BB ##1 c) |=> (AA ##[1:2] (d||AA)); 
endproperty

[ identifier: ] [ (argument_list) ]

创建属性声明的实例。示例:

property P1;
    @(event) a && b ##1 !a && !b;
endproperty
property P2;
    @(posedge clk) rst |-> P1;
endproperty

3. 指令(Directives)#

3.1 断言属性(Assert Property)#

[ label : ] assert property (prop_expr) [ action_block ] ;

在验证过程中检查属性。示例:

property P5 (AA); 
    @(negedge clk) (b ##1 c) |=> (AA ##[1:2] (d||AA)); 
endproperty 
assert property (P5(a));

3.2 假设属性(Assume Property)#

[label:] assume property (prop_expr) [ action_block ] ;

限制验证过程中考虑的输入。在仿真中,处理方式类似于断言。示例:

A1: assume (@(ena) !rst);

3.3 覆盖属性(Cover Property)#

[label:] cover property (prop_expr) [ pass_statement ] ;
[label:] cover sequence (seq_expr) [ pass_statement ] ;

监控属性或序列的覆盖率并报告统计信息。当属性成功时,执行语句。覆盖序列报告所有匹配项。示例:

C1: cover property (@(event) a |-> b ##[2:5] c);

4. 期望语句(Expect Statement)#

expect (prop_expr) [ action_block ] ;

阻塞当前进程,直到属性成功或失败。示例:

expect( @(posedge clk) ##[1:10] top.TX_Monitor.data == value ) 
    success = 1; 
else success = 0;

5. 时钟表达式(Clock Expressions)#

@( {{posedge | negedge} clock | expression} )

声明事件或事件表达式,用于采样断言变量的值。支持多个时钟,以及从仅包含断言的 always 块推断的时钟。示例:

assert property @(posedge clk1) (a ##1 b) |=> @(posedge clk2) (c ##1 d)); 
endproperty

assert property ( @(posedge clk1) (a ##1 b) |=> @(posedge clk2) (c ##1 d) );

always @(posedge clk) begin 
    assert property ( (a ##1 b) |=> (c ##1 d) ); 
    assert property ( (a[*3]) |=> ~c ); 
    cover property ( (a ##1 b ##1 c) |=> (d[*2:4]) ); 
end

6. 默认时钟块(Default Clocking Blocks)#

default clocking [clk_identifier] {identifier | clk_expression} ; 
    clocking_items
end clocking 
default clocking clk_identifier

指定控制属性评估的时钟或事件。示例:

default clocking master_clk @(posedge clk); 
    property p4; 
        (a |=> ##2 b); 
    endproperty 
    assert property (p4); 
endclocking

7. 禁用子句(Disable Clause)#

disable iff (boolean_expr) 
default disable iff (boolean_expr)

指定一个复位表达式。当表达式为真时,属性检查异步终止。示例:

property P4; 
    @(negedge clk) disable iff (rst) (c) |-> (##[max-1:$] d); 
endproperty

8. 属性表达式(Property Expressions)#

8.1 |->#

sequence_expr |-> property_expr

属性表达式必须在序列表达式为真的最后一个周期内为真(重叠)。示例:

property P4; 
    @(negedge clk) disable iff (rst) (c) |-> (##[max-1:$] d); 
endproperty

8.2 |=>#

sequence_expr |=> property_expr

属性表达式必须在序列表达式为真后的第一个周期内为真。示例:

property property P5 (AA); 
    @(negedge clk) (b ##1 c) |=> (AA ##[1:2] (d||AA)); 
endproperty

8.3 and#

property_expr and property_expr

如果两个属性表达式都为真,则返回真。示例:

@(c) v |=> (w ##1 @(d) x) and (y ##1 z)

8.4 not#

not property_expr

返回属性表达式的反值。示例:

property abcd; 
    @(posedge clk) a |-> not (b ##1 c ##1 d); 
endproperty

8.5 if#

if (expression) property_expr1 [ else property_expr2]

如果表达式为真,则 property_expr1 必须成立;如果表达式为假,则 property_expr2 必须成立(如果存在)。示例:

property P2; 
@ (negedge clk) if (a) b |=> c; else d |=> e; 
endproperty

9. 序列操作符(Sequence Operators)#

9.1 and#

sequence_expr1 and sequence_expr2

两个序列必须都发生,但操作数的结束时间可以不同。示例:

(a ##2 b) and (c ##2 d ##2 e) ;

9.2 first_match#

first_match (sequence_expr[, seq_match_item])

一旦找到第一次匹配,就停止对一个或多个序列的评估。示例:

sequence s1; 
first_match(a ##1 b[->1]:N] ## c); 
endsequence

9.3 intersect#

sequence_expr1 intersect sequence_expr2

两个序列必须都发生,且序列表达式的起始和结束时间必须相同。示例:

(a ##2 b) intersect (c ##2 d ##2 e)

9.4 or#

sequence_expr1 or sequence_expr2

至少有一个序列必须发生。示例:

(b ##1 c) or (d[*1:2] ##1 e) or f[*2]

9.5 throughout#

boolean_expr throughout sequence_expr

条件必须在整个序列的持续时间内成立。示例:

(a ##2 b) throughout read_sequence

9.6 within#

sequence_expr1 within sequence_expr2

sequence_expr1 必须在 sequence_expr2 的时间范围内匹配某一时刻。示例:

(a ##2 b ##3 c) within write_enable

10. 序列方法(Sequence Methods)#

sequence_instance.[ ended|matched|triggered]

标识序列的终点。示例:

wait ((AB.triggered) || BC.triggered); 
    if (AB.triggered) $display("AB triggered");

11. 周期延迟(Cycle Delays)#

##integral_number ##Identifier ##(constant_expression) ##[const_expr : const_expr] ##[const_expr : $]

指定从当前时钟周期到下一个指定行为发生的时钟周期数。示例:

property property P5 (AA); 
    @(negedge clk) (b ##1 c) |=> (AA ##[1:2] (d||AA)); 
endproperty

12. 序列和属性中的局部变量(Local Variables in Sequences and Properties)#

(seq_expression {, seq_match_item}) [ repetition_op ]

当 seq_expression 匹配时,执行 seq_match_item。匹配项可以是子程序调用。示例:

sequence data_check; 
int x; 
a ##1 (!a, x=data_in) ##1 !b[*0:$] ##1 b && (data_out=x); 
endsequence

13. 重复(Repetition)#

13.1 连续重复(Consecutive Repetition)#

[* const_or_range_expression ]

连续重复。示例:

(a[*2] ##2 b[*2]) |=> (d)

13.2 跳转重复(Goto Repetition)#

[-> const_or_range_expression ]

跳转重复。示例:

a ##1 b[->5] ##1 c

13.3 非连续重复(Non-Consecutive Repetition)#

[= const_or_range_expression ]

非连续重复。示例:

s1 |=> (b [=5] ##1 c)

14. 快捷方式(Shortcuts)#

  • R[*] 等同于 R[*0:$]
  • ##[*] 等同于 ##[0:$]
  • R[+] 等同于 R[*1:$]
  • ##[+] 等同于 ##[1:S]

15. 断言严重性任务(Assertion Severity Tasks)#

15.1 Fatal#

$fatal ([ 0 | 1 | 2 , ] message [ , args ] ) ;

致命消息任务;消息可以是字符串或表达式。您可以从断言的操作块调用此任务。示例:

$fatal (0);

15.2 错误、警告、信息(Error, Warning, Info)#

$error (message [ , args ] ) ;
$warning (message [ , args ] ) ;
$info (message [ , args ] ) ;

非致命消息任务;消息可以是字符串或表达式。您可以从断言的操作块调用这些任务。示例:

$error("Unsupported memory task command %b", m_task); 
$warning("Enable is set during non-read op: state=>%b", state);

16. 系统函数(System Functions)#

16.1 onehot#

$onehot (bit_vector)

如果表达式中只有一个位为高电平,则返回真。示例:

property p1(Arg) 
@(posedge clk) $onehot(Arg); 
endproperty

16.2 onehot0#

$onehot0 (bit_vector)

如果表达式中至多只有一个位为高电平,则返回真。示例:

property p2(Arg) 
@(posedge clk) $onehot0(Arg); 
endproperty

16.3 isunknown#

$isunknown (bit_vector)

如果表达式中任何一位为 X 或 Z,则返回真。示例:

property p3(Arg) 
@(posedge clk) $isunknown(Arg); 
endproperty

16.4 countones#

$countones (bit_vector)

返回向量中值为 1 的位数。示例:

property p4(Arg) 
@(posedge clk) $countones(Arg) == 4; 
endproperty

17. 采样值函数(Sampled-Value Functions)#

17.1 sampled#

$sampled(expression)

返回表达式在当前时钟周期的采样值。示例:

property propA 
@(posedge clk) (a ##1 b); 
endproperty 
p1: assert (propA) 
$display("%m passed"); 
else $warning("a == %s; b == %s", $sampled(test.inst.a), $sampled(test.inst.b));

17.2 rose#

$rose(expression)

如果表达式的采样值在当前时钟周期改变为 1,则返回真。示例:

Example: (a ##1 b) |-> $rose(test.inst.sig4);

17.3 fell#

$fell(expression)

如果表达式的采样值在当前时钟周期改变为 0,则返回真。示例:

(a ##1 b) |-> $fell(test.inst.c);

17.4 stable#

$stable(expression)

如果表达式的采样值在当前时钟周期内保持不变,则返回真。示例:

(a ##1 b) |-> $stable(test.inst.c);

17.5 past#

$past(expression [ , n_cycles] )

返回表达式在上一个时钟周期或指定时钟周期数之前的采样值。示例:

(a == $past(test.inst.c, 5)

18. 断言控制系统任务(Assertion-Control System Tasks)#

$assertoff [ ( levels [ , list_of_mods_or_assns ] ) ] ; $asserton [ ( levels [ , list_of_mods_or_assns ] ) ] ; $assertkill [ ( levels [ , list_of_mods_or_assns ] ) ] ;

控制仿真过程中的断言检查。示例:

$assertoff (0, top.mod1, top.mod2.net1);