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

    作为一种对设计对象的属性特性或行为特性的的描述，断言（声明，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;

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

    作为一种对设计对象的属性特性或行为特性的的描述，断言（声明，assertion）并不是一个新的概念。实际上在软件设计中，断言已经得到了广泛的应用，它可以帮助软件工程师在软件开发及测试过程中更早更快的发现、定位出软件中可能存在的错误。例如在java中定义了一种断言的语法：assert expression1:expression2，当程序运行到这个断言，如果expression1的值为假，则程序会报错，并根据expression2给出相应的错误信息。许多java的工程师都认为断言是最快也是最有效的调试方法。现在同样的概念越来越多被引入到硬件及soc设计中。

    随着设计复杂度的增加，如何进行有效、充分的硬件设计验证，尤其是功能验证已经成为硬件设计方法学中重要的内容。普遍认为在rtl设计中超过70％的工作在进行功能验证，同时有超过2/3的芯片设计需要进行重新流片以纠正功能错误。本文将说明基于断言的验证（assertion based verification: abv）是硬件设计功能验证的一种有效方法，尤其当我们将断言和形式验证进行有机结合时。

    硬件设计的断言和基于断言的验证

    a. 硬件设计的断言

    每一个硬件设计都包含了设计对象的特性，这些特性保证了硬件能够正常工作。某些特性属于电路本身的属性特性，例如为了避免latch的引入，在case语句的描述中，我们需要进行满足full case特性的描述。另外一些特性属于电路行为的特征，包括静态特性－这些特性在任何时候都应该保持，例如三态总线在任何时