一個簡單的斷言(SVA)示例
時間：2021-11-09 14:28:10
手機看文章
掃描二維碼
隨時隨地手機看文章
[導讀]斷言的英文是Assertion，就是對一些設計屬性的推斷。大型的硬件設計中會有各種各樣的協(xié)議接口。這些協(xié)議接口定義中一般都會有include文件，這些include文件中包含了接口的斷言描述，主要用于協(xié)議的時序檢查。除了這種把斷言語句放到接口協(xié)議里還可以放到具體的design里面...
斷言的英文是Assertion，就是對一些設計屬性的推斷。大型的硬件設計中會有各種各樣的協(xié)議接口。這些協(xié)議接口定義中一般都會有include文件，這些include文件中包含了接口的斷言描述，主要用于協(xié)議的時序檢查。除了這種把斷言語句放到接口協(xié)議里還可以放到具體的design里面，也可以單獨做成一個module的checker，把module checker和設計bind在一起。
斷言可以用Verilog實現(xiàn)，也可以用SystemVerilog Assertion（SVA）實現(xiàn)。由于要檢查時序，過程性語言Verilog并不是很好的選擇，一般會選擇描述性語言SVA實現(xiàn)，SVA對時序的描述近乎完美。本文講介紹一下SVA的簡單例子。如果想系統(tǒng)的學習SVA，可以買一本書《SystemVerilog Assertions 應用指南》。方法1: 直接放到到design里面的方式如下。
ERROR現(xiàn)象符合預期。
方式2：單獨定義一個module 檢驗器，然后通過bind實現(xiàn)。注釋DUT.v 中`include "assertion.svh"，打開test.v中的bind。Module檢驗器文件
斷言可以用Verilog實現(xiàn)，也可以用SystemVerilog Assertion（SVA）實現(xiàn)。由于要檢查時序，過程性語言Verilog并不是很好的選擇，一般會選擇描述性語言SVA實現(xiàn)，SVA對時序的描述近乎完美。本文講介紹一下SVA的簡單例子。如果想系統(tǒng)的學習SVA，可以買一本書《SystemVerilog Assertions 應用指南》。方法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進行判斷，b為1則為成功，否則斷言失敗。//assertion.svh文件property check_p; @(posedge clk) a |->b;endpropertycheck_a : assert property (check_p);運行命令：irun -sv dut.v test.vERROR：ncsim:?*E,ASRTST (./assertion.svh,6):?(time 5 NS) Assertion TOP.dut.check_a has failedERROR現(xiàn)象符合預期。
方式2：單獨定義一個module 檢驗器，然后通過bind實現(xiàn)。注釋DUT.v 中`include "assertion.svh"，打開test.v中的bind。Module檢驗器文件
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運行命令：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 
下載文檔
