2024年6月14日发(作者：)

systemverilog中property用法

在设计和验证数字电路时，验证工程师需要编写验证代码来检

查设计的正确性。SystemVerilog提供了多种验证语言特性，其中

之一是property。property是一种描述设计行为的语言特性，可以

用于检查特定的设计属性是否满足要求。

在本文中，我们将介绍SystemVerilog中property的用法，包

括如何定义property、如何使用property进行验证以及如何将

property与其他验证语言特性结合使用。

定义property

在SystemVerilog中，可以使用property语句来定义

property。property语句的基本语法如下：

property property_name;

@(posedge clk) disable iff(!rst_n) (property_expr);

endproperty

其中，property_name是property的名称，property_expr是

property的表达式，clk是时钟信号，rst_n是复位信号。disable

iff(!rst_n)表示在rst_n为低电平时禁用property。

property_expr是用于描述设计行为的表达式，可以包括多个

时序操作符和逻辑操作符。例如，以下是一个简单的property表达

式：

(a && b) |-> (c || d)

该表达式表示当a和b同时为真时，c或d必须至少有一个为

- 1 -

真。

在property_expr中，可以使用以下时序操作符：

- ##n：表示在n个时钟周期后，后面的表达式成立。

- ##[n,m]：表示在n到m个时钟周期之间，后面的表达式成

立。

- ->：表示前面的表达式成立后，后面的表达式在下一个时钟

周期内成立。

- |->：表示前面的表达式成立后，后面的表达式在未来的某个

时刻成立。

以下是一个使用时序操作符的property表达式的示例：

property p;

@(posedge clk) (a ##1 b ##[2,3] c) |-> d;

endproperty

该表达式表示当a和b之间有一个时钟周期、b和c之间有2

到3个时钟周期，并且d在下一个时钟周期内成立时，该property

表达式成立。

使用property进行验证

定义property后，可以使用assert语句来验证设计是否满足

该property。assert语句的基本语法如下：

assert property_name;

例如，以下是一个使用assert语句验证property的示例：

property p;

- 2 -

@(posedge clk) (a ##1 b ##[2,3] c) |-> d;

endproperty

assert p;

该代码片段表示当property p成立时，assert语句成立。

除了使用assert语句，还可以使用cover语句来检查

property的覆盖率。cover语句的基本语法如下：

cover property_name;

例如，以下是一个使用cover语句检查property覆盖率的示

例：

property p;

@(posedge clk) (a ##1 b ##[2,3] c) |-> d;

endproperty

cover p;

该代码片段表示在验证过程中，检查property p被覆盖的次

数。

将property与其他验证语言特性结合使用

在验证设计时，通常需要使用多种验证语言特性来检查设计的

正确性。SystemVerilog提供了多种验证语言特性，包括assert、

cover、assume、sequence和constraint等。可以将property与

这些验证语言特性结合使用，以实现更全面的验证。

例如，可以使用assume语句来定义假设条件，并与property

结合使用。assume语句的基本语法如下：

- 3 -

assume property_expr;

例如，以下是一个使用assume语句定义假设条件的示例：

assume a && b;

该代码片段表示a和b必须同时为真。

可以将假设条件与property结合使用，以验证设计是否满足该

条件。例如，以下是一个使用假设条件和property进行验证的示

例：

property p;

@(posedge clk) (a ##1 b ##[2,3] c) |-> d;

endproperty

assume a && b;

assert p;

该代码片段表示当a和b同时为真时，property p必须成立。

除了assume语句，还可以使用constraint语句来定义约束条

件，并与property结合使用。constraint语句的基本语法如下：

constraint constraint_expr;

例如，以下是一个使用constraint语句定义约束条件的示例：

constraint a == b;

该代码片段表示a和b必须相等。

可以将约束条件与property结合使用，以验证设计是否满足该

条件。例如，以下是一个使用约束条件和property进行验证的示

例：

- 4 -

property p;

@(posedge clk) (a ##1 b ##[2,3] c) |-> d;

endproperty

constraint a == b;

assert p;

该代码片段表示a和b必须相等，并且当property p成立时，

assert语句成立。

总结

在本文中，我们介绍了SystemVerilog中property的用法，包

括如何定义property、如何使用property进行验证以及如何将

property与其他验证语言特性结合使用。property是一种强大的验

证语言特性，可以用于描述设计行为并检查设计的正确性。通过结

合其他验证语言特性，可以实现更全面的验证。

- 5 -