硬件设计复杂度的增加使功能验证成为硬件设计方法学中的重要内容，基于断言技术的硬件设计验证技术得到越来越多的应用。

　　作为一种对设计对象的属性特性或行为特性的的描述，断言 （声明，assertion）并不是一个新的概念。实际上在软件设计中，断言已经得到了广泛的应用，它可以帮助软件工程师在软件开发及测试过程中更早更快的发现、定位出软件中可能存在的错误。例如在JAVA中定义了一种断言的语法：assert Expression1:Expression2，当程序运行到这个断言，如果Expression1的值为假，则程序会报错，并根据Expression2给出相应的错误信息。许多JAVA的工程师都认为断言是最快也是最有效的调试方法。现在同样的概念越来越多被引入到硬件及SoC设计中。
　　随着设计复杂度的增加，如何进行有效、充分的硬件设计验证，尤其是功能验证已经成为硬件设计方法学中重要的内容。普遍认为在RTL设计中超过70％的工作在进行功能验证，同时有超过2/3的芯片设计需要进行重新流片以纠正功能错误。本文将说明基于断言的验证（Assertion Based Verification: ABV）是硬件设计功能验证的一种有效方法，尤其当我们将断言和形式验证进行有机结合时。
　　硬件设计的断言和基于断言的验证
　　A. 硬件设计的断言
　　每一个硬件设计都包含了设计对象的特性，这些特性保证了硬件能够正常工作。某些特性属于电路本身的属性特性，例如为了避免latch的引入，在case语句的描述中，我们需要进行满足full case特性的描述。另外一些特性属于电路行为的特征，包括静态特性－这些特性在任何时候都应该保持，例如三态总线在任何时候只允许最多一个驱动－和时序（temporal）特性，即只在给定时刻（或时间段内）需要满足的特性。在AMBA AHB的master写操作中，slave可以在数据传输周期插入等待状态以扩展整个写周期。在整个扩展周期里，master要保持数据和控制信号的稳定［1］，如图1所示。

图1，在扩展整个写周期里，master应保持数据和控制信号稳定。

　　我们在设计AHB的master时要遵从这样的特性，同时我们在描述AHB总线的master write测试激励时也要遵从这样的特性。在硬件设计中，实现对这些特性进行检查的方法或实现这些方法的描述则被称为断言。
　　设计特性可以使用各种语言来描述，例如Verilog，VHDL，SystemC等。VHDL已经包含了对一些简单的特性描述的能力［5］，例如在VHDL语言中可以使用如下的断言声明：
　　assert condition report assertion_message;
　　这样在VHDL仿真过程中，当condition的值为“假”的时候，VHDL仿真器会给出assertion_message所定义的信息。但某些特性使用硬件或系统描述语言会非常低效，例如以下的时序特性：当 sigA触发时，在5个时钟周期内，sigB必须触发， 6个时钟周期后，sigA必须复位。如果使用HDL语言来描述这个特性，可能需要一个状态机来描述。为了更方便和高效地描述设计特性，一种方法是基于当前流行的设计语言开发特性描述库，Open Verification Library（OVL,www.accellera.org）是其中的一个例子。
　　同时一些专门用于硬件特性描述的语言（Property Specification Language: PSL）和断言描述的语言已经开始被应用到实际设计之中。IBM公司开发的Suger语言被Accellera组织接受成为PSL的标准[2]。Synopsys的OVA则是另一个经过实际设计验证的断言描述语言。当前设计工程师和验证工程师使用不同的语言，其所带来的弊端显而易见，于是人们希望一个统一的既支持硬件设计又支持硬件验证的语言。Accellera组织采用了SystemVerilog[2]。Synopsys则将OVA捐献到SystemVerilog中作为其用于断言描述的语言基础[3]。
　　B. 基于断言的验证（ABV：Assertion Based Verification）
　　基于断言的验证适用于“白盒”“灰盒”“黑盒”三种验证方法。在“白盒”的情况下，断言是嵌入在设计的实现代码里，应该由设计工程师加入，它和设计的实现紧密相关。例如下面的例子在设计里面加入了断言：
　　module fifo(rst,clk,data,rd_wr,full, empty);
　　input rst,clk, rd_wr;
　　output full, empty;
　　/ ova ova_mutex(!rst,clk,full,empty);
　　input [7:0] data;
　　always @(posedge clk)
　　
　　endmodule
　　断言ova_mutex描述了设计的属性：当rst为0的时候，在clk的上升沿，full和empty不可以同时为1。其中，ova_mutex是定义在ova中的检查库（checker）[4]。支持OVA的验证工具会动态（通过仿真技术）或静态（通过形式验证技术）分析设计描述是否满足所设定的设计属性。
　　在“黑盒”的情况下，断言与设计的具体实现不相关，通常是可以在一个单独的断言描述文件中描述设计接口应该满足的特性。一般应该由验证工程师给出相应的断言文件。下面以OVA为例来说明“黑盒”的基于断言的验证方法。
　　一个典型的OVA文件包括：
　　● 布尔关系的定义 ：定义一组信号之间的逻辑关系；
　　● 时序事件的定义 ：定义信号之间的时序属性；
　　● 断言声明：检测上述定义的时序属性；
　　● 绑定断言与相应的设计
　　下面的一段代码是一个典型的OVA文件：
　　/“unit” 包含了时钟、相应的逻辑信号、布尔关系和时序事件的定义以及断言声明
　　unit protocol( logic clk, logic valid,
　　logic [423:0] framein,
　　logic frame0,logic frame1);
　　clock posedge clk {
　　/信号布尔关系的定义
　　bool b_valid0 : (valid) & (framein[7:4] == 4'b0000); 
　　bool b_valid1 : (valid) & (framein[7:4] == 4'b0001); 
　　/时序事件的定义
　　event e_frame0 : if ((b_valid0)) then #[03] frame0;
　　event e_frame1 : if ((b_valid1)) then #[03] frame1;
　　}
　　/设计属性的断言声明
　　assert a_frame0 : check(e_frame0);
　　assert a_frame1 : check(e_frame1);
　　endunit
　　/绑定相应的断言和设计
　　bind module router : protocol uprotocol
　　(clk,valid,frame_data,frame0,frame1,frame2,frame3);
　　在上述的OVA定义下，不管模块“router”具体的实现细节，我们都要求router的信号满足OVA文件定义的设计属性。
　　“灰盒”的情况处于“白盒”和“黑盒”之间，它包含了一定的设计实现的特性。
　　基于断言的设计验证方法对设计验证方法学带来一些重要的影响，成为先进的设计验证方法学的核心：
　　● 设计功能的验证已经成为复杂设计中的主要任务，尤其是复杂设计中不同子模块之间的接口很容易带来潜在的错误需要验证。断言语言允许验证工程师在较高的描述层次上对设计属性进行定义，这种定义比硬件描述语言的描述要简洁和自然得多。
　　● 用断言语言描述的设计属性具有重用性。由于“黑盒”的断言描述与具体的实现不相关，用户可以方便地在不同的设计中重用已有的属性定义，例如，对PCI、AMBA等所定义的设计属性描述可在不同的设计中用于功能仿真。
　　● 传统的验证覆盖率分析是基于代码覆盖的覆盖率分析，例如，代码行覆盖率、条件分支覆盖率、信号翻转覆盖率等。由于断言定义了设计的属性（或可认为是功能），通过对断言的覆盖率统计我们可以将传统的代码覆盖率分析提升到功能覆盖率分析[6]。功能覆盖率分析对于设计的功能检查具有更加直接的意义。
　　传统上，设计功能的验证是基于动态的仿真，通过观察仿真结果发现、定位设计的缺陷。随着ASIC和SoC设计复杂性的增加，如何有效的构建设计的测试激励，缩短验证周期为功能验证带来了巨大的挑战。因此高效率的测试激励自动生成技术也是当前设计验证的热点技术之一。测试激励自动生成的核心是带约束的随机测试激励自动生成。在仿真过程中，从断言验证而给出的功能测试覆盖信息，我们可以知道哪些功能已经经过测试，根据这些信息我们可以动态调整产生随机测试激励的约束条件，从而明显的提高测试效率。采用上述方法的验证流程如图 2所示。

图2，带约束的随机测试激励自动生成法的验证流程。

　　然而基于断言的验证方法所带来的验证方法学上的巨大变化是将断言与形式验证技术相结合。门级的形式验证技术由于大大提高了门级验证的效率而得到了越来越多的采用。相对于动态的仿真技术，形式验证技术（门级的或更高抽象层次上的）具有以下明显的特点：
　　● 形式验证技术不需要测试激励。
　　● 形式验证技术可以更加有效地发现深层的、不易发现的设计缺陷。
　　在越来越复杂的设计中，基于断言的设计功能、行为的形式验证技术得到了广泛的关注，并在一些实际的复杂设计中加以采用。在这种设计方法中，通过形式验证的方法证明设计的功能、行为是否满足断言所定义的属性。
　　但是形式验证技术，尤其是包括了时序关系的形式验证技术，其计算复杂度随着“状态寄存器”的数目呈指数关系增加，限制了形式验证技术在大规模设计中的应用[7]。为了解决这个问题，一种采用 “动态仿真”和形式验证相结合的“混合形式验证”应用了动态仿真和形式验证两种技术的特点（图3）。通过混合形式验证中的仿真引擎使设计“到达“某一状态，然后在此状态上应用形式验证引擎进行形式验证，分析设计是否遵从断言所定义的属性。然后再应用动态仿真的引擎使设计到达一个新的状态，进行形式验证。重复这样一个过程，直到达到某一设定的验证目标。混合形式验证与传统的形式验证一样也不需要测试激励，而且当设计被证明违反一设计属性时，混合形式验证还可以给出导致这一设计缺陷的测试激励。

图3，混合形式验证技术的图示和采用混合形式验证的设计流程。

　　基于断言的形式验证改变了传统的基于动态仿真的硬件验证方法，从而转向了基于设计属性的定义、描述和分析。而且基于断言的形式验证技术 不依赖于测试激励，能够有效地提高验证效率。这样我们就可以从以往的”先设计，再验证“的设计方法学转变到”先定义，然后设计和验证“的方法学。这种方法学已经在一些非常复杂的设计中得到应用[9][10][11].
　　OVL、OVA和OVA库
　　OVL是由Accellera（www.accellera.com）推出的采用了断言思想的验证库。它实际上是使用HDL语言（VHDL和Verilog）定义和实现了一些非常常用的属性声明。用户可以在设计里面直接使用这些属性声明来检测设计是否遵从了相应的设计属性。最新版本提供了以下属性断言［8］：
　　. assert_always . assert_no_undeRFlow . assert_always_on_edge  . assert_odd_parity
　　. assert_change  . assert_one_cold  . assert_cycle_sequence  . assert_one_hot
　　. assert_decrement  . assert_proposition . assert_delta  . assert_quiescent_state
　　. assert_even_parity  . assert_range . assert_fifo_index  . assert_time
　　. assert_frame.  . assert_transition  . assert_handshake  . assert_unchange
　　. assert_implication  . assert_width . assert_increment  . assert_win_change
　　. assert_never  . assert_win_unchanged . assert_next  . assert_window
　　. assert_no_overflow  . assert_zero_one_hot . assert_no_transition 
　　例如用户可以在Verilog设计中使用assert_never来设定某种情形永不发生的属性特性。下面是使用assert_nerver的一个例子：
　　module guarded_fifo (clk, reset_n, read, write, data_in, data_out);
　　input clk, reset_n, read, write;
　　input [15:0] data_in;
　　output [15:0] data_out;
　　wire fifo_full, fifo_empty;
　　fifo fifo (clk, reset_n, read, write, data_in, data_out, fifo_full, fifo_empty);
　　assert_never #(0, 0, “Fifo overflow”) fifo_overflow (clk, reset_n, fifo_full && write);
　　assert_never #(0, 0, “Fifo underflow”) fifo_underflow (clk,reset_n, fifo_empty && read);
　　endmodule
　　对于更复杂的属性定义，OVL的用户可能需要将多个属性声明配合使用。
　　为了更有效的进行设计属性描述，一些专门的属性描述语言被开发出来。OpenVera Assertion（OVA）是被广泛使用的一种断言描述语言。OpenVera(www.openvera.org)是一个开放的用于硬件测试激励自动生成的语言。在 OpenVera的基础上，Synopsys和Intel一起将Intel的断言描述语言ForSpec融合到OpenVera中并提出了新的断言描述语言OpenVera Assertion[3]。下面简要的介绍一下OVA以及在OVA中定义的设计属性库。
　　像上面OVA的例子中看到的一样，OVA采用一种层次化的结构来对设计对象的属性进行描述。从底到上，这些层次依次是：布尔表达式、事件表达式、断言声明表达式、以及由上述表达式所构成的一个设计属性描述单元。最后，设计属性描述单元绑定到一个设计模块或设计模块的一个例化。
　　· 布尔表达式：布尔表达式用来描述一组信号之间的逻辑关系。
　 　· 事件表达式：事件表达式用来描述一组信号（设计信号或上述布尔表达式所定义的信号）之间的时序关系。OVA通过事件表达式来定义设计的时序属性。通过OVA的事件表达式来描述时序属性比通过HDL进行描述要简单明了的多。例子如下：
　　event chk : if (a) then
　　#1 istrue (a==1) in (#[03] b);
　　表述了这样的时序关系：在任何时候，当信号a为真的时候，信号b必须在此后的1到4个时钟周期内置位为真，并且在此期间，信号a必须一直保持为真，直到b为真。除了支持描述不同信号之间的时序关系外，OVA也支持描述所定义的事件之间的时序关系。例如下面的例子：
　　event e1: posedge rdy #1 proc_1 #1 proc_2;
　　event rule: if (reset)
　　then inst #1 ended e1 #1 branch_back;
　　表述了这样的时序关系：事件e1：在rdy的上升沿一个时钟周期之后，信号proc_1置位为真，再过一个时钟周期，信号proc_2置位为真。事件rule：在reset信号置位的情况下，若信号inst置位则一个时钟周期后事件e1必须结束，再一个时钟周期之后，信号branch_back置位。这样通过描述信号之间的时序关系以及事件之间的时序关系，我们可以方便地由一些简单的事件表达式构成非常复杂的时序关系表示。
　　● 断言声明 ：断言声明指出设计所应遵从的设计属性。断言声明有两类：forbid和check。forbid表示相应的事件在设计中不应发生，而check则表示相应的事件在设计中应该发生。例如下面的例子：
　　unit mutex_check (logic clk, logic a, logic b);
　　clock posedge (clk) {
　　event e_mutex: !(a && b); 
   }
　　assert a_mutex : check(e_mutex);
　　endunit
　　定义了一个事件e_mutex，并且定义了一个断言声明：在设计中，e_mutex应当为真。这样当信号a和b都置位的时候,事件e_mutex为假，仿真或形式验证工具会给出设计违背了断言声明所定义的属性的信息。
　　● 设计属性描述单元和绑定：上述所定义的信号、事件和断言声明可以组成一个设计属性描述单元。可以认为设计属性单元是一个设计属性库，同时在定义设计属性单元时可以使用参数，以增加设计属性单元的通用性、重用性。作为一个设计属性库，设计属性单元可以以两种方式绑定到相应的设计：绑定到一个模块，则在设计中，这个模块的所有的例化都应遵从断言设定的属性；或绑定到一个模块的某一或某几个的例化。下面两个例子是上面两种情形的示例：
　　bind module mpu : states mpu_states
　　#(3, 8, 2, "Not state 2")  (clk, state_var, {{0}, {1}, {2}});
　　上面的例子将模块mpu与设计属性单元states进行绑定。代码的第二行设定了属性描述单元states所包含的参数相应的值。
　　bind instances tb.mpu1, tb.mpu2 : states mpu_states_instances
　　#(3, 8, 2, "Not state 2")  (clk, state_var, {{0}, {1}, {2}});
　　这段代码则将设计单元属性states与模块mpu的两个例化tb.mpu1和tb.mpu2进行绑定。
　　与OVL一样，在OVA中也定义了常用的属性声明，构成了OVA的检查库。OVA的检查库包括以下几类：
　　· 对象值属性检查库
　　. ova_arith_oveRFlow  . ova_asserted  . ova_bits  . ova_check_bool
　　. ova_const . ova_deasserted  . ova_dec . ova_delta
　　. ova_even_parity  .ova_forbid_bool  . ova_inc
　　. ova_odd_parity . ova_overflow . ova_range ova_underflow . ova_value
　　· 状态转移属性检查库
　　. ova_code_distance . ova_driven . ova_mutex&n bsp;. ova_next_state
　　. ova_one_cold . ova_one_hot . ova_quiescent_state . ova_tri_state
　　· 事件定时时序属性检查库
　　. ova_hold . ova_hold_value  . ova_reg_loaded  . ova_sequence
　　. ova_timeout . ova_window
　　· 事件协议属性检查库
　　. ova_arbiter . ova_data_used  . ova_dual_clk_fifo . ova_fifo
　　. ova_follows . ova_memory . ova_memory_async . ova_no_contention
　　. ova_req_requires . ova_req_resp ova_stack  . ova_valid_id
　　结论
　　设计复杂度的增加、IP重用等当前复杂SoC/ASIC设计的特性要求对设计的功能进行更加充分的验证。基于断言技术并结合了动态仿真、形式验证、测试激励自动化等方法的硬件验证平台构成了新的验证方法学，能有效提高验证的质量和效率。

　　参考文献
　　[1] AMBATM Specification(Rev2.0)
　　[2] www.accellera.com
　　[3] Gabe Moretti, “Formal verification is ready for the limelight”, EDN,2002,9,26
　　[4] OpenVera Assertions Language Reference Manual, Synopsys, Inc.
　　[5] 1076TM IEEE Standard VHDL Language Reference Manual
　　[6] Surrendra Dudani, “High Level Functional Verification Closure”, IEEE International Conference on Computer Design, 2002
　　[7] Michael C McFarland, “Formal Verification of Sequential Hardware: A Tutorial”, IEEE Transactions on Computer-aided Design of Integrated Circuites and Systems. Vol 12,No.5, May 1993
　　[8] Open Verification Library, Assertion Monitor Reference Manual.  http://www.verificationlib.org/
　　[9] Bob Bentley, “Validating the Intel Pentium 4 Microprocessor”, Dependable Systems and Networks, 2001. Proeedings. The International Conference on , 1-4 July 2001
　　[10] Patankar,V.A, “Formal Verification of an ARM processor”, VLSI Design, 1999. Proceedings. Twelfth International Conference On , 7-10 Jan. 1999
　　[11] Tasiran,S., “Using a formal specification and a model checker to monitor and direct simulation”, Design Automation Conference, 2003. Proceedings , June 2-6, 2003