SystemVerilog Assertions应用指南 第一章

1.1什么是断言

        断言是设计的属性的描述。
        ●  如果一个在模拟中被检查的属性( property)不像我们期望的那样表现,那么这个断言失败。
        ●  如果一个被禁止在设计中出现的属性在模拟过程中发生,那么这个断言失败。

        一系列的属性可以从设计的功能描述中推知,并且被转换成断言。这些断言能在功能的模拟中不断地被监视。使用形式验证技术,相同的断言能被重用来验证设计。断言,又被称为监视器或者检验器,已经被用作一种调试技术的方式,在设计验证流程中使用了很长时间。传统上,它们由过程语言,比如 Verilog,来实现。它们也能用PLI和C/C++的程序来实现。下面的代码显示了相互断言条件检查的 Verilog实现,其中信号a和信号b不能同时为高电平。如果这种情况发生,则显示这是一个错误信息。

`ifdef ma 
	if(a & b )
	$display("Error ；Mutually asserted check failed .\n");
`endif 

        这种监视器仅作为模拟的一部分而存在,因此只有当需要时才被纳入设计环境中。这可以通过允许 Verilog代码条件编译的指令“‘`ifdef”来实现。

1.2为什么使用 System Verilog断言(SVA)

        虽然Verilog可以很容易地用来实现一些检查,它仍有一些不足之处
        （1） Verilog是一种过程语言,因此并不能很好地控制时序。
         (2)   Verilog是一种冗长的语言,随着断言的数量增加,维护代码将变得很困难。
        （3）语言的过程性这一本质使得测试同一时间段内发生的并行事件相当困难。在一些情况下,一个 Verilog的检验器甚至可能无法捕捉到所有被触发的事件。
        (4) Verilog语言没有提供内嵌的机制来提供功能覆盖的数据。用户必须自己实现这部分代码。

        SVA是一种描述性语言,可以完美地描述时序相关的状况。语言的描述性本质提供了对时间卓越的控制。语言本身非常精确且易于维护。SVA也提供了若干个内嵌函数来测试特定的设计情况,并且提供了一些构造来自动收集功能覆盖数据。例子1.1显示了分别用Ⅴerilog和SVA实现的检验器。这个检验器验证当信号a在当前时钟周期为高电平时,下面1~3个时钟周期内,信号b应该变为高电平。

例子1.1分别用 Verilog和SVA实现的断言实例

用Verilog实现的断言示例

//simple verilog checker
 
always @(posedge a)
	begin
		repeat (1) @(posedge clk );
			fork :a_to_b
				begin
					@(posedge b)
					$display("SUCESS :b arrived in time \n",$time);
					disable a_to_b;
					
				end
				begin
					repeat (3) @(posedge clk);
						$display("ERROR :b did not arrive in time \n",$time);
						disable a_to_b;
				end
				join
	end

用Systemverilog实现的断言示例

//SVA checker
 
a_to_b_chk:
	assert property
	@(posedge clk) $rose (a)|->##[1:3] $rose(b);

        例子1.1很清楚地显示了SVA的优势。本章将讨论SVA语法。检验器代表着一种非常简单的协议。使用SVA实现只需要一行代码,而相同的协议描述用 Verilog则需要好几行。此外,失败和成功的条件必须在 Verilog里额外地被定义,而SVA中断言失败会自动显示错误信息。

1.3 System Verilog的调度

        System Verilog语言被定义成一种基于事件的执行模式。在每时隙( time slot),许多事件按照安排的顺序发生。这个事件的列表依照标准定义的算法执行。依照这个算法,模拟器可以防止任何在设计和测试平台互动中的不一致。断言的评估和执行包括以下三个阶段
        预备( Preponed)在这个阶段,采样断言变量,而且信号(net或变量( variable)的状态不能改变。这样确保在时隙开始的时候样到最稳定的值。
        观察( Observed)在这个阶段,对所有的属性表达式求值。
        响应( Reactive)在这个阶段,调度评估属性成功或失败的代码。图1-2显示了一个简化了的 System Verilog事件进程安排流程表。要彻底地理解 System Verilog的进程安排算法,请参考<>[1]。

1.4SVA术语

        System Verilog语言中定义了两种断言:并发断言和即时断言。

14.1并发断言

        （1）基于时钟周期。
        （2）在时钟边缘根据调用的变量的样值计算测试表达式。
        （3）变量的采样在预备阶段完成,而表达式的计算在调度器的观察阶段完成。
        （4）可以被放到过程块( procedural block)、模块( module)、接口interface),或者一个程序( (program)的定义中
        （5）可以在静态(形式的)验证和动态验证(模拟)工具中使用。
一个并发断言的例子如下：

a_cc : assert property ((@posedge clk ) not (a&&b));

        图1-3显示了并发断言acc的结果。所有的成功显示成向上的箭头,所有的失败显示成向下的箭头。这个例子的核心内容是属性在每一个时钟的上升沿都被检验,不论信号a和信号b是否有值的变化。

1.4.2即时断言

（1）基于模拟事件的语义。
（2）测试表达式的求值就像在过程块中的其他 verilog的表达式一样。
（3）它们本质不是时序相关的,而且立即被求值。
（4）必须放在过程块的定义中。
（5）只能用于动态模拟。
一个即时断言的例子如下：

always_com
	begin
		a_ia:assert(a && b);
		
	end

        即时断言a_ia被写成一个过程块的一部分,它遵循和信号a、b相同的事件调度。当信号a或者信号b发生变化时, always块被执行。区别即时断言和并发断言的关键词是“ property”。图1-4显示了即时断言a_ia的结果:

1.5建立SVA块

        在任何设计模型中,功能总是由多个逻辑事件的组合来表示的。这些事件可以是简单的同一个时钟边缘被求值的布尔表达式,或者是经过几个时钟周期的求值的事件SA用关键词“ sequence”来表示这些事件。序列( sequence)的基本语法是:

sequence name_of_sequence;
    <test expression>
endsequence

        许多序列可以逻辑或者有序地组合起来生成更复杂的序列。SVA提供了一个关键词“ property”来表示这些复杂的有序行为。属性 (roperty)的基本语法是:

property name_of_property;
	<test expression >; or 
	<complex sequence expression>
endproperty

        属性是在模拟过程中被验证的单元。它必须在模拟过程中被断言来发挥作用。SVA提供了关键词“ assert”来检查属性。断言( assert)的基本语法是:

assertion_name: assert property (property_name)

建立SA检验器的步骤如图1-5所示

        一个简单的序列序列s1检查信号“a”在每个时钟上升沿都为高电平。如果信号“a”在任何一个时钟上升沿不为高电平,断言将失败。注意,这相当于“a==1'b1”。

sequence s1
	@(posedge clk ) a;
endsequence

        图1-6显示了信号“a”和序列在模拟中对这个信号响应的波形。信号“a”在第七个时钟上升沿变为0。这一变化在第八个时钟周期被采样到。因为并行断言使用进程安排中预备(“ prepend”)阶段采样到的值,在第七个时钟周期,序列s1采样到的信号“a的最稳定的值是1。因此序列成功。在第八个时钟周期,信号“a”被采样的值为0,因此序列失败。一个向上的箭头表示一次成功,个向下的箭头表示一次失败。表1-1总结了信号“a”每个时钟周期的采样值,直到第十五个时钟周期。

1.7边沿定义的序列

        序列s1使用的是信号的逻辑值。SVA也内嵌了边缘表达式,以便用户监视信号值从一个时钟周期到另一时钟周期的跳变。这使得用户能检查边沿敏感的信号。三种这样有用的内嵌函数如下:

（1）$rose(boolean expression or signal_name
                当信号/表达式的最低位变成1时返回真
（2）fell(boolean expression or signal_name
                当信号表达式的最低位变成0时返回真。
（3）$stable(boolean expression or signal_name
                当表达式不发生变化时返回真

        序列s2检查信号“a”在每一个时钟上升沿都跳变成1。如果跳变没有发生,断言失败。

        sequence s2;
                @(posedge clk)  $rose(a)
        endsequence

        图1-7显示序列s2响应信号“a”跳变的情况。标记1显示了序列s2的第一个成功。在时钟周期1,信号“a”的值从0变到1在这个时钟周期,信号“a”在序列中的采样值是0。在时钟周期1之前,信号“a”没有被赋值,因此值被认定为“x”。值从x到0的转化不是上升沿,因此序列失败。在时钟周期2,信号“a”在序列中的采样值是1。值从0到1的转化是上升沿,因此序列2在时钟周期2成功。在时钟周期9的标记2显示了另一个成功。表1-2总结了信号“a”前9个时钟周期的转化以及序列如何样和更新值。

1.8逻辑关系的序列

        序列s3检査每一个时钟上升沿,信号“a”或信号“b”是高电平。如果两个信号都是低电平,断言失败。

sequence s3;
	@(posedge clk) a|| b;
endsquence

        图1-8显示序列S3如何根据信号“a”和“b”做出反应。标记1显示了时钟周期12,信号“a”和“b”的采样值都是0,因此序列失败。同理,在标记2所在的时钟周期17,序列也失败。在所有其他时钟周期,信号“a”和信号“b”至少有一个其值为1,因此在这些时钟周期,序列都成功。

1.9序列表达式

        通过在序列定义中定义形参,相同的序列能被重用到设计中具有相似行为的信号上。例如,我们可以定义下面这个序列

sequence s3_lib(a, b);
        a||b;
endseqruence

        通用的序列s3_lib能重用在任何两个信号上。例如,我们有两个信号“req1”和“req2”,它们中至少一个信号应该在时钟周期的上升沿为1,我们可以使用下列的序列

sequence s3_lib_inst1;
	s3_lib (req1,req2);
endsequence

        这些在设计中常见的通常的属性可以被开发成一个库以便于重用。比如,one-hot状态机检查,等效性检查等都适合放在这样的检验器库中。

1.10时序关系的序列

        简单的布尔表达式在每个时钟边缘都会被检查。换句话说,它们只是简单的组合逻辑检査。很多时候,我们关心的是检查需要几个时钟周期才能完成的事件。也就是所谓的“时序检查”。在SVA中,时钟周期延迟用“##”来表示。例如,##3表示3个时钟周期。序列s4检查信号“a”在一个给定的时钟上升沿为高电平如果信号“a”不是高电平,序列失败。如果信号“a”在任何个给定的时钟上升沿为高电平,信号“b”应该在两个时钟周期后为高电平。如果信号“b”在两个时钟周期后不为1,断言失败。注意,序列以信号“a”在时钟上升沿为高电平开始。

sequence s4;
	@(posedge clk) a ##2 b;
endsequence

        图1-9显示了序列s4在模拟过程中的响应。表1-3总结了信号“a”和信号“b”在每个时钟周期的采样值。

        与前面小节中的例子不同的是,序列s4的开始时间和结束时间不同。如果信号“a”在任何时钟周期不为高电平,序列在同个时钟周期开始并失败。如果信号“a”是高电平,序列开始。在两个时钟周期后,如果信号“b”是高电平,序列成功(第5和第4时钟周期)。另一方面,如果在两个时钟周期后,信号“b”不是高电平,序列失败。应注意的是,在图中,成功的序列总是标注在序列开始的位置。

1.11SVA中的时钟定义

        一个序列或者属性在模拟过程中本身并不能起什么作用。它们必须像下面的例子那样被断言才能发挥作用。

sequence s5;
	@(posedge clk) a ##2 b;
endsequence
 
property p5;
	s5;
endproperty
 
a5 :assert property (p5);

        注意,序列s5中指定了时钟。这是一种把检查和时钟关联起来的方法,但是还有其他的方法。在序列、属性,甚至一个断言的语句中都可以定义时钟。下面的代码显示了在属性p5a的定义中指定时钟。

sequence s5a;
	a ##2 b;
endsequence
 
property p5a;
	@(posedge clk) s5a;
endproperty
 
a5a : assert property (p5a);

        通常情况下,在属性( property)的定义中指定时钟,并保持序列( sequence)独立于时钟是一种好的编码风格。这可以提高基本序列定义的可重用性。断言一个序列并不一定需要定义一个独立的属性。因为断言语句调用属性,在断言的语句中可以直接调用被检查的表达式,如下面的断言a5b所示。

sequence s5b;
	a ##2 b;
endsequence
 
a5b :assert property (@(posedge clk) s5b);

        当我们在断言的陈述中要调用已经定义了时钟的序列,就不能再次在断言语句中定义时钟。下面的断言a5c就显示了这种错误的编程风格。下列情况是不允许的。

ac5 :assert property (@(posedge clk) s5);

1.12禁止属性

        在之前的所有例子中,属性检查的都是正确的条件。属性也可以被禁止发生。换句话说,我们期望属性永远为假。当属性为真时,断言失败。
        序列s6检查当信号“a”在给定的时钟上升沿为高电平,那么两个时钟周期以后,信号“b”不允许是高电平。关键词“not”用来表示属性应该永远不为真。

sequence s6;
	@(posedge clk)  a ##2 b;
endsequence
 
property p6;
	not s6;
endproperty
 
a6 :assert property(p6);

        图1-10显示了断言a6如何在模拟过程中响应。我们注意到检验器在标记1和2显示的两个位置(时钟5和14)失败。在这两个时钟周期,发生了被禁止的序列,断言因此失败。另一方面,在信号“a”有效的两个位置(时钟2和时钟9检验器成功。因为从这两个时钟周期开始检查,两个时钟周期以后言号“b”不为高,因此检验器成功。在其他时钟周期中,信号“a”都不为高,因此检验器都自动成功。表1-4总结了信号“a”和信号“b”在每个时钟周期的采样值。

1.13一个简单的执行块

        System Verilog语言被定义成每当一个断言检查失败,模拟器在默认情况下都会打印出一条错误信息。模拟器不需要对成功的断言打印任何东西。读者同样也可以使用断言陈述中的“执行块”action block)来打印自定义的成功或失败信息。执行块的基本语法如下所示。

assert_name :
	assert property(property_nmae)
		<success message>;
	else 
		<fail message>;

        下面显示的检验器a7在执行块中使用了简单的显示语句来打印成功和失败信息。

property p7;
	@(posedge clk) a ##2 b;
endproperty
 
a7: assert property(p7)
	$display("Property p7 successed \n");
	else
	$display("property p7 failed \n");

        执行块不仅仅局限于显示成功和失败。它可以有其他的应用,例如:控制模拟环境和收集功能覆盖数据。这些主题将在第2章详细讨论。