時(shí)序電路講究建立時(shí)間、保持時(shí)間需要留有裕量。這也說明了，在電路中信號(hào)的順序以及之間的時(shí)序關(guān)系十分重要

如果激勵(lì)的輸入輸出不滿足設(shè)計(jì)的要求，那么測(cè)試的結(jié)果也是不可靠的。同樣，如果設(shè)計(jì)內(nèi)部不滿足要求，輸入輸出的關(guān)系也不正確。為了檢驗(yàn)這之間的關(guān)系，便引入了assertion.

由參考資料可知幾點(diǎn)，非時(shí)序邏輯時(shí)，assertion的形式如下：

ASSERTION_TEST:
 assert (condition)
 else
  $error("check failed");

而對(duì)于時(shí)序邏輯的assertion，形式如下:

ASSERTION_TEST:
 assert
  property(
  @(posedge clk) disable iff (rst)
   condition
  )
  else
   $error("check failed");

或

property ASSERTION_TEST:
  @(posedge clk) disable iff (rst)
   condition
  )
endproperty

ASSERTION_ACTION: assert property (ASSERTION_TEST)

其它的一些系統(tǒng)函數(shù)，操作符作用如下，可以進(jìn)參考資料查看：

那么，接下來我們就做個(gè)小測(cè)試，使用req ack的握手過程作為檢測(cè)過程。

信號(hào)的時(shí)序圖要求如上圖，握手過程為：

1. req信號(hào)拉高，此時(shí)ack信號(hào)還是低電平
2. 在req信號(hào)拉高后，ack信號(hào)拉高
3. req端檢測(cè)到ack拉高，拉低req信號(hào)
4. ack端的處理結(jié)束，檢測(cè)到req信號(hào)拉低，ack信號(hào)拉低

那么，我們簡(jiǎn)單寫一個(gè)ack應(yīng)答的模塊，內(nèi)容如下：

module req2ack(
  input  clk ,
  input  rst ,

  input  en  ,
  input  req ,
  output reg ack 
);

reg [7:0] req_arr;

always @ (posedge clk or posedge rst)
begin
 if (rst)
  req_arr <= 'd0;
 else if (en)
  req_arr <= {req_arr[5:0], {2{req}}};
end

always @ (posedge clk or posedge rst)
begin
 if (rst) 
  ack <= 1'b1;
 else if (en)
  ack <= req_arr[7] ; 
end

endmodule

req經(jīng)過8個(gè)時(shí)鐘周期和使能信號(hào)的延遲后，ack做出應(yīng)答。

tb簡(jiǎn)單寫為：

module tb;

reg clk ;
reg rst ;
reg en  ;
reg req ;
wire ack;

initial begin
 clk = 0;
 rst = 1;
 en  = 0;
 req = 0;
 #100
 rst = 0;
 en  = 1;
 #100
 req = 1;
 wait(ack);
 req = 0;
 #50
 req = 1;
 #20
 req = 0;
 #50
 $finish;
end

initial begin
 $fsdbDumpfile("tb.fsdb");
 $fsdbDumpvars;
 $fsdbDumpSVA;
end

always #10 clk = ~clk;

req2ack req_inst(
  .clk(clk) ,
  .rst(rst) ,
  .en (en ) ,
  .req(req) ,
  .ack(ack) 
);

`ifdef ASSERTION_ENABLE
 `include "tb_assertion.v"
`endif

endmodule

提供20ns的周期時(shí)鐘，使能信號(hào)；以及兩次req信號(hào)拉高的模擬激勵(lì)。

assertion定義在tb_assertion.v文件中，在仿真時(shí)定義ASSERTION_ENABLE的宏，可以調(diào)用assertion檢查。

tb_assertion.v定義為：

check_req_ack_rise:
    assert property(
 @(posedge clk) disable iff (rst)
  $rose(req) |- > ##1 (req & ~ack)[*0:$] ##1 (req & ack)
 )
 else
   $error("req to ack rising edge is fail");

check_req_ack_fall:
    assert property(
 @(posedge clk) disable iff (rst)
  $rose(ack) |- > (req & ack)[*0:$] ##1 (~req & ack)[*0:$] ##1 (~req & ~ack)
 )
 else
  $error("req to ack falling edge is fail");

第一塊內(nèi)容，檢查req-ack握手過程的1，2兩步；第二塊內(nèi)容，檢查req-ack握手過程的3，4步。

$rose(req)的意思是由上文或參考資料可知，等到req信號(hào)的上升沿有效；

|->操作符表示，LHS(左側(cè)表達(dá)式)條件滿足，則在同一時(shí)刻去檢查RHS的表達(dá)式；

##1 代表延時(shí)1個(gè)時(shí)鐘周期；

(req & ~ ack)[*0:$] 代表此時(shí)req信號(hào)為高，ack信號(hào)為低的情況滿足0或多個(gè)時(shí)鐘周期；周期不確定

第一塊內(nèi)容的意思是，等到req信號(hào)上升沿，過一個(gè)時(shí)鐘周期檢查req拉高，ack為低的情況是否滿足，這個(gè)過程可能持續(xù)多個(gè)周期，不確定；然后就是ack信號(hào)拉高。檢查結(jié)束

第二塊內(nèi)容的意思是，等到ack信號(hào)上升沿，檢查req和ack的信號(hào)是否都拉高，這個(gè)過程可能持續(xù)多個(gè)周期，不確定；然后req信號(hào)拉低，ack保持，也會(huì)持續(xù)多個(gè)周期，最后ack信號(hào)也拉低。

最后，在運(yùn)行vcs時(shí)，需要加入“+fsdb+sva_success -assert”

測(cè)試結(jié)果：

那么，我們對(duì)激勵(lì)稍作修改下：

initial begin
 clk = 0;
 rst = 1;
 en  = 0;
 req = 0;
 #100
 rst = 0;
 en  = 1;
 #100
 req = 1;
 wait(ack);
 #20
 req = 0;
 wait(~ack);
 #50
 $finish;
end

Assertion的結(jié)果：

這只是作為一個(gè)小例子，而且寫的過于匆忙，我相信應(yīng)該是有更好的assertion寫法，所以權(quán)當(dāng)是一次記錄的草稿內(nèi)容。