基于断言的验证

基于断言的验证

断言的概念十分简单。只要在程序中声明，我们相作言某事情必定为真，若不为真，则在屏幕上打印错误信息即可。在 SystemVerilog语言中，断言可以用立即(immediate)和并发(concurrent)两种不同形式的断言来表示。立即断言十分简洁，可以用if、else等语句表示。而并发断言的功能十分强大，所以本节用大部分篇帽福讲解如何编写并发断言。

在 always过程块中可以把这个事实声明为立即断言(该立目即断言相当于一个always_comb过程块，但是为了避免概念混淆，我们只在可综合的RTL模块中使用always_comb)。

always @*
	assert(~(dispense&&ready))
	else $error("dispense and ready both lit!");

上面这个断言每当dispense或者ready信号变化时，就检查它们是否同时为1。但是最好在时钟的正跳变沿检测这个条件，因为我们检查的是一个同步系统。首先把这个条件编写为如下属性property:

property NotDispenseAndReady;
	@(posedge clock)(~(dispense && ready));
 endproperty

然后，作为并发断言的一部分，对这个属性进行测试，其代码如下:

assert property(NotDispenseAndReady);

可以把属性定义和断言声明合并在一起编写。但是常用的编程风格建议，为了属性的重复使用，最好将属性定义和断言声明分成两部分编写。

通常，并发断言