一個簡單的斷言(SVA)示例
時間：2021-11-09 14:28:10
手機(jī)看文章
掃描二維碼
隨時隨地手機(jī)看文章
[導(dǎo)讀]斷言的英文是Assertion，就是對一些設(shè)計(jì)屬性的推斷。大型的硬件設(shè)計(jì)中會有各種各樣的協(xié)議接口。這些協(xié)議接口定義中一般都會有include文件，這些include文件中包含了接口的斷言描述，主要用于協(xié)議的時序檢查。除了這種把斷言語句放到接口協(xié)議里還可以放到具體的design里面...
斷言的英文是Assertion，就是對一些設(shè)計(jì)屬性的推斷。大型的硬件設(shè)計(jì)中會有各種各樣的協(xié)議接口。這些協(xié)議接口定義中一般都會有include文件，這些include文件中包含了接口的斷言描述，主要用于協(xié)議的時序檢查。除了這種把斷言語句放到接口協(xié)議里還可以放到具體的design里面，也可以單獨(dú)做成一個module的checker，把module checker和設(shè)計(jì)bind在一起。
斷言可以用Verilog實(shí)現(xiàn)，也可以用SystemVerilog Assertion（SVA）實(shí)現(xiàn)。由于要檢查時序，過程性語言Verilog并不是很好的選擇，一般會選擇描述性語言SVA實(shí)現(xiàn)，SVA對時序的描述近乎完美。本文講介紹一下SVA的簡單例子。如果想系統(tǒng)的學(xué)習(xí)SVA，可以買一本書《SystemVerilog Assertions 應(yīng)用指南》。方法1: 直接放到到design里面的方式如下。
ERROR現(xiàn)象符合預(yù)期。
方式2：單獨(dú)定義一個module 檢驗(yàn)器，然后通過bind實(shí)現(xiàn)。注釋DUT.v 中`include "assertion.svh"，打開test.v中的bind。Module檢驗(yàn)器文件
斷言可以用Verilog實(shí)現(xiàn)，也可以用SystemVerilog Assertion（SVA）實(shí)現(xiàn)。由于要檢查時序，過程性語言Verilog并不是很好的選擇，一般會選擇描述性語言SVA實(shí)現(xiàn)，SVA對時序的描述近乎完美。本文講介紹一下SVA的簡單例子。如果想系統(tǒng)的學(xué)習(xí)SVA，可以買一本書《SystemVerilog Assertions 應(yīng)用指南》。方法1: 直接放到到design里面的方式如下。
//文件dut.v ， dut很簡單，每個clk上升沿到來時對輸入a取反。`timescale 1ns/1nsmodule DUT (clk,a,b);input clk;input a;output b;reg b; always?@?(posedge?clk?)begin b<=~a;end`include "assertion.svh"endmodule//文件 test.v`timescale 1ns/1nsmodule TOP;reg clk;reg a;wire b;always #5 clk=~clk;initial begin clk <=0; a <=1;#30?$finish;endDUT dut(.clk(clk),.a(a) ,.b(b));//bind TOP.dut dut_assertion dut_assertion_check(.a_(a),.b_(b),.clk_(clk));endmodule每個clk上升沿，如果a=0，則是空成功，不滿足第一個a=1的條件，b就不需要判斷是否等于1，直接判斷為成功。如果a=1，則對b進(jìn)行判斷，b為1則為成功，否則斷言失敗。//assertion.svh文件property check_p; @(posedge clk) a |->b;endpropertycheck_a : assert property (check_p);運(yùn)行命令：irun -sv dut.v test.vERROR：ncsim:?*E,ASRTST (./assertion.svh,6):?(time 5 NS) Assertion TOP.dut.check_a has failedERROR現(xiàn)象符合預(yù)期。
方式2：單獨(dú)定義一個module 檢驗(yàn)器，然后通過bind實(shí)現(xiàn)。注釋DUT.v 中`include "assertion.svh"，打開test.v中的bind。Module檢驗(yàn)器文件
module dut_assertion(a_,b_,clk_);input logic a_,b_,clk_;property check_p;@(posedge clk_) a_ |->b_;endproperty check_a : assert property (check_p);endmodule運(yùn)行命令：irun -sv dut.v test.v assertion_module.svERROR：ncsim: *E,ASRTST (./assertion_module.sv,12): (time 5 NS) Assertion TOP.dut.dut_assertion_check.check_a has failed 
下載文檔
